Adds support for incremental abduction, adds regression for using push/pop in combination with get-abduct, and a use of get-abduct-next.
Adds this method to C++, java API.
Interpolation/abduction not yet supported in Python API, I'm waiting for @yoni206 to add this; getAbductNext will be added to Python API in followup PR.
<< "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, result);
+ TypeNode nullType;
+ bool success = d_slv->getAbduct(*conj.d_node, nullType, result);
if (success)
{
output = Term(this, result);
CVC5_API_TRY_CATCH_END;
}
+bool Solver::getAbductNext(Term& output) const
+{
+ CVC5_API_TRY_CATCH_BEGIN;
+ CVC5_API_CHECK(d_slv->getOptions().smt.produceAbducts)
+ << "Cannot get next abduct unless abducts are enabled (try "
+ "--produce-abducts)";
+ CVC5_API_CHECK(d_slv->getOptions().base.incrementalSolving)
+ << "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;
+ ////////
+ CVC5_API_TRY_CATCH_END;
+}
+
void Solver::blockModel() const
{
CVC5_API_TRY_CATCH_BEGIN;
*/
bool getAbduct(const Term& conj, Grammar& grammar, Term& output) const;
+ /**
+ * Get the next abduct. Can only be called immediately after a successful
+ * call to get-abduct or get-abduct-next. Is guaranteed to produce a
+ * syntactically different abduct wrt the last returned abduct if successful.
+ *
+ * SMT-LIB:
+ *
+ * \verbatim embed:rst:leading-asterisk
+ * .. code:: smtlib
+ *
+ * (get-abduct-next)
+ *
+ * Requires to enable incremental mode, and option
+ * :ref:`produce-abducts <lbl-option-produce-abducts>`.
+ * \endverbatim
+ *
+ * @param output 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
+ */
+ bool getAbductNext(Term& output) const;
+
/**
* Block the current model. Can be called only if immediately preceded by a
* SAT or INVALID query.
private native boolean getAbduct(
long pointer, long conjPointer, long grammarPointer, long outputPointer);
+ /**
+ * Get the next abduct. Can only be called immediately after a successful
+ * call to get-abduct or get-abduct-next. Is guaranteed to produce a
+ * syntactically different abduct wrt the last returned abduct if successful.
+ * SMT-LIB:
+ * {@code
+ * ( 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
+ */
+ public boolean getAbductNext(Term output) {
+ return getAbductNext(pointer, output.getPointer());
+ }
+
+ private native boolean getAbductNext(long pointer, long outputPointer);
+
/**
* Block the current model. Can be called only if immediately preceded by a
* SAT or INVALID query.
CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
}
+/*
+ * Class: io_github_cvc5_api_Solver
+ * Method: getAbductNext
+ * Signature: (JJ)Z
+ */
+JNIEXPORT jboolean JNICALL Java_io_github_cvc5_api_Solver_getAbductNext
+ (JNIEnv * env, jobject, jlong pointer, jlong outputPointer)
+{
+ CVC5_JAVA_API_TRY_CATCH_BEGIN;
+ Solver* solver = reinterpret_cast<Solver*>(pointer);
+ Term* output = reinterpret_cast<Term*>(outputPointer);
+ return (jboolean)solver->getAbductNext(*output);
+ CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
+}
+
/*
* Class: io_github_cvc5_api_Solver
* Method: blockModel
d_declareSorts(&d_context),
d_declareTerms(&d_context),
d_funToSynth(&d_context),
- d_hasPushedScope(&d_context, false)
+ d_hasPushedScope(&d_context, false),
+ d_lastSynthName(&d_context)
{
// use an outermost push, to be able to clear all definitions
d_context.push();
void popScope();
/** Have we pushed a scope (e.g. let or quantifier) in the current context? */
bool hasPushedScope() const;
+ /** Set the last abduct-to-synthesize had the given name. */
+ void setLastSynthName(const std::string& name);
+ /** Get the name of the last abduct-to-synthesize */
+ const std::string& getLastSynthName() const;
private:
/** The context manager for the scope maps. */
* Have we pushed a scope (e.g. a let or quantifier) in the current context?
*/
CDO<bool> d_hasPushedScope;
+ /** The last abduct or interpolant to synthesize name */
+ CDO<std::string> d_lastSynthName;
};
NamingResult SymbolManager::Implementation::setExpressionName(
return d_hasPushedScope.get();
}
+void SymbolManager::Implementation::setLastSynthName(const std::string& name)
+{
+ d_lastSynthName = name;
+}
+
+const std::string& SymbolManager::Implementation::getLastSynthName() const
+{
+ return d_lastSynthName.get();
+}
+
void SymbolManager::Implementation::reset()
{
Trace("sym-manager") << "SymbolManager: reset" << std::endl;
return d_globalDeclarations;
}
+void SymbolManager::setLastSynthName(const std::string& name)
+{
+ d_implementation->setLastSynthName(name);
+}
+
+const std::string& SymbolManager::getLastSynthName() const
+{
+ return d_implementation->getLastSynthName();
+}
+
void SymbolManager::reset()
{
d_symtabAllocated.reset();
void setGlobalDeclarations(bool flag);
/** Get global declarations flag. */
bool getGlobalDeclarations() const;
+ /**
+ * Set the last abduct or interpolant to synthesize had the given name. This
+ * is required since e.g. get-abduct-next must know the name of the
+ * abduct-to-synthesize to print its result. For example, the sequence:
+ * (get-abduct A <conjecture>)
+ * (get-abduct-next)
+ * The latter command must know the symbol "A".
+ */
+ void setLastSynthName(const std::string& name);
+ /** Get the name of the last abduct or interpolant to synthesize */
+ const std::string& getLastSynthName() const;
private:
/** The API Solver object. */
{
cmd->reset(new GetAbductCommand(name, e, g));
}
+ | GET_ABDUCT_NEXT_TOK {
+ PARSER_STATE->checkThatLogicIsSet();
+ cmd->reset(new GetAbductNextCommand);
+ }
| GET_INTERPOL_TOK {
PARSER_STATE->checkThatLogicIsSet();
}
GET_QE_TOK : 'get-qe';
GET_QE_DISJUNCT_TOK : 'get-qe-disjunct';
GET_ABDUCT_TOK : 'get-abduct';
+GET_ABDUCT_NEXT_TOK : 'get-abduct-next';
GET_INTERPOL_TOK : 'get-interpol';
DECLARE_HEAP : 'declare-heap';
DECLARE_POOL : 'declare-pool';
printUnknownCommand(out, "get-abduct");
}
+void Printer::toStreamCmdGetAbductNext(std::ostream& out) const
+{
+ printUnknownCommand(out, "get-abduct-next");
+}
+
void Printer::toStreamCmdGetQuantifierElimination(std::ostream& out,
Node n,
bool doFull) const
Node conj,
TypeNode sygusType) const;
+ /** Print get-abduct-next command */
+ virtual void toStreamCmdGetAbductNext(std::ostream& out) const;
+
/** Print get-quantifier-elimination command */
virtual void toStreamCmdGetQuantifierElimination(std::ostream& out,
Node n,
out << ')' << std::endl;
}
+void Smt2Printer::toStreamCmdGetAbductNext(std::ostream& out) const
+{
+ out << "(get-abduct-next)" << std::endl;
+}
+
void Smt2Printer::toStreamCmdGetQuantifierElimination(std::ostream& out,
Node n,
bool doFull) const
Node conj,
TypeNode sygusType) const override;
+ /** Print get-abduct-next command */
+ void toStreamCmdGetAbductNext(std::ostream& out) const override;
+
/** Print get-quantifier-elimination command */
void toStreamCmdGetQuantifierElimination(std::ostream& out,
Node n,
d_subsolver->setLogic(l);
// assert the abduction query
d_subsolver->assertFormula(aconj);
- return getAbductInternal(axioms, abd);
+ d_axioms = axioms;
+ return getAbductInternal(abd);
}
-bool AbductionSolver::getAbduct(const std::vector<Node>& axioms,
- const Node& goal,
- Node& abd)
+bool AbductionSolver::getAbductNext(Node& abd)
{
- TypeNode grammarType;
- return getAbduct(axioms, goal, grammarType, abd);
+ // Since we are using the subsolver's check-sat interface directly, we
+ // simply call getAbductInternal again here. We assert that the subsolver
+ // is already initialized, which must be the case or else we are not in the
+ // proper SMT mode to make this call. Due to the default behavior of
+ // subsolvers having synthesis conjectures, this is guaranteed to produce
+ // a new solution.
+ Assert(d_subsolver != nullptr);
+ return getAbductInternal(abd);
}
-bool AbductionSolver::getAbductInternal(const std::vector<Node>& axioms,
- Node& abd)
+bool AbductionSolver::getAbductInternal(Node& abd)
{
// should have initialized the subsolver by now
Assert(d_subsolver != nullptr);
// if check abducts option is set, we check the correctness
if (options().smt.checkAbducts)
{
- checkAbduct(axioms, abd);
+ checkAbduct(abd);
}
return true;
}
return false;
}
-void AbductionSolver::checkAbduct(const std::vector<Node>& axioms, Node a)
+void AbductionSolver::checkAbduct(Node a)
{
Assert(a.getType().isBoolean());
Trace("check-abduct") << "SolverEngine::checkAbduct: get expanded assertions"
<< std::endl;
- std::vector<Node> asserts(axioms.begin(), axioms.end());
+ std::vector<Node> asserts(d_axioms.begin(), d_axioms.end());
asserts.push_back(a);
// two checks: first, consistent with assertions, second, implies negated goal
* @param abd This argument is updated to contain the solution C to the
* abduction problem. Notice that this is a formula whose free symbols
* are contained in goal + the parent's current assertion stack.
+ * @return true if the abduct was successfully computed
*
* This method invokes a separate copy of the SMT engine for solving the
* corresponding sygus problem for generating such a solution.
Node& abd);
/**
- * Same as above, but without user-provided grammar restrictions. A default
- * grammar is chosen internally using the sygus grammar constructor utility.
- */
- bool getAbduct(const std::vector<Node>& axioms, const Node& goal, Node& abd);
-
- /**
- * Check that a solution to an abduction conjecture is indeed a solution.
- *
- * The check is made by determining that the assertions conjoined with the
- * solution to the abduction problem (a) is SAT, and the assertions conjoined
- * with the abduct and the goal is UNSAT. If these criteria are not met, an
- * internal error is thrown.
- *
- * @param axioms The expanded assertions of the parent SMT engine
- * @param a The abduct to check.
+ * Get the next abduct, return true if successful and store the result
+ * in abd if so.
+ *
+ * @param abd This argument is updated to contain the solution C to the
+ * abduction problem.
+ * @return true if the abduct was successfully computed
*/
- void checkAbduct(const std::vector<Node>& axioms, Node a);
+ bool getAbductNext(Node& abd);
private:
/**
* This method assumes d_subsolver has been initialized to do abduction
* problems.
*/
- bool getAbductInternal(const std::vector<Node>& axioms, Node& abd);
+ bool getAbductInternal(Node& abd);
+ /**
+ * Check that a solution to an abduction conjecture is indeed a solution.
+ *
+ * The check is made by determining that the assertions conjoined with the
+ * solution to the abduction problem (a) is SAT, and the assertions conjoined
+ * with the abduct and the goal is UNSAT. If these criteria are not met, an
+ * internal error is thrown. We use the expanded assertions of the parent SMT
+ * engine, which are stored in d_axioms.
+ *
+ * @param a The abduct to check.
+ */
+ void checkAbduct(Node a);
/** The SMT engine subsolver
*
* This is a separate copy of the SMT engine which is used for making
* for. This is used for the get-abduct command.
*/
Node d_sssf;
+ /** The list of axioms for the abduction query */
+ std::vector<Node> d_axioms;
};
} // namespace smt
{
try
{
+ // we must remember the name of the abduct, in case get-abduct-next is
+ // called later.
+ sm->setLastSynthName(d_name);
if (d_sygus_grammar == nullptr)
{
d_resultStatus = solver->getAbduct(d_conj, d_result);
out, d_name, termToNode(d_conj), grammarToTypeNode(d_sygus_grammar));
}
+/* -------------------------------------------------------------------------- */
+/* class GetAbductNextCommand */
+/* -------------------------------------------------------------------------- */
+
+GetAbductNextCommand::GetAbductNextCommand() : d_resultStatus(false) {}
+
+api::Term GetAbductNextCommand::getResult() const { return d_result; }
+
+void GetAbductNextCommand::invoke(api::Solver* solver, SymbolManager* sm)
+{
+ try
+ {
+ // Get the name of the abduct from the symbol manager
+ d_name = sm->getLastSynthName();
+ d_resultStatus = solver->getAbductNext(d_result);
+ d_commandStatus = CommandSuccess::instance();
+ }
+ catch (exception& e)
+ {
+ d_commandStatus = new CommandFailure(e.what());
+ }
+}
+
+void GetAbductNextCommand::printResult(std::ostream& out) const
+{
+ if (!ok())
+ {
+ this->Command::printResult(out);
+ }
+ else
+ {
+ options::ioutils::Scope scope(out);
+ options::ioutils::applyDagThresh(out, 0);
+ if (d_resultStatus)
+ {
+ out << "(define-fun " << d_name << " () Bool " << d_result << ")"
+ << std::endl;
+ }
+ else
+ {
+ out << "none" << std::endl;
+ }
+ }
+}
+
+Command* GetAbductNextCommand::clone() const
+{
+ GetAbductNextCommand* c = new GetAbductNextCommand;
+ c->d_result = d_result;
+ c->d_resultStatus = d_resultStatus;
+ return c;
+}
+
+std::string GetAbductNextCommand::getCommandName() const
+{
+ return "get-abduct-next";
+}
+
+void GetAbductNextCommand::toStream(std::ostream& out,
+ int toDepth,
+ size_t dag,
+ Language language) const
+{
+ Printer::getPrinter(language)->toStreamCmdGetAbductNext(out);
+}
+
/* -------------------------------------------------------------------------- */
/* class GetQuantifierEliminationCommand */
/* -------------------------------------------------------------------------- */
api::Term d_result;
}; /* class GetAbductCommand */
+/** The command (get-abduct-next) */
+class CVC5_EXPORT GetAbductNextCommand : public Command
+{
+ public:
+ GetAbductNextCommand();
+ /**
+ * Get the result of the query, which is the solution to the abduction query.
+ */
+ api::Term getResult() const;
+
+ void invoke(api::Solver* solver, SymbolManager* sm) override;
+ void printResult(std::ostream& out) const override;
+ Command* clone() const override;
+ std::string getCommandName() const override;
+ void toStream(std::ostream& out,
+ int toDepth = -1,
+ size_t dag = 1,
+ Language language = Language::LANG_AUTO) const override;
+
+ 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;
+}; /* class GetAbductCommand */
+
class CVC5_EXPORT GetQuantifierEliminationCommand : public Command
{
protected:
{
throw RecoverableModalException(
"Cannot check-synth-next unless immediately preceded by a successful "
- "call to check-synth.");
+ "call to check-synth(-next).");
}
Result r = d_sygusSolver->checkSynth(*d_asserts, isNext);
d_state->notifyCheckSynthResult(r);
finishInit();
std::vector<Node> axioms = getExpandedAssertions();
bool success = d_abductSolver->getAbduct(axioms, conj, grammarType, abd);
- // notify the state of whether the get-abduct call was successfuly, which
+ // notify the state of whether the get-abduct call was successful, which
// impacts the SMT mode.
d_state->notifyGetAbduct(success);
return success;
}
-bool SolverEngine::getAbduct(const Node& conj, Node& abd)
+bool SolverEngine::getAbductNext(Node& abd)
{
- TypeNode grammarType;
- return getAbduct(conj, grammarType, abd);
+ SolverEngineScope smts(this);
+ finishInit();
+ if (d_state->getMode() != SmtMode::ABDUCT)
+ {
+ throw RecoverableModalException(
+ "Cannot get-abduct-next unless immediately preceded by a successful "
+ "call to get-abduct(-next).");
+ }
+ bool success = d_abductSolver->getAbductNext(abd);
+ // notify the state of whether the get-abduct-next call was successful
+ d_state->notifyGetAbduct(success);
+ return success;
}
void SolverEngine::getInstantiatedQuantifiedFormulas(std::vector<Node>& qs)
*/
bool getAbduct(const Node& conj, const TypeNode& grammarType, Node& abd);
- /** Same as above, but without user-provided grammar restrictions */
- bool getAbduct(const Node& conj, Node& abd);
+ /**
+ * 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.
+ */
+ bool getAbductNext(Node& abd);
/**
* Get list of quantified formulas that were instantiated on the last call
# Regression level 1 tests
set(regress_1_tests
+ regress1/abduction/abduction_1255.corecstrs.readable.smt2
+ regress1/abduction/abduction_streq.readable.smt2
+ regress1/abduction/abduction-no-pbe-sym-break.smt2
+ regress1/abduction/abduct-dt.smt2
regress1/abduction/abd-real-const.smt2
- regress1/abduction/sygus-abduct-test-user.smt2
- regress1/abduction/issue5848-4.smt2
+ regress1/abduction/abd-simple-conj-4.smt2
regress1/abduction/issue5848-2.smt2
+ regress1/abduction/issue5848-3-trivial-no-abduct.smt2
+ regress1/abduction/issue5848-4.smt2
regress1/abduction/issue5848.smt2
regress1/abduction/issue6605-1.smt2
- regress1/abduction/abduct-dt.smt2
- regress1/abduction/sygus-abduct-test-ccore.smt2
+ regress1/abduction/simple-incremental.smt2
+ regress1/abduction/simple-incremental-push-pop.smt2
+ regress1/abduction/sygus-abduct-ex1-grammar.smt2
regress1/abduction/sygus-abduct-test.smt2
- regress1/abduction/abd-simple-conj-4.smt2
- regress1/abduction/abduction_streq.readable.smt2
- regress1/abduction/yoni-true-sol.smt2
+ regress1/abduction/sygus-abduct-test-ccore.smt2
+ regress1/abduction/sygus-abduct-test-user.smt2
regress1/abduction/uf-abduct.smt2
- regress1/abduction/abduction_1255.corecstrs.readable.smt2
- regress1/abduction/abduction-no-pbe-sym-break.smt2
- regress1/abduction/issue5848-3-trivial-no-abduct.smt2
- regress1/abduction/sygus-abduct-ex1-grammar.smt2
+ regress1/abduction/yoni-true-sol.smt2
regress1/arith/arith-brab-test.smt2
regress1/arith/arith-int-004.cvc.smt2
regress1/arith/arith-int-011.cvc.smt2
--- /dev/null
+; COMMAND-LINE: --produce-abducts
+; SCRUBBER: grep -v -E '(\(define-fun)'
+; EXIT: 0
+(set-logic QF_LIA)
+(set-option :produce-abducts true)
+(set-option :incremental true)
+(declare-fun x () Int)
+(declare-fun y () Int)
+(push)
+(assert (>= x 0))
+(get-abduct A (>= (+ x y) 2))
+(pop)
+
+(assert (<= x 0))
+(get-abduct A (<= (+ x y) 2))
--- /dev/null
+; COMMAND-LINE: --produce-abducts
+; SCRUBBER: grep -v -E '(\(define-fun)'
+; EXIT: 0
+(set-logic QF_LIA)
+(set-option :produce-abducts true)
+(set-option :incremental true)
+(declare-fun x () Int)
+(declare-fun y () Int)
+(assert (>= x 0))
+(get-abduct A (>= (+ x y) 2))
+(get-abduct-next)
+(get-abduct-next)
ASSERT_THROW(d_solver.getAbduct(conj, output), CVC5ApiException);
}
+TEST_F(TestApiBlackSolver, getAbductNext)
+{
+ d_solver.setLogic("QF_LIA");
+ d_solver.setOption("produce-abducts", "true");
+ d_solver.setOption("incremental", "true");
+
+ Sort intSort = d_solver.getIntegerSort();
+ Term zero = d_solver.mkInteger(0);
+ Term x = d_solver.mkConst(intSort, "x");
+ Term y = d_solver.mkConst(intSort, "y");
+
+ // Assumptions for abduction: x > 0
+ 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));
+ // should produce a different output
+ ASSERT_TRUE(output != output2);
+}
+
TEST_F(TestApiBlackSolver, getInterpolant)
{
d_solver.setLogic("QF_LIA");
assertThrows(CVC5ApiException.class, () -> d_solver.getInfo("asdf"));
}
+ @Test void getAbduct() throws CVC5ApiException
+ {
+ d_solver.setLogic("QF_LIA");
+ d_solver.setOption("produce-abducts", "true");
+ d_solver.setOption("incremental", "false");
+
+ Sort intSort = d_solver.getIntegerSort();
+ Term zero = d_solver.mkInteger(0);
+ Term x = d_solver.mkConst(intSort, "x");
+ Term y = d_solver.mkConst(intSort, "y");
+
+ // Assumptions for abduction: x > 0
+ 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));
+ // We expect the resulting output to be a boolean formula
+ assertTrue(!output.isNull() && output.getSort().isBoolean());
+
+ // try with a grammar, a simple grammar admitting true
+ Sort bsort = d_solver.getBooleanSort();
+ 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});
+ 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));
+ // abduct must be true
+ assertEquals(output2, truen);
+ }
+
+ @Test void getAbduct2() throws CVC5ApiException
+ {
+ d_solver.setLogic("QF_LIA");
+ d_solver.setOption("incremental", "false");
+ Sort intSort = d_solver.getIntegerSort();
+ Term zero = d_solver.mkInteger(0);
+ Term x = d_solver.mkConst(intSort, "x");
+ Term y = d_solver.mkConst(intSort, "y");
+ // Assumptions for abduction: x > 0
+ 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();
+ // Fails due to option not set
+ assertThrows(
+ CVC5ApiException.class, () -> d_solver.getAbduct(conj, output));
+ }
+
+ @Test void getAbductNext() throws CVC5ApiException
+ {
+ d_solver.setLogic("QF_LIA");
+ d_solver.setOption("produce-abducts", "true");
+ d_solver.setOption("incremental", "true");
+
+ Sort intSort = d_solver.getIntegerSort();
+ Term zero = d_solver.mkInteger(0);
+ Term x = d_solver.mkConst(intSort, "x");
+ Term y = d_solver.mkConst(intSort, "y");
+
+ // Assumptions for abduction: x > 0
+ 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));
+ // should produce a different output
+ assertNotEquals(output, output2);
+ }
+
+
@Test void getInterpolant() throws CVC5ApiException
{
d_solver.setLogic("QF_LIA");
projects / cvc5.git / commitdiff