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);
<< "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);
<< "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
<< "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)
<< "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;
}
* \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
*
* @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
* 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.
* \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.
*
* @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
* :ref:`produce-abducts <lbl-option-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
* }
* 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
* 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
* 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.
* }
* 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:
* 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
* ( 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
/*
* 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<Solver*>(pointer);
Term* conj = reinterpret_cast<Term*>(conjPointer);
- Term* output = reinterpret_cast<Term*>(outputPointer);
- return (jboolean)solver->getInterpolant(*conj, *output);
+ Term* result = new Term(solver->getInterpolant(*conj));
+ return reinterpret_cast<jlong>(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<Solver*>(pointer);
Term* conj = reinterpret_cast<Term*>(conjPointer);
Grammar* grammar = reinterpret_cast<Grammar*>(grammarPointer);
- Term* output = reinterpret_cast<Term*>(outputPointer);
- return (jboolean)solver->getInterpolant(*conj, *grammar, *output);
+ Term* result = new Term(solver->getInterpolant(*conj, *grammar));
+ return reinterpret_cast<jlong>(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<Solver*>(pointer);
- Term* output = reinterpret_cast<Term*>(outputPointer);
- return (jboolean)solver->getInterpolantNext(*output);
+ Term* result = new Term(solver->getInterpolantNext());
+ return reinterpret_cast<jlong>(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<Solver*>(pointer);
Term* conj = reinterpret_cast<Term*>(conjPointer);
- Term* output = reinterpret_cast<Term*>(outputPointer);
- return (jboolean)solver->getAbduct(*conj, *output);
+ Term* result = new Term(solver->getAbduct(*conj));
+ return reinterpret_cast<jlong>(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<Solver*>(pointer);
Term* conj = reinterpret_cast<Term*>(conjPointer);
Grammar* grammar = reinterpret_cast<Grammar*>(grammarPointer);
- Term* output = reinterpret_cast<Term*>(outputPointer);
- return (jboolean)solver->getAbduct(*conj, *grammar, *output);
+ Term* result = new Term(solver->getAbduct(*conj, *grammar));
+ return reinterpret_cast<jlong>(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<Solver*>(pointer);
- Term* output = reinterpret_cast<Term*>(outputPointer);
- return (jboolean)solver->getAbductNext(*output);
+ Term* result = new Term(solver->getAbductNext());
+ return reinterpret_cast<jlong>(result);
CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
}
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 +
"""
self.csolver.setOption(option.encode(), value.encode())
+
def getInterpolant(self, Term conj, *args):
"""Get an interpolant.
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, (<Term ?> 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, (<Grammar ?> args[0]).cgrammar, (<Term ?> args[1]).cterm)
+ result.cterm = self.csolver.getInterpolant(conj.cterm, (<Grammar ?> 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.
: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):
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, (<Term ?> 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, (<Grammar ?> args[0]).cgrammar, (<Term ?> args[1]).cterm)
+ result.cterm = self.csolver.getAbduct(conj.cterm, (<Grammar ?> 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.
: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):
/* -------------------------------------------------------------------------- */
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)
{
}
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();
}
{
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;
GetInterpolCommand* c =
new GetInterpolCommand(d_name, d_conj, d_sygus_grammar);
c->d_result = d_result;
- c->d_resultStatus = d_resultStatus;
return c;
}
/* class GetInterpolNextCommand */
/* -------------------------------------------------------------------------- */
-GetInterpolNextCommand::GetInterpolNextCommand() : d_resultStatus(false) {}
+GetInterpolNextCommand::GetInterpolNextCommand() {}
api::Term GetInterpolNextCommand::getResult() const { return d_result; }
{
// 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)
{
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;
{
GetInterpolNextCommand* c = new GetInterpolNextCommand;
c->d_result = d_result;
- c->d_resultStatus = d_resultStatus;
return c;
}
/* -------------------------------------------------------------------------- */
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)
{
}
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();
}
{
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;
{
GetAbductCommand* c = new GetAbductCommand(d_name, d_conj, d_sygus_grammar);
c->d_result = d_result;
- c->d_resultStatus = d_resultStatus;
return c;
}
/* class GetAbductNextCommand */
/* -------------------------------------------------------------------------- */
-GetAbductNextCommand::GetAbductNextCommand() : d_resultStatus(false) {}
+GetAbductNextCommand::GetAbductNextCommand() {}
api::Term GetAbductNextCommand::getResult() const { return d_result; }
{
// 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)
{
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;
{
GetAbductNextCommand* c = new GetAbductNextCommand;
c->d_result = d_result;
- c->d_resultStatus = d_resultStatus;
return c;
}
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 */
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;
};
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 */
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;
};
*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<Node> 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();
"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<Node> 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();
"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<Node>& qs)
* 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
* 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
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());
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);
}
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)
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);
}
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());
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);
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)
Term t488 = slv.mkTerm(Kind::APPLY_UF, {t31, t274});
slv.assertFormula({t488});
Term abduct;
- slv.getAbduct(t488, abduct);
+ abduct = slv.getAbduct(t488);
}
} // namespace test
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());
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);
}
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
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);
}
// 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());
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);
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()
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):
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")
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
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):
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
projects / cvc5.git / commitdiff