From 0cd812af4a6db43a7d6c2c95fff7e58f86e90a78 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 3 Mar 2020 09:18:59 -0600 Subject: [PATCH] Standardize the interface for SMT engine subsolvers (#3836) This standardizes the interface for using SMT engines as subsolvers in various approaches. More refactoring is possible, but this is an initial cut at cleaning things up. This will make it easy to accommodate new feature request for SyGuS (timeouts for calls to verification steps). Notice this also required adding a missing function (mkGroundTerm/isWellFounded for functions) which was caught after standardizing due to an optimization (don't create SmtEngines to check satisfiability of constant Booleans). --- src/CMakeLists.txt | 2 + src/theory/builtin/kinds | 5 +- .../builtin/theory_builtin_type_rules.h | 25 +++ src/theory/quantifiers/expr_miner.cpp | 38 ++-- src/theory/quantifiers/expr_miner.h | 3 +- .../sygus/cegis_core_connective.cpp | 54 ++---- .../quantifiers/sygus/sygus_repair_const.cpp | 39 ++-- .../quantifiers/sygus/synth_conjecture.cpp | 35 ++-- src/theory/quantifiers/sygus/synth_engine.cpp | 10 +- src/theory/smt_engine_subsolver.cpp | 170 ++++++++++++++++++ src/theory/smt_engine_subsolver.h | 119 ++++++++++++ 11 files changed, 375 insertions(+), 125 deletions(-) create mode 100644 src/theory/smt_engine_subsolver.cpp create mode 100644 src/theory/smt_engine_subsolver.h 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& 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 #include #include +#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& 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()) - { - // 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 checkSol; + initializeSubsolver(checkSol); Trace("sygus-ccore") << "----- Check candidate " << an << std::endl; std::vector 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 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 checkSc; + initializeSubsolver(checkSc); std::vector 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 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()); 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& 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& 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& 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 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()) + { + return Result(Result::UNSAT); + } + else + { + return Result(Result::SAT); + } + } + return Result(Result::SAT_UNKNOWN, Result::REQUIRES_FULL_CHECK); +} + +void initializeSubsolver(std::unique_ptr& smte) +{ + NodeManager* nm = NodeManager::currentNM(); + smte.reset(new SmtEngine(nm->toExprManager())); + smte->setIsInternalSubsolver(); + smte->setLogic(smt::currentSmtEngine()->getLogicInfo()); +} + +void initializeSubsolverWithExport(std::unique_ptr& 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& smte, Node query) +{ + initializeSubsolver(smte); + smte->assertFormula(query.toExpr()); +} + +Result checkWithSubsolver(std::unique_ptr& 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 vars; + std::vector modelVals; + return checkWithSubsolver(query, vars, modelVals, needsTimeout, timeout); +} + +Result checkWithSubsolver(Node query, + const std::vector& vars, + std::vector& 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 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 +#include +#include +#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& 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& 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& 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& 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& vars, + std::vector& modelVals, + bool needsTimeout = false, + unsigned long timeout = 0); + +} // namespace theory +} // namespace CVC4 + +#endif /* CVC4__THEORY__SMT_ENGINE_SUBSOLVER_H */ -- 2.30.2