diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/CMakeLists.txt | 2 | ||||
| -rw-r--r-- | src/theory/builtin/kinds | 5 | ||||
| -rw-r--r-- | src/theory/builtin/theory_builtin_type_rules.h | 25 | ||||
| -rw-r--r-- | src/theory/quantifiers/expr_miner.cpp | 38 | ||||
| -rw-r--r-- | src/theory/quantifiers/expr_miner.h | 3 | ||||
| -rw-r--r-- | src/theory/quantifiers/sygus/cegis_core_connective.cpp | 54 | ||||
| -rw-r--r-- | src/theory/quantifiers/sygus/sygus_repair_const.cpp | 39 | ||||
| -rw-r--r-- | src/theory/quantifiers/sygus/synth_conjecture.cpp | 35 | ||||
| -rw-r--r-- | src/theory/quantifiers/sygus/synth_engine.cpp | 10 | ||||
| -rw-r--r-- | src/theory/smt_engine_subsolver.cpp | 170 | ||||
| -rw-r--r-- | src/theory/smt_engine_subsolver.h | 119 |
11 files changed, 375 insertions, 125 deletions
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 52f46147c..201b6a21d 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -665,6 +665,8 @@ libcvc4_add_sources( theory/sets/theory_sets_type_rules.h theory/shared_terms_database.cpp theory/shared_terms_database.h + theory/smt_engine_subsolver.cpp + theory/smt_engine_subsolver.h theory/sort_inference.cpp theory/sort_inference.h theory/strings/base_solver.cpp diff --git a/src/theory/builtin/kinds b/src/theory/builtin/kinds index c90419def..4d5e95119 100644 --- a/src/theory/builtin/kinds +++ b/src/theory/builtin/kinds @@ -309,7 +309,10 @@ operator FUNCTION_TYPE 2: "a function type" cardinality FUNCTION_TYPE \ "::CVC4::theory::builtin::FunctionProperties::computeCardinality(%TYPE%)" \ "theory/builtin/theory_builtin_type_rules.h" -well-founded FUNCTION_TYPE false +well-founded FUNCTION_TYPE \ + "::CVC4::theory::builtin::FunctionProperties::isWellFounded(%TYPE%)" \ + "::CVC4::theory::builtin::FunctionProperties::mkGroundTerm(%TYPE%)" \ + "theory/builtin/theory_builtin_type_rules.h" enumerator FUNCTION_TYPE \ ::CVC4::theory::builtin::FunctionEnumerator \ "theory/builtin/type_enumerator.h" diff --git a/src/theory/builtin/theory_builtin_type_rules.h b/src/theory/builtin/theory_builtin_type_rules.h index d49edbc8c..a3d1776e1 100644 --- a/src/theory/builtin/theory_builtin_type_rules.h +++ b/src/theory/builtin/theory_builtin_type_rules.h @@ -223,6 +223,31 @@ class FunctionProperties { return valueCard ^ argsCard; } + /** Function type is well-founded if its component sorts are */ + static bool isWellFounded(TypeNode type) + { + for (TypeNode::iterator i = type.begin(), i_end = type.end(); i != i_end; + ++i) + { + if (!(*i).isWellFounded()) + { + return false; + } + } + return true; + } + /** + * Ground term for function sorts is (lambda x. t) where x is the + * canonical variable list for its type and t is the canonical ground term of + * its range. + */ + static Node mkGroundTerm(TypeNode type) + { + NodeManager* nm = NodeManager::currentNM(); + Node bvl = nm->getBoundVarListForFunctionType(type); + Node ret = type.getRangeType().mkGroundTerm(); + return nm->mkNode(kind::LAMBDA, bvl, ret); + } };/* class FuctionProperties */ class SExprProperties { diff --git a/src/theory/quantifiers/expr_miner.cpp b/src/theory/quantifiers/expr_miner.cpp index 6b042e294..8645be1a1 100644 --- a/src/theory/quantifiers/expr_miner.cpp +++ b/src/theory/quantifiers/expr_miner.cpp @@ -18,6 +18,7 @@ #include "smt/smt_engine.h" #include "smt/smt_engine_scope.h" #include "theory/quantifiers/term_util.h" +#include "theory/smt_engine_subsolver.h" using namespace std; using namespace CVC4::kind; @@ -76,41 +77,22 @@ void ExprMiner::initializeChecker(std::unique_ptr<SmtEngine>& checker, // Convert bound variables to skolems. This ensures the satisfiability // check is ground. Node squery = convertToSkolem(query); - NodeManager* nm = NodeManager::currentNM(); if (options::sygusExprMinerCheckUseExport()) { - // To support a separate timeout for the subsolver, we need to create - // a separate ExprManager with its own options. This requires that - // the expressions sent to the subsolver can be exported from on - // ExprManager to another. If the export fails, we throw an - // OptionException. - try - { - checker.reset(new SmtEngine(&em)); - checker->setIsInternalSubsolver(); - checker->setTimeLimit(options::sygusExprMinerCheckTimeout(), true); - checker->setLogic(smt::currentSmtEngine()->getLogicInfo()); - checker->setOption("sygus-rr-synth-input", false); - checker->setOption("input-language", "smt2"); - Expr equery = squery.toExpr().exportTo(&em, varMap); - checker->assertFormula(equery); - } - catch (const CVC4::ExportUnsupportedException& e) - { - std::stringstream msg; - msg << "Unable to export " << squery - << " but exporting expressions is " - "required for an expression " - "miner check."; - throw OptionException(msg.str()); - } + initializeSubsolverWithExport(checker, + em, + varMap, + squery.toExpr(), + true, + options::sygusExprMinerCheckTimeout()); + checker->setOption("sygus-rr-synth-input", false); + checker->setOption("input-language", "smt2"); needExport = true; } else { + initializeSubsolver(checker, squery.toExpr()); needExport = false; - checker.reset(new SmtEngine(nm->toExprManager())); - checker->assertFormula(squery.toExpr()); } } diff --git a/src/theory/quantifiers/expr_miner.h b/src/theory/quantifiers/expr_miner.h index 233ef39f7..4625e762a 100644 --- a/src/theory/quantifiers/expr_miner.h +++ b/src/theory/quantifiers/expr_miner.h @@ -20,8 +20,9 @@ #include <map> #include <memory> #include <vector> +#include "expr/expr.h" #include "expr/expr_manager.h" -#include "expr/node.h" +#include "expr/variable_type_map.h" #include "smt/smt_engine.h" #include "theory/quantifiers/sygus_sampler.h" diff --git a/src/theory/quantifiers/sygus/cegis_core_connective.cpp b/src/theory/quantifiers/sygus/cegis_core_connective.cpp index ad281b009..cae5cd823 100644 --- a/src/theory/quantifiers/sygus/cegis_core_connective.cpp +++ b/src/theory/quantifiers/sygus/cegis_core_connective.cpp @@ -24,6 +24,7 @@ #include "theory/quantifiers/sygus/ce_guided_single_inv.h" #include "theory/quantifiers/term_util.h" #include "theory/quantifiers_engine.h" +#include "theory/smt_engine_subsolver.h" #include "util/random.h" using namespace CVC4::kind; @@ -626,36 +627,9 @@ bool CegisCoreConnective::getUnsatCore( Result CegisCoreConnective::checkSat(Node n, std::vector<Node>& mvs) const { - Assert(mvs.empty()); - Assert(n.getType().isBoolean()); Trace("sygus-ccore-debug") << "...check-sat " << n << "..." << std::endl; - n = Rewriter::rewrite(n); - if (n.isConst()) - { - if (n.getConst<bool>()) - { - // default model - for (const Node& v : d_vars) - { - mvs.push_back(v.getType().mkGroundTerm()); - } - return Result(Result::SAT); - } - else - { - return Result(Result::UNSAT); - } - } - SmtEngine smt(NodeManager::currentNM()->toExprManager()); - smt.setIsInternalSubsolver(); - smt.setLogic(smt::currentSmtEngine()->getLogicInfo()); - smt.assertFormula(n.toExpr()); - Result r = smt.checkSat(); + Result r = checkWithSubsolver(n, d_vars, mvs); Trace("sygus-ccore-debug") << "...got " << r << std::endl; - if (r.asSatisfiabilityResult().isSat() == Result::SAT) - { - getModel(smt, mvs); - } return r; } @@ -762,9 +736,8 @@ Node CegisCoreConnective::constructSolutionFromPool(Component& ccheck, { addSuccess = false; // try a new core - SmtEngine checkSol(nm->toExprManager()); - checkSol.setIsInternalSubsolver(); - checkSol.setLogic(smt::currentSmtEngine()->getLogicInfo()); + std::unique_ptr<SmtEngine> checkSol; + initializeSubsolver(checkSol); Trace("sygus-ccore") << "----- Check candidate " << an << std::endl; std::vector<Node> rasserts = asserts; rasserts.push_back(d_sc); @@ -773,9 +746,9 @@ Node CegisCoreConnective::constructSolutionFromPool(Component& ccheck, Node query = rasserts.size() == 1 ? rasserts[0] : nm->mkNode(AND, rasserts); for (const Node& a : rasserts) { - checkSol.assertFormula(a.toExpr()); + checkSol->assertFormula(a.toExpr()); } - Result r = checkSol.checkSat(); + Result r = checkSol->checkSat(); Trace("sygus-ccore") << "----- check-sat returned " << r << std::endl; // In terms of Variant #2, this is the check "if (S ^ D) => B" if (r.asSatisfiabilityResult().isSat() == Result::UNSAT) @@ -788,7 +761,7 @@ Node CegisCoreConnective::constructSolutionFromPool(Component& ccheck, std::unordered_set<Node, NodeHashFunction> queryAsserts; queryAsserts.insert(ccheck.getFormula()); queryAsserts.insert(d_sc); - bool hasQuery = getUnsatCore(checkSol, queryAsserts, uasserts); + bool hasQuery = getUnsatCore(*checkSol, queryAsserts, uasserts); // now, check the side condition bool falseCore = false; if (!d_sc.isNull()) @@ -803,18 +776,17 @@ Node CegisCoreConnective::constructSolutionFromPool(Component& ccheck, { // In terms of Variant #2, this is the check "if S ^ U is unsat" Trace("sygus-ccore") << "----- Check side condition" << std::endl; - SmtEngine checkSc(nm->toExprManager()); - checkSc.setIsInternalSubsolver(); - checkSc.setLogic(smt::currentSmtEngine()->getLogicInfo()); + std::unique_ptr<SmtEngine> checkSc; + initializeSubsolver(checkSc); std::vector<Node> scasserts; scasserts.insert(scasserts.end(), uasserts.begin(), uasserts.end()); scasserts.push_back(d_sc); std::shuffle(scasserts.begin(), scasserts.end(), Random::getRandom()); for (const Node& sca : scasserts) { - checkSc.assertFormula(sca.toExpr()); + checkSc->assertFormula(sca.toExpr()); } - Result rsc = checkSc.checkSat(); + Result rsc = checkSc->checkSat(); Trace("sygus-ccore") << "----- check-sat returned " << rsc << std::endl; if (rsc.asSatisfiabilityResult().isSat() == Result::UNSAT) @@ -825,7 +797,7 @@ Node CegisCoreConnective::constructSolutionFromPool(Component& ccheck, uasserts.clear(); std::unordered_set<Node, NodeHashFunction> queryAsserts2; queryAsserts2.insert(d_sc); - getUnsatCore(checkSc, queryAsserts2, uasserts); + getUnsatCore(*checkSc, queryAsserts2, uasserts); falseCore = true; } } @@ -869,7 +841,7 @@ Node CegisCoreConnective::constructSolutionFromPool(Component& ccheck, // it does not entail the postcondition, add an assertion that blocks // the current point mvs.clear(); - getModel(checkSol, mvs); + getModel(*checkSol, mvs); // should evaluate to true Node ean = evaluate(an, Node::null(), mvs); Assert(ean.isConst() && ean.getConst<bool>()); diff --git a/src/theory/quantifiers/sygus/sygus_repair_const.cpp b/src/theory/quantifiers/sygus/sygus_repair_const.cpp index 9ab94d1bc..5874104ce 100644 --- a/src/theory/quantifiers/sygus/sygus_repair_const.cpp +++ b/src/theory/quantifiers/sygus/sygus_repair_const.cpp @@ -25,6 +25,7 @@ #include "theory/quantifiers/sygus/sygus_grammar_norm.h" #include "theory/quantifiers/sygus/term_database_sygus.h" #include "theory/quantifiers_engine.h" +#include "theory/smt_engine_subsolver.h" using namespace CVC4::kind; @@ -111,36 +112,22 @@ void SygusRepairConst::initializeChecker(std::unique_ptr<SmtEngine>& checker, // To support a separate timeout for the subsolver, we need to create // a separate ExprManager with its own options. This requires that // the expressions sent to the subsolver can be exported from on - // ExprManager to another. If the export fails, we throw an - // OptionException. - try - { - checker.reset(new SmtEngine(&em)); - checker->setIsInternalSubsolver(); - checker->setTimeLimit(options::sygusRepairConstTimeout(), true); - checker->setLogic(smt::currentSmtEngine()->getLogicInfo()); - // renable options disabled by sygus - checker->setOption("miniscope-quant", true); - checker->setOption("miniscope-quant-fv", true); - checker->setOption("quant-split", true); - // export - Expr e_query = query.toExpr().exportTo(&em, varMap); - checker->assertFormula(e_query); - } - catch (const CVC4::ExportUnsupportedException& e) - { - std::stringstream msg; - msg << "Unable to export " << query - << " but exporting expressions is required for " - "--sygus-repair-const-timeout."; - throw OptionException(msg.str()); - } + // ExprManager to another. + initializeSubsolverWithExport(checker, + em, + varMap, + query.toExpr(), + true, + options::sygusRepairConstTimeout()); + // renable options disabled by sygus + checker->setOption("miniscope-quant", true); + checker->setOption("miniscope-quant-fv", true); + checker->setOption("quant-split", true); } else { needExport = false; - checker.reset(new SmtEngine(nm->toExprManager())); - checker->assertFormula(query.toExpr()); + initializeSubsolver(checker, query.toExpr()); } } diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp index fe0e99a4d..1596c30f0 100644 --- a/src/theory/quantifiers/sygus/synth_conjecture.cpp +++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp @@ -20,8 +20,6 @@ #include "options/quantifiers_options.h" #include "printer/printer.h" #include "prop/prop_engine.h" -#include "smt/smt_engine.h" -#include "smt/smt_engine_scope.h" #include "smt/smt_statistics_registry.h" #include "theory/datatypes/theory_datatypes_utils.h" #include "theory/quantifiers/first_order_model.h" @@ -34,6 +32,7 @@ #include "theory/quantifiers/sygus/term_database_sygus.h" #include "theory/quantifiers/term_util.h" #include "theory/quantifiers_engine.h" +#include "theory/smt_engine_subsolver.h" #include "theory/theory_engine.h" using namespace CVC4::kind; @@ -592,24 +591,22 @@ bool SynthConjecture::doCheck(std::vector<Node>& lems) if (options::sygusVerifySubcall()) { Trace("cegqi-engine") << " *** Verify with subcall..." << std::endl; - SmtEngine verifySmt(nm->toExprManager()); - verifySmt.setIsInternalSubsolver(); - verifySmt.setLogic(smt::currentSmtEngine()->getLogicInfo()); - verifySmt.assertFormula(query.toExpr()); - Result r = verifySmt.checkSat(); + + Result r = + checkWithSubsolver(query.toExpr(), d_ce_sk_vars, d_ce_sk_var_mvs); Trace("cegqi-engine") << " ...got " << r << std::endl; if (r.asSatisfiabilityResult().isSat() == Result::SAT) { - Trace("cegqi-engine") << " * Verification lemma failed for:\n "; - // do not send out - for (unsigned i = 0, size = d_ce_sk_vars.size(); i < size; i++) + if (Trace.isOn("cegqi-engine")) { - Node v = d_ce_sk_vars[i]; - Node mv = Node::fromExpr(verifySmt.getValue(v.toExpr())); - Trace("cegqi-engine") << vars[i] << " -> " << mv << " "; - d_ce_sk_var_mvs.push_back(mv); + Trace("cegqi-engine") << " * Verification lemma failed for:\n "; + for (unsigned i = 0, size = d_ce_sk_vars.size(); i < size; i++) + { + Trace("cegqi-engine") + << d_ce_sk_vars[i] << " -> " << d_ce_sk_var_mvs[i] << " "; + } + Trace("cegqi-engine") << std::endl; } - Trace("cegqi-engine") << std::endl; #ifdef CVC4_ASSERTIONS // the values for the query should be a complete model Node squery = query.substitute(d_ce_sk_vars.begin(), @@ -661,15 +658,9 @@ bool SynthConjecture::checkSideCondition(const std::vector<Node>& cvals) const { Node sc = d_embedSideCondition.substitute( d_candidates.begin(), d_candidates.end(), cvals.begin(), cvals.end()); - sc = Rewriter::rewrite(sc); Trace("cegqi-engine") << "Check side condition..." << std::endl; Trace("cegqi-debug") << "Check side condition : " << sc << std::endl; - NodeManager* nm = NodeManager::currentNM(); - SmtEngine scSmt(nm->toExprManager()); - scSmt.setIsInternalSubsolver(); - scSmt.setLogic(smt::currentSmtEngine()->getLogicInfo()); - scSmt.assertFormula(sc.toExpr()); - Result r = scSmt.checkSat(); + Result r = checkWithSubsolver(sc); Trace("cegqi-debug") << "...got side condition : " << r << std::endl; if (r == Result::UNSAT) { diff --git a/src/theory/quantifiers/sygus/synth_engine.cpp b/src/theory/quantifiers/sygus/synth_engine.cpp index c9ed16a5f..a77d3681b 100644 --- a/src/theory/quantifiers/sygus/synth_engine.cpp +++ b/src/theory/quantifiers/sygus/synth_engine.cpp @@ -16,12 +16,11 @@ #include "theory/quantifiers/sygus/synth_engine.h" #include "options/quantifiers_options.h" -#include "smt/smt_engine.h" -#include "smt/smt_engine_scope.h" #include "theory/quantifiers/quantifiers_attributes.h" #include "theory/quantifiers/sygus/term_database_sygus.h" #include "theory/quantifiers/term_util.h" #include "theory/quantifiers_engine.h" +#include "theory/smt_engine_subsolver.h" #include "theory/theory_engine.h" using namespace CVC4::kind; @@ -169,9 +168,8 @@ void SynthEngine::assignConjecture(Node q) if (!sip.isPurelySingleInvocation() && sip.isNonGroundSingleInvocation()) { // create new smt engine to do quantifier elimination - SmtEngine smt_qe(nm->toExprManager()); - smt_qe.setIsInternalSubsolver(); - smt_qe.setLogic(smt::currentSmtEngine()->getLogicInfo()); + std::unique_ptr<SmtEngine> smt_qe; + initializeSubsolver(smt_qe); Trace("cegqi-qep") << "Property is non-ground single invocation, run " "QE to obtain single invocation." << std::endl; @@ -234,7 +232,7 @@ void SynthEngine::assignConjecture(Node q) Trace("cegqi-qep") << "Run quantifier elimination on " << conj_se_ngsi_subs << std::endl; - Expr qe_res = smt_qe.doQuantifierElimination( + Expr qe_res = smt_qe->doQuantifierElimination( conj_se_ngsi_subs.toExpr(), true, false); Trace("cegqi-qep") << "Result : " << qe_res << std::endl; diff --git a/src/theory/smt_engine_subsolver.cpp b/src/theory/smt_engine_subsolver.cpp new file mode 100644 index 000000000..6b856462a --- /dev/null +++ b/src/theory/smt_engine_subsolver.cpp @@ -0,0 +1,170 @@ +/********************* */ +/*! \file smt_engine_subsolver.cpp + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds, Andres Noetzli + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2019 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 Implementation of utilities for initializing subsolvers (copies of + ** SmtEngine) during solving. + **/ + +#include "theory/smt_engine_subsolver.h" + +#include "smt/smt_engine.h" +#include "smt/smt_engine_scope.h" +#include "theory/rewriter.h" + +namespace CVC4 { +namespace theory { + +// optimization: try to rewrite to constant +Result quickCheck(Node& query) +{ + query = theory::Rewriter::rewrite(query); + if (query.isConst()) + { + if (!query.getConst<bool>()) + { + return Result(Result::UNSAT); + } + else + { + return Result(Result::SAT); + } + } + return Result(Result::SAT_UNKNOWN, Result::REQUIRES_FULL_CHECK); +} + +void initializeSubsolver(std::unique_ptr<SmtEngine>& smte) +{ + NodeManager* nm = NodeManager::currentNM(); + smte.reset(new SmtEngine(nm->toExprManager())); + smte->setIsInternalSubsolver(); + smte->setLogic(smt::currentSmtEngine()->getLogicInfo()); +} + +void initializeSubsolverWithExport(std::unique_ptr<SmtEngine>& smte, + ExprManager& em, + ExprManagerMapCollection& varMap, + Node query, + bool needsTimeout, + unsigned long timeout) +{ + // To support a separate timeout for the subsolver, we need to use + // a separate ExprManager with its own options. This requires that + // the expressions sent to the subsolver can be exported from on + // ExprManager to another. If the export fails, we throw an + // OptionException. + try + { + smte.reset(new SmtEngine(&em)); + smte->setIsInternalSubsolver(); + if (needsTimeout) + { + smte->setTimeLimit(timeout, true); + } + smte->setLogic(smt::currentSmtEngine()->getLogicInfo()); + Expr equery = query.toExpr().exportTo(&em, varMap); + smte->assertFormula(equery); + } + catch (const CVC4::ExportUnsupportedException& e) + { + std::stringstream msg; + msg << "Unable to export " << query + << " but exporting expressions is " + "required for a subsolver."; + throw OptionException(msg.str()); + } +} + +void initializeSubsolver(std::unique_ptr<SmtEngine>& smte, Node query) +{ + initializeSubsolver(smte); + smte->assertFormula(query.toExpr()); +} + +Result checkWithSubsolver(std::unique_ptr<SmtEngine>& smte, Node query) +{ + Assert(query.getType().isBoolean()); + Result r = quickCheck(query); + if (!r.isUnknown()) + { + return r; + } + initializeSubsolver(smte, query); + return smte->checkSat(); +} + +Result checkWithSubsolver(Node query, bool needsTimeout, unsigned long timeout) +{ + std::vector<Node> vars; + std::vector<Node> modelVals; + return checkWithSubsolver(query, vars, modelVals, needsTimeout, timeout); +} + +Result checkWithSubsolver(Node query, + const std::vector<Node>& vars, + std::vector<Node>& modelVals, + bool needsTimeout, + unsigned long timeout) +{ + Assert(query.getType().isBoolean()); + Assert(modelVals.empty()); + // ensure clear + modelVals.clear(); + Result r = quickCheck(query); + if (!r.isUnknown()) + { + if (r.asSatisfiabilityResult().isSat() == Result::SAT) + { + // default model + for (const Node& v : vars) + { + modelVals.push_back(v.getType().mkGroundTerm()); + } + } + return r; + } + std::unique_ptr<SmtEngine> smte; + ExprManagerMapCollection varMap; + NodeManager* nm = NodeManager::currentNM(); + ExprManager em(nm->getOptions()); + bool needsExport = false; + if (needsTimeout) + { + needsExport = true; + initializeSubsolverWithExport( + smte, em, varMap, query, needsTimeout, timeout); + } + else + { + initializeSubsolver(smte, query); + } + r = smte->checkSat(); + if (r.asSatisfiabilityResult().isSat() == Result::SAT) + { + for (const Node& v : vars) + { + Expr val; + if (needsExport) + { + Expr ev = v.toExpr().exportTo(&em, varMap); + val = smte->getValue(ev).exportTo(nm->toExprManager(), varMap); + } + else + { + val = smte->getValue(v.toExpr()); + } + modelVals.push_back(Node::fromExpr(val)); + } + } + return r; +} + +} // namespace theory +} // namespace CVC4 diff --git a/src/theory/smt_engine_subsolver.h b/src/theory/smt_engine_subsolver.h new file mode 100644 index 000000000..135175665 --- /dev/null +++ b/src/theory/smt_engine_subsolver.h @@ -0,0 +1,119 @@ +/********************* */ +/*! \file smt_engine_subsolver.h + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2019 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 Utilities for initializing subsolvers (copies of SmtEngine) during + ** solving. + **/ + +#include "cvc4_private.h" + +#ifndef CVC4__THEORY__SMT_ENGINE_SUBSOLVER_H +#define CVC4__THEORY__SMT_ENGINE_SUBSOLVER_H + +#include <map> +#include <memory> +#include <vector> +#include "expr/expr_manager.h" +#include "expr/node.h" +#include "expr/variable_type_map.h" +#include "smt/smt_engine.h" + +namespace CVC4 { +namespace theory { + +/** + * This function initializes the smt engine smte as a subsolver, e.g. it + * creates a new SMT engine and sets the options of the current SMT engine. + */ +void initializeSubsolver(std::unique_ptr<SmtEngine>& smte); + +/** + * Initialize Smt subsolver with exporting + * + * This function initializes the smt engine smte to check the satisfiability + * of the argument "query". + * + * The arguments em and varMap are used for supporting cases where we + * want smte to use a different expression manager instead of the current + * expression manager. The motivation for this so that different options can + * be set for the subcall. + * + * Notice that subsequent expressions extracted from smte (for instance, model + * values) must be exported to the current expression + * manager. + * + * @param smte The smt engine pointer to initialize + * @param em Reference to the expression manager to use + * @param varMap Map used for exporting expressions + * @param query The query to check + * @param needsTimeout Whether we would like to set a timeout + * @param timeout The timeout (in milliseconds) + */ +void initializeSubsolverWithExport(std::unique_ptr<SmtEngine>& smte, + ExprManager& em, + ExprManagerMapCollection& varMap, + Node query, + bool needsTimeout = false, + unsigned long timeout = 0); + +/** + * This function initializes the smt engine smte to check the satisfiability + * of the argument "query", without exporting expressions. + * + * Notice that is not possible to set a timeout value currently without + * exporting since the Options and ExprManager are tied together. + * TODO: eliminate this dependency (cvc4-projects #120). + */ +void initializeSubsolver(std::unique_ptr<SmtEngine>& smte, Node query); + +/** + * This returns the result of checking the satisfiability of formula query. + * + * If necessary, smte is initialized to the SMT engine that checked its + * satisfiability. + */ +Result checkWithSubsolver(std::unique_ptr<SmtEngine>& smte, Node query); + +/** + * This returns the result of checking the satisfiability of formula query. + * + * In contrast to above, this is used if the user of this method is not + * concerned with the state of the SMT engine after the check. + * + * @param query The query to check + * @param needsTimeout Whether we would like to set a timeout + * @param timeout The timeout (in milliseconds) + */ +Result checkWithSubsolver(Node query, + bool needsTimeout = false, + unsigned long timeout = 0); + +/** + * This returns the result of checking the satisfiability of formula query. + * Additionally, if the query is satisfiable, it adds the model values for vars + * into modelVars. + * + * @param query The query to check + * @param vars The variables we are interesting in getting a model for. + * @param modelVals A vector storing the model values of variables in vars. + * @param needsTimeout Whether we would like to set a timeout + * @param timeout The timeout (in milliseconds) + */ +Result checkWithSubsolver(Node query, + const std::vector<Node>& vars, + std::vector<Node>& modelVals, + bool needsTimeout = false, + unsigned long timeout = 0); + +} // namespace theory +} // namespace CVC4 + +#endif /* CVC4__THEORY__SMT_ENGINE_SUBSOLVER_H */ |