diff options
| -rw-r--r-- | src/CMakeLists.txt | 2 | ||||
| -rw-r--r-- | src/smt/abduction_solver.cpp | 202 | ||||
| -rw-r--r-- | src/smt/abduction_solver.h | 120 | ||||
| -rw-r--r-- | src/smt/command.cpp | 18 | ||||
| -rw-r--r-- | src/smt/smt_engine.cpp | 198 | ||||
| -rw-r--r-- | src/smt/smt_engine.h | 100 | ||||
| -rw-r--r-- | src/theory/datatypes/sygus_datatype_utils.cpp | 3 |
7 files changed, 391 insertions, 252 deletions
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 199c14330..28d943ced 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -219,6 +219,8 @@ libcvc4_add_sources( prop/sat_solver_types.h prop/theory_proxy.cpp prop/theory_proxy.h + smt/abduction_solver.cpp + smt/abduction_solver.h smt/command.cpp smt/command.h smt/command_list.cpp diff --git a/src/smt/abduction_solver.cpp b/src/smt/abduction_solver.cpp new file mode 100644 index 000000000..adb80b719 --- /dev/null +++ b/src/smt/abduction_solver.cpp @@ -0,0 +1,202 @@ +/********************* */ +/*! \file abduction_solver.cpp + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief The solver for abduction queries + **/ + +#include "smt/abduction_solver.h" + +#include "options/smt_options.h" +#include "smt/smt_engine.h" +#include "theory/quantifiers/quantifiers_attributes.h" +#include "theory/quantifiers/sygus/sygus_abduct.h" +#include "theory/quantifiers/sygus/sygus_grammar_cons.h" +#include "theory/smt_engine_subsolver.h" + +using namespace CVC4::theory; + +namespace CVC4 { +namespace smt { + +AbductionSolver::AbductionSolver(SmtEngine* parent) : d_parent(parent) {} + +AbductionSolver::~AbductionSolver() {} +bool AbductionSolver::getAbduct(const Node& goal, + const TypeNode& grammarType, + Node& abd) +{ + if (!options::produceAbducts()) + { + const char* msg = "Cannot get abduct when produce-abducts options is off."; + throw ModalException(msg); + } + Trace("sygus-abduct") << "SmtEngine::getAbduct: goal " << goal << std::endl; + std::vector<Expr> easserts = d_parent->getExpandedAssertions(); + std::vector<Node> axioms; + for (unsigned i = 0, size = easserts.size(); i < size; i++) + { + axioms.push_back(Node::fromExpr(easserts[i])); + } + std::vector<Node> asserts(axioms.begin(), axioms.end()); + // must expand definitions + Node conjn = d_parent->expandDefinitions(goal); + // now negate + conjn = conjn.negate(); + d_abdConj = conjn; + asserts.push_back(conjn); + std::string name("A"); + Node aconj = quantifiers::SygusAbduct::mkAbductionConjecture( + name, asserts, axioms, grammarType); + // should be a quantified conjecture with one function-to-synthesize + Assert(aconj.getKind() == kind::FORALL && aconj[0].getNumChildren() == 1); + // remember the abduct-to-synthesize + d_sssf = aconj[0][0]; + Trace("sygus-abduct") << "SmtEngine::getAbduct: made conjecture : " << aconj + << ", solving for " << d_sssf << std::endl; + // we generate a new smt engine to do the abduction query + initializeSubsolver(d_subsolver); + // get the logic + LogicInfo l = d_subsolver->getLogicInfo().getUnlockedCopy(); + // enable everything needed for sygus + l.enableSygus(); + d_subsolver->setLogic(l); + // assert the abduction query + d_subsolver->assertFormula(aconj.toExpr()); + return getAbductInternal(abd); +} + +bool AbductionSolver::getAbduct(const Node& goal, Node& abd) +{ + TypeNode grammarType; + return getAbduct(goal, grammarType, abd); +} + +bool AbductionSolver::getAbductInternal(Node& abd) +{ + // should have initialized the subsolver by now + Assert(d_subsolver != nullptr); + Trace("sygus-abduct") << " SmtEngine::getAbduct check sat..." << std::endl; + Result r = d_subsolver->checkSat(); + Trace("sygus-abduct") << " SmtEngine::getAbduct result: " << r << std::endl; + if (r.asSatisfiabilityResult().isSat() == Result::UNSAT) + { + // get the synthesis solution + std::map<Expr, Expr> sols; + d_subsolver->getSynthSolutions(sols); + Assert(sols.size() == 1); + Expr essf = d_sssf.toExpr(); + std::map<Expr, Expr>::iterator its = sols.find(essf); + if (its != sols.end()) + { + Trace("sygus-abduct") + << "SmtEngine::getAbduct: solution is " << its->second << std::endl; + abd = Node::fromExpr(its->second); + if (abd.getKind() == kind::LAMBDA) + { + abd = abd[1]; + } + // get the grammar type for the abduct + Node agdtbv = d_sssf.getAttribute(SygusSynthFunVarListAttribute()); + Assert(!agdtbv.isNull()); + Assert(agdtbv.getKind() == kind::BOUND_VAR_LIST); + // convert back to original + // must replace formal arguments of abd with the free variables in the + // input problem that they correspond to. + std::vector<Node> vars; + std::vector<Node> syms; + SygusVarToTermAttribute sta; + for (const Node& bv : agdtbv) + { + vars.push_back(bv); + syms.push_back(bv.hasAttribute(sta) ? bv.getAttribute(sta) : bv); + } + abd = abd.substitute(vars.begin(), vars.end(), syms.begin(), syms.end()); + + // if check abducts option is set, we check the correctness + if (options::checkAbducts()) + { + checkAbduct(abd); + } + return true; + } + Trace("sygus-abduct") << "SmtEngine::getAbduct: could not find solution!" + << std::endl; + throw RecoverableModalException("Could not find solution for get-abduct."); + } + return false; +} + +void AbductionSolver::checkAbduct(Node a) +{ + Assert(a.getType().isBoolean()); + Trace("check-abduct") << "SmtEngine::checkAbduct: get expanded assertions" + << std::endl; + + std::vector<Expr> asserts = d_parent->getExpandedAssertions(); + asserts.push_back(a.toExpr()); + + // two checks: first, consistent with assertions, second, implies negated goal + // is unsatisfiable. + for (unsigned j = 0; j < 2; j++) + { + Trace("check-abduct") << "SmtEngine::checkAbduct: phase " << j + << ": make new SMT engine" << std::endl; + // Start new SMT engine to check solution + std::unique_ptr<SmtEngine> abdChecker; + initializeSubsolver(abdChecker); + Trace("check-abduct") << "SmtEngine::checkAbduct: phase " << j + << ": asserting formulas" << std::endl; + for (const Expr& e : asserts) + { + abdChecker->assertFormula(e); + } + Trace("check-abduct") << "SmtEngine::checkAbduct: phase " << j + << ": check the assertions" << std::endl; + Result r = abdChecker->checkSat(); + Trace("check-abduct") << "SmtEngine::checkAbduct: phase " << j + << ": result is " << r << std::endl; + std::stringstream serr; + bool isError = false; + if (j == 0) + { + if (r.asSatisfiabilityResult().isSat() != Result::SAT) + { + isError = true; + serr << "SmtEngine::checkAbduct(): produced solution cannot be shown " + "to be consisconsistenttent with assertions, result was " + << r; + } + Trace("check-abduct") + << "SmtEngine::checkAbduct: goal is " << d_abdConj << std::endl; + // add the goal to the set of assertions + Assert(!d_abdConj.isNull()); + asserts.push_back(d_abdConj.toExpr()); + } + else + { + if (r.asSatisfiabilityResult().isSat() != Result::UNSAT) + { + isError = true; + serr << "SmtEngine::checkAbduct(): negated goal cannot be shown " + "unsatisfiable with produced solution, result was " + << r; + } + } + // did we get an unexpected result? + if (isError) + { + InternalError() << serr.str(); + } + } +} + +} // namespace smt +} // namespace CVC4 diff --git a/src/smt/abduction_solver.h b/src/smt/abduction_solver.h new file mode 100644 index 000000000..2041b961d --- /dev/null +++ b/src/smt/abduction_solver.h @@ -0,0 +1,120 @@ +/********************* */ +/*! \file abduction_solver.h + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief The solver for abduction queries + **/ + +#include "cvc4_private.h" + +#ifndef CVC4__SMT__ABDUCTION_SOLVER_H +#define CVC4__SMT__ABDUCTION_SOLVER_H + +#include "expr/node.h" +#include "expr/type_node.h" + +namespace CVC4 { + +class SmtEngine; + +namespace smt { + +/** + * A solver for abduction queries. + * + * This class is responsible for responding to get-abduct commands. It spawns + * a subsolver SmtEngine for a sygus conjecture that captures the abduction + * query, and implements supporting utility methods such as checkAbduct. + */ +class AbductionSolver +{ + public: + AbductionSolver(SmtEngine* parent); + ~AbductionSolver(); + /** + * This method asks this SMT engine to find an abduct with respect to the + * current assertion stack (call it A) and the goal (call it B). + * If this method returns true, then abd is set to a formula C such that + * A ^ C is satisfiable, and A ^ ~B ^ C is unsatisfiable. + * + * @param goal The goal of the abduction problem. + * @param grammarType A sygus datatype type that encodes the syntax + * restrictions on the shape of possible solutions. + * @param abd This argument is updated to contain the solution to the + * abduction problem. Notice that this is a formula whose free symbols + * are contained in goal + the parent's current assertion stack. + * + * 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& goal, const TypeNode& grammarType, 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 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. + */ + void checkAbduct(Node a); + + private: + /** + * Get abduct internal. + * + * Get the next abduct from the internal subsolver d_subsolver. If + * successful, this method returns true and sets abd to that abduct. + * + * This method assumes d_subsolver has been initialized to do abduction + * problems. + */ + bool getAbductInternal(Node& abd); + /** The parent SMT engine */ + SmtEngine* d_parent; + /** The SMT engine subsolver + * + * This is a separate copy of the SMT engine which is used for making + * calls that cannot be answered by this copy of the SMT engine. An example + * of invoking this subsolver is the get-abduct command, where we wish to + * solve a sygus conjecture based on the current assertions. In particular, + * consider the input: + * (assert A) + * (get-abduct B) + * In the copy of the SMT engine where these commands are issued, we maintain + * A in the assertion stack. To solve the abduction problem, instead of + * modifying the assertion stack to remove A and add the sygus conjecture + * (exists I. ...), we invoke a fresh copy of the SMT engine and leave the + * assertion stack unchaged. This copy of the SMT engine can be further + * queried for information regarding further solutions. + */ + std::unique_ptr<SmtEngine> d_subsolver; + /** + * The conjecture of the current abduction problem. This expression is only + * valid while the parent SmtEngine is in mode SMT_MODE_ABDUCT. + */ + Node d_abdConj; + /** + * If applicable, the function-to-synthesize that the subsolver is solving + * for. This is used for the get-abduct command. + */ + Node d_sssf; +}; + +} // namespace smt +} // namespace CVC4 + +#endif /* CVC4__SMT__ABDUCTION_SOLVER_H */ diff --git a/src/smt/command.cpp b/src/smt/command.cpp index e60f223b4..2e36190b4 100644 --- a/src/smt/command.cpp +++ b/src/smt/command.cpp @@ -1555,7 +1555,8 @@ ExpandDefinitionsCommand::ExpandDefinitionsCommand(Expr term) : d_term(term) {} Expr ExpandDefinitionsCommand::getTerm() const { return d_term; } void ExpandDefinitionsCommand::invoke(SmtEngine* smtEngine) { - d_result = smtEngine->expandDefinitions(d_term); + Node t = Node::fromExpr(d_term); + d_result = smtEngine->expandDefinitions(t).toExpr(); d_commandStatus = CommandSuccess::instance(); } @@ -1623,9 +1624,11 @@ void GetValueCommand::invoke(SmtEngine* smtEngine) for (int i = 0, size = d_terms.size(); i < size; i++) { Expr e = d_terms[i]; + Node eNode = Node::fromExpr(e); Assert(nm == NodeManager::fromExprManager(e.getExprManager())); - Node request = Node::fromExpr( - options::expandDefinitions() ? smtEngine->expandDefinitions(e) : e); + Node request = options::expandDefinitions() + ? smtEngine->expandDefinitions(eNode) + : eNode; Node value = Node::fromExpr(result[i]); if (value.getType().isInteger() && request.getType() == nm->realType()) { @@ -2199,15 +2202,18 @@ void GetAbductCommand::invoke(SmtEngine* smtEngine) { try { + Node conjNode = Node::fromExpr(d_conj); + Node resn; if (d_sygus_grammar_type.isNull()) { - d_resultStatus = smtEngine->getAbduct(d_conj, d_result); + d_resultStatus = smtEngine->getAbduct(conjNode, resn); } else { - d_resultStatus = - smtEngine->getAbduct(d_conj, d_sygus_grammar_type, d_result); + TypeNode gtype = TypeNode::fromType(d_sygus_grammar_type); + d_resultStatus = smtEngine->getAbduct(conjNode, gtype, resn); } + d_result = resn.toExpr(); d_commandStatus = CommandSuccess::instance(); } catch (exception& e) diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 12e0f443e..380878e41 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -81,6 +81,7 @@ #include "proof/theory_proof.h" #include "proof/unsat_core.h" #include "prop/prop_engine.h" +#include "smt/abduction_solver.h" #include "smt/command.h" #include "smt/command_list.h" #include "smt/defined_function.h" @@ -101,7 +102,6 @@ #include "theory/logic_info.h" #include "theory/quantifiers/fun_def_process.h" #include "theory/quantifiers/single_inv_partition.h" -#include "theory/quantifiers/sygus/sygus_abduct.h" #include "theory/quantifiers/sygus/synth_engine.h" #include "theory/quantifiers/term_util.h" #include "theory/quantifiers_engine.h" @@ -642,6 +642,7 @@ SmtEngine::SmtEngine(ExprManager* em, Options* optr) d_proofManager(nullptr), d_rewriter(new theory::Rewriter()), d_definedFunctions(nullptr), + d_abductSolver(nullptr), d_assertionList(nullptr), d_assignments(nullptr), d_modelGlobalCommands(), @@ -817,6 +818,12 @@ void SmtEngine::finishInit() } d_dumpCommands.clear(); + // subsolvers + if (options::produceAbducts()) + { + d_abductSolver.reset(new AbductionSolver(this)); + } + PROOF( ProofManager::currentPM()->setLogic(d_logic); ); PROOF({ for(TheoryId id = theory::THEORY_FIRST; id < theory::THEORY_LAST; ++id) { @@ -2161,18 +2168,17 @@ Expr SmtEngine::simplify(const Expr& ex) return n.toExpr(); } -Expr SmtEngine::expandDefinitions(const Expr& ex) +Node SmtEngine::expandDefinitions(const Node& ex) { d_private->spendResource(ResourceManager::Resource::PreprocessStep); - Assert(ex.getExprManager() == d_exprManager); SmtScope smts(this); finalOptionsAreSet(); doPendingPops(); Trace("smt") << "SMT expandDefinitions(" << ex << ")" << endl; // Substitute out any abstract values in ex. - Expr e = d_private->substituteAbstractValues(Node::fromExpr(ex)).toExpr(); + Node e = d_private->substituteAbstractValues(ex); if(options::typeChecking()) { // Ensure expr is type-checked at this point. e.getType(true); @@ -2180,10 +2186,10 @@ Expr SmtEngine::expandDefinitions(const Expr& ex) unordered_map<Node, Node, NodeHashFunction> cache; Node n = d_private->getProcessAssertions()->expandDefinitions( - Node::fromExpr(e), cache, /* expandOnly = */ true); - n = postprocess(n, TypeNode::fromType(e.getType())); + e, cache, /* expandOnly = */ true); + n = postprocess(n, e.getType()); - return n.toExpr(); + return n; } // TODO(#1108): Simplify the error reporting of this method. @@ -2985,69 +2991,11 @@ void SmtEngine::checkInterpol(Expr interpol, { } -void SmtEngine::checkAbduct(Expr a) +void SmtEngine::checkAbduct(Node a) { Assert(a.getType().isBoolean()); - Trace("check-abduct") << "SmtEngine::checkAbduct: get expanded assertions" - << std::endl; - - std::vector<Expr> asserts = getExpandedAssertions(); - asserts.push_back(a); - - // two checks: first, consistent with assertions, second, implies negated goal - // is unsatisfiable. - for (unsigned j = 0; j < 2; j++) - { - Trace("check-abduct") << "SmtEngine::checkAbduct: phase " << j - << ": make new SMT engine" << std::endl; - // Start new SMT engine to check solution - SmtEngine abdChecker(d_exprManager, &d_options); - abdChecker.setIsInternalSubsolver(); - abdChecker.setLogic(getLogicInfo()); - Trace("check-abduct") << "SmtEngine::checkAbduct: phase " << j - << ": asserting formulas" << std::endl; - for (const Expr& e : asserts) - { - abdChecker.assertFormula(e); - } - Trace("check-abduct") << "SmtEngine::checkAbduct: phase " << j - << ": check the assertions" << std::endl; - Result r = abdChecker.checkSat(); - Trace("check-abduct") << "SmtEngine::checkAbduct: phase " << j - << ": result is " << r << endl; - std::stringstream serr; - bool isError = false; - if (j == 0) - { - if (r.asSatisfiabilityResult().isSat() != Result::SAT) - { - isError = true; - serr << "SmtEngine::checkAbduct(): produced solution cannot be shown " - "to be consisconsistenttent with assertions, result was " - << r; - } - Trace("check-abduct") - << "SmtEngine::checkAbduct: goal is " << d_abdConj << std::endl; - // add the goal to the set of assertions - Assert(!d_abdConj.isNull()); - asserts.push_back(d_abdConj); - } - else - { - if (r.asSatisfiabilityResult().isSat() != Result::UNSAT) - { - isError = true; - serr << "SmtEngine::checkAbduct(): negated goal cannot be shown " - "unsatisfiable with produced solution, result was " - << r; - } - } - // did we get an unexpected result? - if (isError) - { - InternalError() << serr.str(); - } - } + // check it with the abduction solver + return d_abductSolver->checkAbduct(a); } // TODO(#1108): Simplify the error reporting of this method. @@ -3217,54 +3165,11 @@ bool SmtEngine::getInterpol(const Expr& conj, Expr& interpol) return getInterpol(conj, grammarType, interpol); } -bool SmtEngine::getAbduct(const Expr& conj, const Type& grammarType, Expr& abd) +bool SmtEngine::getAbduct(const Node& conj, + const TypeNode& grammarType, + Node& abd) { - SmtScope smts(this); - - if (!options::produceAbducts()) - { - const char* msg = "Cannot get abduct when produce-abducts options is off."; - throw ModalException(msg); - } - Trace("sygus-abduct") << "SmtEngine::getAbduct: conjecture " << conj - << std::endl; - std::vector<Expr> easserts = getExpandedAssertions(); - std::vector<Node> axioms; - for (unsigned i = 0, size = easserts.size(); i < size; i++) - { - axioms.push_back(Node::fromExpr(easserts[i])); - } - std::vector<Node> asserts(axioms.begin(), axioms.end()); - // negate the conjecture - Node conjn = Node::fromExpr(conj); - // must expand definitions - std::unordered_map<Node, Node, NodeHashFunction> cache; - conjn = d_private->getProcessAssertions()->expandDefinitions(conjn, cache); - // now negate - conjn = conjn.negate(); - d_abdConj = conjn.toExpr(); - asserts.push_back(conjn); - std::string name("A"); - Node aconj = theory::quantifiers::SygusAbduct::mkAbductionConjecture( - name, asserts, axioms, TypeNode::fromType(grammarType)); - // should be a quantified conjecture with one function-to-synthesize - Assert(aconj.getKind() == kind::FORALL && aconj[0].getNumChildren() == 1); - // remember the abduct-to-synthesize - d_sssf = aconj[0][0].toExpr(); - Trace("sygus-abduct") << "SmtEngine::getAbduct: made conjecture : " << aconj - << ", solving for " << d_sssf << std::endl; - // we generate a new smt engine to do the abduction query - d_subsolver.reset( - new SmtEngine(NodeManager::currentNM()->toExprManager(), &d_options)); - d_subsolver->setIsInternalSubsolver(); - // get the logic - LogicInfo l = d_logic.getUnlockedCopy(); - // enable everything needed for sygus - l.enableSygus(); - d_subsolver->setLogic(l); - // assert the abduction query - d_subsolver->assertFormula(aconj.toExpr()); - if (getAbductInternal(abd)) + if (d_abductSolver->getAbduct(conj, grammarType, abd)) { // successfully generated an abduct, update to abduct state d_smtMode = SMT_MODE_ABDUCT; @@ -3275,68 +3180,9 @@ bool SmtEngine::getAbduct(const Expr& conj, const Type& grammarType, Expr& abd) return false; } -bool SmtEngine::getAbductInternal(Expr& abd) +bool SmtEngine::getAbduct(const Node& conj, Node& abd) { - // should have initialized the subsolver by now - Assert(d_subsolver != nullptr); - Trace("sygus-abduct") << " SmtEngine::getAbduct check sat..." << std::endl; - Result r = d_subsolver->checkSat(); - Trace("sygus-abduct") << " SmtEngine::getAbduct result: " << r << std::endl; - if (r.asSatisfiabilityResult().isSat() == Result::UNSAT) - { - // get the synthesis solution - std::map<Expr, Expr> sols; - d_subsolver->getSynthSolutions(sols); - Assert(sols.size() == 1); - std::map<Expr, Expr>::iterator its = sols.find(d_sssf); - if (its != sols.end()) - { - Trace("sygus-abduct") - << "SmtEngine::getAbduct: solution is " << its->second << std::endl; - Node abdn = Node::fromExpr(its->second); - if (abdn.getKind() == kind::LAMBDA) - { - abdn = abdn[1]; - } - // get the grammar type for the abduct - Node af = Node::fromExpr(d_sssf); - Node agdtbv = af.getAttribute(theory::SygusSynthFunVarListAttribute()); - Assert(!agdtbv.isNull()); - Assert(agdtbv.getKind() == kind::BOUND_VAR_LIST); - // convert back to original - // must replace formal arguments of abd with the free variables in the - // input problem that they correspond to. - std::vector<Node> vars; - std::vector<Node> syms; - SygusVarToTermAttribute sta; - for (const Node& bv : agdtbv) - { - vars.push_back(bv); - syms.push_back(bv.hasAttribute(sta) ? bv.getAttribute(sta) : bv); - } - abdn = - abdn.substitute(vars.begin(), vars.end(), syms.begin(), syms.end()); - - // convert to expression - abd = abdn.toExpr(); - - // if check abducts option is set, we check the correctness - if (options::checkAbducts()) - { - checkAbduct(abd); - } - return true; - } - Trace("sygus-abduct") << "SmtEngine::getAbduct: could not find solution!" - << std::endl; - throw RecoverableModalException("Could not find solution for get-abduct."); - } - return false; -} - -bool SmtEngine::getAbduct(const Expr& conj, Expr& abd) -{ - Type grammarType; + TypeNode grammarType; return getAbduct(conj, grammarType, abd); } diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index 8db8eadd5..f6b1d08bf 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -91,23 +91,25 @@ namespace prop { /* -------------------------------------------------------------------------- */ namespace smt { - /** - * Representation of a defined function. We keep these around in - * SmtEngine to permit expanding definitions late (and lazily), to - * support getValue() over defined functions, to support user output - * in terms of defined functions, etc. - */ - class DefinedFunction; - - struct SmtEngineStatistics; - class SmtEnginePrivate; - class SmtScope; - class ProcessAssertions; - - ProofManager* currentProofManager(); - - struct CommandCleanup; - typedef context::CDList<Command*, CommandCleanup> CommandList; +/** Subsolvers */ +class AbductionSolver; +/** + * Representation of a defined function. We keep these around in + * SmtEngine to permit expanding definitions late (and lazily), to + * support getValue() over defined functions, to support user output + * in terms of defined functions, etc. + */ +class DefinedFunction; + +struct SmtEngineStatistics; +class SmtEnginePrivate; +class SmtScope; +class ProcessAssertions; + +ProofManager* currentProofManager(); + +struct CommandCleanup; +typedef context::CDList<Command*, CommandCleanup> CommandList; }/* CVC4::smt namespace */ /* -------------------------------------------------------------------------- */ @@ -508,7 +510,7 @@ class CVC4_PUBLIC SmtEngine * * @throw TypeCheckingException, LogicException, UnsafeInterruptException */ - Expr expandDefinitions(const Expr& e); + Node expandDefinitions(const Node& e); /** * Get the assigned value of an expr (only if immediately preceded by a SAT @@ -660,10 +662,10 @@ class CVC4_PUBLIC SmtEngine * This method invokes a separate copy of the SMT engine for solving the * corresponding sygus problem for generating such a solution. */ - bool getAbduct(const Expr& conj, const Type& grammarType, Expr& abd); + bool getAbduct(const Node& conj, const TypeNode& grammarType, Node& abd); /** Same as above, but without user-provided grammar restrictions */ - bool getAbduct(const Expr& conj, Expr& abd); + bool getAbduct(const Node& conj, Node& abd); /** * Get list of quantified formulas that were instantiated on the last call @@ -898,6 +900,13 @@ class CVC4_PUBLIC SmtEngine /** Get the resource manager of this SMT engine */ ResourceManager* getResourceManager(); + + /** + * Get expanded assertions. + * + * Return the set of assertions, after expanding definitions. + */ + std::vector<Expr> getExpandedAssertions(); /* ....................................................................... */ private: /* ....................................................................... */ @@ -994,7 +1003,7 @@ class CVC4_PUBLIC SmtEngine * with the abduct and the goal is UNSAT. If these criteria are not met, an * internal error is thrown. */ - void checkAbduct(Expr a); + void checkAbduct(Node a); /** * Postprocess a value for output to the user. Involves doing things @@ -1111,30 +1120,12 @@ class CVC4_PUBLIC SmtEngine Expr func); /** - * Get abduct internal. - * - * Get the next abduct from the internal subsolver d_subsolver. If - * successful, this method returns true and sets abd to that abduct. - * - * This method assumes d_subsolver has been initialized to do abduction - * problems. - */ - bool getAbductInternal(Expr& abd); - - /** * Helper method to obtain both the heap and nil from the solver. Returns a * std::pair where the first element is the heap expression and the second * element is the nil expression. */ std::pair<Expr, Expr> getSepHeapAndNilExpr(); - /** - * Get expanded assertions. - * - * Return the set of assertions, after expanding definitions. - */ - std::vector<Expr> getExpandedAssertions(); - /* Members -------------------------------------------------------------- */ /** Solver instance that owns this SmtEngine instance. */ @@ -1171,35 +1162,8 @@ class CVC4_PUBLIC SmtEngine /** An index of our defined functions */ DefinedFunctionMap* d_definedFunctions; - /** The SMT engine subsolver - * - * This is a separate copy of the SMT engine which is used for making - * calls that cannot be answered by this copy of the SMT engine. An example - * of invoking this subsolver is the get-abduct command, where we wish to - * solve a sygus conjecture based on the current assertions. In particular, - * consider the input: - * (assert A) - * (get-abduct B) - * In the copy of the SMT engine where these commands are issued, we maintain - * A in the assertion stack. To solve the abduction problem, instead of - * modifying the assertion stack to remove A and add the sygus conjecture - * (exists I. ...), we invoke a fresh copy of the SMT engine and leave the - * assertion stack unchaged. This copy of the SMT engine can be further - * queried for information regarding further solutions. - */ - std::unique_ptr<SmtEngine> d_subsolver; - - /** - * If applicable, the function-to-synthesize that the subsolver is solving - * for. This is used for the get-abduct command. - */ - Expr d_sssf; - - /** - * The conjecture of the current abduction problem. This expression is only - * valid while we are in mode SMT_MODE_ABDUCT. - */ - Expr d_abdConj; + /** The solver for abduction queries */ + std::unique_ptr<smt::AbductionSolver> d_abductSolver; /** * The assertion list (before any conversion) for supporting diff --git a/src/theory/datatypes/sygus_datatype_utils.cpp b/src/theory/datatypes/sygus_datatype_utils.cpp index e95b66bd7..8ff0f8db2 100644 --- a/src/theory/datatypes/sygus_datatype_utils.cpp +++ b/src/theory/datatypes/sygus_datatype_utils.cpp @@ -232,8 +232,7 @@ Node mkSygusTerm(const DType& dt, // ensures we don't try to expand e.g. bitvector extract operators, // whose type is undefined, and thus should not be passed to // expandDefinitions. - opn = Node::fromExpr( - smt::currentSmtEngine()->expandDefinitions(op.toExpr())); + opn = smt::currentSmtEngine()->expandDefinitions(op); opn = Rewriter::rewrite(opn); opn = eliminatePartialOperators(opn); SygusOpRewrittenAttribute sora; |