From 2342e6a157c3e1d8b55ea1d959c2ea40fddc4c4f Mon Sep 17 00:00:00 2001 From: Liye Guo Date: Mon, 23 Jun 2025 23:19:06 +0200 Subject: [PATCH 1/2] Add the inverse of getIVar(). --- .../theorytranslation/TermSmtTranslator.java | 17 ++++++++++++++++- 1 file changed, 16 insertions(+), 1 deletion(-) diff --git a/app/src/main/java/charlie/theorytranslation/TermSmtTranslator.java b/app/src/main/java/charlie/theorytranslation/TermSmtTranslator.java index 5eda2841..51488056 100644 --- a/app/src/main/java/charlie/theorytranslation/TermSmtTranslator.java +++ b/app/src/main/java/charlie/theorytranslation/TermSmtTranslator.java @@ -48,6 +48,7 @@ public class TermSmtTranslator { private TreeMap _ivars; private TreeMap _svars; private TreeMap _bvars; + private TreeMap _varOfIVar; /** * Create a translator for transforming terms into SMT expressions. The given SmtProblem is used @@ -58,6 +59,7 @@ public TermSmtTranslator(SmtProblem problem) { _ivars = new TreeMap(); _svars = new TreeMap(); _bvars = new TreeMap(); + _varOfIVar = new TreeMap(); } /** @@ -69,6 +71,7 @@ public TermSmtTranslator() { _ivars = new TreeMap(); _svars = new TreeMap(); _bvars = new TreeMap(); + _varOfIVar = new TreeMap(); } /** Returns the SmtProblem associated to this translator (and used for translating variables). */ @@ -99,7 +102,11 @@ private CalculationSymbol getCalculationRoot(Term t) { * generates a new IVar and both stores and returns it. */ private IVar getIntegerVariableFor(Variable x) { - if (!_ivars.containsKey(x)) _ivars.put(x, _problem.createIntegerVariable()); + if (!_ivars.containsKey(x)) { + IVar ivar = _problem.createIntegerVariable(); + _ivars.put(x, ivar); + _varOfIVar.put(ivar, x); + } return _ivars.get(x); } @@ -145,6 +152,14 @@ public BVar getBVar(Variable x) { return _bvars.get(x); } + /** + * This is the inverse of getIVar(), i.e., it returns the user Variable that corresponds to the + * given integer variable. + */ + public Variable getVarOfIVar(IVar ivar) { + return _varOfIVar.get(ivar); + } + /** * Helper interface so the translate function can handle all kinds of symbols and values in one * big switch (which is important so we get compiler errors if someone adds a kind of calculation From f5b2dd8af7a11024aa09647b05abc39ee629f49d Mon Sep 17 00:00:00 2001 From: Liye Guo Date: Mon, 23 Jun 2025 23:48:15 +0200 Subject: [PATCH 2/2] Add package cora.template. --- .../java/cora/template/TailupMatcher.java | 310 ++++++++++++++++++ .../java/cora/template/TemplateMatcher.java | 24 ++ .../java/cora/template/TailupMatcherTest.java | 123 +++++++ 3 files changed, 457 insertions(+) create mode 100644 app/src/main/java/cora/template/TailupMatcher.java create mode 100644 app/src/main/java/cora/template/TemplateMatcher.java create mode 100644 app/src/test/java/cora/template/TailupMatcherTest.java diff --git a/app/src/main/java/cora/template/TailupMatcher.java b/app/src/main/java/cora/template/TailupMatcher.java new file mode 100644 index 00000000..42884960 --- /dev/null +++ b/app/src/main/java/cora/template/TailupMatcher.java @@ -0,0 +1,310 @@ +/************************************************************************************************** + Copyright 2025 Cynthia Kop & Liye Guo + + Licensed under the Apache License, Version 2.0 (the "License"); you may not use this file except + in compliance with the License. + You may obtain a copy of the License at + + http://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software distributed under the + License is distributed on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either + express or implied. + See the License for the specific language governing permissions and limitations under the License. + *************************************************************************************************/ + +package cora.template; + +import charlie.exceptions.IndexingException; +import charlie.smt.Addition; +import charlie.smt.Constraint; +import charlie.smt.Geq0; +import charlie.smt.IValue; +import charlie.smt.IVar; +import charlie.smt.SmtFactory; +import charlie.terms.FunctionSymbol; +import charlie.terms.Substitution; +import charlie.terms.Term; +import charlie.terms.TermFactory; +import charlie.terms.TheoryFactory; +import charlie.terms.Variable; +import charlie.terms.position.Position; +import charlie.theorytranslation.TermSmtTranslator; +import charlie.trs.Rule; +import charlie.trs.TrsFactory; +import charlie.types.Type; +import charlie.types.TypeFactory; +import charlie.util.Pair; +import cora.rwinduction.engine.Equation; + +import java.util.List; + +/** + * The Tailup template: + * leftHandSide -> accumulator | loopVariable > upperBound + * leftHandSide -> rightHandSide | loopVariable <= upperBound + * where rightHandSide contains operatorDefinition. + */ +public class TailupMatcher implements TemplateMatcher { + private Term _leftHandSide; + private Variable _accumulator; + private Variable _loopVariable; + private Term _upperBound; + private Term _operatorDefinition; + + private TailupMatcher() {} + + /** + * Checks if there are exactly two rewrite rules and exactly one of them has a variable as its + * right-hand side, then reorders the rules to make it the first. + */ + private static Pair reorderTwoRules(Iterable rules) { + var iter = rules.iterator(); + if (!iter.hasNext()) return null; // there is at least one rule + var fst = iter.next(); + if (!iter.hasNext()) return null; // there are at least two rules + var snd = iter.next(); + if (iter.hasNext()) return null; // there are no more than two rules + if (fst.queryRightSide().isVariable()) { + if (snd.queryRightSide().isVariable()) return null; + return new Pair<>(fst, snd); + } + else { + if (!snd.queryRightSide().isVariable()) return null; + return new Pair<>(snd, fst); + } + } + + /** + * Checks if the left-hand sides are equal (modulo renaming) and satisfy certain conditions, + * then stores a representative. + * @return a substitution subst such that fst.queryLeftSide() subst = snd.queryLeftSide(). + */ + private Substitution setLeftHandSide(Rule fst, Rule snd) { + _leftHandSide = snd.queryLeftSide(); + // The linearity of snd.queryLeftSide() implies the linearity of fst.queryLeftSide(), given + // fst.queryLeftSide() subst = snd.queryLeftSide() and that subst maps variables to variables. + if (!_leftHandSide.isLinear()) return null; + // Likewise, it suffices to check only that fst.queryLeftSide() is a functional term. + if (!fst.queryLeftSide().isFunctionalTerm()) return null; + var subst = fst.queryLeftSide().match(_leftHandSide); + if (subst == null) return null; + // To ensure that the left-hand sides are equal modulo renaming, subst must map variables to + // variables. Because snd.queryLeftSide() is linear, subst is guaranteed to be injective. + for (var x : subst.domain()) { + if (!subst.get(x).isVariable()) return null; + } + return subst; + } + + /** + * Fetches the addends in an addition of form variable + value. + */ + private static Pair fetchAddends(Addition a) { + if (a.numChildren() == 2) { + if (a.queryChild(1) instanceof IVar) { + if (a.queryChild(2) instanceof IValue) { + return new Pair<>((IVar) a.queryChild(1), (IValue) a.queryChild(2)); + } + } + else if (a.queryChild(1) instanceof IValue) { + if (a.queryChild(2) instanceof IVar) { + return new Pair<>((IVar) a.queryChild(2), (IValue) a.queryChild(1)); + } + } + } + return null; + } + + /** + * Determines the loop variable and the upper bound. + * @param constraint should essentially have the form _loopVariable <= _upperBound. + * @param translator must be the one in which constraint has been generated. + * @return true if both components are determined successfully, and false otherwise. + */ + private boolean setLoopVariableAndUpperBound(Constraint constraint, TermSmtTranslator translator) { + if (!(constraint instanceof Geq0)) return false; + // To make use of split(), we first add 0 to the integer expression. + var splitExpr = ((Addition) SmtFactory.createAddition( + ((Geq0) constraint).queryExpression(), + SmtFactory.createValue(0))) + .split(); + + // The loop variable should occur in the negative part, which can be either _loopVariable or + // _loopVariable + value. + int shift = 0; // shift will eventually be added to the upper bound. + if (splitExpr.snd() instanceof IVar) { + _loopVariable = translator.getVarOfIVar((IVar) splitExpr.snd()); + } + else if (splitExpr.snd() instanceof Addition) { + Pair addends = fetchAddends((Addition) splitExpr.snd()); + if (addends == null) return false; + _loopVariable = translator.getVarOfIVar(addends.fst()); + shift -= addends.snd().queryValue(); + } + else { + return false; + } + if (_loopVariable.equals(_accumulator)) return false; + + // The positive part may contain a variable. + Variable y = null; + if (splitExpr.fst() instanceof IVar) { + y = translator.getVarOfIVar((IVar) splitExpr.fst()); + } + else if (splitExpr.fst() instanceof IValue) { + shift += ((IValue) splitExpr.fst()).queryValue(); + } + else if (splitExpr.fst() instanceof Addition) { + Pair addends = fetchAddends((Addition) splitExpr.fst()); + if (addends == null) return false; + y = translator.getVarOfIVar(addends.fst()); + shift += addends.snd().queryValue(); + } + else { + return false; + } + + if (y == null) { + _upperBound = TheoryFactory.createValue(shift); + } + else { + if (y.equals(_accumulator)) return false; + if (shift == 0) { + _upperBound = y; + } + else { + _upperBound = TermFactory.createApp( + TheoryFactory.plusSymbol, + y, + TheoryFactory.createValue(shift)); + } + } + return true; + } + + /** + * Determines the definition of the binary operator for the recursive step. + * @return true if the definition is determined successfully, and false otherwise. + */ + private boolean setOperatorDefinition(Term rightHandSide) { + Pair loopVariable = _leftHandSide.findSubterm( + (t, p) -> t.equals(_loopVariable)); + if (loopVariable == null) return false; + Pair accumulator = _leftHandSide.findSubterm( + (t, p) -> t.equals(_accumulator)); + if (accumulator == null) return false; + + Term loopVariableNew; + Term accumulatorNew; + try { + loopVariableNew = rightHandSide.querySubterm(loopVariable.snd()); + accumulatorNew = rightHandSide.querySubterm(accumulator.snd()); + } + catch (IndexingException e) { + return false; + } + + if (!loopVariableNew.equals(TermFactory.createApp( + TheoryFactory.plusSymbol, _loopVariable, TheoryFactory.createValue(1))) + && !loopVariableNew.equals(TermFactory.createApp( + TheoryFactory.plusSymbol, TheoryFactory.createValue(1), _loopVariable))) { + return false; + } + if (!_leftHandSide.equals(rightHandSide + .replaceSubterm(loopVariable.snd(), _loopVariable) + .replaceSubterm(accumulator.snd(), _accumulator))) { + return false; + } + + for (var x : accumulatorNew.vars()) { + if (!x.equals(_accumulator) && !x.equals(_loopVariable)) return false; + } + _operatorDefinition = accumulatorNew; + return true; + } + + /** + * The method testing for the Tailup template, publicly accessible. + * @param rules collects the rewrite rules defining a certain function symbol. + * @return a matcher object if the rules conform to the template, and null otherwise. + */ + public static TailupMatcher match(Iterable rules) { + var rulePair = reorderTwoRules(rules); + if (rulePair == null) return null; + + var matcher = new TailupMatcher(); + var subst = matcher.setLeftHandSide(rulePair.fst(), rulePair.snd()); + if (subst == null) return null; + matcher._accumulator = (Variable) subst.get(rulePair.fst().queryRightSide().queryVariable()); + // matcher._accumulator is null if the right-hand side of rulePair.fst() does not occur on + // the left-hand side + if (matcher._accumulator == null) return null; + + var translator = new TermSmtTranslator(); + Constraint constraint = translator.translateConstraint(rulePair.snd().queryConstraint()) + .simplify(); + // If the constraint of rulePair.fst() contains any variable that does not occur on the + // left-hand side of rulePair.fst(), the two are not equal either. + if (!translator.translateConstraint(rulePair.fst().queryConstraint().substitute(subst)) + .negate().simplify().equals(constraint)) { + return null; + } + if (!matcher.setLoopVariableAndUpperBound(constraint, translator)) return null; + + if (!matcher.setOperatorDefinition(rulePair.snd().queryRightSide())) return null; + return matcher; + } + + /** + * Generates an equation and possibly an extra rewrite rule for rewriting induction. + */ + public Pair generateEquationAndRule() { + Type typeOperator = TypeFactory.createArrow( + TypeFactory.intSort, + TypeFactory.createArrow( + _accumulator.queryType(), + _operatorDefinition.queryType())); + FunctionSymbol funcTailup = TermFactory.createConstant( + "_tailup", + TypeFactory.createArrow( + typeOperator, + TypeFactory.createArrow( + TypeFactory.intSort, + TypeFactory.createArrow( + TypeFactory.intSort, + TypeFactory.createArrow( + TypeFactory.intSort, + TypeFactory.createArrow( + _accumulator.queryType(), + _leftHandSide.queryType())))))); + + FunctionSymbol f; + Rule rule; + if (_operatorDefinition.isFunctionalTerm() + && _operatorDefinition.numberArguments() == 2 + && _operatorDefinition.queryArgument(1).equals(_loopVariable) + && _operatorDefinition.queryArgument(2).equals(_accumulator)) { + f = _operatorDefinition.queryRoot(); + rule = null; + } + else { + f = TermFactory.createConstant("_f", typeOperator); + rule = TrsFactory.createRule( + TermFactory.createApp(f, _loopVariable, _accumulator), + _operatorDefinition); + } + + Variable x = TermFactory.createVar("_x", TypeFactory.intSort); + Variable y = TermFactory.createVar("_y", TypeFactory.intSort); + var equation = new Equation( + _leftHandSide, + TermFactory.createApp(funcTailup, List.of(f, _loopVariable, x, y, _accumulator)), + TheoryFactory.createConjunction( + TheoryFactory.createConjunction( + TermFactory.createApp(TheoryFactory.leqSymbol, x, _loopVariable), + TermFactory.createApp(TheoryFactory.leqSymbol, _loopVariable, y)), + TheoryFactory.createEquality(y, _upperBound))); + return new Pair<>(equation, rule); + } +} diff --git a/app/src/main/java/cora/template/TemplateMatcher.java b/app/src/main/java/cora/template/TemplateMatcher.java new file mode 100644 index 00000000..9be7351d --- /dev/null +++ b/app/src/main/java/cora/template/TemplateMatcher.java @@ -0,0 +1,24 @@ +/************************************************************************************************** + Copyright 2025 Cynthia Kop & Liye Guo + + Licensed under the Apache License, Version 2.0 (the "License"); you may not use this file except + in compliance with the License. + You may obtain a copy of the License at + + http://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software distributed under the + License is distributed on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either + express or implied. + See the License for the specific language governing permissions and limitations under the License. + *************************************************************************************************/ + +package cora.template; + +import charlie.trs.Rule; +import charlie.util.Pair; +import cora.rwinduction.engine.Equation; + +public interface TemplateMatcher { + Pair generateEquationAndRule(); +} diff --git a/app/src/test/java/cora/template/TailupMatcherTest.java b/app/src/test/java/cora/template/TailupMatcherTest.java new file mode 100644 index 00000000..d502b9b3 --- /dev/null +++ b/app/src/test/java/cora/template/TailupMatcherTest.java @@ -0,0 +1,123 @@ +/************************************************************************************************** + Copyright 2025 Cynthia Kop & Liye Guo + + Licensed under the Apache License, Version 2.0 (the "License"); you may not use this file except + in compliance with the License. + You may obtain a copy of the License at + + http://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software distributed under the + License is distributed on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either + express or implied. + See the License for the specific language governing permissions and limitations under the License. + *************************************************************************************************/ + +package cora.template; + +import charlie.reader.CoraInputReader; +import static charlie.trs.TrsFactory.LCSTRS; + +import org.junit.jupiter.api.Test; +import static org.junit.jupiter.api.Assertions.*; + +public class TailupMatcherTest { + @Test + public void testFactorial() { + var trs = CoraInputReader.readTrsFromString( + "fact :: Int -> Int -> Int -> Int\n" + + "fact(n, i, a) -> a | i > n\n" + + "fact(n, i, a) -> fact(n, i + 1, i * a) | i <= n\n", + LCSTRS); + TailupMatcher matcher = TailupMatcher.match(trs.queryRules()); + assertNotNull(matcher); + var equRul = matcher.generateEquationAndRule(); + assertEquals( + "fact(n, i, a) ≈ _tailup([*], i, _x, _y, a) | _x ≤ i ∧ i ≤ _y ∧ _y = n", + equRul.fst().toString()); + assertNull(equRul.snd()); + } + + @Test + public void testFactorial0() { + var trs = CoraInputReader.readTrsFromString( + "fact0 :: Int -> Int -> Int\n" + + "fact0(i, a) -> a | i > 0\n" + + "fact0(i, a) -> fact0(i + 1, i * a) | i <= 0\n", + LCSTRS); + TailupMatcher matcher = TailupMatcher.match(trs.queryRules()); + assertNotNull(matcher); + var equRul = matcher.generateEquationAndRule(); + assertEquals( + "fact0(i, a) ≈ _tailup([*], i, _x, _y, a) | _x ≤ i ∧ i ≤ _y ∧ _y = 0", + equRul.fst().toString()); + assertNull(equRul.snd()); + } + + @Test + public void testFactorial10() { + var trs = CoraInputReader.readTrsFromString( + "fact10 :: Int -> Int -> Int\n" + + "fact10(i, a) -> a | i > 10\n" + + "fact10(i, a) -> fact10(i + 1, i * a) | i <= 10\n", + LCSTRS); + TailupMatcher matcher = TailupMatcher.match(trs.queryRules()); + assertNotNull(matcher); + var equRul = matcher.generateEquationAndRule(); + assertEquals( + "fact10(i, a) ≈ _tailup([*], i, _x, _y, a) | _x ≤ i ∧ i ≤ _y ∧ _y = 10", + equRul.fst().toString()); + assertNull(equRul.snd()); + } + + @Test + public void testSum() { + var trs = CoraInputReader.readTrsFromString( + "sum :: Int -> Int -> Int -> Int\n" + + "sum(n, i, a) -> a | n < 1 + i\n" + + "sum(n, i, a) -> sum(n, 1 + i, a + i) | n >= 1 + i\n", + LCSTRS); + TailupMatcher matcher = TailupMatcher.match(trs.queryRules()); + assertNotNull(matcher); + var equRul = matcher.generateEquationAndRule(); + assertEquals( + "sum(n, i, a) ≈ _tailup(_f, i, _x, _y, a) | _x ≤ i ∧ i ≤ _y ∧ _y = n - 1", + equRul.fst().toString()); + assertEquals( + "_f(i, a) → a + i", + equRul.snd().toString()); + } + + @Test + public void testTooFewRules() { + var trs = CoraInputReader.readTrsFromString( + "sum :: Int -> Int -> Int -> Int\n" + + "sum(n, i, a) -> a | n < 1 + i\n", + LCSTRS); + TailupMatcher matcher = TailupMatcher.match(trs.queryRules()); + assertNull(matcher); + } + + @Test + public void testTooManyRules() { + var trs = CoraInputReader.readTrsFromString( + "sum :: Int -> Int -> Int -> Int\n" + + "sum(n, i, a) -> a | n < 10\n" + + "sum(n, i, a) -> a | n < 1 + i\n" + + "sum(n, i, a) -> sum(n, 1 + i, a + i) | n >= 1 + i\n", + LCSTRS); + TailupMatcher matcher = TailupMatcher.match(trs.queryRules()); + assertNull(matcher); + } + + @Test + public void testAccumulatorNotOnLeftHandSide() { + var trs = CoraInputReader.readTrsFromString( + "sum :: Int -> Int -> Int -> Int\n" + + "sum(n, i, a) -> b | n < 1 + i\n" + + "sum(n, i, a) -> sum(n, 1 + i, a + i) | n >= 1 + i\n", + LCSTRS); + TailupMatcher matcher = TailupMatcher.match(trs.queryRules()); + assertNull(matcher); + } +}