From 5278d7deb81773f8a801966f7aa7e8475efa5d84 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 11 Mar 2022 15:41:54 -0600 Subject: [PATCH] Update abduction and interpolation API to not use pass/return by reference (#8263) --- src/api/cpp/cvc5.cpp | 70 +++++------------ src/api/cpp/cvc5.h | 52 +++++++------ src/api/java/io/github/cvc5/api/Solver.java | 83 +++++++++++---------- src/api/java/jni/solver.cpp | 78 ++++++++++--------- src/api/python/cvc5.pxd | 12 +-- src/api/python/cvc5.pxi | 43 ++++++----- src/smt/command.cpp | 43 ++++------- src/smt/command.h | 8 -- src/smt/solver_engine.cpp | 28 ++++--- src/smt/solver_engine.h | 15 ++-- test/unit/api/cpp/solver_black.cpp | 28 +++---- test/unit/api/java/SolverTest.java | 22 ++---- test/unit/api/python/test_solver.py | 22 ++---- 13 files changed, 216 insertions(+), 288 deletions(-) diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp index c65db3dd1..a54588b11 100644 --- a/src/api/cpp/cvc5.cpp +++ b/src/api/cpp/cvc5.cpp @@ -7563,7 +7563,7 @@ void Solver::pop(uint32_t nscopes) const CVC5_API_TRY_CATCH_END; } -bool Solver::getInterpolant(const Term& conj, Term& output) const +Term Solver::getInterpolant(const Term& conj) const { CVC5_API_TRY_CATCH_BEGIN; CVC5_API_SOLVER_CHECK_TERM(conj); @@ -7572,21 +7572,14 @@ bool Solver::getInterpolant(const Term& conj, Term& output) const << "Cannot get interpolant unless interpolants are enabled (try " "--produce-interpols=mode)"; //////// all checks before this line - Node result; TypeNode nullType; - bool success = d_slv->getInterpolant(*conj.d_node, nullType, result); - if (success) - { - output = Term(this, result); - } - return success; + Node result = d_slv->getInterpolant(*conj.d_node, nullType); + return Term(this, result); //////// CVC5_API_TRY_CATCH_END; } -bool Solver::getInterpolant(const Term& conj, - Grammar& grammar, - Term& output) const +Term Solver::getInterpolant(const Term& conj, Grammar& grammar) const { CVC5_API_TRY_CATCH_BEGIN; CVC5_API_SOLVER_CHECK_TERM(conj); @@ -7595,19 +7588,13 @@ bool Solver::getInterpolant(const Term& conj, << "Cannot get interpolant unless interpolants are enabled (try " "--produce-interpols=mode)"; //////// all checks before this line - Node result; - bool success = - d_slv->getInterpolant(*conj.d_node, *grammar.resolve().d_type, result); - if (success) - { - output = Term(this, result); - } - return success; + Node result = d_slv->getInterpolant(*conj.d_node, *grammar.resolve().d_type); + return Term(this, result); //////// CVC5_API_TRY_CATCH_END; } -bool Solver::getInterpolantNext(Term& output) const +Term Solver::getInterpolantNext() const { CVC5_API_TRY_CATCH_BEGIN; CVC5_API_CHECK(d_slv->getOptions().smt.produceInterpols @@ -7618,56 +7605,40 @@ bool Solver::getInterpolantNext(Term& output) const << "Cannot get next interpolant when not solving incrementally (try " "--incremental)"; //////// all checks before this line - Node result; - bool success = d_slv->getInterpolantNext(result); - if (success) - { - output = Term(this, result); - } - return success; + Node result = d_slv->getInterpolantNext(); + return Term(this, result); //////// CVC5_API_TRY_CATCH_END; } -bool Solver::getAbduct(const Term& conj, Term& output) const +Term Solver::getAbduct(const Term& conj) const { CVC5_API_TRY_CATCH_BEGIN; CVC5_API_SOLVER_CHECK_TERM(conj); CVC5_API_CHECK(d_slv->getOptions().smt.produceAbducts) << "Cannot get abduct unless abducts are enabled (try --produce-abducts)"; //////// all checks before this line - Node result; TypeNode nullType; - bool success = d_slv->getAbduct(*conj.d_node, nullType, result); - if (success) - { - output = Term(this, result); - } - return success; + Node result = d_slv->getAbduct(*conj.d_node, nullType); + return Term(this, result); //////// CVC5_API_TRY_CATCH_END; } -bool Solver::getAbduct(const Term& conj, Grammar& grammar, Term& output) const +Term Solver::getAbduct(const Term& conj, Grammar& grammar) const { CVC5_API_TRY_CATCH_BEGIN; CVC5_API_SOLVER_CHECK_TERM(conj); CVC5_API_CHECK(d_slv->getOptions().smt.produceAbducts) << "Cannot get abduct unless abducts are enabled (try --produce-abducts)"; //////// all checks before this line - Node result; - bool success = - d_slv->getAbduct(*conj.d_node, *grammar.resolve().d_type, result); - if (success) - { - output = Term(this, result); - } - return success; + Node result = d_slv->getAbduct(*conj.d_node, *grammar.resolve().d_type); + return Term(this, result); //////// CVC5_API_TRY_CATCH_END; } -bool Solver::getAbductNext(Term& output) const +Term Solver::getAbductNext() const { CVC5_API_TRY_CATCH_BEGIN; CVC5_API_CHECK(d_slv->getOptions().smt.produceAbducts) @@ -7677,13 +7648,8 @@ bool Solver::getAbductNext(Term& output) const << "Cannot get next abduct when not solving incrementally (try " "--incremental)"; //////// all checks before this line - Node result; - bool success = d_slv->getAbductNext(result); - if (success) - { - output = Term(this, result); - } - return success; + Node result = d_slv->getAbductNext(); + return Term(this, result); //////// CVC5_API_TRY_CATCH_END; } diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h index 229fe6235..95c2d73b1 100644 --- a/src/api/cpp/cvc5.h +++ b/src/api/cpp/cvc5.h @@ -4422,11 +4422,11 @@ class CVC5_EXPORT Solver * \endverbatim * * @param conj the conjecture term - * @param output a Term I such that A->I and I->B are valid, where A is the - * current set of assertions and B is given in the input by conj. - * @return true if it gets I successfully, false otherwise. + * @return a Term I such that A->I and I->B are valid, where A is the + * current set of assertions and B is given in the input by conj, + * or the null term if such a term cannot be found. */ - bool getInterpolant(const Term& conj, Term& output) const; + Term getInterpolant(const Term& conj) const; /** * Get an interpolant @@ -4445,11 +4445,11 @@ class CVC5_EXPORT Solver * * @param conj the conjecture term * @param grammar the grammar for the interpolant I - * @param output a Term I such that A->I and I->B are valid, where A is the - * current set of assertions and B is given in the input by conj. - * @return true if it gets I successfully, false otherwise. + * @return a Term I such that A->I and I->B are valid, where A is the + * current set of assertions and B is given in the input by conj, + * or the null term if such a term cannot be found. */ - bool getInterpolant(const Term& conj, Grammar& grammar, Term& output) const; + Term getInterpolant(const Term& conj, Grammar& grammar) const; /** * Get the next interpolant. Can only be called immediately after a successful @@ -4469,12 +4469,11 @@ class CVC5_EXPORT Solver * mode different from `none`. * \endverbatim * - * @param output a Term I such that A->I and I->B are valid, where A is the - * current set of assertions and B is given in the input by conj - * on the last call to getInterpolant. - * @return true if it gets interpolant @f$C@f$ successfully, false otherwise + * @return a Term I such that A->I and I->B are valid, where A is the + * current set of assertions and B is given in the input by conj + * on the last call to getInterpolant. */ - bool getInterpolantNext(Term& output) const; + Term getInterpolantNext() const; /** * Get an abduct. @@ -4491,13 +4490,13 @@ class CVC5_EXPORT Solver * \endverbatim * * @param conj the conjecture term - * @param output a term @f$C@f$ such that @f$(A \wedge C)@f$ is satisfiable, - * and @f$(A \wedge \neg B \wedge C)@f$ is unsatisfiable, where - * @f$A@f$ is the current set of assertions and @f$B@f$ is - * given in the input by ``conj``. - * @return true if it gets abduct @f$C@f$ successfully, false otherwise + * @return a term @f$C@f$ such that @f$(A \wedge C)@f$ is satisfiable, + * and @f$(A \wedge \neg B \wedge C)@f$ is unsatisfiable, where + * @f$A@f$ is the current set of assertions and @f$B@f$ is + * given in the input by ``conj``, or the null term if such a term + * cannot be found. */ - bool getAbduct(const Term& conj, Term& output) const; + Term getAbduct(const Term& conj) const; /** * Get an abduct. @@ -4515,13 +4514,12 @@ class CVC5_EXPORT Solver * * @param conj the conjecture term * @param grammar the grammar for the abduct @f$C@f$ - * @param output a term C such that @f$(A \wedge C)@f$ is satisfiable, and + * @return a term C such that @f$(A \wedge C)@f$ is satisfiable, and * @f$(A \wedge \neg B \wedge C)@f$ is unsatisfiable, where @f$A@f$ is * the current set of assertions and @f$B@f$ is given in the input by - * ``conj`` - * @return true if it gets abduct @f$C@f$ successfully, false otherwise + * ``conj``, or the null term if such a term cannot be found. */ - bool getAbduct(const Term& conj, Grammar& grammar, Term& output) const; + Term getAbduct(const Term& conj, Grammar& grammar) const; /** * Get the next abduct. Can only be called immediately after a successful @@ -4539,13 +4537,13 @@ class CVC5_EXPORT Solver * :ref:`produce-abducts `. * \endverbatim * - * @param output a term C such that @f$(A \wedge C)@f$ is satisfiable, and + * @return a term C such that @f$(A \wedge C)@f$ is satisfiable, and * @f$(A \wedge \neg B \wedge C)@f$ is unsatisfiable, where @f$A@f$ is * the current set of assertions and @f$B@f$ is given in the input by - * the last call to getAbduct. - * @return true if it gets abduct @f$C@f$ successfully, false otherwise + * the last call to getAbduct, or the null term if such a term cannot + * be found. */ - bool getAbductNext(Term& output) const; + Term getAbductNext() const; /** * Block the current model. Can be called only if immediately preceded by a diff --git a/src/api/java/io/github/cvc5/api/Solver.java b/src/api/java/io/github/cvc5/api/Solver.java index 62e6d94eb..5b985c4cb 100644 --- a/src/api/java/io/github/cvc5/api/Solver.java +++ b/src/api/java/io/github/cvc5/api/Solver.java @@ -2166,16 +2166,17 @@ public class Solver implements IPointer, AutoCloseable * } * Requires 'produce-interpols' to be set to a mode different from 'none'. * @param conj the conjecture term - * @param output a Term I such that {@code A->I} and {@code I->B} are valid, where A is the - * current set of assertions and B is given in the input by conj. - * @return true if it gets I successfully, false otherwise. + * @return a Term I such that {@code A->I} and {@code I->B} are valid, where + * A is the current set of assertions and B is given in the input by + * conj, or the null term if such a term cannot be found. */ - public boolean getInterpolant(Term conj, Term output) + public Term getInterpolant(Term conj) { - return getInterpolant(pointer, conj.getPointer(), output.getPointer()); + long interpolPtr = getInterpolant(pointer, conj.getPointer()); + return new Term(this, interpolPtr); } - private native boolean getInterpolant(long pointer, long conjPointer, long outputPointer); + private native long getInterpolant(long pointer, long conjPointer); /** * Get an interpolant @@ -2186,17 +2187,17 @@ public class Solver implements IPointer, AutoCloseable * Requires 'produce-interpols' to be set to a mode different from 'none'. * @param conj the conjecture term * @param grammar the grammar for the interpolant I - * @param output a Term I such that {@code A->I} and {@code I->B} are valid, where A is the - * current set of assertions and B is given in the input by conj. - * @return true if it gets I successfully, false otherwise. + * @return a Term I such that {@code A->I} and {@code I->B} are valid, where + * A is the current set of assertions and B is given in the input by + * conj, or the null term if such a term cannot be found. */ - public boolean getInterpolant(Term conj, Grammar grammar, Term output) + public Term getInterpolant(Term conj, Grammar grammar) { - return getInterpolant(pointer, conj.getPointer(), grammar.getPointer(), output.getPointer()); + long interpolPtr = getInterpolant(pointer, conj.getPointer(), grammar.getPointer()); + return new Term(this, interpolPtr); } - private native boolean getInterpolant( - long pointer, long conjPointer, long grammarPointer, long outputPointer); + private native long getInterpolant(long pointer, long conjPointer, long grammarPointer); /** * Get the next interpolant. Can only be called immediately after a successful @@ -2215,17 +2216,18 @@ public class Solver implements IPointer, AutoCloseable * set to a mode different from 'none'. * \endverbatim * - * @param output a Term I such that {@code A->I} and {@code I->B} are valid, + * @return a Term I such that {@code A->I} and {@code I->B} are valid, * where A is the current set of assertions and B is given in the input - * by conj on the last call to getInterpolant. - * @return true if it gets interpolant @f$C@f$ successfully, false otherwise + * by conj on the last call to getInterpolant, or the null term if such + * a term cannot be found. */ - public boolean getInterpolantNext(Term output) + public Term getInterpolantNext() { - return getInterpolantNext(pointer, output.getPointer()); + long interpolPtr = getInterpolantNext(pointer); + return new Term(this, interpolPtr); } - private native boolean getInterpolantNext(long pointer, long outputPointer); + private native long getInterpolantNext(long pointer); /** * Get an abduct. @@ -2235,17 +2237,18 @@ public class Solver implements IPointer, AutoCloseable * } * Requires enabling option 'produce-abducts' * @param conj the conjecture term - * @param output a term C such that A^C is satisfiable, and A^~B^C is + * @return a term C such that A^C is satisfiable, and A^~B^C is * unsatisfiable, where A is the current set of assertions and B is - * given in the input by conj - * @return true if it gets C successfully, false otherwise + * given in the input by conj, or the null term if such a term cannot + * be found. */ - public boolean getAbduct(Term conj, Term output) + public Term getAbduct(Term conj) { - return getAbduct(pointer, conj.getPointer(), output.getPointer()); + long abdPtr = getAbduct(pointer, conj.getPointer()); + return new Term(this, abdPtr); } - private native boolean getAbduct(long pointer, long conjPointer, long outputPointer); + private native long getAbduct(long pointer, long conjPointer); /** * Get an abduct. * SMT-LIB: @@ -2255,18 +2258,18 @@ public class Solver implements IPointer, AutoCloseable * Requires enabling option 'produce-abducts' * @param conj the conjecture term * @param grammar the grammar for the abduct C - * @param output a term C such that A^C is satisfiable, and A^~B^C is + * @return a term C such that A^C is satisfiable, and A^~B^C is * unsatisfiable, where A is the current set of assertions and B is - * given in the input by conj - * @return true if it gets C successfully, false otherwise + * given in the input by conj, or the null term if such a term cannot + * be found. */ - public boolean getAbduct(Term conj, Grammar grammar, Term output) + public Term getAbduct(Term conj, Grammar grammar) { - return getAbduct(pointer, conj.getPointer(), grammar.getPointer(), output.getPointer()); + long abdPtr = getAbduct(pointer, conj.getPointer(), grammar.getPointer()); + return new Term(this, abdPtr); } - private native boolean getAbduct( - long pointer, long conjPointer, long grammarPointer, long outputPointer); + private native long getAbduct(long pointer, long conjPointer, long grammarPointer); /** * Get the next abduct. Can only be called immediately after a successful @@ -2277,16 +2280,18 @@ public class Solver implements IPointer, AutoCloseable * ( get-abduct-next ) * } * Requires enabling incremental mode and option 'produce-abducts' - * @param output a term C such that A^C is satisfiable, and A^~B^C is - * unsatisfiable, where A is the current set of assertions and B is - * given in the input by conj in the last call to getAbduct. - * @return true if it gets C successfully, false otherwise + * @return a term C such that A^C is satisfiable, and A^~B^C is + * unsatisfiable, where A is the current set of assertions and B is + * given in the input by conj in the last call to getAbduct, or the + * null term if such a term cannot be found. */ - public boolean getAbductNext(Term output) { - return getAbductNext(pointer, output.getPointer()); + public Term getAbductNext() + { + long abdPtr = getAbductNext(pointer); + return new Term(this, abdPtr); } - private native boolean getAbductNext(long pointer, long outputPointer); + private native long getAbductNext(long pointer); /** * Block the current model. Can be called only if immediately preceded by a diff --git a/src/api/java/jni/solver.cpp b/src/api/java/jni/solver.cpp index 63a6c179a..7d4d2acd6 100644 --- a/src/api/java/jni/solver.cpp +++ b/src/api/java/jni/solver.cpp @@ -2178,106 +2178,104 @@ JNIEXPORT void JNICALL Java_io_github_cvc5_api_Solver_pop(JNIEnv* env, /* * Class: io_github_cvc5_api_Solver * Method: getInterpolant - * Signature: (JJJ)Z + * Signature: (JJ)J */ -JNIEXPORT jboolean JNICALL Java_io_github_cvc5_api_Solver_getInterpolant__JJJ( - JNIEnv* env, jobject, jlong pointer, jlong conjPointer, jlong outputPointer) +JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_getInterpolant__JJ( + JNIEnv* env, jobject, jlong pointer, jlong conjPointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Solver* solver = reinterpret_cast(pointer); Term* conj = reinterpret_cast(conjPointer); - Term* output = reinterpret_cast(outputPointer); - return (jboolean)solver->getInterpolant(*conj, *output); + Term* result = new Term(solver->getInterpolant(*conj)); + return reinterpret_cast(result); CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); } /* * Class: io_github_cvc5_api_Solver * Method: getInterpolant - * Signature: (JJJJ)Z + * Signature: (JJJ)J */ -JNIEXPORT jboolean JNICALL -Java_io_github_cvc5_api_Solver_getInterpolant__JJJJ(JNIEnv* env, - jobject, - jlong pointer, - jlong conjPointer, - jlong grammarPointer, - jlong outputPointer) +JNIEXPORT jlong JNICALL +Java_io_github_cvc5_api_Solver_getInterpolant__JJJ(JNIEnv* env, + jobject, + jlong pointer, + jlong conjPointer, + jlong grammarPointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Solver* solver = reinterpret_cast(pointer); Term* conj = reinterpret_cast(conjPointer); Grammar* grammar = reinterpret_cast(grammarPointer); - Term* output = reinterpret_cast(outputPointer); - return (jboolean)solver->getInterpolant(*conj, *grammar, *output); + Term* result = new Term(solver->getInterpolant(*conj, *grammar)); + return reinterpret_cast(result); CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); } /* * Class: io_github_cvc5_api_Solver * Method: getInterpolantNext - * Signature: (JJ)Z + * Signature: (J)J */ -JNIEXPORT jboolean JNICALL Java_io_github_cvc5_api_Solver_getInterpolantNext( - JNIEnv* env, jobject, jlong pointer, jlong outputPointer) +JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_getInterpolantNext( + JNIEnv* env, jobject, jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Solver* solver = reinterpret_cast(pointer); - Term* output = reinterpret_cast(outputPointer); - return (jboolean)solver->getInterpolantNext(*output); + Term* result = new Term(solver->getInterpolantNext()); + return reinterpret_cast(result); CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); } /* * Class: io_github_cvc5_api_Solver * Method: getAbduct - * Signature: (JJJ)Z + * Signature: (JJ)J */ -JNIEXPORT jboolean JNICALL Java_io_github_cvc5_api_Solver_getAbduct__JJJ( - JNIEnv* env, jobject, jlong pointer, jlong conjPointer, jlong outputPointer) +JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_getAbduct__JJ( + JNIEnv* env, jobject, jlong pointer, jlong conjPointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Solver* solver = reinterpret_cast(pointer); Term* conj = reinterpret_cast(conjPointer); - Term* output = reinterpret_cast(outputPointer); - return (jboolean)solver->getAbduct(*conj, *output); + Term* result = new Term(solver->getAbduct(*conj)); + return reinterpret_cast(result); CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); } /* * Class: io_github_cvc5_api_Solver * Method: getAbduct - * Signature: (JJJJ)Z + * Signature: (JJJ)J */ -JNIEXPORT jboolean JNICALL -Java_io_github_cvc5_api_Solver_getAbduct__JJJJ(JNIEnv* env, - jobject, - jlong pointer, - jlong conjPointer, - jlong grammarPointer, - jlong outputPointer) +JNIEXPORT jlong JNICALL +Java_io_github_cvc5_api_Solver_getAbduct__JJJ(JNIEnv* env, + jobject, + jlong pointer, + jlong conjPointer, + jlong grammarPointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Solver* solver = reinterpret_cast(pointer); Term* conj = reinterpret_cast(conjPointer); Grammar* grammar = reinterpret_cast(grammarPointer); - Term* output = reinterpret_cast(outputPointer); - return (jboolean)solver->getAbduct(*conj, *grammar, *output); + Term* result = new Term(solver->getAbduct(*conj, *grammar)); + return reinterpret_cast(result); CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); } /* * Class: io_github_cvc5_api_Solver * Method: getAbductNext - * Signature: (JJ)Z + * Signature: (J)J */ -JNIEXPORT jboolean JNICALL Java_io_github_cvc5_api_Solver_getAbductNext - (JNIEnv * env, jobject, jlong pointer, jlong outputPointer) +JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_getAbductNext( + JNIEnv* env, jobject, jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Solver* solver = reinterpret_cast(pointer); - Term* output = reinterpret_cast(outputPointer); - return (jboolean)solver->getAbductNext(*output); + Term* result = new Term(solver->getAbductNext()); + return reinterpret_cast(result); CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); } diff --git a/src/api/python/cvc5.pxd b/src/api/python/cvc5.pxd index bff77fbce..740a58a03 100644 --- a/src/api/python/cvc5.pxd +++ b/src/api/python/cvc5.pxd @@ -295,12 +295,12 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5::api": void setInfo(string& keyword, const string& value) except + void setLogic(const string& logic) except + void setOption(const string& option, const string& value) except + - bint getInterpolant(const Term& conj, Term& output) except + - bint getInterpolant(const Term& conj, Grammar& grammar, Term& output) except + - bint getInterpolantNext(const Term& conj) except + - bint getAbduct(const Term& conj, Term& output) except + - bint getAbduct(const Term& conj, Grammar& grammar, Term& output) except + - bint getAbductNext(const Term& conj) except + + Term getInterpolant(const Term& conj) except + + Term getInterpolant(const Term& conj, Grammar& grammar) except + + Term getInterpolantNext() except + + Term getAbduct(const Term& conj) except + + Term getAbduct(const Term& conj, Grammar& grammar) except + + Term getAbductNext() except + void blockModel() except + void blockModelValues(const vector[Term]& terms) except + string getInstantiations() except + diff --git a/src/api/python/cvc5.pxi b/src/api/python/cvc5.pxi index 2c535b2e4..b259687b4 100644 --- a/src/api/python/cvc5.pxi +++ b/src/api/python/cvc5.pxi @@ -2246,6 +2246,7 @@ cdef class Solver: """ self.csolver.setOption(option.encode(), value.encode()) + def getInterpolant(self, Term conj, *args): """Get an interpolant. @@ -2260,27 +2261,25 @@ cdef class Solver: Supports the following variants: - - ``bool getInteprolant(Term conj, Term output)`` - - ``bool getInteprolant(Term conj, Grammar grammar, Term output)`` + - ``Term getInteprolant(Term conj)`` + - ``Term getInteprolant(Term conj, Grammar grammar)`` :param conj: the conjecture term :param output: the term where the result will be stored :param grammar: a grammar for the inteprolant :return: True iff an interpolant was found """ - result = False - if len(args) == 1: - assert isinstance(args[0], Term) - result = self.csolver.getInterpolant(conj.cterm, ( args[0]).cterm) + cdef Term result = Term(self) + if len(args) == 0: + result.cterm = self.csolver.getInterpolant(conj.cterm) else: - assert len(args) == 2 + assert len(args) == 1 assert isinstance(args[0], Grammar) - assert isinstance(args[1], Term) - result = self.csolver.getInterpolant(conj.cterm, ( args[0]).cgrammar, ( args[1]).cterm) + result.cterm = self.csolver.getInterpolant(conj.cterm, ( args[0]).cgrammar) return result - def getInterpolantNext(self, Term output): + def getInterpolantNext(self): """ Get the next interpolant. Can only be called immediately after a succesful call to get-interpol or get-interpol-next. @@ -2299,7 +2298,8 @@ cdef class Solver: :param output: the term where the result will be stored :return: True iff an interpolant was found """ - result = self.csolver.getInterpolantNext(output.cterm) + cdef Term result = Term(self) + result.cterm = self.csolver.getInterpolantNext() return result def getAbduct(self, Term conj, *args): @@ -2316,26 +2316,24 @@ cdef class Solver: Supports the following variants: - - ``bool getAbduct(Term conj, Term output)`` - - ``bool getAbduct(Term conj, Grammar grammar, Term output)`` + - ``Term getAbduct(Term conj)`` + - ``Term getAbduct(Term conj, Grammar grammar)`` :param conj: the conjecture term :param output: the term where the result will be stored :param grammar: a grammar for the abduct :return: True iff an abduct was found """ - result = False - if len(args) == 1: - assert isinstance(args[0], Term) - result = self.csolver.getAbduct(conj.cterm, ( args[0]).cterm) + cdef Term result = Term(self) + if len(args) == 0: + result.cterm = self.csolver.getAbduct(conj.cterm) else: - assert len(args) == 2 + assert len(args) == 1 assert isinstance(args[0], Grammar) - assert isinstance(args[1], Term) - result = self.csolver.getAbduct(conj.cterm, ( args[0]).cgrammar, ( args[1]).cterm) + result.cterm = self.csolver.getAbduct(conj.cterm, ( args[0]).cgrammar) return result - def getAbductNext(self, Term output): + def getAbductNext(self): """ Get the next abduct. Can only be called immediately after a succesful call to get-abduct or get-abduct-next. @@ -2353,7 +2351,8 @@ cdef class Solver: :param output: the term where the result will be stored :return: True iff an abduct was found """ - result = self.csolver.getAbductNext(output.cterm) + cdef Term result = Term(self) + result.cterm = self.csolver.getAbductNext() return result def blockModel(self): diff --git a/src/smt/command.cpp b/src/smt/command.cpp index 2766c6510..1474ed240 100644 --- a/src/smt/command.cpp +++ b/src/smt/command.cpp @@ -1944,16 +1944,13 @@ void GetInstantiationsCommand::toStream(std::ostream& out, /* -------------------------------------------------------------------------- */ GetInterpolCommand::GetInterpolCommand(const std::string& name, api::Term conj) - : d_name(name), - d_conj(conj), - d_sygus_grammar(nullptr), - d_resultStatus(false) + : d_name(name), d_conj(conj), d_sygus_grammar(nullptr) { } GetInterpolCommand::GetInterpolCommand(const std::string& name, api::Term conj, api::Grammar* g) - : d_name(name), d_conj(conj), d_sygus_grammar(g), d_resultStatus(false) + : d_name(name), d_conj(conj), d_sygus_grammar(g) { } @@ -1975,12 +1972,11 @@ void GetInterpolCommand::invoke(api::Solver* solver, SymbolManager* sm) sm->setLastSynthName(d_name); if (d_sygus_grammar == nullptr) { - d_resultStatus = solver->getInterpolant(d_conj, d_result); + d_result = solver->getInterpolant(d_conj); } else { - d_resultStatus = - solver->getInterpolant(d_conj, *d_sygus_grammar, d_result); + d_result = solver->getInterpolant(d_conj, *d_sygus_grammar); } d_commandStatus = CommandSuccess::instance(); } @@ -2000,7 +1996,7 @@ void GetInterpolCommand::printResult(std::ostream& out) const { options::ioutils::Scope scope(out); options::ioutils::applyDagThresh(out, 0); - if (d_resultStatus) + if (!d_result.isNull()) { out << "(define-fun " << d_name << " () Bool " << d_result << ")" << std::endl; @@ -2017,7 +2013,6 @@ Command* GetInterpolCommand::clone() const GetInterpolCommand* c = new GetInterpolCommand(d_name, d_conj, d_sygus_grammar); c->d_result = d_result; - c->d_resultStatus = d_resultStatus; return c; } @@ -2039,7 +2034,7 @@ void GetInterpolCommand::toStream(std::ostream& out, /* class GetInterpolNextCommand */ /* -------------------------------------------------------------------------- */ -GetInterpolNextCommand::GetInterpolNextCommand() : d_resultStatus(false) {} +GetInterpolNextCommand::GetInterpolNextCommand() {} api::Term GetInterpolNextCommand::getResult() const { return d_result; } @@ -2049,7 +2044,7 @@ void GetInterpolNextCommand::invoke(api::Solver* solver, SymbolManager* sm) { // Get the name of the interpolant from the symbol manager d_name = sm->getLastSynthName(); - d_resultStatus = solver->getInterpolantNext(d_result); + d_result = solver->getInterpolantNext(); d_commandStatus = CommandSuccess::instance(); } catch (exception& e) @@ -2068,7 +2063,7 @@ void GetInterpolNextCommand::printResult(std::ostream& out) const { options::ioutils::Scope scope(out); options::ioutils::applyDagThresh(out, 0); - if (d_resultStatus) + if (!d_result.isNull()) { out << "(define-fun " << d_name << " () Bool " << d_result << ")" << std::endl; @@ -2084,7 +2079,6 @@ Command* GetInterpolNextCommand::clone() const { GetInterpolNextCommand* c = new GetInterpolNextCommand; c->d_result = d_result; - c->d_resultStatus = d_resultStatus; return c; } @@ -2106,16 +2100,13 @@ void GetInterpolNextCommand::toStream(std::ostream& out, /* -------------------------------------------------------------------------- */ GetAbductCommand::GetAbductCommand(const std::string& name, api::Term conj) - : d_name(name), - d_conj(conj), - d_sygus_grammar(nullptr), - d_resultStatus(false) + : d_name(name), d_conj(conj), d_sygus_grammar(nullptr) { } GetAbductCommand::GetAbductCommand(const std::string& name, api::Term conj, api::Grammar* g) - : d_name(name), d_conj(conj), d_sygus_grammar(g), d_resultStatus(false) + : d_name(name), d_conj(conj), d_sygus_grammar(g) { } @@ -2138,11 +2129,11 @@ void GetAbductCommand::invoke(api::Solver* solver, SymbolManager* sm) sm->setLastSynthName(d_name); if (d_sygus_grammar == nullptr) { - d_resultStatus = solver->getAbduct(d_conj, d_result); + d_result = solver->getAbduct(d_conj); } else { - d_resultStatus = solver->getAbduct(d_conj, *d_sygus_grammar, d_result); + d_result = solver->getAbduct(d_conj, *d_sygus_grammar); } d_commandStatus = CommandSuccess::instance(); } @@ -2162,7 +2153,7 @@ void GetAbductCommand::printResult(std::ostream& out) const { options::ioutils::Scope scope(out); options::ioutils::applyDagThresh(out, 0); - if (d_resultStatus) + if (!d_result.isNull()) { out << "(define-fun " << d_name << " () Bool " << d_result << ")" << std::endl; @@ -2178,7 +2169,6 @@ Command* GetAbductCommand::clone() const { GetAbductCommand* c = new GetAbductCommand(d_name, d_conj, d_sygus_grammar); c->d_result = d_result; - c->d_resultStatus = d_resultStatus; return c; } @@ -2197,7 +2187,7 @@ void GetAbductCommand::toStream(std::ostream& out, /* class GetAbductNextCommand */ /* -------------------------------------------------------------------------- */ -GetAbductNextCommand::GetAbductNextCommand() : d_resultStatus(false) {} +GetAbductNextCommand::GetAbductNextCommand() {} api::Term GetAbductNextCommand::getResult() const { return d_result; } @@ -2207,7 +2197,7 @@ void GetAbductNextCommand::invoke(api::Solver* solver, SymbolManager* sm) { // Get the name of the abduct from the symbol manager d_name = sm->getLastSynthName(); - d_resultStatus = solver->getAbductNext(d_result); + d_result = solver->getAbductNext(); d_commandStatus = CommandSuccess::instance(); } catch (exception& e) @@ -2226,7 +2216,7 @@ void GetAbductNextCommand::printResult(std::ostream& out) const { options::ioutils::Scope scope(out); options::ioutils::applyDagThresh(out, 0); - if (d_resultStatus) + if (!d_result.isNull()) { out << "(define-fun " << d_name << " () Bool " << d_result << ")" << std::endl; @@ -2242,7 +2232,6 @@ Command* GetAbductNextCommand::clone() const { GetAbductNextCommand* c = new GetAbductNextCommand; c->d_result = d_result; - c->d_resultStatus = d_resultStatus; return c; } diff --git a/src/smt/command.h b/src/smt/command.h index b250d0b59..66c678ba8 100644 --- a/src/smt/command.h +++ b/src/smt/command.h @@ -1052,8 +1052,6 @@ class CVC5_EXPORT GetInterpolCommand : public Command api::Term d_conj; /** The (optional) grammar of the interpolation query */ api::Grammar* d_sygus_grammar; - /** the return status of the command */ - bool d_resultStatus; /** the return expression of the command */ api::Term d_result; }; /* class GetInterpolCommand */ @@ -1081,8 +1079,6 @@ class CVC5_EXPORT GetInterpolNextCommand : public Command protected: /** The name of the interpolation predicate */ std::string d_name; - /** the return status of the command */ - bool d_resultStatus; /** the return expression of the command */ api::Term d_result; }; @@ -1131,8 +1127,6 @@ class CVC5_EXPORT GetAbductCommand : public Command api::Term d_conj; /** The (optional) grammar of the abduction query */ api::Grammar* d_sygus_grammar; - /** the return status of the command */ - bool d_resultStatus; /** the return expression of the command */ api::Term d_result; }; /* class GetAbductCommand */ @@ -1159,8 +1153,6 @@ class CVC5_EXPORT GetAbductNextCommand : public Command protected: /** The name of the abduction predicate */ std::string d_name; - /** the return status of the command */ - bool d_resultStatus; /** the return expression of the command */ api::Term d_result; }; diff --git a/src/smt/solver_engine.cpp b/src/smt/solver_engine.cpp index 583eaae7b..9d8311392 100644 --- a/src/smt/solver_engine.cpp +++ b/src/smt/solver_engine.cpp @@ -1666,22 +1666,22 @@ Node SolverEngine::getQuantifierElimination(Node q, bool doFull) *d_asserts, q, doFull, d_isInternalSubsolver); } -bool SolverEngine::getInterpolant(const Node& conj, - const TypeNode& grammarType, - Node& interpol) +Node SolverEngine::getInterpolant(const Node& conj, const TypeNode& grammarType) { SolverEngineScope smts(this); finishInit(); std::vector axioms = getExpandedAssertions(); + Node interpol; bool success = d_interpolSolver->getInterpolant(axioms, conj, grammarType, interpol); // notify the state of whether the get-interpol call was successfuly, which // impacts the SMT mode. d_state->notifyGetInterpol(success); - return success; + Assert(success == !interpol.isNull()); + return interpol; } -bool SolverEngine::getInterpolantNext(Node& interpol) +Node SolverEngine::getInterpolantNext() { SolverEngineScope smts(this); finishInit(); @@ -1691,27 +1691,29 @@ bool SolverEngine::getInterpolantNext(Node& interpol) "Cannot get-interpol-next unless immediately preceded by a successful " "call to get-interpol(-next)."); } + Node interpol; bool success = d_interpolSolver->getInterpolantNext(interpol); // notify the state of whether the get-interpolant-next call was successful d_state->notifyGetInterpol(success); - return success; + Assert(success == !interpol.isNull()); + return interpol; } -bool SolverEngine::getAbduct(const Node& conj, - const TypeNode& grammarType, - Node& abd) +Node SolverEngine::getAbduct(const Node& conj, const TypeNode& grammarType) { SolverEngineScope smts(this); finishInit(); std::vector axioms = getExpandedAssertions(); + Node abd; bool success = d_abductSolver->getAbduct(axioms, conj, grammarType, abd); // notify the state of whether the get-abduct call was successful, which // impacts the SMT mode. d_state->notifyGetAbduct(success); - return success; + Assert(success == !abd.isNull()); + return abd; } -bool SolverEngine::getAbductNext(Node& abd) +Node SolverEngine::getAbductNext() { SolverEngineScope smts(this); finishInit(); @@ -1721,10 +1723,12 @@ bool SolverEngine::getAbductNext(Node& abd) "Cannot get-abduct-next unless immediately preceded by a successful " "call to get-abduct(-next)."); } + Node abd; bool success = d_abductSolver->getAbductNext(abd); // notify the state of whether the get-abduct-next call was successful d_state->notifyGetAbduct(success); - return success; + Assert(success == !abd.isNull()); + return abd; } void SolverEngine::getInstantiatedQuantifiedFormulas(std::vector& qs) diff --git a/src/smt/solver_engine.h b/src/smt/solver_engine.h index c6cd77dd7..ae8013965 100644 --- a/src/smt/solver_engine.h +++ b/src/smt/solver_engine.h @@ -639,18 +639,15 @@ class CVC5_EXPORT SolverEngine * This method invokes a separate copy of the SMT engine for solving the * corresponding sygus problem for generating such a solution. */ - bool getInterpolant(const Node& conj, - const TypeNode& grammarType, - Node& interpol); + Node getInterpolant(const Node& conj, const TypeNode& grammarType); /** * Get next interpolant. This can only be called immediately after a * successful call to getInterpolant or getInterpolantNext. * - * Returns true if an interpolant was found, and sets interpol to the - * interpolant. + * Returns the interpolant if one exists, or the null node otherwise. */ - bool getInterpolantNext(Node& interpol); + Node getInterpolantNext(); /** * This method asks this SMT engine to find an abduct with respect to the @@ -664,15 +661,15 @@ class CVC5_EXPORT SolverEngine * This method invokes a separate copy of the SMT engine for solving the * corresponding sygus problem for generating such a solution. */ - bool getAbduct(const Node& conj, const TypeNode& grammarType, Node& abd); + Node getAbduct(const Node& conj, const TypeNode& grammarType); /** * Get next abduct. This can only be called immediately after a successful * call to getAbduct or getAbductNext. * - * Returns true if an abduct was found, and sets abd to the abduct. + * Returns the abduct if one exists, or the null node otherwise. */ - bool getAbductNext(Node& abd); + Node getAbductNext(); /** * Get list of quantified formulas that were instantiated on the last call diff --git a/test/unit/api/cpp/solver_black.cpp b/test/unit/api/cpp/solver_black.cpp index d057154fc..4ea0b7ff1 100644 --- a/test/unit/api/cpp/solver_black.cpp +++ b/test/unit/api/cpp/solver_black.cpp @@ -1343,9 +1343,8 @@ TEST_F(TestApiBlackSolver, getAbduct) d_solver.assertFormula(d_solver.mkTerm(GT, x, zero)); // Conjecture for abduction: y > 0 Term conj = d_solver.mkTerm(GT, y, zero); - Term output; // Call the abduction api, while the resulting abduct is the output - ASSERT_TRUE(d_solver.getAbduct(conj, output)); + Term output = d_solver.getAbduct(conj); // We expect the resulting output to be a boolean formula ASSERT_TRUE(!output.isNull() && output.getSort().isBoolean()); @@ -1358,7 +1357,7 @@ TEST_F(TestApiBlackSolver, getAbduct) 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 - ASSERT_TRUE(d_solver.getAbduct(conj2, g, output2)); + output2 = d_solver.getAbduct(conj2, g); // abduct must be true ASSERT_EQ(output2, truen); } @@ -1375,9 +1374,8 @@ TEST_F(TestApiBlackSolver, getAbduct2) d_solver.assertFormula(d_solver.mkTerm(GT, x, zero)); // Conjecture for abduction: y > 0 Term conj = d_solver.mkTerm(GT, y, zero); - Term output; // Fails due to option not set - ASSERT_THROW(d_solver.getAbduct(conj, output), CVC5ApiException); + ASSERT_THROW(d_solver.getAbduct(conj), CVC5ApiException); } TEST_F(TestApiBlackSolver, getAbductNext) @@ -1395,11 +1393,9 @@ TEST_F(TestApiBlackSolver, getAbductNext) d_solver.assertFormula(d_solver.mkTerm(GT, x, zero)); // Conjecture for abduction: y > 0 Term conj = d_solver.mkTerm(GT, y, zero); - Term output; // Call the abduction api, while the resulting abduct is the output - ASSERT_TRUE(d_solver.getAbduct(conj, output)); - Term output2; - ASSERT_TRUE(d_solver.getAbductNext(output2)); + Term output = d_solver.getAbduct(conj); + Term output2 = d_solver.getAbductNext(); // should produce a different output ASSERT_TRUE(output != output2); } @@ -1424,9 +1420,8 @@ TEST_F(TestApiBlackSolver, getInterpolant) d_solver.mkTerm(OR, d_solver.mkTerm(GT, d_solver.mkTerm(ADD, y, z), zero), d_solver.mkTerm(LT, z, zero)); - Term output; // Call the interpolation api, while the resulting interpolant is the output - d_solver.getInterpolant(conj, output); + Term output = d_solver.getInterpolant(conj); // We expect the resulting output to be a boolean formula ASSERT_TRUE(output.getSort().isBoolean()); @@ -1451,10 +1446,8 @@ TEST_F(TestApiBlackSolver, getInterpolantNext) d_solver.mkTerm(OR, d_solver.mkTerm(GT, d_solver.mkTerm(ADD, y, z), zero), d_solver.mkTerm(LT, z, zero)); - Term output; - d_solver.getInterpolant(conj, output); - Term output2; - d_solver.getInterpolantNext(output2); + Term output = d_solver.getInterpolant(conj); + Term output2 = d_solver.getInterpolantNext(); // We expect the next output to be distinct ASSERT_TRUE(output != output2); @@ -3134,9 +3127,8 @@ TEST_F(TestApiBlackSolver, proj_issue436) t23 = slv.mkBitVector(bw, 1); } Term t33 = slv.mkTerm(Kind::BITVECTOR_ULT, {t17, t23}); - Term abduct; // solve-bv-as-int is incompatible with get-abduct - ASSERT_THROW(slv.getAbduct(t33, abduct), CVC5ApiException); + ASSERT_THROW(slv.getAbduct(t33), CVC5ApiException); } TEST_F(TestApiBlackSolver, proj_issue431) @@ -3250,7 +3242,7 @@ TEST_F(TestApiBlackSolver, projIssue431) Term t488 = slv.mkTerm(Kind::APPLY_UF, {t31, t274}); slv.assertFormula({t488}); Term abduct; - slv.getAbduct(t488, abduct); + abduct = slv.getAbduct(t488); } } // namespace test diff --git a/test/unit/api/java/SolverTest.java b/test/unit/api/java/SolverTest.java index 6bcd38e92..f4b3f7f91 100644 --- a/test/unit/api/java/SolverTest.java +++ b/test/unit/api/java/SolverTest.java @@ -1333,7 +1333,7 @@ class SolverTest Term conj = d_solver.mkTerm(GT, y, zero); Term output = d_solver.getNullTerm(); // Call the abduction api, while the resulting abduct is the output - assertTrue(d_solver.getAbduct(conj, output)); + output = d_solver.getAbduct(conj); // We expect the resulting output to be a boolean formula assertTrue(!output.isNull() && output.getSort().isBoolean()); @@ -1346,7 +1346,7 @@ class SolverTest Term conj2 = d_solver.mkTerm(GT, x, zero); assertDoesNotThrow(() -> g.addRule(start, truen)); // Call the abduction api, while the resulting abduct is the output - assertTrue(d_solver.getAbduct(conj2, g, output2)); + output2 = d_solver.getAbduct(conj2, g); // abduct must be true assertEquals(output2, truen); } @@ -1365,8 +1365,7 @@ class SolverTest Term conj = d_solver.mkTerm(GT, y, zero); Term output = d_solver.getNullTerm(); // Fails due to option not set - assertThrows( - CVC5ApiException.class, () -> d_solver.getAbduct(conj, output)); + assertThrows(CVC5ApiException.class, () -> d_solver.getAbduct(conj)); } @Test void getAbductNext() throws CVC5ApiException @@ -1384,11 +1383,9 @@ class SolverTest d_solver.assertFormula(d_solver.mkTerm(GT, x, zero)); // Conjecture for abduction: y > 0 Term conj = d_solver.mkTerm(GT, y, zero); - Term output = d_solver.getNullTerm(); // Call the abduction api, while the resulting abduct is the output - assertTrue(d_solver.getAbduct(conj, output)); - Term output2 = d_solver.getNullTerm(); - assertTrue(d_solver.getAbductNext(output2)); + Term output = d_solver.getAbduct(conj); + Term output2 = d_solver.getAbductNext(); // should produce a different output assertNotEquals(output, output2); } @@ -1412,9 +1409,8 @@ class SolverTest // Conjecture for interpolation: y + z > 0 \/ z < 0 Term conj = d_solver.mkTerm( OR, d_solver.mkTerm(GT, d_solver.mkTerm(ADD, y, z), zero), d_solver.mkTerm(LT, z, zero)); - Term output = d_solver.getNullTerm(); // Call the interpolation api, while the resulting interpolant is the output - d_solver.getInterpolant(conj, output); + Term output = d_solver.getInterpolant(conj); // We expect the resulting output to be a boolean formula assertTrue(output.getSort().isBoolean()); @@ -1436,10 +1432,8 @@ class SolverTest d_solver.assertFormula(d_solver.mkTerm(LT, x, zero)); Term conj = d_solver.mkTerm( OR, d_solver.mkTerm(GT, d_solver.mkTerm(ADD, y, z), zero), d_solver.mkTerm(LT, z, zero)); - Term output = d_solver.getNullTerm(); - d_solver.getInterpolant(conj, output); - Term output2 = d_solver.getNullTerm(); - d_solver.getInterpolantNext(output2); + Term output = d_solver.getInterpolant(conj); + Term output2 = d_solver.getInterpolantNext(); // We expect the next output to be distinct assertNotEquals(output, output2); diff --git a/test/unit/api/python/test_solver.py b/test/unit/api/python/test_solver.py index 69b08e092..a535c2502 100644 --- a/test/unit/api/python/test_solver.py +++ b/test/unit/api/python/test_solver.py @@ -2078,8 +2078,7 @@ def test_get_abduct(solver): solver.assertFormula(solver.mkTerm(Kind.Gt, x, zero)) conj = solver.mkTerm(Kind.Gt, y, zero) - output = cvc5.Term(solver) - assert solver.getAbduct(conj, output) + output = solver.getAbduct(conj) assert not output.isNull() and output.getSort().isBoolean() boolean = solver.getBooleanSort() @@ -2089,7 +2088,7 @@ def test_get_abduct(solver): g = solver.mkSygusGrammar([], [start]) conj2 = solver.mkTerm(Kind.Gt, x, zero) g.addRule(start, truen) - assert solver.getAbduct(conj2, g, output2) + output2 = solver.getAbduct(conj2, g) assert output2 == truen def test_get_abduct2(solver): @@ -2103,7 +2102,7 @@ def test_get_abduct2(solver): conj = solver.mkTerm(Kind.Gt, y, zero) output = cvc5.Term(solver) with pytest.raises(RuntimeError): - solver.getAbduct(conj, output) + solver.getAbduct(conj) def test_get_abduct_next(solver): solver.setLogic("QF_LIA") @@ -2117,10 +2116,8 @@ def test_get_abduct_next(solver): solver.assertFormula(solver.mkTerm(Kind.Gt, x, zero)) conj = solver.mkTerm(Kind.Gt, y, zero) - output = cvc5.Term(solver) - assert solver.getAbduct(conj, output) - output2 = cvc5.Term(solver) - assert solver.getAbductNext(output2) + output = solver.getAbduct(conj) + output2 = solver.getAbductNext() assert output != output2 @@ -2142,8 +2139,7 @@ def test_get_interpolant(solver): Kind.Or, solver.mkTerm(Kind.Gt, solver.mkTerm(Kind.Add, y, z), zero), solver.mkTerm(Kind.Lt, z, zero)) - output = cvc5.Term(solver) - solver.getInterpolant(conj, output) + output = solver.getInterpolant(conj) assert output.getSort().isBoolean() def test_get_interpolant_next(solver): @@ -2164,10 +2160,8 @@ def test_get_interpolant_next(solver): Kind.Or, solver.mkTerm(Kind.Gt, solver.mkTerm(Kind.Add, y, z), zero), solver.mkTerm(Kind.Lt, z, zero)) - output = cvc5.Term(solver) - solver.getInterpolant(conj, output) - output2 = cvc5.Term(solver) - solver.getInterpolantNext(output2) + output = solver.getInterpolant(conj) + output2 = solver.getInterpolantNext() assert output != output2 -- 2.30.2