From df6ce0361d549c3cef4303d05d72ee8b5c8612b1 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Sat, 2 Apr 2022 14:40:41 -0500 Subject: [PATCH] Rename mkSygusGrammar to mkGrammar (#8544) --- examples/api/cpp/sygus-fun.cpp | 2 +- examples/api/cpp/sygus-grammar.cpp | 2 +- examples/api/java/SygusFun.java | 3 ++- examples/api/java/SygusGrammar.java | 2 +- examples/api/python/sygus-fun.py | 2 +- examples/api/python/sygus-grammar.py | 6 ++--- src/api/cpp/cvc5.cpp | 4 +-- src/api/cpp/cvc5.h | 4 +-- src/api/java/io/github/cvc5/Solver.java | 8 +++--- src/api/java/jni/solver.cpp | 15 +++++------ src/api/python/cvc5.pxd | 2 +- src/api/python/cvc5.pxi | 4 +-- src/parser/smt2/smt2.cpp | 2 +- test/unit/api/cpp/grammar_black.cpp | 10 +++---- test/unit/api/cpp/solver_black.cpp | 30 ++++++++++----------- test/unit/api/java/GrammarTest.java | 10 +++---- test/unit/api/java/SolverTest.java | 36 +++++++++++++------------ test/unit/api/python/test_grammar.py | 10 +++---- test/unit/api/python/test_solver.py | 28 +++++++++---------- 19 files changed, 91 insertions(+), 89 deletions(-) diff --git a/examples/api/cpp/sygus-fun.cpp b/examples/api/cpp/sygus-fun.cpp index 15a53c36e..b9e939f38 100644 --- a/examples/api/cpp/sygus-fun.cpp +++ b/examples/api/cpp/sygus-fun.cpp @@ -59,7 +59,7 @@ int main() Term leq = slv.mkTerm(LEQ, {start, start}); // create the grammar object - Grammar g = slv.mkSygusGrammar({x, y}, {start, start_bool}); + Grammar g = slv.mkGrammar({x, y}, {start, start_bool}); // bind each non-terminal to its rules g.addRules(start, {zero, one, x, y, plus, minus, ite}); diff --git a/examples/api/cpp/sygus-grammar.cpp b/examples/api/cpp/sygus-grammar.cpp index a69382e12..a5f051c6c 100644 --- a/examples/api/cpp/sygus-grammar.cpp +++ b/examples/api/cpp/sygus-grammar.cpp @@ -49,7 +49,7 @@ int main() Term plus = slv.mkTerm(ADD, {x, start}); // create the grammar object - Grammar g1 = slv.mkSygusGrammar({x}, {start}); + Grammar g1 = slv.mkGrammar({x}, {start}); // bind each non-terminal to its rules g1.addRules(start, {neg_x, plus}); diff --git a/examples/api/java/SygusFun.java b/examples/api/java/SygusFun.java index 4f0626748..aa52fd008 100644 --- a/examples/api/java/SygusFun.java +++ b/examples/api/java/SygusFun.java @@ -57,7 +57,8 @@ public class SygusFun Term leq = slv.mkTerm(LEQ, start, start); // create the grammar object - Grammar g = slv.mkSygusGrammar(new Term[] {x, y}, new Term[] {start, start_bool}); + Grammar g = + slv.mkGrammar(new Term[] {x, y}, new Term[] {start, start_bool}); // bind each non-terminal to its rules g.addRules(start, new Term[] {zero, one, x, y, plus, minus, ite}); diff --git a/examples/api/java/SygusGrammar.java b/examples/api/java/SygusGrammar.java index c97fb23e0..35c4b9846 100644 --- a/examples/api/java/SygusGrammar.java +++ b/examples/api/java/SygusGrammar.java @@ -48,7 +48,7 @@ public class SygusGrammar Term plus = slv.mkTerm(ADD, x, start); // create the grammar object - Grammar g1 = slv.mkSygusGrammar(new Term[] {x}, new Term[] {start}); + Grammar g1 = slv.mkGrammar(new Term[] {x}, new Term[] {start}); // bind each non-terminal to its rules g1.addRules(start, new Term[] {neg_x, plus}); diff --git a/examples/api/python/sygus-fun.py b/examples/api/python/sygus-fun.py index 9781ddb67..f81fd7fd4 100644 --- a/examples/api/python/sygus-fun.py +++ b/examples/api/python/sygus-fun.py @@ -54,7 +54,7 @@ if __name__ == "__main__": leq = slv.mkTerm(Kind.LEQ, start, start) # create the grammar object - g = slv.mkSygusGrammar([x, y], [start, start_bool]) + g = slv.mkGrammar([x, y], [start, start_bool]) # bind each non-terminal to its rules g.addRules(start, {zero, one, x, y, plus, minus, ite}) diff --git a/examples/api/python/sygus-grammar.py b/examples/api/python/sygus-grammar.py index c70b0d9c8..20eb0ddf8 100644 --- a/examples/api/python/sygus-grammar.py +++ b/examples/api/python/sygus-grammar.py @@ -45,9 +45,9 @@ if __name__ == "__main__": plus = slv.mkTerm(Kind.ADD, x, start) # create the grammar object - g1 = slv.mkSygusGrammar({x}, {start}) - g2 = slv.mkSygusGrammar({x}, {start}) - g3 = slv.mkSygusGrammar({x}, {start}) + g1 = slv.mkGrammar({x}, {start}) + g2 = slv.mkGrammar({x}, {start}) + g3 = slv.mkGrammar({x}, {start}) # bind each non-terminal to its rules g1.addRules(start, {neg_x, plus}) diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp index 1c9d85240..768ec181b 100644 --- a/src/api/cpp/cvc5.cpp +++ b/src/api/cpp/cvc5.cpp @@ -7378,8 +7378,8 @@ Term Solver::declareSygusVar(const std::string& symbol, const Sort& sort) const CVC5_API_TRY_CATCH_END; } -Grammar Solver::mkSygusGrammar(const std::vector& boundVars, - const std::vector& ntSymbols) const +Grammar Solver::mkGrammar(const std::vector& boundVars, + const std::vector& ntSymbols) const { CVC5_API_TRY_CATCH_BEGIN; CVC5_API_ARG_SIZE_CHECK_EXPECTED(!ntSymbols.empty(), ntSymbols) diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h index eba7dbdb9..ef366cfe5 100644 --- a/src/api/cpp/cvc5.h +++ b/src/api/cpp/cvc5.h @@ -4681,8 +4681,8 @@ class CVC5_EXPORT Solver * @param ntSymbols the pre-declaration of the non-terminal symbols * @return the grammar */ - Grammar mkSygusGrammar(const std::vector& boundVars, - const std::vector& ntSymbols) const; + Grammar mkGrammar(const std::vector& boundVars, + const std::vector& ntSymbols) const; /** * Synthesize n-ary function. diff --git a/src/api/java/io/github/cvc5/Solver.java b/src/api/java/io/github/cvc5/Solver.java index feaed83e5..87ca11cc0 100644 --- a/src/api/java/io/github/cvc5/Solver.java +++ b/src/api/java/io/github/cvc5/Solver.java @@ -2457,15 +2457,15 @@ public class Solver implements IPointer, AutoCloseable * @param ntSymbols the pre-declaration of the non-terminal symbols * @return the grammar */ - public Grammar mkSygusGrammar(Term[] boundVars, Term[] ntSymbols) - { + public Grammar mkGrammar(Term[] boundVars, Term[] ntSymbols) { long[] boundVarPointers = Utils.getPointers(boundVars); long[] ntSymbolPointers = Utils.getPointers(ntSymbols); - long grammarPointer = mkSygusGrammar(pointer, boundVarPointers, ntSymbolPointers); + long grammarPointer = + mkGrammar(pointer, boundVarPointers, ntSymbolPointers); return new Grammar(this, grammarPointer); } - private native long mkSygusGrammar( + private native long mkGrammar( long pointer, long[] boundVarPointers, long[] ntSymbolPointers); /** diff --git a/src/api/java/jni/solver.cpp b/src/api/java/jni/solver.cpp index 75db6960a..a5a93a61a 100644 --- a/src/api/java/jni/solver.cpp +++ b/src/api/java/jni/solver.cpp @@ -2395,22 +2395,21 @@ JNIEXPORT jlong JNICALL Java_io_github_cvc5_Solver_declareSygusVar( /* * Class: io_github_cvc5_Solver - * Method: mkSygusGrammar + * Method: mkGrammar * Signature: (J[J[J)J */ JNIEXPORT jlong JNICALL -Java_io_github_cvc5_Solver_mkSygusGrammar(JNIEnv* env, - jobject, - jlong pointer, - jlongArray jBoundVars, - jlongArray jNtSymbols) +Java_io_github_cvc5_Solver_mkGrammar(JNIEnv* env, + jobject, + jlong pointer, + jlongArray jBoundVars, + jlongArray jNtSymbols) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Solver* solver = reinterpret_cast(pointer); std::vector boundVars = getObjectsFromPointers(env, jBoundVars); std::vector ntSymbols = getObjectsFromPointers(env, jNtSymbols); - Grammar* retPointer = - new Grammar(solver->mkSygusGrammar(boundVars, ntSymbols)); + Grammar* retPointer = new Grammar(solver->mkGrammar(boundVars, ntSymbols)); return reinterpret_cast(retPointer); CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); } diff --git a/src/api/python/cvc5.pxd b/src/api/python/cvc5.pxd index c62094341..52d697492 100644 --- a/src/api/python/cvc5.pxd +++ b/src/api/python/cvc5.pxd @@ -237,7 +237,7 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5": Op mkOp(Kind kind, const string& arg) except + Op mkOp(Kind kind, const vector[uint32_t]& args) except + # Sygus related functions - Grammar mkSygusGrammar(const vector[Term]& boundVars, const vector[Term]& ntSymbols) except + + Grammar mkGrammar(const vector[Term]& boundVars, const vector[Term]& ntSymbols) except + Term declareSygusVar(const string& symbol, Sort sort) except + void addSygusConstraint(Term term) except + void addSygusAssume(Term term) except + diff --git a/src/api/python/cvc5.pxi b/src/api/python/cvc5.pxi index 441648f67..90aa5decc 100644 --- a/src/api/python/cvc5.pxi +++ b/src/api/python/cvc5.pxi @@ -1656,7 +1656,7 @@ cdef class Solver: r.cr = self.csolver.checkSat() return r - def mkSygusGrammar(self, boundVars, ntSymbols): + def mkGrammar(self, boundVars, ntSymbols): """ Create a SyGuS grammar. The first non-terminal is treated as the starting non-terminal, so the order of non-terminals matters. @@ -1673,7 +1673,7 @@ cdef class Solver: bvc.push_back(( bv).cterm) for nt in ntSymbols: ntc.push_back(( nt).cterm) - grammar.cgrammar = self.csolver.mkSygusGrammar( bvc, ntc) + grammar.cgrammar = self.csolver.mkGrammar( bvc, ntc) return grammar def declareSygusVar(self, str symbol, Sort sort): diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index 63cc3af4e..3bdf8a08c 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -711,7 +711,7 @@ cvc5::Grammar* Smt2::mkGrammar(const std::vector& boundVars, const std::vector& ntSymbols) { d_allocGrammars.emplace_back( - new cvc5::Grammar(d_solver->mkSygusGrammar(boundVars, ntSymbols))); + new cvc5::Grammar(d_solver->mkGrammar(boundVars, ntSymbols))); return d_allocGrammars.back().get(); } diff --git a/test/unit/api/cpp/grammar_black.cpp b/test/unit/api/cpp/grammar_black.cpp index 0b5899f88..be05d39c8 100644 --- a/test/unit/api/cpp/grammar_black.cpp +++ b/test/unit/api/cpp/grammar_black.cpp @@ -33,7 +33,7 @@ TEST_F(TestApiBlackGrammar, addRule) Term start = d_solver.mkVar(boolean); Term nts = d_solver.mkVar(boolean); - Grammar g = d_solver.mkSygusGrammar({}, {start}); + Grammar g = d_solver.mkGrammar({}, {start}); ASSERT_NO_THROW(g.addRule(start, d_solver.mkBoolean(false))); @@ -59,7 +59,7 @@ TEST_F(TestApiBlackGrammar, addRules) Term start = d_solver.mkVar(boolean); Term nts = d_solver.mkVar(boolean); - Grammar g = d_solver.mkSygusGrammar({}, {start}); + Grammar g = d_solver.mkGrammar({}, {start}); ASSERT_NO_THROW(g.addRules(start, {d_solver.mkBoolean(false)})); @@ -85,7 +85,7 @@ TEST_F(TestApiBlackGrammar, addAnyConstant) Term start = d_solver.mkVar(boolean); Term nts = d_solver.mkVar(boolean); - Grammar g = d_solver.mkSygusGrammar({}, {start}); + Grammar g = d_solver.mkGrammar({}, {start}); ASSERT_NO_THROW(g.addAnyConstant(start)); ASSERT_NO_THROW(g.addAnyConstant(start)); @@ -108,8 +108,8 @@ TEST_F(TestApiBlackGrammar, addAnyVariable) Term start = d_solver.mkVar(boolean); Term nts = d_solver.mkVar(boolean); - Grammar g1 = d_solver.mkSygusGrammar({x}, {start}); - Grammar g2 = d_solver.mkSygusGrammar({}, {start}); + Grammar g1 = d_solver.mkGrammar({x}, {start}); + Grammar g2 = d_solver.mkGrammar({}, {start}); ASSERT_NO_THROW(g1.addAnyVariable(start)); ASSERT_NO_THROW(g1.addAnyVariable(start)); diff --git a/test/unit/api/cpp/solver_black.cpp b/test/unit/api/cpp/solver_black.cpp index 7183d1d0c..1e0ff5a66 100644 --- a/test/unit/api/cpp/solver_black.cpp +++ b/test/unit/api/cpp/solver_black.cpp @@ -1357,7 +1357,7 @@ TEST_F(TestApiBlackSolver, getAbduct) Term truen = d_solver.mkBoolean(true); Term start = d_solver.mkVar(boolean); Term output2; - Grammar g = d_solver.mkSygusGrammar({}, {start}); + Grammar g = d_solver.mkGrammar({}, {start}); Term conj2 = d_solver.mkTerm(GT, {x, zero}); ASSERT_NO_THROW(g.addRule(start, truen)); // Call the abduction api, while the resulting abduct is the output @@ -2530,25 +2530,25 @@ TEST_F(TestApiBlackSolver, declareSygusVar) ASSERT_THROW(slv.declareSygusVar("", boolSort), CVC5ApiException); } -TEST_F(TestApiBlackSolver, mkSygusGrammar) +TEST_F(TestApiBlackSolver, mkGrammar) { Term nullTerm; Term boolTerm = d_solver.mkBoolean(true); Term boolVar = d_solver.mkVar(d_solver.getBooleanSort()); Term intVar = d_solver.mkVar(d_solver.getIntegerSort()); - ASSERT_NO_THROW(d_solver.mkSygusGrammar({}, {intVar})); - ASSERT_NO_THROW(d_solver.mkSygusGrammar({boolVar}, {intVar})); - ASSERT_THROW(d_solver.mkSygusGrammar({}, {}), CVC5ApiException); - ASSERT_THROW(d_solver.mkSygusGrammar({}, {nullTerm}), CVC5ApiException); - ASSERT_THROW(d_solver.mkSygusGrammar({}, {boolTerm}), CVC5ApiException); - ASSERT_THROW(d_solver.mkSygusGrammar({boolTerm}, {intVar}), CVC5ApiException); + ASSERT_NO_THROW(d_solver.mkGrammar({}, {intVar})); + ASSERT_NO_THROW(d_solver.mkGrammar({boolVar}, {intVar})); + ASSERT_THROW(d_solver.mkGrammar({}, {}), CVC5ApiException); + ASSERT_THROW(d_solver.mkGrammar({}, {nullTerm}), CVC5ApiException); + ASSERT_THROW(d_solver.mkGrammar({}, {boolTerm}), CVC5ApiException); + ASSERT_THROW(d_solver.mkGrammar({boolTerm}, {intVar}), CVC5ApiException); Solver slv; Term boolVar2 = slv.mkVar(slv.getBooleanSort()); Term intVar2 = slv.mkVar(slv.getIntegerSort()); - ASSERT_NO_THROW(slv.mkSygusGrammar({boolVar2}, {intVar2})); - ASSERT_THROW(slv.mkSygusGrammar({boolVar}, {intVar2}), CVC5ApiException); - ASSERT_THROW(slv.mkSygusGrammar({boolVar2}, {intVar}), CVC5ApiException); + ASSERT_NO_THROW(slv.mkGrammar({boolVar2}, {intVar2})); + ASSERT_THROW(slv.mkGrammar({boolVar}, {intVar2}), CVC5ApiException); + ASSERT_THROW(slv.mkGrammar({boolVar2}, {intVar}), CVC5ApiException); } TEST_F(TestApiBlackSolver, synthFun) @@ -2564,10 +2564,10 @@ TEST_F(TestApiBlackSolver, synthFun) Term start1 = d_solver.mkVar(boolean); Term start2 = d_solver.mkVar(integer); - Grammar g1 = d_solver.mkSygusGrammar({x}, {start1}); + Grammar g1 = d_solver.mkGrammar({x}, {start1}); g1.addRule(start1, d_solver.mkBoolean(false)); - Grammar g2 = d_solver.mkSygusGrammar({x}, {start2}); + Grammar g2 = d_solver.mkGrammar({x}, {start2}); g2.addRule(start2, d_solver.mkInteger(0)); ASSERT_NO_THROW(d_solver.synthFun("", {}, boolean)); @@ -2599,10 +2599,10 @@ TEST_F(TestApiBlackSolver, synthInv) Term start1 = d_solver.mkVar(boolean); Term start2 = d_solver.mkVar(integer); - Grammar g1 = d_solver.mkSygusGrammar({x}, {start1}); + Grammar g1 = d_solver.mkGrammar({x}, {start1}); g1.addRule(start1, d_solver.mkBoolean(false)); - Grammar g2 = d_solver.mkSygusGrammar({x}, {start2}); + Grammar g2 = d_solver.mkGrammar({x}, {start2}); g2.addRule(start2, d_solver.mkInteger(0)); ASSERT_NO_THROW(d_solver.synthInv("", {})); diff --git a/test/unit/api/java/GrammarTest.java b/test/unit/api/java/GrammarTest.java index 0e71ddd53..f72190a09 100644 --- a/test/unit/api/java/GrammarTest.java +++ b/test/unit/api/java/GrammarTest.java @@ -50,7 +50,7 @@ class GrammarTest Term start = d_solver.mkVar(bool); Term nts = d_solver.mkVar(bool); - Grammar g = d_solver.mkSygusGrammar(new Term[] {}, new Term[] {start}); + Grammar g = d_solver.mkGrammar(new Term[] {}, new Term[] {start}); assertDoesNotThrow(() -> g.addRule(start, d_solver.mkBoolean(false))); @@ -76,7 +76,7 @@ class GrammarTest Term start = d_solver.mkVar(bool); Term nts = d_solver.mkVar(bool); - Grammar g = d_solver.mkSygusGrammar(new Term[] {}, new Term[] {start}); + Grammar g = d_solver.mkGrammar(new Term[] {}, new Term[] {start}); assertDoesNotThrow(() -> g.addRules(start, new Term[] {d_solver.mkBoolean(false)})); @@ -105,7 +105,7 @@ class GrammarTest Term start = d_solver.mkVar(bool); Term nts = d_solver.mkVar(bool); - Grammar g = d_solver.mkSygusGrammar(new Term[] {}, new Term[] {start}); + Grammar g = d_solver.mkGrammar(new Term[] {}, new Term[] {start}); assertDoesNotThrow(() -> g.addAnyConstant(start)); assertDoesNotThrow(() -> g.addAnyConstant(start)); @@ -129,8 +129,8 @@ class GrammarTest Term start = d_solver.mkVar(bool); Term nts = d_solver.mkVar(bool); - Grammar g1 = d_solver.mkSygusGrammar(new Term[] {x}, new Term[] {start}); - Grammar g2 = d_solver.mkSygusGrammar(new Term[] {}, new Term[] {start}); + Grammar g1 = d_solver.mkGrammar(new Term[] {x}, new Term[] {start}); + Grammar g2 = d_solver.mkGrammar(new Term[] {}, new Term[] {start}); assertDoesNotThrow(() -> g1.addAnyVariable(start)); assertDoesNotThrow(() -> g1.addAnyVariable(start)); diff --git a/test/unit/api/java/SolverTest.java b/test/unit/api/java/SolverTest.java index 6327bb553..4cfbfcb88 100644 --- a/test/unit/api/java/SolverTest.java +++ b/test/unit/api/java/SolverTest.java @@ -1418,7 +1418,7 @@ class SolverTest Term truen = d_solver.mkBoolean(true); Term start = d_solver.mkVar(bsort); Term output2 = d_solver.getNullTerm(); - Grammar g = d_solver.mkSygusGrammar(new Term[] {}, new Term[] {start}); + Grammar g = d_solver.mkGrammar(new Term[] {}, new Term[] {start}); Term conj2 = d_solver.mkTerm(GT, x, zero); assertDoesNotThrow(() -> g.addRule(start, truen)); // Call the abduction api, while the resulting abduct is the output @@ -2599,35 +2599,37 @@ class SolverTest } @Test - void mkSygusGrammar() throws CVC5ApiException - { + void mkGrammar() throws CVC5ApiException { Term nullTerm = d_solver.getNullTerm(); Term boolTerm = d_solver.mkBoolean(true); Term boolVar = d_solver.mkVar(d_solver.getBooleanSort()); Term intVar = d_solver.mkVar(d_solver.getIntegerSort()); - assertDoesNotThrow(() -> d_solver.mkSygusGrammar(new Term[] {}, new Term[] {intVar})); - assertDoesNotThrow(() -> d_solver.mkSygusGrammar(new Term[] {boolVar}, new Term[] {intVar})); + assertDoesNotThrow( + () -> d_solver.mkGrammar(new Term[] {}, new Term[] {intVar})); + assertDoesNotThrow( + () -> d_solver.mkGrammar(new Term[] {boolVar}, new Term[] {intVar})); - assertThrows( - CVC5ApiException.class, () -> d_solver.mkSygusGrammar(new Term[] {}, new Term[] {})); assertThrows(CVC5ApiException.class, - () -> d_solver.mkSygusGrammar(new Term[] {}, new Term[] {nullTerm})); + () -> d_solver.mkGrammar(new Term[] {}, new Term[] {})); + assertThrows(CVC5ApiException.class, + () -> d_solver.mkGrammar(new Term[] {}, new Term[] {nullTerm})); assertThrows(CVC5ApiException.class, - () -> d_solver.mkSygusGrammar(new Term[] {}, new Term[] {boolTerm})); + () -> d_solver.mkGrammar(new Term[] {}, new Term[] {boolTerm})); assertThrows(CVC5ApiException.class, - () -> d_solver.mkSygusGrammar(new Term[] {boolTerm}, new Term[] {intVar})); + () -> d_solver.mkGrammar(new Term[] {boolTerm}, new Term[] {intVar})); Solver slv = new Solver(); slv.setOption("sygus", "true"); Term boolVar2 = slv.mkVar(slv.getBooleanSort()); Term intVar2 = slv.mkVar(slv.getIntegerSort()); - assertDoesNotThrow(() -> slv.mkSygusGrammar(new Term[] {boolVar2}, new Term[] {intVar2})); + assertDoesNotThrow( + () -> slv.mkGrammar(new Term[] {boolVar2}, new Term[] {intVar2})); assertThrows(CVC5ApiException.class, - () -> slv.mkSygusGrammar(new Term[] {boolVar}, new Term[] {intVar2})); + () -> slv.mkGrammar(new Term[] {boolVar}, new Term[] {intVar2})); assertThrows(CVC5ApiException.class, - () -> slv.mkSygusGrammar(new Term[] {boolVar2}, new Term[] {intVar})); + () -> slv.mkGrammar(new Term[] {boolVar2}, new Term[] {intVar})); slv.close(); } @@ -2645,10 +2647,10 @@ class SolverTest Term start1 = d_solver.mkVar(bool); Term start2 = d_solver.mkVar(integer); - Grammar g1 = d_solver.mkSygusGrammar(new Term[] {x}, new Term[] {start1}); + Grammar g1 = d_solver.mkGrammar(new Term[] {x}, new Term[] {start1}); g1.addRule(start1, d_solver.mkBoolean(false)); - Grammar g2 = d_solver.mkSygusGrammar(new Term[] {x}, new Term[] {start2}); + Grammar g2 = d_solver.mkGrammar(new Term[] {x}, new Term[] {start2}); g2.addRule(start2, d_solver.mkInteger(0)); assertDoesNotThrow(() -> d_solver.synthFun("", new Term[] {}, bool)); @@ -2685,10 +2687,10 @@ class SolverTest Term start1 = d_solver.mkVar(bool); Term start2 = d_solver.mkVar(integer); - Grammar g1 = d_solver.mkSygusGrammar(new Term[] {x}, new Term[] {start1}); + Grammar g1 = d_solver.mkGrammar(new Term[] {x}, new Term[] {start1}); g1.addRule(start1, d_solver.mkBoolean(false)); - Grammar g2 = d_solver.mkSygusGrammar(new Term[] {x}, new Term[] {start2}); + Grammar g2 = d_solver.mkGrammar(new Term[] {x}, new Term[] {start2}); g2.addRule(start2, d_solver.mkInteger(0)); assertDoesNotThrow(() -> d_solver.synthInv("", new Term[] {})); diff --git a/test/unit/api/python/test_grammar.py b/test/unit/api/python/test_grammar.py index 6bdd504f2..1c00da13c 100644 --- a/test/unit/api/python/test_grammar.py +++ b/test/unit/api/python/test_grammar.py @@ -34,7 +34,7 @@ def test_add_rule(solver): nts = solver.mkVar(boolean) # expecting no error - g = solver.mkSygusGrammar([], [start]) + g = solver.mkGrammar([], [start]) g.addRule(start, solver.mkBoolean(False)) @@ -67,7 +67,7 @@ def test_add_rules(solver): start = solver.mkVar(boolean) nts = solver.mkVar(boolean) - g = solver.mkSygusGrammar([], [start]) + g = solver.mkGrammar([], [start]) g.addRules(start, {solver.mkBoolean(False)}) @@ -98,7 +98,7 @@ def test_add_any_constant(solver): start = solver.mkVar(boolean) nts = solver.mkVar(boolean) - g = solver.mkSygusGrammar({}, {start}) + g = solver.mkGrammar({}, {start}) g.addAnyConstant(start) g.addAnyConstant(start) @@ -123,8 +123,8 @@ def test_add_any_variable(solver): start = solver.mkVar(boolean) nts = solver.mkVar(boolean) - g1 = solver.mkSygusGrammar({x}, {start}) - g2 = solver.mkSygusGrammar({}, {start}) + g1 = solver.mkGrammar({x}, {start}) + g2 = solver.mkGrammar({}, {start}) g1.addAnyVariable(start) g1.addAnyVariable(start) diff --git a/test/unit/api/python/test_solver.py b/test/unit/api/python/test_solver.py index 657df3306..019edc251 100644 --- a/test/unit/api/python/test_solver.py +++ b/test/unit/api/python/test_solver.py @@ -1885,24 +1885,24 @@ def test_mk_sygus_grammar(solver): boolVar = solver.mkVar(solver.getBooleanSort()) intVar = solver.mkVar(solver.getIntegerSort()) - solver.mkSygusGrammar([], [intVar]) - solver.mkSygusGrammar([boolVar], [intVar]) + solver.mkGrammar([], [intVar]) + solver.mkGrammar([boolVar], [intVar]) with pytest.raises(RuntimeError): - solver.mkSygusGrammar([], []) + solver.mkGrammar([], []) with pytest.raises(RuntimeError): - solver.mkSygusGrammar([], [nullTerm]) + solver.mkGrammar([], [nullTerm]) with pytest.raises(RuntimeError): - solver.mkSygusGrammar([], [boolTerm]) + solver.mkGrammar([], [boolTerm]) with pytest.raises(RuntimeError): - solver.mkSygusGrammar([boolTerm], [intVar]) + solver.mkGrammar([boolTerm], [intVar]) slv = cvc5.Solver() boolVar2 = slv.mkVar(slv.getBooleanSort()) intVar2 = slv.mkVar(slv.getIntegerSort()) - slv.mkSygusGrammar([boolVar2], [intVar2]) + slv.mkGrammar([boolVar2], [intVar2]) with pytest.raises(RuntimeError): - slv.mkSygusGrammar([boolVar], [intVar2]) + slv.mkGrammar([boolVar], [intVar2]) with pytest.raises(RuntimeError): - slv.mkSygusGrammar([boolVar2], [intVar]) + slv.mkGrammar([boolVar2], [intVar]) def test_synth_inv(solver): @@ -1916,10 +1916,10 @@ def test_synth_inv(solver): start1 = solver.mkVar(boolean) start2 = solver.mkVar(integer) - g1 = solver.mkSygusGrammar([x], [start1]) + g1 = solver.mkGrammar([x], [start1]) g1.addRule(start1, solver.mkBoolean(False)) - g2 = solver.mkSygusGrammar([x], [start2]) + g2 = solver.mkGrammar([x], [start2]) g2.addRule(start2, solver.mkInteger(0)) solver.synthInv("", []) @@ -2114,7 +2114,7 @@ def test_get_abduct(solver): truen = solver.mkBoolean(True) start = solver.mkVar(boolean) output2 = cvc5.Term(solver) - g = solver.mkSygusGrammar([], [start]) + g = solver.mkGrammar([], [start]) conj2 = solver.mkTerm(Kind.GT, x, zero) g.addRule(start, truen) output2 = solver.getAbduct(conj2, g) @@ -2520,10 +2520,10 @@ def test_synth_fun(solver): start1 = solver.mkVar(boolean) start2 = solver.mkVar(integer) - g1 = solver.mkSygusGrammar(x, [start1]) + g1 = solver.mkGrammar(x, [start1]) g1.addRule(start1, solver.mkBoolean(False)) - g2 = solver.mkSygusGrammar(x, [start2]) + g2 = solver.mkGrammar(x, [start2]) g2.addRule(start2, solver.mkInteger(0)) solver.synthFun("", [], boolean) -- 2.30.2