summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/smt/set_defaults.cpp9
-rw-r--r--src/theory/quantifiers/ematching/instantiation_engine.cpp113
-rw-r--r--src/theory/quantifiers/ematching/instantiation_engine.h2
-rw-r--r--src/theory/quantifiers/quantifiers_attributes.cpp18
-rw-r--r--src/theory/quantifiers/quantifiers_attributes.h30
-rw-r--r--src/theory/strings/theory_strings_preprocess.cpp52
-rw-r--r--src/theory/strings/theory_strings_preprocess.h8
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 */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback