From: Andrew Reynolds Date: Tue, 21 Dec 2021 18:21:40 +0000 (-0600) Subject: Support get-abduct-next (#7850) X-Git-Tag: cvc5-1.0.0~623 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=36f93a1431e93979744f2c2a1f3d06b2b9008a4f;p=cvc5.git Support get-abduct-next (#7850) 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. --- diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp index bdaef769e..4c43dbd5b 100644 --- a/src/api/cpp/cvc5.cpp +++ b/src/api/cpp/cvc5.cpp @@ -7618,7 +7618,8 @@ bool Solver::getAbduct(const Term& conj, Term& output) const << "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); @@ -7647,6 +7648,27 @@ bool Solver::getAbduct(const Term& conj, Grammar& grammar, Term& output) const 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; diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h index 3b22f0c6f..7e4dc3cc8 100644 --- a/src/api/cpp/cvc5.h +++ b/src/api/cpp/cvc5.h @@ -4507,6 +4507,30 @@ class CVC5_EXPORT Solver */ 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 `. + * \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. diff --git a/src/api/java/io/github/cvc5/api/Solver.java b/src/api/java/io/github/cvc5/api/Solver.java index 64bef09c9..32ddf0691 100644 --- a/src/api/java/io/github/cvc5/api/Solver.java +++ b/src/api/java/io/github/cvc5/api/Solver.java @@ -2258,6 +2258,26 @@ public class Solver implements IPointer, AutoCloseable 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. diff --git a/src/api/java/jni/solver.cpp b/src/api/java/jni/solver.cpp index 73e481b49..524c52796 100644 --- a/src/api/java/jni/solver.cpp +++ b/src/api/java/jni/solver.cpp @@ -2281,6 +2281,21 @@ Java_io_github_cvc5_api_Solver_getAbduct__JJJJ(JNIEnv* env, 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(pointer); + Term* output = reinterpret_cast(outputPointer); + return (jboolean)solver->getAbductNext(*output); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); +} + /* * Class: io_github_cvc5_api_Solver * Method: blockModel diff --git a/src/expr/symbol_manager.cpp b/src/expr/symbol_manager.cpp index 687f4963f..240e043c6 100644 --- a/src/expr/symbol_manager.cpp +++ b/src/expr/symbol_manager.cpp @@ -41,7 +41,8 @@ class SymbolManager::Implementation 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(); @@ -84,6 +85,10 @@ class SymbolManager::Implementation 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. */ @@ -102,6 +107,8 @@ class SymbolManager::Implementation * Have we pushed a scope (e.g. a let or quantifier) in the current context? */ CDO d_hasPushedScope; + /** The last abduct or interpolant to synthesize name */ + CDO d_lastSynthName; }; NamingResult SymbolManager::Implementation::setExpressionName( @@ -256,6 +263,16 @@ bool SymbolManager::Implementation::hasPushedScope() const 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; @@ -388,6 +405,16 @@ bool SymbolManager::getGlobalDeclarations() const 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(); diff --git a/src/expr/symbol_manager.h b/src/expr/symbol_manager.h index d8b7e23bd..e3084904f 100644 --- a/src/expr/symbol_manager.h +++ b/src/expr/symbol_manager.h @@ -160,6 +160,17 @@ class CVC5_EXPORT SymbolManager 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 ) + * (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. */ diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 7f95368b0..31171b278 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -1007,6 +1007,10 @@ extendedCommand[std::unique_ptr* cmd] { cmd->reset(new GetAbductCommand(name, e, g)); } + | GET_ABDUCT_NEXT_TOK { + PARSER_STATE->checkThatLogicIsSet(); + cmd->reset(new GetAbductNextCommand); + } | GET_INTERPOL_TOK { PARSER_STATE->checkThatLogicIsSet(); } @@ -2238,6 +2242,7 @@ INCLUDE_TOK : 'include'; 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'; diff --git a/src/printer/printer.cpp b/src/printer/printer.cpp index d1c2c58a5..a4ff10014 100644 --- a/src/printer/printer.cpp +++ b/src/printer/printer.cpp @@ -413,6 +413,11 @@ void Printer::toStreamCmdGetAbduct(std::ostream& out, 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 diff --git a/src/printer/printer.h b/src/printer/printer.h index d55723443..74eb8970b 100644 --- a/src/printer/printer.h +++ b/src/printer/printer.h @@ -206,6 +206,9 @@ class Printer 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, diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 2a20bba36..e6c99c707 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -1934,6 +1934,11 @@ void Smt2Printer::toStreamCmdGetAbduct(std::ostream& out, 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 diff --git a/src/printer/smt2/smt2_printer.h b/src/printer/smt2/smt2_printer.h index b97ad2ffb..aad3948fe 100644 --- a/src/printer/smt2/smt2_printer.h +++ b/src/printer/smt2/smt2_printer.h @@ -180,6 +180,9 @@ class Smt2Printer : public cvc5::Printer 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, diff --git a/src/smt/abduction_solver.cpp b/src/smt/abduction_solver.cpp index f17e768c9..3e5912837 100644 --- a/src/smt/abduction_solver.cpp +++ b/src/smt/abduction_solver.cpp @@ -73,19 +73,23 @@ bool AbductionSolver::getAbduct(const std::vector& axioms, 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& 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& axioms, - Node& abd) +bool AbductionSolver::getAbductInternal(Node& abd) { // should have initialized the subsolver by now Assert(d_subsolver != nullptr); @@ -133,7 +137,7 @@ bool AbductionSolver::getAbductInternal(const std::vector& axioms, // if check abducts option is set, we check the correctness if (options().smt.checkAbducts) { - checkAbduct(axioms, abd); + checkAbduct(abd); } return true; } @@ -144,13 +148,13 @@ bool AbductionSolver::getAbductInternal(const std::vector& axioms, return false; } -void AbductionSolver::checkAbduct(const std::vector& axioms, Node a) +void AbductionSolver::checkAbduct(Node a) { Assert(a.getType().isBoolean()); Trace("check-abduct") << "SolverEngine::checkAbduct: get expanded assertions" << std::endl; - std::vector asserts(axioms.begin(), axioms.end()); + std::vector asserts(d_axioms.begin(), d_axioms.end()); asserts.push_back(a); // two checks: first, consistent with assertions, second, implies negated goal diff --git a/src/smt/abduction_solver.h b/src/smt/abduction_solver.h index 326713418..309b6c971 100644 --- a/src/smt/abduction_solver.h +++ b/src/smt/abduction_solver.h @@ -53,6 +53,7 @@ class AbductionSolver : protected EnvObj * @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. @@ -63,23 +64,14 @@ class AbductionSolver : protected EnvObj 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& 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& axioms, Node a); + bool getAbductNext(Node& abd); private: /** @@ -91,7 +83,19 @@ class AbductionSolver : protected EnvObj * This method assumes d_subsolver has been initialized to do abduction * problems. */ - bool getAbductInternal(const std::vector& 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 @@ -119,6 +123,8 @@ class AbductionSolver : protected EnvObj * for. This is used for the get-abduct command. */ Node d_sssf; + /** The list of axioms for the abduction query */ + std::vector d_axioms; }; } // namespace smt diff --git a/src/smt/command.cpp b/src/smt/command.cpp index ac393d568..8161dfb49 100644 --- a/src/smt/command.cpp +++ b/src/smt/command.cpp @@ -2101,6 +2101,9 @@ void GetAbductCommand::invoke(api::Solver* solver, SymbolManager* sm) { 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); @@ -2158,6 +2161,72 @@ void GetAbductCommand::toStream(std::ostream& out, 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 */ /* -------------------------------------------------------------------------- */ diff --git a/src/smt/command.h b/src/smt/command.h index 1a00c2ada..68ff7ffab 100644 --- a/src/smt/command.h +++ b/src/smt/command.h @@ -1108,6 +1108,34 @@ class CVC5_EXPORT GetAbductCommand : public Command 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: diff --git a/src/smt/solver_engine.cpp b/src/smt/solver_engine.cpp index 09814c300..2df3eafa1 100644 --- a/src/smt/solver_engine.cpp +++ b/src/smt/solver_engine.cpp @@ -942,7 +942,7 @@ Result SolverEngine::checkSynth(bool isNext) { 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); @@ -1661,16 +1661,26 @@ bool SolverEngine::getAbduct(const Node& conj, finishInit(); std::vector 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& qs) diff --git a/src/smt/solver_engine.h b/src/smt/solver_engine.h index ecfb521a0..165424594 100644 --- a/src/smt/solver_engine.h +++ b/src/smt/solver_engine.h @@ -658,8 +658,13 @@ class CVC5_EXPORT SolverEngine */ 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 diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 4a54e2fcb..5c4cdcd4a 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1534,23 +1534,25 @@ set(regress_0_tests # 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 diff --git a/test/regress/regress1/abduction/simple-incremental-push-pop.smt2 b/test/regress/regress1/abduction/simple-incremental-push-pop.smt2 new file mode 100644 index 000000000..2c2215838 --- /dev/null +++ b/test/regress/regress1/abduction/simple-incremental-push-pop.smt2 @@ -0,0 +1,15 @@ +; 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)) diff --git a/test/regress/regress1/abduction/simple-incremental.smt2 b/test/regress/regress1/abduction/simple-incremental.smt2 new file mode 100644 index 000000000..50d2385ef --- /dev/null +++ b/test/regress/regress1/abduction/simple-incremental.smt2 @@ -0,0 +1,12 @@ +; 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) diff --git a/test/unit/api/cpp/solver_black.cpp b/test/unit/api/cpp/solver_black.cpp index 960d4bb69..934e0da0d 100644 --- a/test/unit/api/cpp/solver_black.cpp +++ b/test/unit/api/cpp/solver_black.cpp @@ -1395,6 +1395,30 @@ TEST_F(TestApiBlackSolver, getAbduct2) 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"); diff --git a/test/unit/api/java/SolverTest.java b/test/unit/api/java/SolverTest.java index 128141bfa..3fb9ca50e 100644 --- a/test/unit/api/java/SolverTest.java +++ b/test/unit/api/java/SolverTest.java @@ -1335,6 +1335,84 @@ class SolverTest 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");