diff options
Diffstat (limited to 'src')
-rw-r--r-- | src/smt/set_defaults.cpp | 9 | ||||
-rw-r--r-- | src/theory/quantifiers/ematching/instantiation_engine.cpp | 113 | ||||
-rw-r--r-- | src/theory/quantifiers/ematching/instantiation_engine.h | 2 | ||||
-rw-r--r-- | src/theory/quantifiers/quantifiers_attributes.cpp | 18 | ||||
-rw-r--r-- | src/theory/quantifiers/quantifiers_attributes.h | 30 | ||||
-rw-r--r-- | src/theory/strings/theory_strings_preprocess.cpp | 52 | ||||
-rw-r--r-- | src/theory/strings/theory_strings_preprocess.h | 8 |
7 files changed, 172 insertions, 60 deletions
diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp index 32e716ab2..4ad198a82 100644 --- a/src/smt/set_defaults.cpp +++ b/src/smt/set_defaults.cpp @@ -239,13 +239,6 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) options::fmfBound.set(true); Trace("smt") << "turning on fmf-bound-int, for strings-exp" << std::endl; } - // Turn off E-matching, since some bounded quantifiers introduced by strings - // (e.g. for replaceall) admit matching loops. - if (!options::eMatching.wasSetByUser()) - { - options::eMatching.set(false); - Trace("smt") << "turning off E-matching, for strings-exp" << std::endl; - } // Do not eliminate extended arithmetic symbols from quantified formulas, // since some strategies, e.g. --re-elim-agg, introduce them. if (!options::elimExtArithQuant.wasSetByUser()) @@ -254,6 +247,8 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) Trace("smt") << "turning off elim-ext-arith-quant, for strings-exp" << std::endl; } + // Note we allow E-matching by default to support combinations of sequences + // and quantifiers. } if (options::arraysExp()) { diff --git a/src/theory/quantifiers/ematching/instantiation_engine.cpp b/src/theory/quantifiers/ematching/instantiation_engine.cpp index a00ac6c86..ad9c53e0f 100644 --- a/src/theory/quantifiers/ematching/instantiation_engine.cpp +++ b/src/theory/quantifiers/ematching/instantiation_engine.cpp @@ -18,19 +18,21 @@ #include "theory/quantifiers/ematching/inst_strategy_e_matching.h" #include "theory/quantifiers/ematching/trigger.h" #include "theory/quantifiers/first_order_model.h" +#include "theory/quantifiers/quantifiers_attributes.h" #include "theory/quantifiers/term_database.h" #include "theory/quantifiers/term_util.h" #include "theory/quantifiers_engine.h" #include "theory/theory_engine.h" using namespace std; -using namespace CVC4; using namespace CVC4::kind; using namespace CVC4::context; -using namespace CVC4::theory; -using namespace CVC4::theory::quantifiers; using namespace CVC4::theory::inst; +namespace CVC4 { +namespace theory { +namespace quantifiers { + InstantiationEngine::InstantiationEngine(QuantifiersEngine* qe) : QuantifiersModule(qe), d_instStrategies(), @@ -123,42 +125,64 @@ void InstantiationEngine::reset_round( Theory::Effort e ){ void InstantiationEngine::check(Theory::Effort e, QEffort quant_e) { CodeTimer codeTimer(d_quantEngine->d_statistics.d_ematching_time); - if (quant_e == QEFFORT_STANDARD) + if (quant_e != QEFFORT_STANDARD) { - double clSet = 0; - if( Trace.isOn("inst-engine") ){ - clSet = double(clock())/double(CLOCKS_PER_SEC); - Trace("inst-engine") << "---Instantiation Engine Round, effort = " << e << "---" << std::endl; - } - //collect all active quantified formulas belonging to this - bool quantActive = false; - d_quants.clear(); - for( unsigned i=0; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){ - Node q = d_quantEngine->getModel()->getAssertedQuantifier( i, true ); - if( d_quantEngine->hasOwnership( q, this ) && d_quantEngine->getModel()->isQuantifierActive( q ) ){ - quantActive = true; - d_quants.push_back( q ); - } + return; + } + double clSet = 0; + if (Trace.isOn("inst-engine")) + { + clSet = double(clock()) / double(CLOCKS_PER_SEC); + Trace("inst-engine") << "---Instantiation Engine Round, effort = " << e + << "---" << std::endl; + } + // collect all active quantified formulas belonging to this + bool quantActive = false; + d_quants.clear(); + FirstOrderModel* m = d_quantEngine->getModel(); + size_t nquant = m->getNumAssertedQuantifiers(); + for (size_t i = 0; i < nquant; i++) + { + Node q = d_quantEngine->getModel()->getAssertedQuantifier(i, true); + if (shouldProcess(q) && m->isQuantifierActive(q)) + { + quantActive = true; + d_quants.push_back(q); } - Trace("inst-engine-debug") << "InstEngine: check: # asserted quantifiers " << d_quants.size() << "/"; - Trace("inst-engine-debug") << d_quantEngine->getModel()->getNumAssertedQuantifiers() << " " << quantActive << std::endl; - if( quantActive ){ - unsigned lastWaiting = d_quantEngine->getNumLemmasWaiting(); - doInstantiationRound( e ); - if( d_quantEngine->inConflict() ){ - Assert(d_quantEngine->getNumLemmasWaiting() > lastWaiting); - Trace("inst-engine") << "Conflict, added lemmas = " << (d_quantEngine->getNumLemmasWaiting()-lastWaiting) << std::endl; - }else if( d_quantEngine->hasAddedLemma() ){ - Trace("inst-engine") << "Added lemmas = " << (d_quantEngine->getNumLemmasWaiting()-lastWaiting) << std::endl; - } - }else{ - d_quants.clear(); + } + Trace("inst-engine-debug") + << "InstEngine: check: # asserted quantifiers " << d_quants.size() << "/"; + Trace("inst-engine-debug") << nquant << " " << quantActive << std::endl; + if (quantActive) + { + unsigned lastWaiting = d_quantEngine->getNumLemmasWaiting(); + doInstantiationRound(e); + if (d_quantEngine->inConflict()) + { + Assert(d_quantEngine->getNumLemmasWaiting() > lastWaiting); + Trace("inst-engine") << "Conflict, added lemmas = " + << (d_quantEngine->getNumLemmasWaiting() + - lastWaiting) + << std::endl; } - if( Trace.isOn("inst-engine") ){ - double clSet2 = double(clock())/double(CLOCKS_PER_SEC); - Trace("inst-engine") << "Finished instantiation engine, time = " << (clSet2-clSet) << std::endl; + else if (d_quantEngine->hasAddedLemma()) + { + Trace("inst-engine") << "Added lemmas = " + << (d_quantEngine->getNumLemmasWaiting() + - lastWaiting) + << std::endl; } } + else + { + d_quants.clear(); + } + if (Trace.isOn("inst-engine")) + { + double clSet2 = double(clock()) / double(CLOCKS_PER_SEC); + Trace("inst-engine") << "Finished instantiation engine, time = " + << (clSet2 - clSet) << std::endl; + } } bool InstantiationEngine::checkCompleteFor( Node q ) { @@ -185,7 +209,7 @@ void InstantiationEngine::checkOwnership(Node q) void InstantiationEngine::registerQuantifier(Node q) { - if (!d_quantEngine->hasOwnership(q, this)) + if (!shouldProcess(q)) { return; } @@ -225,3 +249,22 @@ void InstantiationEngine::addUserNoPattern(Node q, Node pat) { d_i_ag->addUserNoPattern(q, pat); } } + +bool InstantiationEngine::shouldProcess(Node q) +{ + if (!d_quantEngine->hasOwnership(q, this)) + { + return false; + } + // also ignore internal quantifiers + QuantAttributes* qattr = d_quantEngine->getQuantAttributes(); + if (qattr->isInternal(q)) + { + return false; + } + return true; +} + +} // namespace quantifiers +} // namespace theory +} // namespace CVC4 diff --git a/src/theory/quantifiers/ematching/instantiation_engine.h b/src/theory/quantifiers/ematching/instantiation_engine.h index 1bd3af99c..f2f013f1c 100644 --- a/src/theory/quantifiers/ematching/instantiation_engine.h +++ b/src/theory/quantifiers/ematching/instantiation_engine.h @@ -88,6 +88,8 @@ class InstantiationEngine : public QuantifiersModule { std::string identify() const override { return "InstEngine"; } private: + /** Return true if this module should process quantified formula q */ + bool shouldProcess(Node q); /** for computing relevance of quantifiers */ std::unique_ptr<QuantRelevance> d_quant_rel; }; /* class InstantiationEngine */ diff --git a/src/theory/quantifiers/quantifiers_attributes.cpp b/src/theory/quantifiers/quantifiers_attributes.cpp index 8961a7c90..808137fd6 100644 --- a/src/theory/quantifiers/quantifiers_attributes.cpp +++ b/src/theory/quantifiers/quantifiers_attributes.cpp @@ -30,7 +30,8 @@ namespace quantifiers { bool QAttributes::isStandard() const { - return !d_sygus && !d_quant_elim && !isFunDef() && d_name.isNull(); + return !d_sygus && !d_quant_elim && !isFunDef() && d_name.isNull() + && !d_isInternal; } QuantAttributes::QuantAttributes( QuantifiersEngine * qe ) : @@ -250,6 +251,11 @@ void QuantAttributes::computeQuantAttributes( Node q, QAttributes& qa ){ qa.d_quant_elim_partial = true; //don't set owner, should happen naturally } + if (avar.getAttribute(InternalQuantAttribute())) + { + Trace("quant-attr") << "Attribute : internal : " << q << std::endl; + qa.d_isInternal = true; + } if( avar.hasAttribute(QuantIdNumAttribute()) ){ qa.d_qid_num = avar; Trace("quant-attr") << "Attribute : id number " << qa.d_qid_num.getAttribute(QuantIdNumAttribute()) << " : " << q << std::endl; @@ -304,6 +310,16 @@ bool QuantAttributes::isQuantElimPartial( Node q ) { } } +bool QuantAttributes::isInternal(Node q) const +{ + std::map<Node, QAttributes>::const_iterator it = d_qattr.find(q); + if (it != d_qattr.end()) + { + return it->second.d_isInternal; + } + return false; +} + Node QuantAttributes::getQuantName(Node q) const { std::map<Node, QAttributes>::const_iterator it = d_qattr.find(q); diff --git a/src/theory/quantifiers/quantifiers_attributes.h b/src/theory/quantifiers/quantifiers_attributes.h index e9abbc9ed..88f291b2b 100644 --- a/src/theory/quantifiers/quantifiers_attributes.h +++ b/src/theory/quantifiers/quantifiers_attributes.h @@ -88,11 +88,24 @@ struct SygusVarToTermAttributeId typedef expr::Attribute<SygusVarToTermAttributeId, Node> SygusVarToTermAttribute; -namespace quantifiers { +/** + * Attribute true for quantifiers that have been internally generated, e.g. + * for reductions of string operators. + * + * Currently, this attribute is used for indicating that E-matching should + * not be applied, as E-matching should not be applied to quantifiers + * generated for strings reductions. + * + * This attribute can potentially be generalized to an identifier indicating + * the internal source of the quantified formula (of which strings reduction + * is one possibility). + */ +struct InternalQuantAttributeId +{ +}; +typedef expr::Attribute<InternalQuantAttributeId, bool> InternalQuantAttribute; -/** Attribute priority for rewrite rules */ -//struct RrPriorityAttributeId {}; -//typedef expr::Attribute< RrPriorityAttributeId, uint64_t > RrPriorityAttribute; +namespace quantifiers { /** This struct stores attributes for a single quantified formula */ struct QAttributes @@ -103,7 +116,8 @@ struct QAttributes d_sygus(false), d_qinstLevel(-1), d_quant_elim(false), - d_quant_elim_partial(false) + d_quant_elim_partial(false), + d_isInternal(false) { } ~QAttributes(){} @@ -123,6 +137,8 @@ struct QAttributes bool d_quant_elim; /** is this formula marked for partial quantifier elimination? */ bool d_quant_elim_partial; + /** Is this formula internally generated? */ + bool d_isInternal; /** the instantiation pattern list for this quantified formula (its 3rd child) */ Node d_ipl; @@ -192,12 +208,12 @@ public: bool isSygus( Node q ); /** get instantiation level */ int getQuantInstLevel( Node q ); - /** get rewrite rule priority */ - int getRewriteRulePriority( Node q ); /** is quant elim */ bool isQuantElim( Node q ); /** is quant elim partial */ bool isQuantElimPartial( Node q ); + /** is internal quantifier */ + bool isInternal(Node q) const; /** get quant name, which is used for :qid */ Node getQuantName(Node q) const; /** get (internal) quant id num */ diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp index 820e6f70f..966964bc8 100644 --- a/src/theory/strings/theory_strings_preprocess.cpp +++ b/src/theory/strings/theory_strings_preprocess.cpp @@ -23,6 +23,7 @@ #include "options/strings_options.h" #include "proof/proof_manager.h" #include "smt/logic_exception.h" +#include "theory/quantifiers/quantifiers_attributes.h" #include "theory/strings/arith_entail.h" #include "theory/strings/sequences_rewriter.h" #include "theory/strings/word.h" @@ -34,6 +35,13 @@ namespace CVC4 { namespace theory { namespace strings { +/** Mapping to a dummy node for marking an attribute on internal quantified + * formulas */ +struct QInternalVarAttributeId +{ +}; +typedef expr::Attribute<QInternalVarAttributeId, Node> QInternalVarAttribute; + StringsPreprocess::StringsPreprocess(SkolemCache* sc, context::UserContext* u, SequencesStatistics& stats) @@ -295,7 +303,7 @@ Node StringsPreprocess::reduce(Node t, Node ux1lem = nm->mkNode(GEQ, n, ux1); lem = nm->mkNode(OR, g.negate(), nm->mkNode(AND, eq, cb, ux1lem)); - lem = nm->mkNode(FORALL, xbv, lem); + lem = mkForallInternal(xbv, lem); conc.push_back(lem); Node nonneg = nm->mkNode(GEQ, n, zero); @@ -382,7 +390,7 @@ Node StringsPreprocess::reduce(Node t, Node ux1lem = nm->mkNode(GEQ, stoit, ux1); lem = nm->mkNode(OR, g.negate(), nm->mkNode(AND, eq, cb, ux1lem)); - lem = nm->mkNode(FORALL, xbv, lem); + lem = mkForallInternal(xbv, lem); conc2.push_back(lem); Node sneg = nm->mkNode(LT, stoit, zero); @@ -519,8 +527,8 @@ Node StringsPreprocess::reduce(Node t, flem.push_back( ufip1.eqNode(nm->mkNode(PLUS, ii, nm->mkNode(STRING_LENGTH, y)))); - Node q = nm->mkNode( - FORALL, bvli, nm->mkNode(OR, bound.negate(), nm->mkNode(AND, flem))); + Node body = nm->mkNode(OR, bound.negate(), nm->mkNode(AND, flem)); + Node q = mkForallInternal(bvli, body); lem.push_back(q); // assert: @@ -689,8 +697,8 @@ Node StringsPreprocess::reduce(Node t, .eqNode(nm->mkNode( STRING_CONCAT, pfxMatch, z, nm->mkNode(APPLY_UF, us, ip1)))); - Node forall = nm->mkNode( - FORALL, bvli, nm->mkNode(OR, bound.negate(), nm->mkNode(AND, flem))); + Node body = nm->mkNode(OR, bound.negate(), nm->mkNode(AND, flem)); + Node forall = mkForallInternal(bvli, body); lemmas.push_back(forall); // IF in_re(x, re.++(_*, y', _*)) @@ -745,8 +753,8 @@ Node StringsPreprocess::reduce(Node t, Node bound = nm->mkNode(AND, nm->mkNode(LEQ, zero, i), nm->mkNode(LT, i, lenr)); - Node rangeA = - nm->mkNode(FORALL, bvi, nm->mkNode(OR, bound.negate(), ri.eqNode(res))); + Node body = nm->mkNode(OR, bound.negate(), ri.eqNode(res)); + Node rangeA = mkForallInternal(bvi, body); // upper 65 ... 90 // lower 97 ... 122 @@ -780,8 +788,8 @@ Node StringsPreprocess::reduce(Node t, Node bound = nm->mkNode(AND, nm->mkNode(LEQ, zero, i), nm->mkNode(LT, i, lenr)); - Node rangeA = nm->mkNode( - FORALL, bvi, nm->mkNode(OR, bound.negate(), ssr.eqNode(ssx))); + Node body = nm->mkNode(OR, bound.negate(), ssr.eqNode(ssx)); + Node rangeA = mkForallInternal(bvi, body); // assert: // len(r) = len(x) ^ // forall i. 0 <= i < len(r) => @@ -982,6 +990,30 @@ void StringsPreprocess::processAssertions( std::vector< Node > &vec_node ){ } } +Node StringsPreprocess::mkForallInternal(Node bvl, Node body) +{ + NodeManager* nm = NodeManager::currentNM(); + QInternalVarAttribute qiva; + Node qvar; + if (bvl.hasAttribute(qiva)) + { + qvar = bvl.getAttribute(qiva); + } + else + { + qvar = nm->mkSkolem("qinternal", nm->booleanType()); + // this dummy variable marks that the quantified formula is internal + qvar.setAttribute(InternalQuantAttribute(), true); + // remember the dummy variable + bvl.setAttribute(qiva, qvar); + } + // make the internal attribute, and put it in a singleton list + Node ip = nm->mkNode(INST_ATTRIBUTE, qvar); + Node ipl = nm->mkNode(INST_PATTERN_LIST, ip); + // make the overall formula + return nm->mkNode(FORALL, bvl, body, ipl); +} + }/* CVC4::theory::strings namespace */ }/* CVC4::theory namespace */ }/* CVC4 namespace */ diff --git a/src/theory/strings/theory_strings_preprocess.h b/src/theory/strings/theory_strings_preprocess.h index f84ae4247..124a09a4c 100644 --- a/src/theory/strings/theory_strings_preprocess.h +++ b/src/theory/strings/theory_strings_preprocess.h @@ -100,6 +100,14 @@ class StringsPreprocess { Node simplifyRec(Node t, std::vector<Node>& asserts, std::map<Node, Node>& visited); + /** + * Make internal quantified formula with bound variable list bvl and body. + * Internally, we get a node corresponding to marking a quantified formula as + * an "internal" one. This node is provided as the third argument of the + * FORALL returned by this method. This ensures that E-matching is not applied + * to the quantified formula. + */ + static Node mkForallInternal(Node bvl, Node body); }; }/* CVC4::theory::strings namespace */ |