This does not disable E-matching when strings are enabled with --strings-exp, due to potential applications where strings are combined with user-provided quantified formulas.
Notice that by default, we do not want E-matching applied to quantified formulas corresponding to reductions for extended string functions. To correct this, all quantified formulas generated by strings are marked with an "internal quantified formula" attribute, which causes E-matching to ignore them. This feature can in theory be generalized later for other internal sources of quantified formulas.
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())
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())
{
#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(),
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 ) {
void InstantiationEngine::registerQuantifier(Node q)
{
- if (!d_quantEngine->hasOwnership(q, this))
+ if (!shouldProcess(q))
{
return;
}
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
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 */
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 ) :
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;
}
}
+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);
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
d_sygus(false),
d_qinstLevel(-1),
d_quant_elim(false),
- d_quant_elim_partial(false)
+ d_quant_elim_partial(false),
+ d_isInternal(false)
{
}
~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;
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 */
#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"
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)
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);
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);
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:
.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', _*))
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
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) =>
}
}
+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 */
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 */
regress1/quantifiers/set-choice-koikonomou.cvc
regress1/quantifiers/set8.smt2
regress1/quantifiers/seu169+1.smt2
+ regress1/quantifiers/seq-solved-enum.smt2
+ regress1/quantifiers/seq-unsolved-ematch.smt2
regress1/quantifiers/small-pipeline-fixpoint-3.smt2
regress1/quantifiers/smtcomp-qbv-053118.smt2
regress1/quantifiers/smtlib384a03.smt2
--- /dev/null
+; COMMAND-LINE: --strings-exp --full-saturate-quant
+; EXPECT: unsat
+(set-logic ALL)
+
+(declare-fun s () (Seq Int))
+
+(declare-fun x () Int)
+
+(declare-fun y () Int)
+
+(assert (and (<= 0 x) (<= x y) (< y (seq.len s))))
+
+(assert (forall ((i Int) (j Int)) (=> (and (<= 0 i) (<= i j) (< j (seq.len s))) (<= (seq.nth s i) (seq.nth s j)))))
+
+(assert (not (<= (seq.nth s x) (seq.nth s y))))
+
+(check-sat)
--- /dev/null
+; COMMAND-LINE: --strings-exp --full-saturate-quant
+; EXPECT: unsat
+(set-logic ALL)
+
+(declare-fun s () (Seq Int))
+
+(declare-fun x () Int)
+
+(assert (and (<= 0 x) (< x (seq.len s))))
+
+(assert (forall ((i Int)) (=> (and (<= 0 i) (< i (seq.len s))) (= (seq.nth s i) 0))))
+
+(assert (not (= (seq.nth s x) 0)))
+
+(check-sat)
projects / cvc5.git / commitdiff