diff options
51 files changed, 613 insertions, 454 deletions
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 12e3f24b3..654ccb40c 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -726,6 +726,8 @@ libcvc4_add_sources( theory/quantifiers/quant_split.h theory/quantifiers/quant_util.cpp theory/quantifiers/quant_util.h + theory/quantifiers/quant_module.cpp + theory/quantifiers/quant_module.h theory/quantifiers/quantifiers_attributes.cpp theory/quantifiers/quantifiers_attributes.h theory/quantifiers/quantifiers_inference_manager.cpp diff --git a/src/preprocessing/passes/quantifier_macros.cpp b/src/preprocessing/passes/quantifier_macros.cpp index 69b665854..eef0326b6 100644 --- a/src/preprocessing/passes/quantifier_macros.cpp +++ b/src/preprocessing/passes/quantifier_macros.cpp @@ -24,8 +24,8 @@ #include "smt/smt_engine_scope.h" #include "theory/arith/arith_msum.h" #include "theory/quantifiers/ematching/pattern_term_selector.h" +#include "theory/quantifiers/quantifiers_registry.h" #include "theory/quantifiers/term_database.h" -#include "theory/quantifiers/term_util.h" #include "theory/quantifiers_engine.h" #include "theory/rewriter.h" @@ -196,8 +196,8 @@ bool QuantifierMacros::isGroundUfTerm(Node q, Node n) { Node icn = d_preprocContext->getTheoryEngine() ->getQuantifiersEngine() - ->getTermUtil() - ->substituteBoundVariablesToInstConstants(n, q); + ->getQuantifiersRegistry() + .substituteBoundVariablesToInstConstants(n, q); Trace("macros-debug2") << "Get free variables in " << icn << std::endl; std::vector< Node > var; quantifiers::TermUtil::computeInstConstContainsForQuant(q, icn, var); diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp index c37054fdd..e4881b112 100644 --- a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp +++ b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp @@ -103,7 +103,7 @@ bool InstStrategyCegqi::registerCbqiLemma(Node q) //add cbqi lemma //get the counterexample literal Node ceLit = getCounterexampleLiteral(q); - Node ceBody = d_quantEngine->getTermUtil()->getInstConstantBody( q ); + Node ceBody = d_qreg.getInstConstantBody(q); if( !ceBody.isNull() ){ //add counterexample lemma Node lem = NodeManager::currentNM()->mkNode( OR, ceLit.negate(), ceBody.negate() ); @@ -369,19 +369,18 @@ void InstStrategyCegqi::registerCounterexampleLemma(Node q, Node lem) // must register with the instantiator // must explicitly remove ITEs so that we record dependencies std::vector<Node> ce_vars; - TermUtil* tutil = d_quantEngine->getTermUtil(); - for (unsigned i = 0, nics = tutil->getNumInstantiationConstants(q); i < nics; + for (size_t i = 0, nics = d_qreg.getNumInstantiationConstants(q); i < nics; i++) { - ce_vars.push_back(tutil->getInstantiationConstant(q, i)); + ce_vars.push_back(d_qreg.getInstantiationConstant(q, i)); } // send the lemma - d_quantEngine->getOutputChannel().lemma(lem); + d_qim.lemma(lem, InferenceId::UNKNOWN); // get the preprocessed form of the lemma we just sent std::vector<Node> skolems; std::vector<Node> skAsserts; - Node ppLem = d_quantEngine->getValuation().getPreprocessedTerm( - lem, skAsserts, skolems); + Node ppLem = + d_qstate.getValuation().getPreprocessedTerm(lem, skAsserts, skolems); std::vector<Node> lemp{ppLem}; lemp.insert(lemp.end(), skAsserts.begin(), skAsserts.end()); ppLem = NodeManager::currentNM()->mkAnd(lemp); diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h index 7d39efc6b..18c71e77e 100644 --- a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h +++ b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h @@ -24,7 +24,7 @@ #include "theory/quantifiers/cegqi/nested_qe.h" #include "theory/quantifiers/cegqi/vts_term_cache.h" #include "theory/quantifiers/instantiate.h" -#include "theory/quantifiers/quant_util.h" +#include "theory/quantifiers/quant_module.h" #include "util/statistics_registry.h" namespace CVC4 { diff --git a/src/theory/quantifiers/conjecture_generator.h b/src/theory/quantifiers/conjecture_generator.h index 644461da2..9a9492d00 100644 --- a/src/theory/quantifiers/conjecture_generator.h +++ b/src/theory/quantifiers/conjecture_generator.h @@ -20,7 +20,7 @@ #include "context/cdhashmap.h" #include "expr/node_trie.h" #include "expr/term_canonize.h" -#include "theory/quantifiers/quant_util.h" +#include "theory/quantifiers/quant_module.h" #include "theory/type_enumerator.h" namespace CVC4 { diff --git a/src/theory/quantifiers/ematching/ho_trigger.cpp b/src/theory/quantifiers/ematching/ho_trigger.cpp index 0ab2988d2..4c606a273 100644 --- a/src/theory/quantifiers/ematching/ho_trigger.cpp +++ b/src/theory/quantifiers/ematching/ho_trigger.cpp @@ -17,7 +17,6 @@ #include "theory/quantifiers/ematching/ho_trigger.h" #include "theory/quantifiers/instantiate.h" #include "theory/quantifiers/term_database.h" -#include "theory/quantifiers/term_util.h" #include "theory/quantifiers_engine.h" #include "theory/uf/theory_uf_rewriter.h" #include "util/hash.h" @@ -31,10 +30,11 @@ namespace inst { HigherOrderTrigger::HigherOrderTrigger( QuantifiersEngine* qe, quantifiers::QuantifiersInferenceManager& qim, + quantifiers::QuantifiersRegistry& qr, Node q, std::vector<Node>& nodes, std::map<Node, std::vector<Node> >& ho_apps) - : Trigger(qe, qim, q, nodes), d_ho_var_apps(ho_apps) + : Trigger(qe, qim, qr, q, nodes), d_ho_var_apps(ho_apps) { NodeManager* nm = NodeManager::currentNM(); // process the higher-order variable applications @@ -201,11 +201,10 @@ bool HigherOrderTrigger::sendInstantiation(InstMatch& m) // get substitution corresponding to m std::vector<TNode> vars; std::vector<TNode> subs; - quantifiers::TermUtil* tutil = d_quantEngine->getTermUtil(); for (unsigned i = 0, size = d_quant[0].getNumChildren(); i < size; i++) { subs.push_back(m.d_vals[i]); - vars.push_back(tutil->getInstantiationConstant(d_quant, i)); + vars.push_back(d_qreg.getInstantiationConstant(d_quant, i)); } Trace("ho-unif-debug") << "Run higher-order unification..." << std::endl; diff --git a/src/theory/quantifiers/ematching/ho_trigger.h b/src/theory/quantifiers/ematching/ho_trigger.h index e424f69d1..af7020bfc 100644 --- a/src/theory/quantifiers/ematching/ho_trigger.h +++ b/src/theory/quantifiers/ematching/ho_trigger.h @@ -94,6 +94,7 @@ class HigherOrderTrigger : public Trigger private: HigherOrderTrigger(QuantifiersEngine* qe, quantifiers::QuantifiersInferenceManager& qim, + quantifiers::QuantifiersRegistry& qr, Node q, std::vector<Node>& nodes, std::map<Node, std::vector<Node> >& ho_apps); diff --git a/src/theory/quantifiers/ematching/inst_match_generator_multi.cpp b/src/theory/quantifiers/ematching/inst_match_generator_multi.cpp index a0114ba80..4f393bc4f 100644 --- a/src/theory/quantifiers/ematching/inst_match_generator_multi.cpp +++ b/src/theory/quantifiers/ematching/inst_match_generator_multi.cpp @@ -238,8 +238,6 @@ void InstMatchGeneratorMulti::processNewInstantiations(QuantifiersEngine* qe, if (trieIndex < iio->d_order.size()) { size_t curr_index = iio->d_order[trieIndex]; - // Node curr_ic = qe->getTermUtil()->getInstantiationConstant( d_quant, - // curr_index ); Node n = m.get(curr_index); if (n.isNull()) { diff --git a/src/theory/quantifiers/ematching/inst_strategy.cpp b/src/theory/quantifiers/ematching/inst_strategy.cpp index fc85703c0..fe771b4e7 100644 --- a/src/theory/quantifiers/ematching/inst_strategy.cpp +++ b/src/theory/quantifiers/ematching/inst_strategy.cpp @@ -22,8 +22,9 @@ namespace quantifiers { InstStrategy::InstStrategy(QuantifiersEngine* qe, QuantifiersState& qs, - QuantifiersInferenceManager& qim) - : d_quantEngine(qe), d_qstate(qs), d_qim(qim) + QuantifiersInferenceManager& qim, + QuantifiersRegistry& qr) + : d_quantEngine(qe), d_qstate(qs), d_qim(qim), d_qreg(qr) { } InstStrategy::~InstStrategy() {} diff --git a/src/theory/quantifiers/ematching/inst_strategy.h b/src/theory/quantifiers/ematching/inst_strategy.h index b9d0aa745..1455ce0c5 100644 --- a/src/theory/quantifiers/ematching/inst_strategy.h +++ b/src/theory/quantifiers/ematching/inst_strategy.h @@ -31,6 +31,7 @@ namespace quantifiers { class QuantifiersState; class QuantifiersInferenceManager; +class QuantifiersRegistry; /** A status response to process */ enum class InstStrategyStatus @@ -49,7 +50,8 @@ class InstStrategy public: InstStrategy(QuantifiersEngine* qe, QuantifiersState& qs, - QuantifiersInferenceManager& qim); + QuantifiersInferenceManager& qim, + QuantifiersRegistry& qr); virtual ~InstStrategy(); /** presolve */ virtual void presolve(); @@ -72,6 +74,8 @@ class InstStrategy QuantifiersState& d_qstate; /** The quantifiers inference manager object */ QuantifiersInferenceManager& d_qim; + /** The quantifiers registry */ + QuantifiersRegistry& d_qreg; }; /* class InstStrategy */ } // namespace quantifiers diff --git a/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp b/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp index 90d8de128..2a1e38c3c 100644 --- a/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp +++ b/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp @@ -62,8 +62,9 @@ InstStrategyAutoGenTriggers::InstStrategyAutoGenTriggers( QuantifiersEngine* qe, QuantifiersState& qs, QuantifiersInferenceManager& qim, - QuantRelevance* qr) - : InstStrategy(qe, qs, qim), d_quant_rel(qr) + QuantifiersRegistry& qr, + QuantRelevance* qrlv) + : InstStrategy(qe, qs, qim, qr), d_quant_rel(qrlv) { //how to select trigger terms d_tr_strategy = options::triggerSelMode(); @@ -283,6 +284,7 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f ){ { tr = Trigger::mkTrigger(d_quantEngine, d_qim, + d_qreg, f, patTerms[0], false, @@ -320,6 +322,7 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f ){ // will possibly want to get an old trigger tr = Trigger::mkTrigger(d_quantEngine, d_qim, + d_qreg, f, patTerms, false, @@ -362,6 +365,7 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f ){ d_single_trigger_gen[patTerms[index]] = true; Trigger* tr2 = Trigger::mkTrigger(d_quantEngine, d_qim, + d_qreg, f, patTerms[index], false, @@ -390,7 +394,6 @@ bool InstStrategyAutoGenTriggers::generatePatternTerms(Node f) bool ntrivTriggers = options::relationalTriggers(); std::vector<Node> patTermsF; std::map<Node, inst::TriggerTermInfo> tinfo; - TermUtil* tu = d_quantEngine->getTermUtil(); NodeManager* nm = NodeManager::currentNM(); // well-defined function: can assume LHS is only pattern if (options::quantFunWellDefined()) @@ -398,7 +401,7 @@ bool InstStrategyAutoGenTriggers::generatePatternTerms(Node f) Node hd = QuantAttributes::getFunDefHead(f); if (!hd.isNull()) { - hd = tu->substituteBoundVariablesToInstConstants(hd, f); + hd = d_qreg.substituteBoundVariablesToInstConstants(hd, f); patTermsF.push_back(hd); tinfo[hd].init(f, hd); } @@ -406,7 +409,7 @@ bool InstStrategyAutoGenTriggers::generatePatternTerms(Node f) // otherwise, use algorithm for collecting pattern terms if (patTermsF.empty()) { - Node bd = tu->getInstConstantBody(f); + Node bd = d_qreg.getInstConstantBody(f); PatternTermSelector pts(f, d_tr_strategy, d_user_no_gen[f], true); pts.collect(bd, patTermsF, tinfo); if (ntrivTriggers) @@ -486,7 +489,7 @@ bool InstStrategyAutoGenTriggers::generatePatternTerms(Node f) std::vector<Node> vcs[2]; for (size_t i = 0, nchild = f[0].getNumChildren(); i < nchild; i++) { - Node ic = tu->getInstantiationConstant(f, i); + Node ic = d_qreg.getInstantiationConstant(f, i); vcs[vcMap.find(ic) == vcMap.end() ? 0 : 1].push_back(f[0][i]); } for (size_t i = 0; i < 2; i++) @@ -621,8 +624,7 @@ void InstStrategyAutoGenTriggers::addTrigger( inst::Trigger * tr, Node q ) { NodeManager* nm = NodeManager::currentNM(); // partial trigger : generate implication to mark user pattern Node pat = - d_quantEngine->getTermUtil()->substituteInstConstantsToBoundVariables( - tr->getInstPattern(), q); + d_qreg.substituteInstConstantsToBoundVariables(tr->getInstPattern(), q); Node ipl = nm->mkNode(INST_PATTERN_LIST, pat); Node qq = nm->mkNode(FORALL, d_vc_partition[1][q], diff --git a/src/theory/quantifiers/ematching/inst_strategy_e_matching.h b/src/theory/quantifiers/ematching/inst_strategy_e_matching.h index 81b40f067..6170d3067 100644 --- a/src/theory/quantifiers/ematching/inst_strategy_e_matching.h +++ b/src/theory/quantifiers/ematching/inst_strategy_e_matching.h @@ -88,7 +88,8 @@ class InstStrategyAutoGenTriggers : public InstStrategy InstStrategyAutoGenTriggers(QuantifiersEngine* qe, QuantifiersState& qs, QuantifiersInferenceManager& qim, - QuantRelevance* qr); + QuantifiersRegistry& qr, + QuantRelevance* qrlv); ~InstStrategyAutoGenTriggers() {} /** get auto-generated trigger */ diff --git a/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.cpp b/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.cpp index cf6405b38..ca2f1bdc5 100644 --- a/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.cpp +++ b/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.cpp @@ -27,8 +27,9 @@ namespace quantifiers { InstStrategyUserPatterns::InstStrategyUserPatterns( QuantifiersEngine* ie, QuantifiersState& qs, - QuantifiersInferenceManager& qim) - : InstStrategy(ie, qs, qim) + QuantifiersInferenceManager& qim, + QuantifiersRegistry& qr) + : InstStrategy(ie, qs, qim, qr) { } InstStrategyUserPatterns::~InstStrategyUserPatterns() {} @@ -105,8 +106,13 @@ InstStrategyStatus InstStrategyUserPatterns::process(Node q, std::vector<std::vector<Node> >& ugw = d_user_gen_wait[q]; for (size_t i = 0, usize = ugw.size(); i < usize; i++) { - Trigger* t = Trigger::mkTrigger( - d_quantEngine, d_qim, q, ugw[i], true, Trigger::TR_RETURN_NULL); + Trigger* t = Trigger::mkTrigger(d_quantEngine, + d_qim, + d_qreg, + q, + ugw[i], + true, + Trigger::TR_RETURN_NULL); if (t) { d_user_gen[q].push_back(t); @@ -165,7 +171,7 @@ void InstStrategyUserPatterns::addUserPattern(Node q, Node pat) return; } Trigger* t = Trigger::mkTrigger( - d_quantEngine, d_qim, q, nodes, true, Trigger::TR_MAKE_NEW); + d_quantEngine, d_qim, d_qreg, q, nodes, true, Trigger::TR_MAKE_NEW); if (t) { d_user_gen[q].push_back(t); diff --git a/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.h b/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.h index 996adc444..1cad77fef 100644 --- a/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.h +++ b/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.h @@ -36,7 +36,8 @@ class InstStrategyUserPatterns : public InstStrategy public: InstStrategyUserPatterns(QuantifiersEngine* qe, QuantifiersState& qs, - QuantifiersInferenceManager& qim); + QuantifiersInferenceManager& qim, + QuantifiersRegistry& qr); ~InstStrategyUserPatterns(); /** add pattern */ void addUserPattern(Node q, Node pat); diff --git a/src/theory/quantifiers/ematching/instantiation_engine.cpp b/src/theory/quantifiers/ematching/instantiation_engine.cpp index 50d91a1e1..3e344f7fb 100644 --- a/src/theory/quantifiers/ematching/instantiation_engine.cpp +++ b/src/theory/quantifiers/ematching/instantiation_engine.cpp @@ -53,13 +53,13 @@ InstantiationEngine::InstantiationEngine(QuantifiersEngine* qe, // user-provided patterns if (options::userPatternsQuant() != options::UserPatMode::IGNORE) { - d_isup.reset(new InstStrategyUserPatterns(d_quantEngine, qs, qim)); + d_isup.reset(new InstStrategyUserPatterns(d_quantEngine, qs, qim, qr)); d_instStrategies.push_back(d_isup.get()); } // auto-generated patterns d_i_ag.reset(new InstStrategyAutoGenTriggers( - d_quantEngine, qs, qim, d_quant_rel.get())); + d_quantEngine, qs, qim, qr, d_quant_rel.get())); d_instStrategies.push_back(d_i_ag.get()); } } @@ -228,9 +228,7 @@ void InstantiationEngine::registerQuantifier(Node q) // take into account user patterns if (q.getNumChildren() == 3) { - Node subsPat = - d_quantEngine->getTermUtil()->substituteBoundVariablesToInstConstants( - q[2], q); + Node subsPat = d_qreg.substituteBoundVariablesToInstConstants(q[2], q); // add patterns for (const Node& p : subsPat) { diff --git a/src/theory/quantifiers/ematching/instantiation_engine.h b/src/theory/quantifiers/ematching/instantiation_engine.h index 016784152..e27277933 100644 --- a/src/theory/quantifiers/ematching/instantiation_engine.h +++ b/src/theory/quantifiers/ematching/instantiation_engine.h @@ -20,8 +20,8 @@ #include <vector> #include "theory/quantifiers/ematching/inst_strategy.h" +#include "theory/quantifiers/quant_module.h" #include "theory/quantifiers/quant_relevance.h" -#include "theory/quantifiers/quant_util.h" namespace CVC4 { namespace theory { diff --git a/src/theory/quantifiers/ematching/trigger.cpp b/src/theory/quantifiers/ematching/trigger.cpp index 3bc5ded16..ac43d3bc9 100644 --- a/src/theory/quantifiers/ematching/trigger.cpp +++ b/src/theory/quantifiers/ematching/trigger.cpp @@ -36,9 +36,10 @@ namespace inst { /** trigger class constructor */ Trigger::Trigger(QuantifiersEngine* qe, quantifiers::QuantifiersInferenceManager& qim, + quantifiers::QuantifiersRegistry& qr, Node q, std::vector<Node>& nodes) - : d_quantEngine(qe), d_qim(qim), d_quant(q) + : d_quantEngine(qe), d_qim(qim), d_qreg(qr), d_quant(q) { // We must ensure that the ground subterms of the trigger have been // preprocessed. @@ -233,6 +234,7 @@ bool Trigger::mkTriggerTerms(Node q, Trigger* Trigger::mkTrigger(QuantifiersEngine* qe, quantifiers::QuantifiersInferenceManager& qim, + quantifiers::QuantifiersRegistry& qr, Node f, std::vector<Node>& nodes, bool keepAll, @@ -273,11 +275,11 @@ Trigger* Trigger::mkTrigger(QuantifiersEngine* qe, Trigger* t; if (!ho_apps.empty()) { - t = new HigherOrderTrigger(qe, qim, f, trNodes, ho_apps); + t = new HigherOrderTrigger(qe, qim, qr, f, trNodes, ho_apps); } else { - t = new Trigger(qe, qim, f, trNodes); + t = new Trigger(qe, qim, qr, f, trNodes); } qe->getTriggerDatabase()->addTrigger( trNodes, t ); @@ -286,6 +288,7 @@ Trigger* Trigger::mkTrigger(QuantifiersEngine* qe, Trigger* Trigger::mkTrigger(QuantifiersEngine* qe, quantifiers::QuantifiersInferenceManager& qim, + quantifiers::QuantifiersRegistry& qr, Node f, Node n, bool keepAll, @@ -294,7 +297,7 @@ Trigger* Trigger::mkTrigger(QuantifiersEngine* qe, { std::vector< Node > nodes; nodes.push_back( n ); - return mkTrigger(qe, qim, f, nodes, keepAll, trOption, useNVars); + return mkTrigger(qe, qim, qr, f, nodes, keepAll, trOption, useNVars); } int Trigger::getActiveScore() { diff --git a/src/theory/quantifiers/ematching/trigger.h b/src/theory/quantifiers/ematching/trigger.h index e2ce61bd1..21888ff8f 100644 --- a/src/theory/quantifiers/ematching/trigger.h +++ b/src/theory/quantifiers/ematching/trigger.h @@ -31,6 +31,7 @@ class QuantifiersEngine; namespace quantifiers { class QuantifiersInferenceManager; +class QuantifiersRegistry; } namespace inst { @@ -163,6 +164,7 @@ class Trigger { }; static Trigger* mkTrigger(QuantifiersEngine* qe, quantifiers::QuantifiersInferenceManager& qim, + quantifiers::QuantifiersRegistry& qr, Node q, std::vector<Node>& nodes, bool keepAll = true, @@ -171,6 +173,7 @@ class Trigger { /** single trigger version that calls the above function */ static Trigger* mkTrigger(QuantifiersEngine* qe, quantifiers::QuantifiersInferenceManager& qim, + quantifiers::QuantifiersRegistry& qr, Node q, Node n, bool keepAll = true, @@ -194,6 +197,7 @@ class Trigger { /** trigger constructor, intentionally protected (use Trigger::mkTrigger). */ Trigger(QuantifiersEngine* ie, quantifiers::QuantifiersInferenceManager& qim, + quantifiers::QuantifiersRegistry& qr, Node q, std::vector<Node>& nodes); /** add an instantiation (called by InstMatchGenerator) @@ -243,6 +247,8 @@ class Trigger { QuantifiersEngine* d_quantEngine; /** Reference to the quantifiers inference manager */ quantifiers::QuantifiersInferenceManager& d_qim; + /** The quantifiers registry */ + quantifiers::QuantifiersRegistry& d_qreg; /** The quantified formula this trigger is for. */ Node d_quant; /** match generator diff --git a/src/theory/quantifiers/extended_rewrite.cpp b/src/theory/quantifiers/extended_rewrite.cpp index 37a3396e2..7b5bd92b8 100644 --- a/src/theory/quantifiers/extended_rewrite.cpp +++ b/src/theory/quantifiers/extended_rewrite.cpp @@ -20,6 +20,7 @@ #include "theory/quantifiers/term_util.h" #include "theory/rewriter.h" #include "theory/strings/sequences_rewriter.h" +#include "theory/theory.h" using namespace CVC4::kind; using namespace std; diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp index db977c53d..593ec98f9 100644 --- a/src/theory/quantifiers/first_order_model.cpp +++ b/src/theory/quantifiers/first_order_model.cpp @@ -35,9 +35,11 @@ namespace quantifiers { FirstOrderModel::FirstOrderModel(QuantifiersEngine* qe, QuantifiersState& qs, + QuantifiersRegistry& qr, std::string name) : TheoryModel(qs.getSatContext(), name, true), d_qe(qe), + d_qreg(qr), d_forall_asserts(qs.getSatContext()), d_forallRlvComputed(false) { @@ -301,8 +303,7 @@ Node FirstOrderModel::getModelBasis(Node q, Node n) d_model_basis_terms[q].push_back(getModelBasisTerm(q[0][j].getType())); } } - Node gn = d_qe->getTermUtil()->substituteInstConstants( - n, q, d_model_basis_terms[q]); + Node gn = d_qreg.substituteInstConstants(n, q, d_model_basis_terms[q]); return gn; } @@ -337,8 +338,9 @@ unsigned FirstOrderModel::getModelBasisArg(Node n) FirstOrderModelFmc::FirstOrderModelFmc(QuantifiersEngine* qe, QuantifiersState& qs, + QuantifiersRegistry& qr, std::string name) - : FirstOrderModel(qe, qs, name) + : FirstOrderModel(qe, qs, qr, name) { } diff --git a/src/theory/quantifiers/first_order_model.h b/src/theory/quantifiers/first_order_model.h index e4236a95d..ebc68ca53 100644 --- a/src/theory/quantifiers/first_order_model.h +++ b/src/theory/quantifiers/first_order_model.h @@ -19,7 +19,6 @@ #include "context/cdlist.h" #include "expr/attribute.h" -#include "theory/quantifiers/quantifiers_state.h" #include "theory/theory_model.h" #include "theory/uf/theory_uf_model.h" @@ -43,6 +42,8 @@ typedef expr::Attribute<ModelBasisArgAttributeId, uint64_t> namespace quantifiers { class TermDb; +class QuantifiersState; +class QuantifiersRegistry; namespace fmcheck { class FirstOrderModelFmc; @@ -57,6 +58,7 @@ class FirstOrderModel : public TheoryModel public: FirstOrderModel(QuantifiersEngine* qe, QuantifiersState& qs, + QuantifiersRegistry& qr, std::string name); virtual fmcheck::FirstOrderModelFmc* asFirstOrderModelFmc() { return nullptr; } @@ -134,6 +136,8 @@ class FirstOrderModel : public TheoryModel protected: /** quant engine */ QuantifiersEngine* d_qe; + /** The quantifiers registry */ + QuantifiersRegistry& d_qreg; /** list of quantifiers asserted in the current context */ context::CDList<Node> d_forall_asserts; /** @@ -203,6 +207,7 @@ class FirstOrderModelFmc : public FirstOrderModel public: FirstOrderModelFmc(QuantifiersEngine* qe, QuantifiersState& qs, + QuantifiersRegistry& qr, std::string name); ~FirstOrderModelFmc() override; FirstOrderModelFmc* asFirstOrderModelFmc() override { return this; } diff --git a/src/theory/quantifiers/fmf/bounded_integers.cpp b/src/theory/quantifiers/fmf/bounded_integers.cpp index 5a0407f1f..3ade304e8 100644 --- a/src/theory/quantifiers/fmf/bounded_integers.cpp +++ b/src/theory/quantifiers/fmf/bounded_integers.cpp @@ -546,7 +546,7 @@ void BoundedIntegers::getBoundVarIndices(Node q, { for (const Node& v : it->second) { - indices.push_back(d_quantEngine->getTermUtil()->getVariableNum(q, v)); + indices.push_back(TermUtil::getVariableNum(q, v)); } } } diff --git a/src/theory/quantifiers/fmf/bounded_integers.h b/src/theory/quantifiers/fmf/bounded_integers.h index 74ff8a19b..dce515d0d 100644 --- a/src/theory/quantifiers/fmf/bounded_integers.h +++ b/src/theory/quantifiers/fmf/bounded_integers.h @@ -18,7 +18,7 @@ #ifndef CVC4__BOUNDED_INTEGERS_H #define CVC4__BOUNDED_INTEGERS_H -#include "theory/quantifiers/quant_util.h" +#include "theory/quantifiers/quant_module.h" #include "context/cdhashmap.h" #include "context/context.h" diff --git a/src/theory/quantifiers/fmf/model_engine.cpp b/src/theory/quantifiers/fmf/model_engine.cpp index 428c435df..1c0a74013 100644 --- a/src/theory/quantifiers/fmf/model_engine.cpp +++ b/src/theory/quantifiers/fmf/model_engine.cpp @@ -21,7 +21,6 @@ #include "theory/quantifiers/quant_rep_bound_ext.h" #include "theory/quantifiers/quantifiers_attributes.h" #include "theory/quantifiers/term_database.h" -#include "theory/quantifiers/term_util.h" #include "theory/quantifiers_engine.h" using namespace std; @@ -268,7 +267,8 @@ void ModelEngine::exhaustiveInstantiate( Node f, int effort ){ if( Trace.isOn("fmf-exh-inst-debug") ){ Trace("fmf-exh-inst-debug") << " Instantiation Constants: "; for( size_t i=0; i<f[0].getNumChildren(); i++ ){ - Trace("fmf-exh-inst-debug") << d_quantEngine->getTermUtil()->getInstantiationConstant( f, i ) << " "; + Trace("fmf-exh-inst-debug") + << d_qreg.getInstantiationConstant(f, i) << " "; } Trace("fmf-exh-inst-debug") << std::endl; } diff --git a/src/theory/quantifiers/fmf/model_engine.h b/src/theory/quantifiers/fmf/model_engine.h index 1cb780dd0..b3006cad1 100644 --- a/src/theory/quantifiers/fmf/model_engine.h +++ b/src/theory/quantifiers/fmf/model_engine.h @@ -18,7 +18,7 @@ #define CVC4__THEORY__QUANTIFIERS__MODEL_ENGINE_H #include "theory/quantifiers/fmf/model_builder.h" -#include "theory/quantifiers/quant_util.h" +#include "theory/quantifiers/quant_module.h" #include "theory/theory_model.h" namespace CVC4 { diff --git a/src/theory/quantifiers/inst_match.cpp b/src/theory/quantifiers/inst_match.cpp index 5d6779406..96e8a40be 100644 --- a/src/theory/quantifiers/inst_match.cpp +++ b/src/theory/quantifiers/inst_match.cpp @@ -15,7 +15,6 @@ #include "theory/quantifiers/inst_match.h" #include "theory/quantifiers/instantiate.h" -#include "theory/quantifiers/quant_util.h" #include "theory/quantifiers/term_database.h" #include "theory/quantifiers_engine.h" diff --git a/src/theory/quantifiers/inst_strategy_enumerative.h b/src/theory/quantifiers/inst_strategy_enumerative.h index 35c43d740..1c606998a 100644 --- a/src/theory/quantifiers/inst_strategy_enumerative.h +++ b/src/theory/quantifiers/inst_strategy_enumerative.h @@ -19,7 +19,7 @@ #include "context/context.h" #include "context/context_mm.h" -#include "theory/quantifiers/quant_util.h" +#include "theory/quantifiers/quant_module.h" #include "theory/quantifiers/relevant_domain.h" namespace CVC4 { diff --git a/src/theory/quantifiers/instantiate.cpp b/src/theory/quantifiers/instantiate.cpp index b4fed5b13..729dd6100 100644 --- a/src/theory/quantifiers/instantiate.cpp +++ b/src/theory/quantifiers/instantiate.cpp @@ -39,13 +39,14 @@ namespace quantifiers { Instantiate::Instantiate(QuantifiersEngine* qe, QuantifiersState& qs, QuantifiersInferenceManager& qim, + QuantifiersRegistry& qr, ProofNodeManager* pnm) : d_qe(qe), d_qstate(qs), d_qim(qim), + d_qreg(qr), d_pnm(pnm), d_term_db(nullptr), - d_term_util(nullptr), d_total_inst_debug(qs.getUserContext()), d_c_inst_match_trie_dom(qs.getUserContext()), d_pfInst(pnm ? new CDProof(pnm) : nullptr) @@ -75,7 +76,6 @@ bool Instantiate::reset(Theory::Effort e) d_recorded_inst.clear(); } d_term_db = d_qe->getTermDatabase(); - d_term_util = d_qe->getTermUtil(); return true; } @@ -111,7 +111,6 @@ bool Instantiate::addInstantiation( Assert(!d_qstate.isInConflict()); Assert(terms.size() == q[0].getNumChildren()); Assert(d_term_db != nullptr); - Assert(d_term_util != nullptr); Trace("inst-add-debug") << "For quantified formula " << q << ", add instantiation: " << std::endl; for (unsigned i = 0, size = terms.size(); i < size; i++) @@ -167,7 +166,7 @@ bool Instantiate::addInstantiation( << terms[i] << std::endl; bad_inst = true; } - else if (expr::hasSubterm(terms[i], d_term_util->d_inst_constants[q])) + else if (expr::hasSubterm(terms[i], d_qreg.d_inst_constants[q])) { Trace("inst") << "***& inst contains inst constants : " << terms[i] << std::endl; @@ -250,10 +249,9 @@ bool Instantiate::addInstantiation( // construct the instantiation Trace("inst-add-debug") << "Constructing instantiation..." << std::endl; - Assert(d_term_util->d_vars[q].size() == terms.size()); + Assert(d_qreg.d_vars[q].size() == terms.size()); // get the instantiation - Node body = - getInstantiation(q, d_term_util->d_vars[q], terms, doVts, pfTmp.get()); + Node body = getInstantiation(q, d_qreg.d_vars[q], terms, doVts, pfTmp.get()); Node orig_body = body; // now preprocess, storing the trust node for the rewrite TrustNode tpBody = quantifiers::QuantifiersRewriter::preprocess(body, true); @@ -466,15 +464,15 @@ Node Instantiate::getInstantiation(Node q, Node Instantiate::getInstantiation(Node q, InstMatch& m, bool doVts) { - Assert(d_term_util->d_vars.find(q) != d_term_util->d_vars.end()); + Assert(d_qreg.d_vars.find(q) != d_qreg.d_vars.end()); Assert(m.d_vals.size() == q[0].getNumChildren()); - return getInstantiation(q, d_term_util->d_vars[q], m.d_vals, doVts); + return getInstantiation(q, d_qreg.d_vars[q], m.d_vals, doVts); } Node Instantiate::getInstantiation(Node q, std::vector<Node>& terms, bool doVts) { - Assert(d_term_util->d_vars.find(q) != d_term_util->d_vars.end()); - return getInstantiation(q, d_term_util->d_vars[q], terms, doVts); + Assert(d_qreg.d_vars.find(q) != d_qreg.d_vars.end()); + return getInstantiation(q, d_qreg.d_vars[q], terms, doVts); } bool Instantiate::recordInstantiationInternal(Node q, diff --git a/src/theory/quantifiers/instantiate.h b/src/theory/quantifiers/instantiate.h index aad1762c5..4188311ec 100644 --- a/src/theory/quantifiers/instantiate.h +++ b/src/theory/quantifiers/instantiate.h @@ -33,7 +33,9 @@ class QuantifiersEngine; namespace quantifiers { class TermDb; -class TermUtil; +class QuantifiersState; +class QuantifiersInferenceManager; +class QuantifiersRegistry; /** Instantiation rewriter * @@ -91,6 +93,7 @@ class Instantiate : public QuantifiersUtil Instantiate(QuantifiersEngine* qe, QuantifiersState& qs, QuantifiersInferenceManager& qim, + QuantifiersRegistry& qr, ProofNodeManager* pnm = nullptr); ~Instantiate(); @@ -293,12 +296,12 @@ class Instantiate : public QuantifiersUtil QuantifiersState& d_qstate; /** Reference to the quantifiers inference manager */ QuantifiersInferenceManager& d_qim; + /** The quantifiers registry */ + QuantifiersRegistry& d_qreg; /** pointer to the proof node manager */ ProofNodeManager* d_pnm; /** cache of term database for quantifiers engine */ TermDb* d_term_db; - /** cache of term util for quantifiers engine */ - TermUtil* d_term_util; /** instantiation rewriter classes */ std::vector<InstantiationRewriter*> d_instRewrite; diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp index 0829ccd9c..f89f9f0ea 100644 --- a/src/theory/quantifiers/quant_conflict_find.cpp +++ b/src/theory/quantifiers/quant_conflict_find.cpp @@ -628,8 +628,8 @@ bool QuantInfo::isTConstraintSpurious(QuantConflictFind* p, //check constraints for( std::map< Node, bool >::iterator it = d_tconstraints.begin(); it != d_tconstraints.end(); ++it ){ //apply substitution to the tconstraint - Node cons = - p->getTermUtil()->substituteBoundVariables(it->first, d_q, terms); + Node cons = p->getQuantifiersRegistry().substituteBoundVariables( + it->first, d_q, terms); cons = it->second ? cons : cons.negate(); if (!entailmentTest(p, cons, p->atConflictEffort())) { return true; diff --git a/src/theory/quantifiers/quant_conflict_find.h b/src/theory/quantifiers/quant_conflict_find.h index 086d492f4..aea03984c 100644 --- a/src/theory/quantifiers/quant_conflict_find.h +++ b/src/theory/quantifiers/quant_conflict_find.h @@ -23,7 +23,7 @@ #include "context/cdhashmap.h" #include "context/cdlist.h" #include "expr/node_trie.h" -#include "theory/quantifiers/quant_util.h" +#include "theory/quantifiers/quant_module.h" namespace CVC4 { namespace theory { diff --git a/src/theory/quantifiers/quant_module.cpp b/src/theory/quantifiers/quant_module.cpp new file mode 100644 index 000000000..1d2da7e79 --- /dev/null +++ b/src/theory/quantifiers/quant_module.cpp @@ -0,0 +1,92 @@ +/********************* */ +/*! \file quant_module.cpp + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds, Morgan Deters + ** 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 Implementation of quantifier module + **/ + +#include "theory/quantifiers/quant_module.h" +#include "theory/quantifiers/inst_match.h" +#include "theory/quantifiers/term_database.h" +#include "theory/quantifiers/term_util.h" +#include "theory/quantifiers_engine.h" + +using namespace CVC4::kind; + +namespace CVC4 { +namespace theory { + +QuantifiersModule::QuantifiersModule( + quantifiers::QuantifiersState& qs, + quantifiers::QuantifiersInferenceManager& qim, + quantifiers::QuantifiersRegistry& qr, + QuantifiersEngine* qe) + : d_quantEngine(qe), d_qstate(qs), d_qim(qim), d_qreg(qr) +{ +} + +QuantifiersModule::QEffort QuantifiersModule::needsModel(Theory::Effort e) +{ + return QEFFORT_NONE; +} + +eq::EqualityEngine* QuantifiersModule::getEqualityEngine() const +{ + return d_qstate.getEqualityEngine(); +} + +bool QuantifiersModule::areEqual(TNode n1, TNode n2) const +{ + return d_qstate.areEqual(n1, n2); +} + +bool QuantifiersModule::areDisequal(TNode n1, TNode n2) const +{ + return d_qstate.areDisequal(n1, n2); +} + +TNode QuantifiersModule::getRepresentative(TNode n) const +{ + return d_qstate.getRepresentative(n); +} + +QuantifiersEngine* QuantifiersModule::getQuantifiersEngine() const +{ + return d_quantEngine; +} + +quantifiers::TermDb* QuantifiersModule::getTermDatabase() const +{ + return d_quantEngine->getTermDatabase(); +} + +quantifiers::TermUtil* QuantifiersModule::getTermUtil() const +{ + return d_quantEngine->getTermUtil(); +} + +quantifiers::QuantifiersState& QuantifiersModule::getState() +{ + return d_qstate; +} + +quantifiers::QuantifiersInferenceManager& +QuantifiersModule::getInferenceManager() +{ + return d_qim; +} + +quantifiers::QuantifiersRegistry& QuantifiersModule::getQuantifiersRegistry() +{ + return d_qreg; +} + +} // namespace theory +} /* namespace CVC4 */ diff --git a/src/theory/quantifiers/quant_module.h b/src/theory/quantifiers/quant_module.h new file mode 100644 index 000000000..4d0481484 --- /dev/null +++ b/src/theory/quantifiers/quant_module.h @@ -0,0 +1,186 @@ +/********************* */ +/*! \file quant_module.h + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds, Morgan Deters, Mathias Preiner + ** 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 quantifier module + **/ + +#include "cvc4_private.h" + +#ifndef CVC4__THEORY__QUANT_MODULE_H +#define CVC4__THEORY__QUANT_MODULE_H + +#include <iostream> +#include <map> +#include <vector> + +#include "theory/quantifiers/quantifiers_inference_manager.h" +#include "theory/quantifiers/quantifiers_registry.h" +#include "theory/quantifiers/quantifiers_state.h" +#include "theory/theory.h" +#include "theory/uf/equality_engine.h" + +namespace CVC4 { +namespace theory { + +class QuantifiersEngine; + +namespace quantifiers { +class TermDb; +class TermUtil; +} // namespace quantifiers + +/** QuantifiersModule class + * + * This is the virtual class for defining subsolvers of the quantifiers theory. + * It has a similar interface to a Theory object. + */ +class QuantifiersModule +{ + public: + /** effort levels for quantifiers modules check */ + enum QEffort + { + // conflict effort, for conflict-based instantiation + QEFFORT_CONFLICT, + // standard effort, for heuristic instantiation + QEFFORT_STANDARD, + // model effort, for model-based instantiation + QEFFORT_MODEL, + // last call effort, for last resort techniques + QEFFORT_LAST_CALL, + // none + QEFFORT_NONE, + }; + + public: + QuantifiersModule(quantifiers::QuantifiersState& qs, + quantifiers::QuantifiersInferenceManager& qim, + quantifiers::QuantifiersRegistry& qr, + QuantifiersEngine* qe); + virtual ~QuantifiersModule() {} + /** Presolve. + * + * Called at the beginning of check-sat call. + */ + virtual void presolve() {} + /** Needs check. + * + * Returns true if this module wishes a call to be made + * to check(e) during QuantifiersEngine::check(e). + */ + virtual bool needsCheck(Theory::Effort e) + { + return e >= Theory::EFFORT_LAST_CALL; + } + /** Needs model. + * + * Whether this module needs a model built during a + * call to QuantifiersEngine::check(e) + * It returns one of QEFFORT_* from quantifiers_engine.h, + * which specifies the quantifiers effort in which it requires the model to + * be built. + */ + virtual QEffort needsModel(Theory::Effort e); + /** Reset. + * + * Called at the beginning of QuantifiersEngine::check(e). + */ + virtual void reset_round(Theory::Effort e) {} + /** Check. + * + * Called during QuantifiersEngine::check(e) depending + * if needsCheck(e) returns true. + */ + virtual void check(Theory::Effort e, QEffort quant_e) = 0; + /** Check complete? + * + * Returns false if the module's reasoning was globally incomplete + * (e.g. "sat" must be replaced with "incomplete"). + * + * This is called just before the quantifiers engine will return + * with no lemmas added during a LAST_CALL effort check. + */ + virtual bool checkComplete() { return true; } + /** Check was complete for quantified formula q + * + * If for each quantified formula q, some module returns true for + * checkCompleteFor( q ), + * and no lemmas are added by the quantifiers theory, then we may answer + * "sat", unless + * we are incomplete for other reasons. + */ + virtual bool checkCompleteFor(Node q) { return false; } + /** Check ownership + * + * Called once for new quantified formulas that are registered by the + * quantifiers theory. The primary purpose of this function is to establish + * if this module is the owner of quantified formula q. + */ + virtual void checkOwnership(Node q) {} + /** Register quantifier + * + * Called once for new quantified formulas q that are pre-registered by the + * quantifiers theory, after internal ownership of quantified formulas is + * finalized. This does context-independent initialization of this module + * for quantified formula q. + */ + virtual void registerQuantifier(Node q) {} + /** Pre-register quantifier + * + * Called once for new quantified formulas that are + * pre-registered by the quantifiers theory, after + * internal ownership of quantified formulas is finalized. + */ + virtual void preRegisterQuantifier(Node q) {} + /** Assert node. + * + * Called when a quantified formula q is asserted to the quantifiers theory + */ + virtual void assertNode(Node q) {} + /** Identify this module (for debugging, dynamic configuration, etc..) */ + virtual std::string identify() const = 0; + //----------------------------general queries + /** get currently used the equality engine */ + eq::EqualityEngine* getEqualityEngine() const; + /** are n1 and n2 equal in the current used equality engine? */ + bool areEqual(TNode n1, TNode n2) const; + /** are n1 and n2 disequal in the current used equality engine? */ + bool areDisequal(TNode n1, TNode n2) const; + /** get the representative of n in the current used equality engine */ + TNode getRepresentative(TNode n) const; + /** get quantifiers engine that owns this module */ + QuantifiersEngine* getQuantifiersEngine() const; + /** get currently used term database */ + quantifiers::TermDb* getTermDatabase() const; + /** get currently used term utility object */ + quantifiers::TermUtil* getTermUtil() const; + /** get the quantifiers state */ + quantifiers::QuantifiersState& getState(); + /** get the quantifiers inference manager */ + quantifiers::QuantifiersInferenceManager& getInferenceManager(); + /** get the quantifiers registry */ + quantifiers::QuantifiersRegistry& getQuantifiersRegistry(); + //----------------------------end general queries + protected: + /** pointer to the quantifiers engine that owns this module */ + QuantifiersEngine* d_quantEngine; + /** The state of the quantifiers engine */ + quantifiers::QuantifiersState& d_qstate; + /** The quantifiers inference manager */ + quantifiers::QuantifiersInferenceManager& d_qim; + /** The quantifiers registry */ + quantifiers::QuantifiersRegistry& d_qreg; +}; /* class QuantifiersModule */ + +} // namespace theory +} // namespace CVC4 + +#endif /* CVC4__THEORY__QUANT_UTIL_H */ diff --git a/src/theory/quantifiers/quant_split.h b/src/theory/quantifiers/quant_split.h index 8fb9b4eb6..a51575f93 100644 --- a/src/theory/quantifiers/quant_split.h +++ b/src/theory/quantifiers/quant_split.h @@ -18,7 +18,7 @@ #define CVC4__THEORY__QUANT_SPLIT_H #include "context/cdo.h" -#include "theory/quantifiers/quant_util.h" +#include "theory/quantifiers/quant_module.h" namespace CVC4 { namespace theory { diff --git a/src/theory/quantifiers/quant_util.cpp b/src/theory/quantifiers/quant_util.cpp index db643d96b..7516ea529 100644 --- a/src/theory/quantifiers/quant_util.cpp +++ b/src/theory/quantifiers/quant_util.cpp @@ -13,76 +13,14 @@ **/ #include "theory/quantifiers/quant_util.h" -#include "theory/quantifiers/inst_match.h" -#include "theory/quantifiers/term_database.h" + #include "theory/quantifiers/term_util.h" -#include "theory/quantifiers_engine.h" using namespace CVC4::kind; namespace CVC4 { namespace theory { -QuantifiersModule::QuantifiersModule( - quantifiers::QuantifiersState& qs, - quantifiers::QuantifiersInferenceManager& qim, - quantifiers::QuantifiersRegistry& qr, - QuantifiersEngine* qe) - : d_quantEngine(qe), d_qstate(qs), d_qim(qim), d_qreg(qr) -{ -} - -QuantifiersModule::QEffort QuantifiersModule::needsModel(Theory::Effort e) -{ - return QEFFORT_NONE; -} - -eq::EqualityEngine* QuantifiersModule::getEqualityEngine() const -{ - return d_qstate.getEqualityEngine(); -} - -bool QuantifiersModule::areEqual(TNode n1, TNode n2) const -{ - return d_qstate.areEqual(n1, n2); -} - -bool QuantifiersModule::areDisequal(TNode n1, TNode n2) const -{ - return d_qstate.areDisequal(n1, n2); -} - -TNode QuantifiersModule::getRepresentative(TNode n) const -{ - return d_qstate.getRepresentative(n); -} - -QuantifiersEngine* QuantifiersModule::getQuantifiersEngine() const -{ - return d_quantEngine; -} - -quantifiers::TermDb* QuantifiersModule::getTermDatabase() const -{ - return d_quantEngine->getTermDatabase(); -} - -quantifiers::TermUtil* QuantifiersModule::getTermUtil() const -{ - return d_quantEngine->getTermUtil(); -} - -quantifiers::QuantifiersState& QuantifiersModule::getState() -{ - return d_qstate; -} - -quantifiers::QuantifiersInferenceManager& -QuantifiersModule::getInferenceManager() -{ - return d_qim; -} - QuantPhaseReq::QuantPhaseReq( Node n, bool computeEq ){ initialize( n, computeEq ); } diff --git a/src/theory/quantifiers/quant_util.h b/src/theory/quantifiers/quant_util.h index 551143e40..e0cb11712 100644 --- a/src/theory/quantifiers/quant_util.h +++ b/src/theory/quantifiers/quant_util.h @@ -21,165 +21,17 @@ #include <map> #include <vector> -#include "theory/quantifiers/quantifiers_inference_manager.h" -#include "theory/quantifiers/quantifiers_registry.h" -#include "theory/quantifiers/quantifiers_state.h" +#include "expr/node.h" #include "theory/theory.h" -#include "theory/uf/equality_engine.h" namespace CVC4 { namespace theory { -class QuantifiersEngine; - -namespace quantifiers { - class TermDb; - class TermUtil; -} - -/** QuantifiersModule class -* -* This is the virtual class for defining subsolvers of the quantifiers theory. -* It has a similar interface to a Theory object. -*/ -class QuantifiersModule { - public: - /** effort levels for quantifiers modules check */ - enum QEffort - { - // conflict effort, for conflict-based instantiation - QEFFORT_CONFLICT, - // standard effort, for heuristic instantiation - QEFFORT_STANDARD, - // model effort, for model-based instantiation - QEFFORT_MODEL, - // last call effort, for last resort techniques - QEFFORT_LAST_CALL, - // none - QEFFORT_NONE, - }; - - public: - QuantifiersModule(quantifiers::QuantifiersState& qs, - quantifiers::QuantifiersInferenceManager& qim, - quantifiers::QuantifiersRegistry& qr, - QuantifiersEngine* qe); - virtual ~QuantifiersModule(){} - /** Presolve. - * - * Called at the beginning of check-sat call. - */ - virtual void presolve() {} - /** Needs check. - * - * Returns true if this module wishes a call to be made - * to check(e) during QuantifiersEngine::check(e). - */ - virtual bool needsCheck( Theory::Effort e ) { return e>=Theory::EFFORT_LAST_CALL; } - /** Needs model. - * - * Whether this module needs a model built during a - * call to QuantifiersEngine::check(e) - * It returns one of QEFFORT_* from quantifiers_engine.h, - * which specifies the quantifiers effort in which it requires the model to - * be built. - */ - virtual QEffort needsModel(Theory::Effort e); - /** Reset. - * - * Called at the beginning of QuantifiersEngine::check(e). - */ - virtual void reset_round( Theory::Effort e ){} - /** Check. - * - * Called during QuantifiersEngine::check(e) depending - * if needsCheck(e) returns true. - */ - virtual void check(Theory::Effort e, QEffort quant_e) = 0; - /** Check complete? - * - * Returns false if the module's reasoning was globally incomplete - * (e.g. "sat" must be replaced with "incomplete"). - * - * This is called just before the quantifiers engine will return - * with no lemmas added during a LAST_CALL effort check. - */ - virtual bool checkComplete() { return true; } - /** Check was complete for quantified formula q - * - * If for each quantified formula q, some module returns true for - * checkCompleteFor( q ), - * and no lemmas are added by the quantifiers theory, then we may answer - * "sat", unless - * we are incomplete for other reasons. - */ - virtual bool checkCompleteFor( Node q ) { return false; } - /** Check ownership - * - * Called once for new quantified formulas that are registered by the - * quantifiers theory. The primary purpose of this function is to establish - * if this module is the owner of quantified formula q. - */ - virtual void checkOwnership(Node q) {} - /** Register quantifier - * - * Called once for new quantified formulas q that are pre-registered by the - * quantifiers theory, after internal ownership of quantified formulas is - * finalized. This does context-independent initialization of this module - * for quantified formula q. - */ - virtual void registerQuantifier(Node q) {} - /** Pre-register quantifier - * - * Called once for new quantified formulas that are - * pre-registered by the quantifiers theory, after - * internal ownership of quantified formulas is finalized. - */ - virtual void preRegisterQuantifier(Node q) {} - /** Assert node. - * - * Called when a quantified formula q is asserted to the quantifiers theory - */ - virtual void assertNode(Node q) {} - /** Identify this module (for debugging, dynamic configuration, etc..) */ - virtual std::string identify() const = 0; - //----------------------------general queries - /** get currently used the equality engine */ - eq::EqualityEngine* getEqualityEngine() const; - /** are n1 and n2 equal in the current used equality engine? */ - bool areEqual(TNode n1, TNode n2) const; - /** are n1 and n2 disequal in the current used equality engine? */ - bool areDisequal(TNode n1, TNode n2) const; - /** get the representative of n in the current used equality engine */ - TNode getRepresentative(TNode n) const; - /** get quantifiers engine that owns this module */ - QuantifiersEngine* getQuantifiersEngine() const; - /** get currently used term database */ - quantifiers::TermDb* getTermDatabase() const; - /** get currently used term utility object */ - quantifiers::TermUtil* getTermUtil() const; - /** get the quantifiers state */ - quantifiers::QuantifiersState& getState(); - /** get the quantifiers inference manager */ - quantifiers::QuantifiersInferenceManager& getInferenceManager(); - //----------------------------end general queries - protected: - /** pointer to the quantifiers engine that owns this module */ - QuantifiersEngine* d_quantEngine; - /** The state of the quantifiers engine */ - quantifiers::QuantifiersState& d_qstate; - /** The quantifiers inference manager */ - quantifiers::QuantifiersInferenceManager& d_qim; - /** The quantifiers registry */ - quantifiers::QuantifiersRegistry& d_qreg; -};/* class QuantifiersModule */ - /** Quantifiers utility -* -* This is a lightweight version of a quantifiers module that does not implement -* methods -* for checking satisfiability. -*/ + * + * This is a lightweight version of a quantifiers module that does not implement + * methods for checking satisfiability. + */ class QuantifiersUtil { public: QuantifiersUtil(){} diff --git a/src/theory/quantifiers/quantifiers_modules.cpp b/src/theory/quantifiers/quantifiers_modules.cpp index f1a05f401..74f553800 100644 --- a/src/theory/quantifiers/quantifiers_modules.cpp +++ b/src/theory/quantifiers/quantifiers_modules.cpp @@ -93,7 +93,7 @@ void QuantifiersModules::initialize(QuantifiersEngine* qe, // full saturation : instantiate from relevant domain, then arbitrary terms if (options::fullSaturateQuant() || options::fullSaturateInterleave()) { - d_rel_dom.reset(new RelevantDomain(qe)); + d_rel_dom.reset(new RelevantDomain(qe, qr)); d_fs.reset(new InstStrategyEnum(qe, qs, qim, qr, d_rel_dom.get())); modules.push_back(d_fs.get()); } diff --git a/src/theory/quantifiers/quantifiers_registry.cpp b/src/theory/quantifiers/quantifiers_registry.cpp index 1633382c8..e6d4c75fe 100644 --- a/src/theory/quantifiers/quantifiers_registry.cpp +++ b/src/theory/quantifiers/quantifiers_registry.cpp @@ -14,12 +14,45 @@ #include "theory/quantifiers/quantifiers_registry.h" -#include "theory/quantifiers/quant_util.h" +#include "theory/quantifiers/quant_module.h" +#include "theory/quantifiers/term_util.h" namespace CVC4 { namespace theory { namespace quantifiers { +void QuantifiersRegistry::registerQuantifier(Node q) +{ + if (d_inst_constants.find(q) != d_inst_constants.end()) + { + return; + } + NodeManager* nm = NodeManager::currentNM(); + Debug("quantifiers-engine") + << "Instantiation constants for " << q << " : " << std::endl; + for (size_t i = 0, nvars = q[0].getNumChildren(); i < nvars; i++) + { + d_vars[q].push_back(q[0][i]); + // make instantiation constants + Node ic = nm->mkInstConstant(q[0][i].getType()); + d_inst_constants_map[ic] = q; + d_inst_constants[q].push_back(ic); + Debug("quantifiers-engine") << " " << ic << std::endl; + // set the var number attribute + InstVarNumAttribute ivna; + ic.setAttribute(ivna, i); + InstConstantAttribute ica; + ic.setAttribute(ica, q); + } +} + +bool QuantifiersRegistry::reset(Theory::Effort e) { return true; } + +std::string QuantifiersRegistry::identify() const +{ + return "QuantifiersRegistry"; +} + QuantifiersModule* QuantifiersRegistry::getOwner(Node q) const { std::map<Node, QuantifiersModule*>::const_iterator it = d_owner.find(q); @@ -60,6 +93,82 @@ bool QuantifiersRegistry::hasOwnership(Node q, QuantifiersModule* m) const return mo == m || mo == nullptr; } +Node QuantifiersRegistry::getInstantiationConstant(Node q, size_t i) const +{ + std::map<Node, std::vector<Node> >::const_iterator it = + d_inst_constants.find(q); + if (it != d_inst_constants.end()) + { + return it->second[i]; + } + return Node::null(); +} + +size_t QuantifiersRegistry::getNumInstantiationConstants(Node q) const +{ + std::map<Node, std::vector<Node> >::const_iterator it = + d_inst_constants.find(q); + if (it != d_inst_constants.end()) + { + return it->second.size(); + } + return 0; +} + +Node QuantifiersRegistry::getInstConstantBody(Node q) +{ + std::map<Node, Node>::const_iterator it = d_inst_const_body.find(q); + if (it == d_inst_const_body.end()) + { + Node n = substituteBoundVariablesToInstConstants(q[1], q); + d_inst_const_body[q] = n; + return n; + } + return it->second; +} + +Node QuantifiersRegistry::substituteBoundVariablesToInstConstants(Node n, + Node q) +{ + registerQuantifier(q); + return n.substitute(d_vars[q].begin(), + d_vars[q].end(), + d_inst_constants[q].begin(), + d_inst_constants[q].end()); +} + +Node QuantifiersRegistry::substituteInstConstantsToBoundVariables(Node n, + Node q) +{ + registerQuantifier(q); + return n.substitute(d_inst_constants[q].begin(), + d_inst_constants[q].end(), + d_vars[q].begin(), + d_vars[q].end()); +} + +Node QuantifiersRegistry::substituteBoundVariables(Node n, + Node q, + std::vector<Node>& terms) +{ + registerQuantifier(q); + Assert(d_vars[q].size() == terms.size()); + return n.substitute( + d_vars[q].begin(), d_vars[q].end(), terms.begin(), terms.end()); +} + +Node QuantifiersRegistry::substituteInstConstants(Node n, + Node q, + std::vector<Node>& terms) +{ + registerQuantifier(q); + Assert(d_inst_constants[q].size() == terms.size()); + return n.substitute(d_inst_constants[q].begin(), + d_inst_constants[q].end(), + terms.begin(), + terms.end()); +} + } // namespace quantifiers } // namespace theory } // namespace CVC4 diff --git a/src/theory/quantifiers/quantifiers_registry.h b/src/theory/quantifiers/quantifiers_registry.h index 59db1dfe2..b89a2c01b 100644 --- a/src/theory/quantifiers/quantifiers_registry.h +++ b/src/theory/quantifiers/quantifiers_registry.h @@ -18,6 +18,7 @@ #define CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_REGISTRY_H #include "expr/node.h" +#include "theory/quantifiers/quant_util.h" namespace CVC4 { namespace theory { @@ -26,15 +27,29 @@ class QuantifiersModule; namespace quantifiers { +class Instantiate; + /** * The quantifiers registry, which manages basic information about which - * quantifiers modules have ownership of quantified formulas. + * quantifiers modules have ownership of quantified formulas, and manages + * the allocation of instantiation constants per quantified formula. */ -class QuantifiersRegistry +class QuantifiersRegistry : public QuantifiersUtil { + friend class Instantiate; + public: QuantifiersRegistry() {} ~QuantifiersRegistry() {} + /** + * Register quantifier, which allocates the instantiation constants for q. + */ + void registerQuantifier(Node q) override; + /** reset */ + bool reset(Theory::Effort e) override; + /** identify */ + std::string identify() const override; + //----------------------------- ownership /** get the owner of quantified formula q */ QuantifiersModule* getOwner(Node q) const; /** @@ -47,7 +62,28 @@ class QuantifiersRegistry * Return true if module q has no owner registered or if its registered owner is m. */ bool hasOwnership(Node q, QuantifiersModule* m) const; - + //----------------------------- end ownership + //----------------------------- instantiation constants + /** get the i^th instantiation constant of q */ + Node getInstantiationConstant(Node q, size_t i) const; + /** get number of instantiation constants for q */ + size_t getNumInstantiationConstants(Node q) const; + /** get the ce body q[e/x] */ + Node getInstConstantBody(Node q); + /** returns node n with bound vars of q replaced by instantiation constants of + q node n : is the future pattern node q : is the quantifier containing + which bind the variable return a pattern where the variable are replaced by + variable for instantiation. + */ + Node substituteBoundVariablesToInstConstants(Node n, Node q); + /** substitute { instantiation constants of q -> bound variables of q } in n + */ + Node substituteInstConstantsToBoundVariables(Node n, Node q); + /** substitute { variables of q -> terms } in n */ + Node substituteBoundVariables(Node n, Node q, std::vector<Node>& terms); + /** substitute { instantiation constants of q -> terms } in n */ + Node substituteInstConstants(Node n, Node q, std::vector<Node>& terms); + //----------------------------- end instantiation constants private: /** * Maps quantified formulas to the module that owns them, if any module has @@ -60,6 +96,14 @@ class QuantifiersRegistry * precendence. */ std::map<Node, int32_t> d_owner_priority; + /** map from universal quantifiers to the list of variables */ + std::map<Node, std::vector<Node> > d_vars; + /** map from universal quantifiers to their inst constant body */ + std::map<Node, Node> d_inst_const_body; + /** instantiation constants to universal quantifiers */ + std::map<Node, Node> d_inst_constants_map; + /** map from universal quantifiers to the list of instantiation constants */ + std::map<Node, std::vector<Node> > d_inst_constants; }; } // namespace quantifiers diff --git a/src/theory/quantifiers/relevant_domain.cpp b/src/theory/quantifiers/relevant_domain.cpp index 1743cafe5..3cef2884f 100644 --- a/src/theory/quantifiers/relevant_domain.cpp +++ b/src/theory/quantifiers/relevant_domain.cpp @@ -69,10 +69,10 @@ void RelevantDomain::RDomain::removeRedundantTerms(QuantifiersState& qs) } } - - -RelevantDomain::RelevantDomain( QuantifiersEngine* qe ) : d_qe( qe ){ - d_is_computed = false; +RelevantDomain::RelevantDomain(QuantifiersEngine* qe, QuantifiersRegistry& qr) + : d_qe(qe), d_qreg(qr) +{ + d_is_computed = false; } RelevantDomain::~RelevantDomain() { @@ -111,7 +111,7 @@ void RelevantDomain::compute(){ FirstOrderModel* fm = d_qe->getModel(); for( unsigned i=0; i<fm->getNumAssertedQuantifiers(); i++ ){ Node q = fm->getAssertedQuantifier( i ); - Node icf = d_qe->getTermUtil()->getInstConstantBody( q ); + Node icf = d_qreg.getInstConstantBody(q); Trace("rel-dom-debug") << "compute relevant domain for " << icf << std::endl; computeRelevantDomain( q, icf, true, true ); } @@ -204,12 +204,13 @@ void RelevantDomain::computeRelevantDomain( Node q, Node n, bool hasPol, bool po void RelevantDomain::computeRelevantDomainOpCh( RDomain * rf, Node n ) { if( n.getKind()==INST_CONSTANT ){ - Node q = d_qe->getTermUtil()->getInstConstAttr( n ); + Node q = TermUtil::getInstConstAttr(n); //merge the RDomains unsigned id = n.getAttribute(InstVarNumAttribute()); Assert(q[0][id].getType() == n.getType()); Trace("rel-dom-debug") << n << " is variable # " << id << " for " << q; - Trace("rel-dom-debug") << " with body : " << d_qe->getTermUtil()->getInstConstantBody( q ) << std::endl; + Trace("rel-dom-debug") << " with body : " << d_qreg.getInstConstantBody(q) + << std::endl; RDomain * rq = getRDomain( q, id ); if( rf!=rq ){ rq->merge( rf ); @@ -226,12 +227,11 @@ void RelevantDomain::computeRelevantDomainLit( Node q, bool hasPol, bool pol, No d_rel_dom_lit[hasPol][pol][n].d_merge = false; int varCount = 0; int varCh = -1; - TermUtil* tu = d_qe->getTermUtil(); for( unsigned i=0; i<n.getNumChildren(); i++ ){ if( n[i].getKind()==INST_CONSTANT ){ // must get the quantified formula this belongs to, which may be // different from q - Node qi = tu->getInstConstAttr(n[i]); + Node qi = TermUtil::getInstConstAttr(n[i]); unsigned id = n[i].getAttribute(InstVarNumAttribute()); d_rel_dom_lit[hasPol][pol][n].d_rd[i] = getRDomain(qi, id, false); varCount++; @@ -262,7 +262,7 @@ void RelevantDomain::computeRelevantDomainLit( Node q, bool hasPol, bool pol, No bool hasNonVar = false; for( std::map< Node, Node >::iterator it = msum.begin(); it != msum.end(); ++it ){ if (!it->first.isNull() && it->first.getKind() == INST_CONSTANT - && tu->getInstConstAttr(it->first) == q) + && TermUtil::getInstConstAttr(it->first) == q) { if( var.isNull() ){ var = it->first; diff --git a/src/theory/quantifiers/relevant_domain.h b/src/theory/quantifiers/relevant_domain.h index 36364191c..68ffbefe5 100644 --- a/src/theory/quantifiers/relevant_domain.h +++ b/src/theory/quantifiers/relevant_domain.h @@ -24,6 +24,8 @@ namespace CVC4 { namespace theory { namespace quantifiers { +class QuantifiersRegistry; + /** Relevant Domain * * This class computes the relevant domain of @@ -40,7 +42,7 @@ namespace quantifiers { class RelevantDomain : public QuantifiersUtil { public: - RelevantDomain(QuantifiersEngine* qe); + RelevantDomain(QuantifiersEngine* qe, QuantifiersRegistry& qr); virtual ~RelevantDomain(); /** Reset. */ bool reset(Theory::Effort e) override; @@ -117,6 +119,8 @@ class RelevantDomain : public QuantifiersUtil std::map< RDomain *, int > d_ri_map; /** Quantifiers engine associated with this utility. */ QuantifiersEngine* d_qe; + /** The quantifiers registry */ + QuantifiersRegistry& d_qreg; /** have we computed the relevant domain on this full effort check? */ bool d_is_computed; /** relevant domain literal diff --git a/src/theory/quantifiers/single_inv_partition.cpp b/src/theory/quantifiers/single_inv_partition.cpp index c329d924b..f1307f142 100644 --- a/src/theory/quantifiers/single_inv_partition.cpp +++ b/src/theory/quantifiers/single_inv_partition.cpp @@ -16,6 +16,7 @@ #include "expr/node_algorithm.h" #include "theory/quantifiers/term_util.h" +#include "theory/rewriter.h" using namespace CVC4; using namespace CVC4::kind; diff --git a/src/theory/quantifiers/skolemize.h b/src/theory/quantifiers/skolemize.h index b28854baf..c959758a0 100644 --- a/src/theory/quantifiers/skolemize.h +++ b/src/theory/quantifiers/skolemize.h @@ -23,7 +23,7 @@ #include "context/cdhashmap.h" #include "expr/node.h" #include "expr/type_node.h" -#include "theory/quantifiers/quant_util.h" +#include "theory/eager_proof_generator.h" #include "theory/trust_node.h" namespace CVC4 { @@ -31,8 +31,13 @@ namespace CVC4 { class DTypeConstructor; namespace theory { + +class QuantifiersEngine; + namespace quantifiers { +class QuantifiersState; + /** Skolemization utility * * This class constructs Skolemization lemmas. diff --git a/src/theory/quantifiers/sygus/synth_engine.h b/src/theory/quantifiers/sygus/synth_engine.h index 4cb73d450..0e0068c7b 100644 --- a/src/theory/quantifiers/sygus/synth_engine.h +++ b/src/theory/quantifiers/sygus/synth_engine.h @@ -19,7 +19,7 @@ #define CVC4__THEORY__QUANTIFIERS__SYNTH_ENGINE_H #include "context/cdhashmap.h" -#include "theory/quantifiers/quant_util.h" +#include "theory/quantifiers/quant_module.h" #include "theory/quantifiers/sygus/sygus_qe_preproc.h" #include "theory/quantifiers/sygus/sygus_stats.h" #include "theory/quantifiers/sygus/synth_conjecture.h" diff --git a/src/theory/quantifiers/sygus_inst.h b/src/theory/quantifiers/sygus_inst.h index 123ec1f5e..3116f35e6 100644 --- a/src/theory/quantifiers/sygus_inst.h +++ b/src/theory/quantifiers/sygus_inst.h @@ -21,7 +21,7 @@ #include <unordered_set> #include "context/cdhashset.h" -#include "theory/quantifiers/quant_util.h" +#include "theory/quantifiers/quant_module.h" namespace CVC4 { namespace theory { diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index 61a62a820..28eb715a3 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -36,10 +36,12 @@ namespace quantifiers { TermDb::TermDb(QuantifiersState& qs, QuantifiersInferenceManager& qim, + QuantifiersRegistry& qr, QuantifiersEngine* qe) : d_quantEngine(qe), d_qstate(qs), d_qim(qim), + d_qreg(qr), d_termsContext(), d_termsContextUse(options::termDbCd() ? qs.getSatContext() : &d_termsContext), @@ -65,10 +67,10 @@ TermDb::~TermDb(){ } void TermDb::registerQuantifier( Node q ) { - Assert(q[0].getNumChildren() - == d_quantEngine->getTermUtil()->getNumInstantiationConstants(q)); - for( unsigned i=0; i<q[0].getNumChildren(); i++ ){ - Node ic = d_quantEngine->getTermUtil()->getInstantiationConstant( q, i ); + Assert(q[0].getNumChildren() == d_qreg.getNumInstantiationConstants(q)); + for (size_t i = 0, nvars = q[0].getNumChildren(); i < nvars; i++) + { + Node ic = d_qreg.getInstantiationConstant(q, i); setTermInactive( ic ); } } @@ -688,10 +690,10 @@ Node TermDb::evaluateTerm2(TNode n, { if (ret.getKind() == EQUAL || ret.getKind() == GEQ) { - TheoryEngine* te = d_quantEngine->getTheoryEngine(); + Valuation& val = d_qstate.getValuation(); for (unsigned j = 0; j < 2; j++) { - std::pair<bool, Node> et = te->entailmentCheck( + std::pair<bool, Node> et = val.entailmentCheck( options::TheoryOfMode::THEORY_OF_TYPE_BASED, j == 0 ? ret : ret.negate()); if (et.first) diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h index b2f964a3a..89d77e169 100644 --- a/src/theory/quantifiers/term_database.h +++ b/src/theory/quantifiers/term_database.h @@ -33,8 +33,9 @@ class QuantifiersEngine; namespace quantifiers { -class ConjectureGenerator; -class TermGenEnv; +class QuantifiersState; +class QuantifiersInferenceManager; +class QuantifiersRegistry; /** Context-dependent list of nodes */ class DbList @@ -76,6 +77,7 @@ class TermDb : public QuantifiersUtil { public: TermDb(QuantifiersState& qs, QuantifiersInferenceManager& qim, + QuantifiersRegistry& qr, QuantifiersEngine* qe); ~TermDb(); /** presolve (called once per user check-sat) */ @@ -295,6 +297,8 @@ class TermDb : public QuantifiersUtil { QuantifiersState& d_qstate; /** The quantifiers inference manager */ QuantifiersInferenceManager& d_qim; + /** The quantifiers registry */ + QuantifiersRegistry& d_qreg; /** A context for the data structures below, when not context-dependent */ context::Context d_termsContext; /** The context we are using for the data structures below */ diff --git a/src/theory/quantifiers/term_util.cpp b/src/theory/quantifiers/term_util.cpp index b0a067630..97a731fb9 100644 --- a/src/theory/quantifiers/term_util.cpp +++ b/src/theory/quantifiers/term_util.cpp @@ -47,24 +47,11 @@ TermUtil::~TermUtil(){ } -void TermUtil::registerQuantifier( Node q ){ - if( d_inst_constants.find( q )==d_inst_constants.end() ){ - Debug("quantifiers-engine") << "Instantiation constants for " << q << " : " << std::endl; - for( unsigned i=0; i<q[0].getNumChildren(); i++ ){ - d_vars[q].push_back( q[0][i] ); - d_var_num[q][q[0][i]] = i; - //make instantiation constants - Node ic = NodeManager::currentNM()->mkInstConstant( q[0][i].getType() ); - d_inst_constants_map[ic] = q; - d_inst_constants[ q ].push_back( ic ); - Debug("quantifiers-engine") << " " << ic << std::endl; - //set the var number attribute - InstVarNumAttribute ivna; - ic.setAttribute( ivna, i ); - InstConstantAttribute ica; - ic.setAttribute( ica, q ); - } - } +size_t TermUtil::getVariableNum(Node q, Node v) +{ + Node::iterator it = std::find(q[0].begin(), q[0].end(), v); + Assert(it != q[0].end()); + return it - q[0].begin(); } Node TermUtil::getRemoveQuantifiers2( Node n, std::map< Node, Node >& visited ) { @@ -168,68 +155,6 @@ Node TermUtil::getQuantSimplify( Node n ) { return getRemoveQuantifiers(q); } -/** get the i^th instantiation constant of q */ -Node TermUtil::getInstantiationConstant( Node q, int i ) const { - std::map< Node, std::vector< Node > >::const_iterator it = d_inst_constants.find( q ); - if( it!=d_inst_constants.end() ){ - return it->second[i]; - }else{ - return Node::null(); - } -} - -/** get number of instantiation constants for q */ -unsigned TermUtil::getNumInstantiationConstants( Node q ) const { - std::map< Node, std::vector< Node > >::const_iterator it = d_inst_constants.find( q ); - if( it!=d_inst_constants.end() ){ - return it->second.size(); - }else{ - return 0; - } -} - -Node TermUtil::getInstConstantBody( Node q ){ - std::map< Node, Node >::iterator it = d_inst_const_body.find( q ); - if( it==d_inst_const_body.end() ){ - Node n = substituteBoundVariablesToInstConstants(q[1], q); - d_inst_const_body[ q ] = n; - return n; - }else{ - return it->second; - } -} - -Node TermUtil::substituteBoundVariablesToInstConstants(Node n, Node q) -{ - registerQuantifier( q ); - return n.substitute( d_vars[q].begin(), d_vars[q].end(), d_inst_constants[q].begin(), d_inst_constants[q].end() ); -} - -Node TermUtil::substituteInstConstantsToBoundVariables(Node n, Node q) -{ - registerQuantifier( q ); - return n.substitute( d_inst_constants[q].begin(), d_inst_constants[q].end(), d_vars[q].begin(), d_vars[q].end() ); -} - -Node TermUtil::substituteBoundVariables(Node n, - Node q, - std::vector<Node>& terms) -{ - registerQuantifier(q); - Assert(d_vars[q].size() == terms.size()); - return n.substitute( d_vars[q].begin(), d_vars[q].end(), terms.begin(), terms.end() ); -} - -Node TermUtil::substituteInstConstants(Node n, Node q, std::vector<Node>& terms) -{ - registerQuantifier(q); - Assert(d_inst_constants[q].size() == terms.size()); - return n.substitute(d_inst_constants[q].begin(), - d_inst_constants[q].end(), - terms.begin(), - terms.end()); -} - void TermUtil::computeInstConstContains(Node n, std::vector<Node>& ics) { computeVarContainsInternal(n, INST_CONSTANT, ics); diff --git a/src/theory/quantifiers/term_util.h b/src/theory/quantifiers/term_util.h index 4033c888f..e9e3c7e98 100644 --- a/src/theory/quantifiers/term_util.h +++ b/src/theory/quantifiers/term_util.h @@ -21,7 +21,6 @@ #include <unordered_set> #include "expr/attribute.h" -#include "theory/quantifiers/quant_util.h" #include "theory/type_enumerator.h" namespace CVC4 { @@ -61,15 +60,10 @@ namespace inst{ namespace quantifiers { class TermDatabase; -class Instantiate; // TODO : #1216 split this class, most of the functions in this class should be dispersed to where they are used. -class TermUtil : public QuantifiersUtil +class TermUtil { - // TODO : remove these - friend class ::CVC4::theory::QuantifiersEngine; - friend class Instantiate; - public: TermUtil(); ~TermUtil(); @@ -80,46 +74,10 @@ class TermUtil : public QuantifiersUtil Node d_zero; Node d_one; - /** reset */ - bool reset(Theory::Effort e) override { return true; } - /** register quantifier */ - void registerQuantifier(Node q) override; - /** identify */ - std::string identify() const override { return "TermUtil"; } // for inst constant - private: - /** map from universal quantifiers to the list of variables */ - std::map< Node, std::vector< Node > > d_vars; - std::map< Node, std::map< Node, unsigned > > d_var_num; - /** map from universal quantifiers to their inst constant body */ - std::map< Node, Node > d_inst_const_body; - /** instantiation constants to universal quantifiers */ - std::map< Node, Node > d_inst_constants_map; -public: - /** map from universal quantifiers to the list of instantiation constants */ - std::map< Node, std::vector< Node > > d_inst_constants; - /** get variable number */ - unsigned getVariableNum( Node q, Node v ) { return d_var_num[q][v]; } - /** get the i^th instantiation constant of q */ - Node getInstantiationConstant( Node q, int i ) const; - /** get number of instantiation constants for q */ - unsigned getNumInstantiationConstants( Node q ) const; - /** get the ce body q[e/x] */ - Node getInstConstantBody( Node q ); - /** returns node n with bound vars of q replaced by instantiation constants of q - node n : is the future pattern - node q : is the quantifier containing which bind the variable - return a pattern where the variable are replaced by variable for - instantiation. - */ - Node substituteBoundVariablesToInstConstants(Node n, Node q); - /** substitute { instantiation constants of q -> bound variables of q } in n - */ - Node substituteInstConstantsToBoundVariables(Node n, Node q); - /** substitute { variables of q -> terms } in n */ - Node substituteBoundVariables(Node n, Node q, std::vector<Node>& terms); - /** substitute { instantiation constants of q -> terms } in n */ - Node substituteInstConstants(Node n, Node q, std::vector<Node>& terms); + public: + /** Get the index of BOUND_VARIABLE v in quantifier q */ + static size_t getVariableNum(Node q, Node v); static Node getInstConstAttr( Node n ); static bool hasInstConstAttr( Node n ); diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index e85d6f2ff..9c56c1ba5 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -45,11 +45,12 @@ QuantifiersEngine::QuantifiersEngine( d_model(nullptr), d_builder(nullptr), d_term_util(new quantifiers::TermUtil), - d_term_db(new quantifiers::TermDb(qstate, qim, this)), + d_term_db(new quantifiers::TermDb(qstate, qim, d_qreg, this)), d_eq_query(nullptr), d_sygus_tdb(nullptr), d_quant_attr(new quantifiers::QuantAttributes), - d_instantiate(new quantifiers::Instantiate(this, qstate, qim, pnm)), + d_instantiate( + new quantifiers::Instantiate(this, qstate, qim, d_qreg, pnm)), d_skolemize(new quantifiers::Skolemize(this, qstate, pnm)), d_term_enum(new quantifiers::TermEnumeration), d_quants_prereg(qstate.getUserContext()), @@ -59,8 +60,8 @@ QuantifiersEngine::QuantifiersEngine( d_presolve_cache(qstate.getUserContext()) { //---- utilities - // term util must come before the other utilities - d_util.push_back(d_term_util.get()); + // quantifiers registry must come before the other utilities + d_util.push_back(&d_qreg); d_util.push_back(d_term_db.get()); if (options::sygus() || options::sygusInst()) @@ -88,17 +89,17 @@ QuantifiersEngine::QuantifiersEngine( { Trace("quant-engine-debug") << "...make fmc builder." << std::endl; d_model.reset(new quantifiers::fmcheck::FirstOrderModelFmc( - this, qstate, "FirstOrderModelFmc")); + this, qstate, d_qreg, "FirstOrderModelFmc")); d_builder.reset(new quantifiers::fmcheck::FullModelChecker(this, qstate)); }else{ Trace("quant-engine-debug") << "...make default model builder." << std::endl; - d_model.reset( - new quantifiers::FirstOrderModel(this, qstate, "FirstOrderModel")); + d_model.reset(new quantifiers::FirstOrderModel( + this, qstate, d_qreg, "FirstOrderModel")); d_builder.reset(new quantifiers::QModelBuilder(this, qstate)); } }else{ - d_model.reset( - new quantifiers::FirstOrderModel(this, qstate, "FirstOrderModel")); + d_model.reset(new quantifiers::FirstOrderModel( + this, qstate, d_qreg, "FirstOrderModel")); } d_eq_query.reset(new quantifiers::EqualityQueryQuantifiersEngine( qstate, d_term_db.get(), d_model.get())); @@ -142,6 +143,12 @@ QuantifiersEngine::getInferenceManager() { return d_qim; } + +quantifiers::QuantifiersRegistry& QuantifiersEngine::getQuantifiersRegistry() +{ + return d_qreg; +} + quantifiers::QModelBuilder* QuantifiersEngine::getModelBuilder() const { return d_builder.get(); @@ -737,7 +744,7 @@ void QuantifiersEngine::assertQuantifier( Node f, bool pol ){ { mdl->assertNode(f); } - addTermToDatabase(d_term_util->getInstConstantBody(f), true); + addTermToDatabase(d_qreg.getInstConstantBody(f), true); } void QuantifiersEngine::addTermToDatabase(Node n, bool withinQuant) diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index 99e4ad5cc..2fbf6b70f 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -28,6 +28,7 @@ #include "theory/quantifiers/first_order_model.h" #include "theory/quantifiers/fmf/model_builder.h" #include "theory/quantifiers/instantiate.h" +#include "theory/quantifiers/quant_module.h" #include "theory/quantifiers/quant_util.h" #include "theory/quantifiers/quantifiers_attributes.h" #include "theory/quantifiers/quantifiers_inference_manager.h" @@ -77,6 +78,8 @@ class QuantifiersEngine { quantifiers::QuantifiersState& getState(); /** The quantifiers inference manager */ quantifiers::QuantifiersInferenceManager& getInferenceManager(); + /** The quantifiers registry */ + quantifiers::QuantifiersRegistry& getQuantifiersRegistry(); //---------------------- end external interface //---------------------- utilities /** get the model builder */ |