From 4689ed968658db8c499c0e232d3d2343e918fe6e Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 25 May 2022 15:52:08 -0500 Subject: [PATCH] Add model-based quantifier instantiation (#8729) This is a straightforward reimplementation of Ge/deMoura from CAV 2009. --- src/CMakeLists.txt | 2 + src/options/quantifiers_options.toml | 8 + src/preprocessing/passes/sort_infer.cpp | 13 +- src/smt/set_defaults.cpp | 18 +- src/smt/solver_engine.cpp | 7 - src/theory/inference_id.cpp | 1 + src/theory/inference_id.h | 2 + .../quantifiers/inst_strategy_enumerative.h | 1 - src/theory/quantifiers/inst_strategy_mbqi.cpp | 510 ++++++++++++++++++ src/theory/quantifiers/inst_strategy_mbqi.h | 108 ++++ .../quantifiers/quantifiers_modules.cpp | 5 + src/theory/quantifiers/quantifiers_modules.h | 3 + src/theory/quantifiers/skolemize.h | 6 +- src/theory/smt_engine_subsolver.cpp | 6 + test/regress/cli/CMakeLists.txt | 1 + test/regress/cli/regress0/ho/issue6536.smt2 | 4 +- .../cli/regress0/push-pop/inc-double-u.smt2 | 6 +- .../cli/regress0/quantifiers/mbqi-simple.smt2 | 13 + test/regress/cli/regress1/bug567.smt2 | 6 +- test/regress/cli/regress1/fmf/issue3587.smt2 | 4 +- .../regress1/quantifiers/dt-tc-opt-small.smt2 | 3 +- .../regress1/quantifiers/issue3724-quant.smt2 | 4 +- 22 files changed, 700 insertions(+), 31 deletions(-) create mode 100644 src/theory/quantifiers/inst_strategy_mbqi.cpp create mode 100644 src/theory/quantifiers/inst_strategy_mbqi.h create mode 100644 test/regress/cli/regress0/quantifiers/mbqi-simple.smt2 diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index c045f77c8..d231276be 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -817,6 +817,8 @@ libcvc5_add_sources( theory/quantifiers/inst_match_trie.h theory/quantifiers/inst_strategy_enumerative.cpp theory/quantifiers/inst_strategy_enumerative.h + theory/quantifiers/inst_strategy_mbqi.cpp + theory/quantifiers/inst_strategy_mbqi.h theory/quantifiers/inst_strategy_pool.cpp theory/quantifiers/inst_strategy_pool.h theory/quantifiers/instantiate.cpp diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml index a624aae92..8ee7eebf6 100644 --- a/src/options/quantifiers_options.toml +++ b/src/options/quantifiers_options.toml @@ -184,6 +184,14 @@ name = "Quantifiers" default = "false" help = "do global negation of input formula" +[[option]] + name = "mbqi" + category = "expert" + long = "mbqi" + type = "bool" + default = "false" + help = "use model-based quantifier instantiation" + #### E-matching options [[option]] diff --git a/src/preprocessing/passes/sort_infer.cpp b/src/preprocessing/passes/sort_infer.cpp index a530eb234..eb0102c8e 100644 --- a/src/preprocessing/passes/sort_infer.cpp +++ b/src/preprocessing/passes/sort_infer.cpp @@ -72,12 +72,13 @@ PreprocessingPassResult SortInferencePass::applyInternal( // could indicate correspondence between the functions // for (f1, f2) in model_replace_f, f1's model should be based on f2. // See cvc4-wishues/issues/75. - } - // only need to compute monotonicity on the resulting formula if we are - // using this option - if (options().uf.ufssFairnessMonotone) - { - si->computeMonotonicity(assertionsToPreprocess->ref()); + + // only need to compute monotonicity on the resulting formula if we are + // using this option + if (options().uf.ufssFairnessMonotone) + { + si->computeMonotonicity(assertionsToPreprocess->ref()); + } } return PreprocessingPassResult::NO_CONFLICT; } diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp index d9a6f5fbc..ad3eebcef 100644 --- a/src/smt/set_defaults.cpp +++ b/src/smt/set_defaults.cpp @@ -1395,13 +1395,25 @@ void SetDefaults::setDefaultsQuantifiers(const LogicInfo& logic, // must have finite model finding on opts.writeQuantifiers().finiteModelFind = true; } - if (opts.quantifiers.instMaxLevel != -1) { - verbose(1) << "SolverEngine: turning off cbqi to support instMaxLevel" - << std::endl; + notifyModifyOption("cegqi", "false", "instMaxLevel"); opts.writeQuantifiers().cegqi = false; } + if (opts.quantifiers.mbqi) + { + // MBQI is an alternative to CEGQI/SyQI + if (!opts.quantifiers.cegqiWasSetByUser) + { + notifyModifyOption("cegqi", "false", "mbqi"); + opts.writeQuantifiers().cegqi = false; + } + if (!opts.quantifiers.sygusInstWasSetByUser) + { + notifyModifyOption("sygusInst", "false", "mbqi"); + opts.writeQuantifiers().sygusInst = false; + } + } if (opts.quantifiers.fmfBoundLazyWasSetByUser && opts.quantifiers.fmfBoundLazy) diff --git a/src/smt/solver_engine.cpp b/src/smt/solver_engine.cpp index 91f0b9b63..952db55ff 100644 --- a/src/smt/solver_engine.cpp +++ b/src/smt/solver_engine.cpp @@ -1461,13 +1461,6 @@ void SolverEngine::checkUnsatCore() coreChecker->getOptions().writeSmt().produceProofs = false; coreChecker->getOptions().writeSmt().checkProofs = false; - // set up separation logic heap if necessary - TypeNode sepLocType, sepDataType; - if (getSepHeapTypes(sepLocType, sepDataType)) - { - coreChecker->declareSepHeap(sepLocType, sepDataType); - } - d_env->verbose(1) << "SolverEngine::checkUnsatCore(): pushing core assertions" << std::endl; theory::TrustSubstitutionMap& tls = d_env->getTopLevelSubstitutions(); diff --git a/src/theory/inference_id.cpp b/src/theory/inference_id.cpp index 2c9c8eb04..300cad111 100644 --- a/src/theory/inference_id.cpp +++ b/src/theory/inference_id.cpp @@ -227,6 +227,7 @@ const char* toString(InferenceId i) return "QUANTIFIERS_INST_FMF_FMC_EXH"; case InferenceId::QUANTIFIERS_INST_CEGQI: return "QUANTIFIERS_INST_CEGQI"; case InferenceId::QUANTIFIERS_INST_SYQI: return "QUANTIFIERS_INST_SYQI"; + case InferenceId::QUANTIFIERS_INST_MBQI: return "QUANTIFIERS_INST_MBQI"; case InferenceId::QUANTIFIERS_INST_ENUM: return "QUANTIFIERS_INST_ENUM"; case InferenceId::QUANTIFIERS_INST_POOL: return "QUANTIFIERS_INST_POOL"; case InferenceId::QUANTIFIERS_BINT_PROXY: return "QUANTIFIERS_BINT_PROXY"; diff --git a/src/theory/inference_id.h b/src/theory/inference_id.h index 7ed9bfc26..774a5b586 100644 --- a/src/theory/inference_id.h +++ b/src/theory/inference_id.h @@ -333,6 +333,8 @@ enum class InferenceId QUANTIFIERS_INST_CEGQI, // instantiations from syntax-guided instantiation QUANTIFIERS_INST_SYQI, + // instantiations from model-based instantiation + QUANTIFIERS_INST_MBQI, // instantiations from enumerative instantiation QUANTIFIERS_INST_ENUM, // instantiations from pool instantiation diff --git a/src/theory/quantifiers/inst_strategy_enumerative.h b/src/theory/quantifiers/inst_strategy_enumerative.h index 2ec193efc..4e4cd7abd 100644 --- a/src/theory/quantifiers/inst_strategy_enumerative.h +++ b/src/theory/quantifiers/inst_strategy_enumerative.h @@ -18,7 +18,6 @@ #ifndef CVC5__INST_STRATEGY_ENUMERATIVE_H #define CVC5__INST_STRATEGY_ENUMERATIVE_H -#include "smt/env_obj.h" #include "theory/quantifiers/quant_module.h" namespace cvc5::internal { diff --git a/src/theory/quantifiers/inst_strategy_mbqi.cpp b/src/theory/quantifiers/inst_strategy_mbqi.cpp new file mode 100644 index 000000000..a151b225c --- /dev/null +++ b/src/theory/quantifiers/inst_strategy_mbqi.cpp @@ -0,0 +1,510 @@ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2022 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. + * **************************************************************************** + * + * Model-based quantifier instantiation + */ + +#include "theory/quantifiers/inst_strategy_mbqi.h" + +#include "expr/node_algorithm.h" +#include "expr/skolem_manager.h" +#include "expr/subs.h" +#include "theory/quantifiers/first_order_model.h" +#include "theory/quantifiers/instantiate.h" +#include "theory/quantifiers/quantifiers_rewriter.h" +#include "theory/quantifiers/skolemize.h" +#include "theory/smt_engine_subsolver.h" + +using namespace std; +using namespace cvc5::internal::kind; + +namespace cvc5::internal { +namespace theory { +namespace quantifiers { + +InstStrategyMbqi::InstStrategyMbqi(Env& env, + QuantifiersState& qs, + QuantifiersInferenceManager& qim, + QuantifiersRegistry& qr, + TermRegistry& tr) + : QuantifiersModule(env, qs, qim, qr, tr) +{ + // some kinds may appear in model values that cannot be asserted + d_nonClosedKinds.insert(STORE_ALL); + d_nonClosedKinds.insert(CODATATYPE_BOUND_VARIABLE); + d_nonClosedKinds.insert(UNINTERPRETED_SORT_VALUE); +} + +void InstStrategyMbqi::reset_round(Theory::Effort e) { d_quantChecked.clear(); } + +bool InstStrategyMbqi::needsCheck(Theory::Effort e) +{ + return e >= Theory::EFFORT_LAST_CALL; +} + +QuantifiersModule::QEffort InstStrategyMbqi::needsModel(Theory::Effort e) +{ + return QEFFORT_MODEL; +} + +void InstStrategyMbqi::check(Theory::Effort e, QEffort quant_e) +{ + if (e != Theory::EFFORT_LAST_CALL || quant_e != QEFFORT_MODEL) + { + return; + } + // see if the negation of each quantified formula is satisfiable in the model + std::vector disj; + FirstOrderModel* fm = d_treg.getModel(); + std::vector visit; + for (size_t i = 0, nquant = fm->getNumAssertedQuantifiers(); i < nquant; i++) + { + Node q = fm->getAssertedQuantifier(i); + if (!d_qreg.hasOwnership(q, this)) + { + continue; + } + process(q); + } +} + +bool InstStrategyMbqi::checkCompleteFor(Node q) +{ + return d_quantChecked.find(q) != d_quantChecked.end(); +} + +void InstStrategyMbqi::process(Node q) +{ + Assert(q.getKind() == FORALL); + Trace("mbqi") << "Process quantified formula: " << q << std::endl; + // Cache mapping terms in the skolemized body of q to the form passed to + // the subsolver. This is local to this call. + std::unordered_map tmpConvertMap; + // list of fresh variables per type + std::map > freshVarType; + // model values to the fresh variables + std::map mvToFreshVar; + + NodeManager* nm = NodeManager::currentNM(); + SkolemManager* sm = nm->getSkolemManager(); + const RepSet* rs = d_treg.getModel()->getRepSet(); + FirstOrderModel* fm = d_treg.getModel(); + + // allocate the skolem variables + Subs skolems; + for (const Node& v : q[0]) + { + Node k = sm->mkPurifySkolem(v, "mbk"); + skolems.add(v, k); + // do not take its model value (which does not exist) in conversion below + tmpConvertMap[k] = k; + } + // compute the skolemization in a separate traversal instead of mapping + // bound variables to skolems. This is to ensure we avoid variable shadowing + // for model values for functions + Node skq = skolems.apply(q[1]); + // convert to query + Node cbody = convertToQuery(skq, tmpConvertMap, freshVarType); + Trace("mbqi") << "- converted body: " << cbody << std::endl; + + // check if there are any bad kinds + if (cbody.isNull()) + { + Trace("mbqi") << "...failed to convert to query" << std::endl; + return; + } + Assert(!expr::hasSubtermKinds(d_nonClosedKinds, cbody)); + + std::vector constraints; + + // constraint: the negation of the skolemized body + Node bquery = rewrite(cbody.negate()); + if (!bquery.isConst()) + { + constraints.push_back(bquery); + } + else if (!bquery.getConst()) + { + d_quantChecked.insert(q); + Trace("mbqi") << "...success, by rewriting" << std::endl; + return; + } + // ensure the entire domain of uninterpreted sorts are converted + std::unordered_set processedUsort; + for (const Node& k : skolems.d_subs) + { + TypeNode tn = k.getType(); + if (!tn.isUninterpretedSort() + || processedUsort.find(tn) != processedUsort.end()) + { + continue; + } + processedUsort.insert(tn); + const std::vector* treps = rs->getTypeRepsOrNull(tn); + if (treps != nullptr) + { + for (const Node& r : *treps) + { + Node rv = fm->getValue(r); + Assert(rv.getKind() == kind::UNINTERPRETED_SORT_VALUE); + convertToQuery(rv, tmpConvertMap, freshVarType); + } + } + } + // constraint: the skolems of the given type are equal to one of the variables + // introduced for uninterpreted sorts + std::map >::iterator itk; + for (const Node& k : skolems.d_subs) + { + TypeNode tn = k.getType(); + itk = freshVarType.find(tn); + if (itk == freshVarType.end()) + { + // not an uninterpreted sort, continue + continue; + } + if (itk->second.empty()) + { + Trace("mbqi") << "warning: failed to get vars for type " << tn + << std::endl; + // this should never happen but we explicitly guard for it, since + // otherwise we would be model unsound below + Assert(false); + continue; + } + std::vector disj; + for (const Node& fv : itk->second) + { + disj.push_back(k.eqNode(fv)); + } + Node instCardCons = nm->mkOr(disj); + constraints.push_back(instCardCons); + } + + // constraint: distinctness of variables introduced for uninterpreted + // constants + std::vector allVars; + for (const std::pair >& fv : + freshVarType) + { + Assert(!fv.second.empty()); + allVars.insert(allVars.end(), fv.second.begin(), fv.second.end()); + if (fv.second.size() > 1) + { + std::vector fvars(fv.second.begin(), fv.second.end()); + constraints.push_back(nm->mkNode(DISTINCT, fvars)); + } + } + + // make the query + Node query = nm->mkAnd(constraints); + + std::unique_ptr mbqiChecker; + initializeSubsolver(mbqiChecker, d_env); + mbqiChecker->setOption("produce-models", "true"); + mbqiChecker->assertFormula(query); + Trace("mbqi") << "*** Check sat..." << std::endl; + Trace("mbqi") << " query is : " << query << std::endl; + Result r = mbqiChecker->checkSat(); + Trace("mbqi") << " ...got : " << r << std::endl; + if (r.getStatus() == Result::UNSAT) + { + d_quantChecked.insert(q); + Trace("mbqi") << "...success, SAT" << std::endl; + return; + } + + // get the model values for all fresh variables + for (const Node& v : allVars) + { + Node mv = mbqiChecker->getValue(v); + Assert(mvToFreshVar.find(mv) == mvToFreshVar.end()); + mvToFreshVar[mv] = v; + } + + // get the model values for skolems + std::vector terms; + getModelFromSubsolver(*mbqiChecker.get(), skolems.d_subs, terms); + Assert(skolems.size() == terms.size()); + if (TraceIsOn("mbqi")) + { + Trace("mbqi") << "...model from subsolver is: " << std::endl; + for (size_t i = 0, nterms = skolems.size(); i < nterms; i++) + { + Trace("mbqi") << " " << skolems.d_subs[i] << " -> " << terms[i] + << std::endl; + } + } + // try to convert those terms to an instantiation + tmpConvertMap.clear(); + for (Node& v : terms) + { + Node vc = convertFromModel(v, tmpConvertMap, mvToFreshVar); + Assert(!vc.isNull()); + if (expr::hasSubtermKinds(d_nonClosedKinds, vc)) + { + Trace("mbqi") << "warning: failed to process model value " << vc + << ", from " << v + << ", use arbitrary term for instantiation" << std::endl; + vc = nm->mkGroundTerm(v.getType()); + } + v = vc; + } + + // get a term that has the same model value as the value each fresh variable + // represents + Subs fvToInst; + for (const Node& v : allVars) + { + // get a term that witnesses this variable + Node ov = sm->getOriginalForm(v); + Node mvt = rs->getTermForRepresentative(ov); + if (mvt.isNull()) + { + Trace("mbqi") << "warning: failed to get term from value " << ov + << ", use arbitrary term in query" << std::endl; + mvt = nm->mkGroundTerm(ov.getType()); + } + Assert(v.getType() == mvt.getType()); + fvToInst.add(v, mvt); + } + + // now convert fresh variables into terms + for (Node& v : terms) + { + v = fvToInst.apply(v); + } + + // try to add instantiation + Instantiate* qinst = d_qim.getInstantiate(); + if (!qinst->addInstantiation(q, terms, InferenceId::QUANTIFIERS_INST_MBQI)) + { + Trace("mbqi") << "...failed to add instantiation" << std::endl; + return; + } + Trace("mbqi") << "...success, instantiated" << std::endl; +} + +Node InstStrategyMbqi::convertToQuery( + Node t, + std::unordered_map& cmap, + std::map >& freshVarType) +{ + NodeManager* nm = NodeManager::currentNM(); + SkolemManager* sm = nm->getSkolemManager(); + FirstOrderModel* fm = d_treg.getModel(); + std::unordered_map::iterator it; + std::map modelValue; + std::unordered_set processingChildren; + std::vector visit; + visit.push_back(t); + TNode cur; + do + { + cur = visit.back(); + visit.pop_back(); + it = cmap.find(cur); + Trace("mbqi-debug") << "convertToQuery: " << cur << " " << cur.getKind() + << " " << cur.getType() << std::endl; + if (it != cmap.end()) + { + // already computed + continue; + } + if (processingChildren.find(cur) == processingChildren.end()) + { + Kind ck = cur.getKind(); + if (ck == BOUND_VARIABLE) + { + cmap[cur] = cur; + } + else if (ck == UNINTERPRETED_SORT_VALUE) + { + Assert(cur.getType().isUninterpretedSort()); + // return the fresh variable for this term + Node k = sm->mkPurifySkolem(cur, "mbk"); + freshVarType[cur.getType()].insert(k); + cmap[cur] = k; + continue; + } + else if (cur.isVar()) + { + if (!cur.getType().isFirstClass()) + { + // can be e.g. tester/constructor/selector + cmap[cur] = cur; + } + else + { + std::map::iterator itm = modelValue.find(cur); + if (itm == modelValue.end()) + { + Node mval = fm->getValue(cur); + Trace("mbqi-model") << " M[" << cur << "] = " << mval << "\n"; + modelValue[cur] = mval; + if (cur == mval) + { + // failed to evaluate in model, keep itself + cmap[cur] = cur; + } + else + { + visit.push_back(cur); + visit.push_back(mval); + } + } + else + { + Assert(cmap.find(itm->second) != cmap.end()) + << "Missing " << itm->second; + cmap[cur] = cmap[itm->second]; + } + } + } + else if (cur.getNumChildren() == 0) + { + // if this is a bad kind, fail immediately + if (d_nonClosedKinds.find(ck) != d_nonClosedKinds.end()) + { + return Node::null(); + } + cmap[cur] = cur; + } + else + { + processingChildren.insert(cur); + visit.push_back(cur); + if (cur.getMetaKind() == kind::metakind::PARAMETERIZED) + { + visit.push_back(cur.getOperator()); + } + visit.insert(visit.end(), cur.begin(), cur.end()); + } + continue; + } + processingChildren.erase(cur); + bool childChanged = false; + std::vector children; + if (cur.getMetaKind() == kind::metakind::PARAMETERIZED) + { + children.push_back(cur.getOperator()); + } + children.insert(children.end(), cur.begin(), cur.end()); + for (Node& cn : children) + { + it = cmap.find(cn); + Assert(it != cmap.end()); + Assert(!it->second.isNull()); + childChanged = childChanged || cn != it->second; + cn = it->second; + } + Node ret = cur; + if (childChanged) + { + ret = rewrite(nm->mkNode(cur.getKind(), children)); + } + cmap[cur] = ret; + } while (!visit.empty()); + + Assert(cmap.find(cur) != cmap.end()); + return cmap[cur]; +} + +Node InstStrategyMbqi::convertFromModel( + Node t, + std::unordered_map& cmap, + const std::map& mvToFreshVar) +{ + NodeManager* nm = NodeManager::currentNM(); + std::unordered_map::iterator it; + std::map modelValue; + std::unordered_set processingChildren; + std::vector visit; + visit.push_back(t); + TNode cur; + do + { + cur = visit.back(); + visit.pop_back(); + it = cmap.find(cur); + Trace("mbqi-debug") << "convertFromModel: " << cur << " " << cur.getKind() + << " " << cur.getType() << std::endl; + if (it != cmap.end()) + { + // already computed + continue; + } + if (processingChildren.find(cur) == processingChildren.end()) + { + Kind ck = cur.getKind(); + if (ck == UNINTERPRETED_SORT_VALUE) + { + Assert(cur.getType().isUninterpretedSort()); + // converting from query, find the variable that it is equal to + std::map::const_iterator itmv = mvToFreshVar.find(cur); + if (itmv != mvToFreshVar.end()) + { + cmap[cur] = itmv->second; + } + else + { + // failed to find equal, keep the value + cmap[cur] = cur; + } + } + else if (cur.getNumChildren() == 0) + { + cmap[cur] = cur; + } + else + { + processingChildren.insert(cur); + visit.push_back(cur); + if (cur.getMetaKind() == kind::metakind::PARAMETERIZED) + { + visit.push_back(cur.getOperator()); + } + visit.insert(visit.end(), cur.begin(), cur.end()); + } + continue; + } + processingChildren.erase(cur); + bool childChanged = false; + std::vector children; + if (cur.getMetaKind() == kind::metakind::PARAMETERIZED) + { + children.push_back(cur.getOperator()); + } + children.insert(children.end(), cur.begin(), cur.end()); + for (Node& cn : children) + { + it = cmap.find(cn); + Assert(it != cmap.end()); + Assert(!it->second.isNull()); + childChanged = childChanged || cn != it->second; + cn = it->second; + } + Node ret = cur; + if (childChanged) + { + ret = rewrite(nm->mkNode(cur.getKind(), children)); + } + cmap[cur] = ret; + } while (!visit.empty()); + + Assert(cmap.find(cur) != cmap.end()); + return cmap[cur]; +} + +} // namespace quantifiers +} // namespace theory +} // namespace cvc5::internal diff --git a/src/theory/quantifiers/inst_strategy_mbqi.h b/src/theory/quantifiers/inst_strategy_mbqi.h new file mode 100644 index 000000000..5695d3be8 --- /dev/null +++ b/src/theory/quantifiers/inst_strategy_mbqi.h @@ -0,0 +1,108 @@ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2022 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. + * **************************************************************************** + * + * Model-based quantifier instantiation + */ + +#include "cvc5_private.h" + +#ifndef CVC5__THEORY__QUANTIFIERS__INST_STRATEGY_MBQI_H +#define CVC5__THEORY__QUANTIFIERS__INST_STRATEGY_MBQI_H + +#include +#include + +#include "theory/quantifiers/quant_module.h" + +namespace cvc5::internal { +namespace theory { +namespace quantifiers { + +/** + * InstStrategyMbqi + * + * A basic implementation of Ge/de Moura CAV 2009. This class can be used to + * check whether the current model satisfies quantified formulas using + * subsolvers. The negation of the quantified formula is added as an assertion, + * along with embeddings of the models of uninterpreted sorts. If the query + * to the subsolver is unsat, then the quantified formula is satisfied. + * Otherwise, the model from the subsolver is used to construct an + * instantiation. + */ +class InstStrategyMbqi : public QuantifiersModule +{ + public: + InstStrategyMbqi(Env& env, + QuantifiersState& qs, + QuantifiersInferenceManager& qim, + QuantifiersRegistry& qr, + TermRegistry& tr); + ~InstStrategyMbqi() {} + /** reset round */ + void reset_round(Theory::Effort e) override; + /** needs check */ + bool needsCheck(Theory::Effort e) override; + /** needs model */ + QEffort needsModel(Theory::Effort e) override; + /** check */ + void check(Theory::Effort e, QEffort quant_e) override; + /** Check was complete for quantified formula q */ + bool checkCompleteFor(Node q) override; + /** identify */ + std::string identify() const override { return "InstStrategyMbqi"; } + + private: + /** + * Process quantified formula q, which may add q to d_quantChecked, add an + * instantiation for q, or do nothing if something went wrong (e.g. if the + * query to the subsolver could not be constructed). + */ + void process(Node q); + /** + * Convert to query. + * + * This converts term t that is the body of a quantified + * formula into a term that can be sent to the subsolver. Its free constants + * are replaced by their model values. The map freshVarType maintains fresh + * variables that were introduced corresponding to values of uninterpreted + * sort constants. + * + * cmap caches the results of the conversion. + */ + Node convertToQuery( + Node t, + std::unordered_map& cmap, + std::map >& freshVarType); + /** + * Convert from model + * + * This converts a term t that was returned as a model + * value by a subsolver. We use the mapping mvToFreshVar to convert + * uninterpreted constants to the fresh variables that were used for + * that value in the model from the subsolver. + * + * cmap caches the results of the conversion. + */ + Node convertFromModel(Node t, + std::unordered_map& cmap, + const std::map& mvToFreshVar); + /** The quantified formulas that we succeeded in checking */ + std::unordered_set d_quantChecked; + /** Kinds that cannot appear in queries */ + std::unordered_set d_nonClosedKinds; +}; + +} // namespace quantifiers +} // namespace theory +} // namespace cvc5::internal + +#endif /* CVC5__THEORY__QUANTIFIERS__INST_STRATEGY_MBQI_H */ diff --git a/src/theory/quantifiers/quantifiers_modules.cpp b/src/theory/quantifiers/quantifiers_modules.cpp index 243218214..a1f26122d 100644 --- a/src/theory/quantifiers/quantifiers_modules.cpp +++ b/src/theory/quantifiers/quantifiers_modules.cpp @@ -117,6 +117,11 @@ void QuantifiersModules::initialize(Env& env, d_sygus_inst.reset(new SygusInst(env, qs, qim, qr, tr)); modules.push_back(d_sygus_inst.get()); } + if (options.quantifiers.mbqi) + { + d_mbqi.reset(new InstStrategyMbqi(env, qs, qim, qr, tr)); + modules.push_back(d_mbqi.get()); + } if (options.quantifiers.oracles) { d_oracleEngine.reset(new OracleEngine(env, qs, qim, qr, tr)); diff --git a/src/theory/quantifiers/quantifiers_modules.h b/src/theory/quantifiers/quantifiers_modules.h index 599aaece1..5499b8edc 100644 --- a/src/theory/quantifiers/quantifiers_modules.h +++ b/src/theory/quantifiers/quantifiers_modules.h @@ -26,6 +26,7 @@ #include "theory/quantifiers/fmf/model_builder.h" #include "theory/quantifiers/fmf/model_engine.h" #include "theory/quantifiers/inst_strategy_enumerative.h" +#include "theory/quantifiers/inst_strategy_mbqi.h" #include "theory/quantifiers/inst_strategy_pool.h" #include "theory/quantifiers/oracle_engine.h" #include "theory/quantifiers/quant_conflict_find.h" @@ -95,6 +96,8 @@ class QuantifiersModules std::unique_ptr d_qsplit; /** SyGuS instantiation engine */ std::unique_ptr d_sygus_inst; + /** model-based quantifier instantiation */ + std::unique_ptr d_mbqi; /** Oracle engine */ std::unique_ptr d_oracleEngine; }; diff --git a/src/theory/quantifiers/skolemize.h b/src/theory/quantifiers/skolemize.h index 5c673f768..123fe0d95 100644 --- a/src/theory/quantifiers/skolemize.h +++ b/src/theory/quantifiers/skolemize.h @@ -108,7 +108,11 @@ class Skolemize : protected EnvObj std::vector& sk, Node& sub, std::vector& sub_vars); - /** get the skolemized body for quantified formula q */ + /** get the skolemized body for quantified formula q + * + * For example, if q is forall x. P( x ), this returns the formula P( k ) for + * a fresh Skolem constant k. + */ Node getSkolemizedBody(Node q); /** is n a variable that we can apply inductive strenghtening to? */ static bool isInductionTerm(Node n); diff --git a/src/theory/smt_engine_subsolver.cpp b/src/theory/smt_engine_subsolver.cpp index bb9f4cb2f..08ef7144f 100644 --- a/src/theory/smt_engine_subsolver.cpp +++ b/src/theory/smt_engine_subsolver.cpp @@ -64,6 +64,12 @@ void initializeSubsolver(std::unique_ptr& smte, { initializeSubsolver( smte, env.getOptions(), env.getLogicInfo(), needsTimeout, timeout); + // set up separation logic heap if necessary + TypeNode sepLocType, sepDataType; + if (env.getSepHeapTypes(sepLocType, sepDataType)) + { + smte->declareSepHeap(sepLocType, sepDataType); + } } Result checkWithSubsolver(std::unique_ptr& smte, diff --git a/test/regress/cli/CMakeLists.txt b/test/regress/cli/CMakeLists.txt index 82e07c46e..53a8dbb39 100644 --- a/test/regress/cli/CMakeLists.txt +++ b/test/regress/cli/CMakeLists.txt @@ -1091,6 +1091,7 @@ set(regress_0_tests regress0/quantifiers/macros-int-real.smt2 regress0/quantifiers/macros-real-arg.smt2 regress0/quantifiers/matching-lia-1arg.smt2 + regress0/quantifiers/mbqi-simple.smt2 regress0/quantifiers/mix-complete-strat.smt2 regress0/quantifiers/mix-match.smt2 regress0/quantifiers/mix-simp.smt2 diff --git a/test/regress/cli/regress0/ho/issue6536.smt2 b/test/regress/cli/regress0/ho/issue6536.smt2 index ed4d453a6..5f27e543a 100644 --- a/test/regress/cli/regress0/ho/issue6536.smt2 +++ b/test/regress/cli/regress0/ho/issue6536.smt2 @@ -1,5 +1,5 @@ -; COMMAND-LINE: --strings-exp -; EXPECT: unknown +; COMMAND-LINE: --strings-exp --mbqi +; EXPECT: sat (set-logic HO_ALL) (declare-datatypes ((a 0) (b 0)) (((c) (d)) ((h (j b)) (e)))) (declare-fun f () b) diff --git a/test/regress/cli/regress0/push-pop/inc-double-u.smt2 b/test/regress/cli/regress0/push-pop/inc-double-u.smt2 index a01643df3..e82a3d0de 100644 --- a/test/regress/cli/regress0/push-pop/inc-double-u.smt2 +++ b/test/regress/cli/regress0/push-pop/inc-double-u.smt2 @@ -1,12 +1,12 @@ -; COMMAND-LINE: --incremental +; COMMAND-LINE: --incremental --mbqi (set-logic UFLIA) (declare-fun P (Int) Bool) (declare-fun R (Int) Bool) (assert (forall ((x Int)) (=> (R x) (not (P x))))) -; EXPECT: unknown +; EXPECT: sat (check-sat) (assert (R 0)) -; EXPECT: unknown +; EXPECT: sat (check-sat) (assert (forall ((x Int)) (P x))) ; EXPECT: unsat diff --git a/test/regress/cli/regress0/quantifiers/mbqi-simple.smt2 b/test/regress/cli/regress0/quantifiers/mbqi-simple.smt2 new file mode 100644 index 000000000..1661cd426 --- /dev/null +++ b/test/regress/cli/regress0/quantifiers/mbqi-simple.smt2 @@ -0,0 +1,13 @@ +; COMMAND-LINE: --mbqi +; EXPECT: sat +(set-logic ALL) +(set-info :status sat) +(declare-fun Q (Int) Bool) +(declare-fun P (Int) Bool) +(assert (forall ((x Int)) (=> (Q x) (P x)))) +(assert (not (P 1))) +(assert (not (P 3))) +(assert (not (P 7))) +(assert (not (Q 2))) +(assert (not (Q 5))) +(check-sat) diff --git a/test/regress/cli/regress1/bug567.smt2 b/test/regress/cli/regress1/bug567.smt2 index 5b9bffd6f..71ce43e6f 100644 --- a/test/regress/cli/regress1/bug567.smt2 +++ b/test/regress/cli/regress1/bug567.smt2 @@ -1,7 +1,7 @@ -; COMMAND-LINE: --incremental -; EXPECT: unknown +; COMMAND-LINE: --incremental --mbqi +; EXPECT: unsat +; EXPECT: unsat ; EXPECT: unsat -; EXPECT: unknown (set-logic ALL) (declare-datatypes ((OptInt0 0)) (((Some (value0 Int)) (None)))) (declare-datatypes ((List0 0)) (((Cons (head0 Int) (tail0 List0)) (Nil)))) diff --git a/test/regress/cli/regress1/fmf/issue3587.smt2 b/test/regress/cli/regress1/fmf/issue3587.smt2 index 5ca5e4f16..9d8b714a1 100644 --- a/test/regress/cli/regress1/fmf/issue3587.smt2 +++ b/test/regress/cli/regress1/fmf/issue3587.smt2 @@ -1,5 +1,5 @@ -; COMMAND-LINE: --fmf-bound -; EXPECT: unknown +; COMMAND-LINE: --fmf-bound --mbqi +; EXPECT: unsat (set-logic ALL) (declare-sort a 0) (declare-datatypes ((prod 0)) (((Pair (gx a) (gy a))))) diff --git a/test/regress/cli/regress1/quantifiers/dt-tc-opt-small.smt2 b/test/regress/cli/regress1/quantifiers/dt-tc-opt-small.smt2 index 6cf81e80a..97f27662b 100644 --- a/test/regress/cli/regress1/quantifiers/dt-tc-opt-small.smt2 +++ b/test/regress/cli/regress1/quantifiers/dt-tc-opt-small.smt2 @@ -1,4 +1,5 @@ -; EXPECT: unknown +; COMMAND-LINE: --mbqi +; EXPECT: sat ; This triggered a failure related to datatypes model building (when symfpu is enabled) (set-logic ALL) diff --git a/test/regress/cli/regress1/quantifiers/issue3724-quant.smt2 b/test/regress/cli/regress1/quantifiers/issue3724-quant.smt2 index 32e82a8b5..21494ec39 100644 --- a/test/regress/cli/regress1/quantifiers/issue3724-quant.smt2 +++ b/test/regress/cli/regress1/quantifiers/issue3724-quant.smt2 @@ -1,5 +1,5 @@ -; COMMAND-LINE: -; EXPECT: unknown +; COMMAND-LINE: --mbqi +; EXPECT: unsat (set-logic HO_ALL) (assert (forall ((BOUND_VARIABLE_313 Bool) (BOUND_VARIABLE_314 (-> Int Bool)) (BOUND_VARIABLE_315 (-> Int Int)) (BOUND_VARIABLE_316 Int) (BOUND_VARIABLE_317 (-> Int Bool)) (BOUND_VARIABLE_318 Int)) (! (not (and (not (and (= (ite (and (not (= BOUND_VARIABLE_318 0)) (BOUND_VARIABLE_314 (BOUND_VARIABLE_315 (ite (not (BOUND_VARIABLE_314 0)) 0 (ite BOUND_VARIABLE_313 0 (ite (and (not (or (and BOUND_VARIABLE_313 BOUND_VARIABLE_313) BOUND_VARIABLE_313)) (BOUND_VARIABLE_314 0)) 0 (ite (and (not (or (and BOUND_VARIABLE_313 BOUND_VARIABLE_313) BOUND_VARIABLE_313)) (or (not BOUND_VARIABLE_313) BOUND_VARIABLE_313)) 0 (ite (not (or (and BOUND_VARIABLE_313 BOUND_VARIABLE_313) BOUND_VARIABLE_313)) 0 9)))))))) (ite (BOUND_VARIABLE_317 (BOUND_VARIABLE_315 (ite (not (BOUND_VARIABLE_314 0)) 0 (ite BOUND_VARIABLE_313 0 (ite (and (not (or (and BOUND_VARIABLE_313 BOUND_VARIABLE_313) BOUND_VARIABLE_313)) (BOUND_VARIABLE_314 0)) 0 (ite (and (not (or (and BOUND_VARIABLE_313 BOUND_VARIABLE_313) BOUND_VARIABLE_313)) (or (not BOUND_VARIABLE_313) BOUND_VARIABLE_313)) 0 (ite (not (or (and BOUND_VARIABLE_313 BOUND_VARIABLE_313) BOUND_VARIABLE_313)) 0 9))))))) BOUND_VARIABLE_316 0) 0) 0) (not (BOUND_VARIABLE_314 (BOUND_VARIABLE_315 (ite (not (BOUND_VARIABLE_314 0)) 0 (ite BOUND_VARIABLE_313 0 (ite (and (not (or (and BOUND_VARIABLE_313 BOUND_VARIABLE_313) BOUND_VARIABLE_313)) (BOUND_VARIABLE_314 0)) 0 (ite (and (not (or (and BOUND_VARIABLE_313 BOUND_VARIABLE_313) BOUND_VARIABLE_313)) (or (not BOUND_VARIABLE_313) BOUND_VARIABLE_313)) 0 (ite (not (or (and BOUND_VARIABLE_313 BOUND_VARIABLE_313) BOUND_VARIABLE_313)) 0 9)))))))))) true)) :pattern (true))) -- 2.30.2