From 36b9c04591067491854cb1d4caaf391572357375 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 12 Oct 2021 10:29:38 -0500 Subject: [PATCH] Minor cleaning of instantiation utilities (#7334) Also fixes a bug in the quantifiers macro utility which did not compute the instantiation constant body of a quantified formula properly. This is work towards a major refactoring of conflict-based instantiation / entailment checks. --- .../quantifiers/cegqi/inst_strategy_cegqi.cpp | 12 ++--- .../quantifiers/cegqi/inst_strategy_cegqi.h | 4 +- src/theory/quantifiers/instantiate.cpp | 18 +++++--- src/theory/quantifiers/instantiate.h | 18 ++++---- src/theory/quantifiers/quant_module.cpp | 5 +++ src/theory/quantifiers/quant_module.h | 2 + src/theory/quantifiers/quantifiers_macros.cpp | 3 +- .../quantifiers/quantifiers_registry.cpp | 45 ++++++++++--------- src/theory/quantifiers/quantifiers_registry.h | 4 +- 9 files changed, 61 insertions(+), 50 deletions(-) diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp index 0337d8959..339524d94 100644 --- a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp +++ b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp @@ -40,10 +40,8 @@ InstRewriterCegqi::InstRewriterCegqi(InstStrategyCegqi* p) { } -TrustNode InstRewriterCegqi::rewriteInstantiation(Node q, - std::vector& terms, - Node inst, - bool doVts) +TrustNode InstRewriterCegqi::rewriteInstantiation( + Node q, const std::vector& terms, Node inst, bool doVts) { return d_parent->rewriteInstantiation(q, terms, inst, doVts); } @@ -344,10 +342,8 @@ void InstStrategyCegqi::preRegisterQuantifier(Node q) } } } -TrustNode InstStrategyCegqi::rewriteInstantiation(Node q, - std::vector& terms, - Node inst, - bool doVts) +TrustNode InstStrategyCegqi::rewriteInstantiation( + Node q, const std::vector& terms, Node inst, bool doVts) { Node prevInst = inst; if (doVts) diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h index a568b0b4d..5a886e28d 100644 --- a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h +++ b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h @@ -49,7 +49,7 @@ class InstRewriterCegqi : public InstantiationRewriter * corresponding to the rewrite and its proof generator. */ TrustNode rewriteInstantiation(Node q, - std::vector& terms, + const std::vector& terms, Node inst, bool doVts) override; @@ -116,7 +116,7 @@ class InstStrategyCegqi : public QuantifiersModule * proof generator. */ TrustNode rewriteInstantiation(Node q, - std::vector& terms, + const std::vector& terms, Node inst, bool doVts); /** get the instantiation rewriter object */ diff --git a/src/theory/quantifiers/instantiate.cpp b/src/theory/quantifiers/instantiate.cpp index 0807188d5..f756fcfd1 100644 --- a/src/theory/quantifiers/instantiate.cpp +++ b/src/theory/quantifiers/instantiate.cpp @@ -485,7 +485,7 @@ bool Instantiate::addInstantiationExpFail(Node q, } void Instantiate::recordInstantiation(Node q, - std::vector& terms, + const std::vector& terms, bool doVts) { Trace("inst-debug") << "Record instantiation for " << q << std::endl; @@ -497,7 +497,7 @@ void Instantiate::recordInstantiation(Node q, } bool Instantiate::existsInstantiation(Node q, - std::vector& terms, + const std::vector& terms, bool modEq) { if (options::incrementalSolving()) @@ -520,8 +520,8 @@ bool Instantiate::existsInstantiation(Node q, } Node Instantiate::getInstantiation(Node q, - std::vector& vars, - std::vector& terms, + const std::vector& vars, + const std::vector& terms, InferenceId id, Node pfArg, bool doVts, @@ -576,14 +576,17 @@ Node Instantiate::getInstantiation(Node q, return body; } -Node Instantiate::getInstantiation(Node q, std::vector& terms, bool doVts) +Node Instantiate::getInstantiation(Node q, + const std::vector& terms, + bool doVts) { Assert(d_qreg.d_vars.find(q) != d_qreg.d_vars.end()); return getInstantiation( q, d_qreg.d_vars[q], terms, InferenceId::UNKNOWN, Node::null(), doVts); } -bool Instantiate::recordInstantiationInternal(Node q, std::vector& terms) +bool Instantiate::recordInstantiationInternal(Node q, + const std::vector& terms) { if (options::incrementalSolving()) { @@ -601,7 +604,8 @@ bool Instantiate::recordInstantiationInternal(Node q, std::vector& terms) return d_inst_match_trie[q].addInstMatch(d_qstate, q, terms); } -bool Instantiate::removeInstantiationInternal(Node q, std::vector& terms) +bool Instantiate::removeInstantiationInternal(Node q, + const std::vector& terms) { if (options::incrementalSolving()) { diff --git a/src/theory/quantifiers/instantiate.h b/src/theory/quantifiers/instantiate.h index 753213f35..b4972a7b6 100644 --- a/src/theory/quantifiers/instantiate.h +++ b/src/theory/quantifiers/instantiate.h @@ -65,7 +65,7 @@ class InstantiationRewriter * and its proof generator. */ virtual TrustNode rewriteInstantiation(Node q, - std::vector& terms, + const std::vector& terms, Node inst, bool doVts) = 0; }; @@ -203,7 +203,7 @@ class Instantiate : public QuantifiersUtil * but does not enqueue an instantiation lemma. */ void recordInstantiation(Node q, - std::vector& terms, + const std::vector& terms, bool doVts = false); /** exists instantiation * @@ -212,7 +212,7 @@ class Instantiate : public QuantifiersUtil * modEq : whether to check for duplication modulo equality */ bool existsInstantiation(Node q, - std::vector& terms, + const std::vector& terms, bool modEq = false); //--------------------------------------general utilities /** get instantiation @@ -225,8 +225,8 @@ class Instantiate : public QuantifiersUtil * single INSTANTIATE step concluding the instantiated body of q from q. */ Node getInstantiation(Node q, - std::vector& vars, - std::vector& terms, + const std::vector& vars, + const std::vector& terms, InferenceId id = InferenceId::UNKNOWN, Node pfArg = Node::null(), bool doVts = false, @@ -235,7 +235,9 @@ class Instantiate : public QuantifiersUtil * * Same as above but with vars equal to the bound variables of q. */ - Node getInstantiation(Node q, std::vector& terms, bool doVts = false); + Node getInstantiation(Node q, + const std::vector& terms, + bool doVts = false); //--------------------------------------end general utilities /** @@ -297,9 +299,9 @@ class Instantiate : public QuantifiersUtil private: /** record instantiation, return true if it was not a duplicate */ - bool recordInstantiationInternal(Node q, std::vector& terms); + bool recordInstantiationInternal(Node q, const std::vector& terms); /** remove instantiation from the cache */ - bool removeInstantiationInternal(Node q, std::vector& terms); + bool removeInstantiationInternal(Node q, const std::vector& terms); /** * Ensure that n has type tn, return a term equivalent to it for that type * if possible. diff --git a/src/theory/quantifiers/quant_module.cpp b/src/theory/quantifiers/quant_module.cpp index 8fb37c548..db4eb9d34 100644 --- a/src/theory/quantifiers/quant_module.cpp +++ b/src/theory/quantifiers/quant_module.cpp @@ -76,5 +76,10 @@ quantifiers::QuantifiersRegistry& QuantifiersModule::getQuantifiersRegistry() return d_qreg; } +quantifiers::TermRegistry& QuantifiersModule::getTermRegistry() +{ + return d_treg; +} + } // namespace theory } // namespace cvc5 diff --git a/src/theory/quantifiers/quant_module.h b/src/theory/quantifiers/quant_module.h index 639f9c2b4..ce6c1b04c 100644 --- a/src/theory/quantifiers/quant_module.h +++ b/src/theory/quantifiers/quant_module.h @@ -167,6 +167,8 @@ class QuantifiersModule : protected EnvObj quantifiers::QuantifiersInferenceManager& getInferenceManager(); /** get the quantifiers registry */ quantifiers::QuantifiersRegistry& getQuantifiersRegistry(); + /** get the term registry */ + quantifiers::TermRegistry& getTermRegistry(); //----------------------------end general queries protected: /** Reference to the state of the quantifiers engine */ diff --git a/src/theory/quantifiers/quantifiers_macros.cpp b/src/theory/quantifiers/quantifiers_macros.cpp index a3bdf10ad..9b9580b02 100644 --- a/src/theory/quantifiers/quantifiers_macros.cpp +++ b/src/theory/quantifiers/quantifiers_macros.cpp @@ -88,7 +88,7 @@ Node QuantifiersMacros::solve(Node lit, bool reqGround) << "...does not contain bad (recursive) operator." << std::endl; // must be ground UF term if mode is GROUND_UF if (options::macrosQuantMode() != options::MacrosQuantMode::GROUND_UF - || preservesTriggerVariables(body, n_def)) + || preservesTriggerVariables(lit, n_def)) { Trace("macros-debug") << "...respects ground-uf constraint." << std::endl; @@ -139,6 +139,7 @@ bool QuantifiersMacros::containsBadOp(Node n, Node op, bool reqGround) bool QuantifiersMacros::preservesTriggerVariables(Node q, Node n) { + Assert(q.getKind() == FORALL) << "Expected quantified formula, got " << q; Node icn = d_qreg.substituteBoundVariablesToInstConstants(n, q); Trace("macros-debug2") << "Get free variables in " << icn << std::endl; std::vector var; diff --git a/src/theory/quantifiers/quantifiers_registry.cpp b/src/theory/quantifiers/quantifiers_registry.cpp index 6d5e00363..487bcc0fe 100644 --- a/src/theory/quantifiers/quantifiers_registry.cpp +++ b/src/theory/quantifiers/quantifiers_registry.cpp @@ -38,6 +38,7 @@ void QuantifiersRegistry::registerQuantifier(Node q) { return; } + Assert(q.getKind() == kind::FORALL); NodeManager* nm = NodeManager::currentNM(); Debug("quantifiers-engine") << "Instantiation constants for " << q << " : " << std::endl; @@ -144,42 +145,42 @@ 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()); + std::vector& vars = d_vars.at(q); + std::vector& consts = d_inst_constants.at(q); + Assert(vars.size() == q[0].getNumChildren()); + Assert(vars.size() == consts.size()); + return n.substitute(vars.begin(), vars.end(), consts.begin(), consts.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()); + std::vector& vars = d_vars.at(q); + std::vector& consts = d_inst_constants.at(q); + Assert(vars.size() == q[0].getNumChildren()); + Assert(vars.size() == consts.size()); + return n.substitute(consts.begin(), consts.end(), vars.begin(), vars.end()); } -Node QuantifiersRegistry::substituteBoundVariables(Node n, - Node q, - std::vector& terms) +Node QuantifiersRegistry::substituteBoundVariables( + Node n, Node q, const std::vector& 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()); + std::vector& vars = d_vars.at(q); + Assert(vars.size() == q[0].getNumChildren()); + Assert(vars.size() == terms.size()); + return n.substitute(vars.begin(), vars.end(), terms.begin(), terms.end()); } -Node QuantifiersRegistry::substituteInstConstants(Node n, - Node q, - std::vector& terms) +Node QuantifiersRegistry::substituteInstConstants( + Node n, Node q, const std::vector& 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()); + std::vector& consts = d_inst_constants.at(q); + Assert(consts.size() == q[0].getNumChildren()); + Assert(consts.size() == terms.size()); + return n.substitute(consts.begin(), consts.end(), terms.begin(), terms.end()); } QuantAttributes& QuantifiersRegistry::getQuantAttributes() diff --git a/src/theory/quantifiers/quantifiers_registry.h b/src/theory/quantifiers/quantifiers_registry.h index 559939bbe..858a85cae 100644 --- a/src/theory/quantifiers/quantifiers_registry.h +++ b/src/theory/quantifiers/quantifiers_registry.h @@ -84,9 +84,9 @@ class QuantifiersRegistry : public QuantifiersUtil */ Node substituteInstConstantsToBoundVariables(Node n, Node q); /** substitute { variables of q -> terms } in n */ - Node substituteBoundVariables(Node n, Node q, std::vector& terms); + Node substituteBoundVariables(Node n, Node q, const std::vector& terms); /** substitute { instantiation constants of q -> terms } in n */ - Node substituteInstConstants(Node n, Node q, std::vector& terms); + Node substituteInstConstants(Node n, Node q, const std::vector& terms); //----------------------------- end instantiation constants /** Get quantifiers attributes utility class */ QuantAttributes& getQuantAttributes(); -- 2.30.2