summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/CMakeLists.txt2
-rw-r--r--src/theory/strings/inference_manager.cpp46
-rw-r--r--src/theory/strings/inference_manager.h26
-rw-r--r--src/theory/strings/regexp_solver.cpp10
-rw-r--r--src/theory/strings/regexp_solver.h4
-rw-r--r--src/theory/strings/solver_state.cpp283
-rw-r--r--src/theory/strings/solver_state.h187
-rw-r--r--src/theory/strings/theory_strings.cpp771
-rw-r--r--src/theory/strings/theory_strings.h159
-rw-r--r--src/theory/strings/theory_strings_utils.cpp26
-rw-r--r--src/theory/strings/theory_strings_utils.h22
11 files changed, 879 insertions, 657 deletions
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index a24a2e31a..14d4ef8ae 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -662,6 +662,8 @@ libcvc4_add_sources(
theory/strings/regexp_solver.h
theory/strings/skolem_cache.cpp
theory/strings/skolem_cache.h
+ theory/strings/solver_state.cpp
+ theory/strings/solver_state.h
theory/strings/theory_strings.cpp
theory/strings/theory_strings.h
theory/strings/theory_strings_preprocess.cpp
diff --git a/src/theory/strings/inference_manager.cpp b/src/theory/strings/inference_manager.cpp
index 56a46eed5..5c08fdee3 100644
--- a/src/theory/strings/inference_manager.cpp
+++ b/src/theory/strings/inference_manager.cpp
@@ -32,9 +32,9 @@ namespace strings {
InferenceManager::InferenceManager(TheoryStrings& p,
context::Context* c,
context::UserContext* u,
- eq::EqualityEngine& ee,
+ SolverState& s,
OutputChannel& out)
- : d_parent(p), d_ee(ee), d_out(out), d_keep(c)
+ : d_parent(p), d_state(s), d_out(out), d_keep(c)
{
d_true = NodeManager::currentNM()->mkConst(true);
d_false = NodeManager::currentNM()->mkConst(false);
@@ -63,15 +63,15 @@ bool InferenceManager::sendInternalInference(std::vector<Node>& exp,
{
for (unsigned i = 0; i < 2; i++)
{
- if (!lit[i].isConst() && !d_parent.hasTerm(lit[i]))
+ if (!lit[i].isConst() && !d_state.hasTerm(lit[i]))
{
// introduces a new non-constant term, do not infer
return false;
}
}
// does it already hold?
- if (pol ? d_parent.areEqual(lit[0], lit[1])
- : d_parent.areDisequal(lit[0], lit[1]))
+ if (pol ? d_state.areEqual(lit[0], lit[1])
+ : d_state.areDisequal(lit[0], lit[1]))
{
return true;
}
@@ -85,12 +85,12 @@ bool InferenceManager::sendInternalInference(std::vector<Node>& exp,
return true;
}
}
- else if (!d_parent.hasTerm(lit))
+ else if (!d_state.hasTerm(lit))
{
// introduces a new non-constant term, do not infer
return false;
}
- else if (d_parent.areEqual(lit, pol ? d_true : d_false))
+ else if (d_state.areEqual(lit, pol ? d_true : d_false))
{
// already holds
return true;
@@ -192,7 +192,7 @@ void InferenceManager::sendLemma(Node ant, Node conc, const char* c)
Trace("strings-assert")
<< "(assert (not " << ant << ")) ; conflict " << c << std::endl;
d_out.conflict(ant);
- d_parent.d_conflict = true;
+ d_state.setConflict();
return;
}
Node lem;
@@ -279,10 +279,31 @@ void InferenceManager::sendPhaseRequirement(Node lit, bool pol)
d_pendingReqPhase[lit] = pol;
}
+void InferenceManager::addToExplanation(Node a,
+ Node b,
+ std::vector<Node>& exp) const
+{
+ if (a != b)
+ {
+ Debug("strings-explain")
+ << "Add to explanation : " << a << " == " << b << std::endl;
+ Assert(d_state.areEqual(a, b));
+ exp.push_back(a.eqNode(b));
+ }
+}
+
+void InferenceManager::addToExplanation(Node lit, std::vector<Node>& exp) const
+{
+ if (!lit.isNull())
+ {
+ exp.push_back(lit);
+ }
+}
+
void InferenceManager::doPendingFacts()
{
size_t i = 0;
- while (!hasConflict() && i < d_pending.size())
+ while (!d_state.isInConflict() && i < d_pending.size())
{
Node fact = d_pending[i];
Node exp = d_pendingExp[fact];
@@ -309,7 +330,7 @@ void InferenceManager::doPendingFacts()
void InferenceManager::doPendingLemmas()
{
- if (!hasConflict())
+ if (!d_state.isInConflict())
{
for (const Node& lc : d_pendingLem)
{
@@ -327,7 +348,10 @@ void InferenceManager::doPendingLemmas()
d_pendingReqPhase.clear();
}
-bool InferenceManager::hasConflict() const { return d_parent.d_conflict; }
+bool InferenceManager::hasProcessed() const
+{
+ return d_state.isInConflict() || !d_pendingLem.empty() || !d_pending.empty();
+}
void InferenceManager::inferSubstitutionProxyVars(
Node n,
diff --git a/src/theory/strings/inference_manager.h b/src/theory/strings/inference_manager.h
index bb78b4a1a..85855fab9 100644
--- a/src/theory/strings/inference_manager.h
+++ b/src/theory/strings/inference_manager.h
@@ -25,6 +25,7 @@
#include "expr/node.h"
#include "theory/output_channel.h"
#include "theory/strings/infer_info.h"
+#include "theory/strings/solver_state.h"
#include "theory/uf/equality_engine.h"
namespace CVC4 {
@@ -70,7 +71,7 @@ class InferenceManager
InferenceManager(TheoryStrings& p,
context::Context* c,
context::UserContext* u,
- eq::EqualityEngine& ee,
+ SolverState& s,
OutputChannel& out);
~InferenceManager() {}
@@ -162,6 +163,15 @@ class InferenceManager
* decided with polarity pol.
*/
void sendPhaseRequirement(Node lit, bool pol);
+ //----------------------------constructing antecedants
+ /**
+ * Adds equality a = b to the vector exp if a and b are distinct terms. It
+ * must be the case that areEqual( a, b ) holds in this context.
+ */
+ void addToExplanation(Node a, Node b, std::vector<Node>& exp) const;
+ /** Adds lit to the vector exp if it is non-null */
+ void addToExplanation(Node lit, std::vector<Node>& exp) const;
+ //----------------------------end constructing antecedants
/** Do pending facts
*
* This method asserts pending facts (d_pending) with explanations
@@ -196,16 +206,11 @@ class InferenceManager
* this returns true if we have a pending fact or lemma, or have encountered
* a conflict.
*/
- bool hasProcessed() const
- {
- return hasConflict() || !d_pendingLem.empty() || !d_pending.empty();
- }
+ bool hasProcessed() const;
/** Do we have a pending fact to add to the equality engine? */
bool hasPendingFact() const { return !d_pending.empty(); }
/** Do we have a pending lemma to send on the output channel? */
bool hasPendingLemma() const { return !d_pendingLem.empty(); }
- /** Are we in conflict? */
- bool hasConflict() const;
private:
/**
@@ -229,11 +234,10 @@ class InferenceManager
/** the parent theory of strings object */
TheoryStrings& d_parent;
- /** the equality engine
- *
- * This is a reference to the equality engine of the theory of strings.
+ /**
+ * This is a reference to the solver state of the theory of strings.
*/
- eq::EqualityEngine& d_ee;
+ SolverState& d_state;
/** the output channel
*
* This is a reference to the output channel of the theory of strings.
diff --git a/src/theory/strings/regexp_solver.cpp b/src/theory/strings/regexp_solver.cpp
index db4c9012c..0e44c9461 100644
--- a/src/theory/strings/regexp_solver.cpp
+++ b/src/theory/strings/regexp_solver.cpp
@@ -34,10 +34,12 @@ namespace theory {
namespace strings {
RegExpSolver::RegExpSolver(TheoryStrings& p,
+ SolverState& s,
InferenceManager& im,
context::Context* c,
context::UserContext* u)
: d_parent(p),
+ d_state(s),
d_im(im),
d_regexp_ucached(u),
d_regexp_ccached(c),
@@ -134,7 +136,7 @@ void RegExpSolver::check(const std::map<Node, std::vector<Node> >& mems)
bool flag = true;
Node x = atom[0];
Node r = atom[1];
- Assert(rep == d_parent.getRepresentative(x));
+ Assert(rep == d_state.getRepresentative(x));
// The following code takes normal forms into account for the purposes
// of simplifying a regular expression membership x in R. For example,
// if x = "A" in the current context, then we may be interested in
@@ -250,7 +252,7 @@ void RegExpSolver::check(const std::map<Node, std::vector<Node> >& mems)
repUnfold.insert(rep);
}
}
- if (d_im.hasConflict())
+ if (d_state.isInConflict())
{
break;
}
@@ -259,7 +261,7 @@ void RegExpSolver::check(const std::map<Node, std::vector<Node> >& mems)
}
if (addedLemma)
{
- if (!d_im.hasConflict())
+ if (!d_state.isInConflict())
{
for (unsigned i = 0; i < processed.size(); i++)
{
@@ -468,7 +470,7 @@ bool RegExpSolver::checkEqcIntersect(const std::vector<Node>& mems)
bool RegExpSolver::checkPDerivative(
Node x, Node r, Node atom, bool& addedLemma, std::vector<Node>& nf_exp)
{
- if (d_parent.areEqual(x, d_emptyString))
+ if (d_state.areEqual(x, d_emptyString))
{
Node exp;
switch (d_regexp_opr.delta(r, exp))
diff --git a/src/theory/strings/regexp_solver.h b/src/theory/strings/regexp_solver.h
index c4d6afda0..0b84ebc79 100644
--- a/src/theory/strings/regexp_solver.h
+++ b/src/theory/strings/regexp_solver.h
@@ -25,6 +25,7 @@
#include "expr/node.h"
#include "theory/strings/inference_manager.h"
#include "theory/strings/regexp_operation.h"
+#include "theory/strings/solver_state.h"
#include "util/regexp.h"
namespace CVC4 {
@@ -44,6 +45,7 @@ class RegExpSolver
public:
RegExpSolver(TheoryStrings& p,
+ SolverState& s,
InferenceManager& im,
context::Context* c,
context::UserContext* u);
@@ -100,6 +102,8 @@ class RegExpSolver
Node d_false;
/** the parent of this object */
TheoryStrings& d_parent;
+ /** The solver state of the parent of this object */
+ SolverState& d_state;
/** the output channel of the parent of this object */
InferenceManager& d_im;
// check membership constraints
diff --git a/src/theory/strings/solver_state.cpp b/src/theory/strings/solver_state.cpp
new file mode 100644
index 000000000..c370558b5
--- /dev/null
+++ b/src/theory/strings/solver_state.cpp
@@ -0,0 +1,283 @@
+/********************* */
+/*! \file solver_state.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2019 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 the solver state of the theory of strings.
+ **/
+
+#include "theory/strings/solver_state.h"
+
+#include "theory/strings/theory_strings_utils.h"
+
+using namespace std;
+using namespace CVC4::context;
+using namespace CVC4::kind;
+
+namespace CVC4 {
+namespace theory {
+namespace strings {
+
+EqcInfo::EqcInfo(context::Context* c)
+ : d_lengthTerm(c),
+ d_codeTerm(c),
+ d_cardinalityLemK(c),
+ d_normalizedLength(c),
+ d_prefixC(c),
+ d_suffixC(c)
+{
+}
+
+Node EqcInfo::addEndpointConst(Node t, Node c, bool isSuf)
+{
+ // check conflict
+ Node prev = isSuf ? d_suffixC : d_prefixC;
+ if (!prev.isNull())
+ {
+ Trace("strings-eager-pconf-debug") << "Check conflict " << prev << ", " << t
+ << " post=" << isSuf << std::endl;
+ Node prevC = utils::getConstantEndpoint(prev, isSuf);
+ Assert(!prevC.isNull());
+ Assert(prevC.getKind() == CONST_STRING);
+ if (c.isNull())
+ {
+ c = utils::getConstantEndpoint(t, isSuf);
+ Assert(!c.isNull());
+ }
+ Assert(c.getKind() == CONST_STRING);
+ bool conflict = false;
+ // if the constant prefixes are different
+ if (c != prevC)
+ {
+ // conflicts between constants should be handled by equality engine
+ Assert(!t.isConst() || !prev.isConst());
+ Trace("strings-eager-pconf-debug")
+ << "Check conflict constants " << prevC << ", " << c << std::endl;
+ const String& ps = prevC.getConst<String>();
+ const String& cs = c.getConst<String>();
+ unsigned pvs = ps.size();
+ unsigned cvs = cs.size();
+ if (pvs == cvs || (pvs > cvs && t.isConst())
+ || (cvs > pvs && prev.isConst()))
+ {
+ // If equal length, cannot be equal due to node check above.
+ // If one is fully constant and has less length than the other, then the
+ // other will not fit and we are in conflict.
+ conflict = true;
+ }
+ else
+ {
+ const String& larges = pvs > cvs ? ps : cs;
+ const String& smalls = pvs > cvs ? cs : ps;
+ if (isSuf)
+ {
+ conflict = !larges.hasSuffix(smalls);
+ }
+ else
+ {
+ conflict = !larges.hasPrefix(smalls);
+ }
+ }
+ if (!conflict && (pvs > cvs || prev.isConst()))
+ {
+ // current is subsumed, either shorter prefix or the other is a full
+ // constant
+ return Node::null();
+ }
+ }
+ else if (!t.isConst())
+ {
+ // current is subsumed since the other may be a full constant
+ return Node::null();
+ }
+ if (conflict)
+ {
+ Trace("strings-eager-pconf")
+ << "Conflict for " << prevC << ", " << c << std::endl;
+ std::vector<Node> ccs;
+ Node r[2];
+ for (unsigned i = 0; i < 2; i++)
+ {
+ Node tp = i == 0 ? t : prev;
+ if (tp.getKind() == STRING_IN_REGEXP)
+ {
+ ccs.push_back(tp);
+ r[i] = tp[0];
+ }
+ else
+ {
+ r[i] = tp;
+ }
+ }
+ if (r[0] != r[1])
+ {
+ ccs.push_back(r[0].eqNode(r[1]));
+ }
+ Assert(!ccs.empty());
+ Node ret =
+ ccs.size() == 1 ? ccs[0] : NodeManager::currentNM()->mkNode(AND, ccs);
+ Trace("strings-eager-pconf")
+ << "String: eager prefix conflict: " << ret << std::endl;
+ return ret;
+ }
+ }
+ if (isSuf)
+ {
+ d_suffixC = t;
+ }
+ else
+ {
+ d_prefixC = t;
+ }
+ return Node::null();
+}
+
+SolverState::SolverState(context::Context* c, eq::EqualityEngine& ee)
+ : d_context(c), d_ee(ee), d_conflict(c, false), d_pendingConflict(c)
+{
+}
+SolverState::~SolverState()
+{
+ for (std::pair<const Node, EqcInfo*>& it : d_eqcInfo)
+ {
+ delete it.second;
+ }
+}
+
+Node SolverState::getRepresentative(Node t) const
+{
+ if (d_ee.hasTerm(t))
+ {
+ return d_ee.getRepresentative(t);
+ }
+ return t;
+}
+
+bool SolverState::hasTerm(Node a) const { return d_ee.hasTerm(a); }
+
+bool SolverState::areEqual(Node a, Node b) const
+{
+ if (a == b)
+ {
+ return true;
+ }
+ else if (hasTerm(a) && hasTerm(b))
+ {
+ return d_ee.areEqual(a, b);
+ }
+ return false;
+}
+
+bool SolverState::areDisequal(Node a, Node b) const
+{
+ if (a == b)
+ {
+ return false;
+ }
+ else if (hasTerm(a) && hasTerm(b))
+ {
+ Node ar = d_ee.getRepresentative(a);
+ Node br = d_ee.getRepresentative(b);
+ return (ar != br && ar.isConst() && br.isConst())
+ || d_ee.areDisequal(ar, br, false);
+ }
+ Node ar = getRepresentative(a);
+ Node br = getRepresentative(b);
+ return ar != br && ar.isConst() && br.isConst();
+}
+
+eq::EqualityEngine* SolverState::getEqualityEngine() const { return &d_ee; }
+
+EqcInfo* SolverState::getOrMakeEqcInfo(Node eqc, bool doMake)
+{
+ std::map<Node, EqcInfo*>::iterator eqc_i = d_eqcInfo.find(eqc);
+ if (eqc_i != d_eqcInfo.end())
+ {
+ return eqc_i->second;
+ }
+ if (doMake)
+ {
+ EqcInfo* ei = new EqcInfo(d_context);
+ d_eqcInfo[eqc] = ei;
+ return ei;
+ }
+ return nullptr;
+}
+
+void SolverState::addEndpointsToEqcInfo(Node t, Node concat, Node eqc)
+{
+ Assert(concat.getKind() == STRING_CONCAT
+ || concat.getKind() == REGEXP_CONCAT);
+ EqcInfo* ei = nullptr;
+ // check each side
+ for (unsigned r = 0; r < 2; r++)
+ {
+ unsigned index = r == 0 ? 0 : concat.getNumChildren() - 1;
+ Node c = utils::getConstantComponent(concat[index]);
+ if (!c.isNull())
+ {
+ if (ei == nullptr)
+ {
+ ei = getOrMakeEqcInfo(eqc);
+ }
+ Trace("strings-eager-pconf-debug")
+ << "New term: " << concat << " for " << t << " with prefix " << c
+ << " (" << (r == 1) << ")" << std::endl;
+ setPendingConflictWhen(ei->addEndpointConst(t, c, r == 1));
+ }
+ }
+}
+
+Node SolverState::getLengthExp(Node t, std::vector<Node>& exp, Node te)
+{
+ Assert(areEqual(t, te));
+ Node lt = utils::mkNLength(te);
+ if (hasTerm(lt))
+ {
+ // use own length if it exists, leads to shorter explanation
+ return lt;
+ }
+ EqcInfo* ei = getOrMakeEqcInfo(t, false);
+ Node lengthTerm = ei ? ei->d_lengthTerm : Node::null();
+ if (lengthTerm.isNull())
+ {
+ // typically shouldnt be necessary
+ lengthTerm = t;
+ }
+ Debug("strings") << "SolverState::getLengthTerm " << t << " is " << lengthTerm
+ << std::endl;
+ if (te != lengthTerm)
+ {
+ exp.push_back(te.eqNode(lengthTerm));
+ }
+ return Rewriter::rewrite(
+ NodeManager::currentNM()->mkNode(STRING_LENGTH, lengthTerm));
+}
+
+Node SolverState::getLength(Node t, std::vector<Node>& exp)
+{
+ return getLengthExp(t, exp, t);
+}
+
+void SolverState::setConflict() { d_conflict = true; }
+bool SolverState::isInConflict() const { return d_conflict; }
+
+void SolverState::setPendingConflictWhen(Node conf)
+{
+ if (!conf.isNull() && d_pendingConflict.get().isNull())
+ {
+ d_pendingConflict = conf;
+ }
+}
+
+Node SolverState::getPendingConflict() const { return d_pendingConflict; }
+
+} // namespace strings
+} // namespace theory
+} // namespace CVC4
diff --git a/src/theory/strings/solver_state.h b/src/theory/strings/solver_state.h
new file mode 100644
index 000000000..f14b4b4af
--- /dev/null
+++ b/src/theory/strings/solver_state.h
@@ -0,0 +1,187 @@
+/********************* */
+/*! \file solver_state.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2019 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 The solver state of the theory of strings
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__THEORY__STRINGS__SOLVER_STATE_H
+#define CVC4__THEORY__STRINGS__SOLVER_STATE_H
+
+#include <map>
+
+#include "context/cdo.h"
+#include "context/context.h"
+#include "expr/node.h"
+#include "theory/uf/equality_engine.h"
+
+namespace CVC4 {
+namespace theory {
+namespace strings {
+
+/**
+ * SAT-context-dependent information about an equivalence class. This
+ * information is updated eagerly as assertions are processed by the theory of
+ * strings at standard effort.
+ */
+class EqcInfo
+{
+ public:
+ EqcInfo(context::Context* c);
+ ~EqcInfo() {}
+ /** add prefix constant
+ *
+ * This informs this equivalence class info that a term t in its
+ * equivalence class has a constant prefix (if isSuf=true) or suffix
+ * (if isSuf=false). The constant c (if non-null) is the value of that
+ * constant, if it has been computed already.
+ *
+ * If this method returns a non-null node ret, then ret is a conjunction
+ * corresponding to a conflict that holds in the current context.
+ */
+ Node addEndpointConst(Node t, Node c, bool isSuf);
+ /**
+ * If non-null, this is a term x from this eq class such that str.len( x )
+ * occurs as a term in this SAT context.
+ */
+ context::CDO<Node> d_lengthTerm;
+ /**
+ * If non-null, this is a term x from this eq class such that str.code( x )
+ * occurs as a term in this SAT context.
+ */
+ context::CDO<Node> d_codeTerm;
+ context::CDO<unsigned> d_cardinalityLemK;
+ context::CDO<Node> d_normalizedLength;
+ /**
+ * A node that explains the longest constant prefix known of this
+ * equivalence class. This can either be:
+ * (1) A term from this equivalence class, including a constant "ABC" or
+ * concatenation term (str.++ "ABC" ...), or
+ * (2) A membership of the form (str.in.re x R) where x is in this
+ * equivalence class and R is a regular expression of the form
+ * (str.to.re "ABC") or (re.++ (str.to.re "ABC") ...).
+ */
+ context::CDO<Node> d_prefixC;
+ /** same as above, for suffix. */
+ context::CDO<Node> d_suffixC;
+};
+
+/**
+ * Solver state for strings.
+ *
+ * The purpose of this class is track and provide query functions for the state
+ * of the assertions for the theory of strings. This includes:
+ * (1) Equality queries via the equality engine,
+ * (2) Whether the set of assertions is in conflict.
+ * (3) Equivalence class information as in the class above.
+ */
+class SolverState
+{
+ public:
+ SolverState(context::Context* c, eq::EqualityEngine& ee);
+ ~SolverState();
+ //-------------------------------------- equality information
+ /**
+ * Get the representative of t in the equality engine of this class, or t
+ * itself if it is not registered as a term.
+ */
+ Node getRepresentative(Node t) const;
+ /** Is t registered as a term in the equality engine of this class? */
+ bool hasTerm(Node a) const;
+ /**
+ * Are a and b equal according to the equality engine of this class? Also
+ * returns true if a and b are identical.
+ */
+ bool areEqual(Node a, Node b) const;
+ /**
+ * Are a and b disequal according to the equality engine of this class? Also
+ * returns true if the representative of a and b are distinct constants.
+ */
+ bool areDisequal(Node a, Node b) const;
+ /** get equality engine */
+ eq::EqualityEngine* getEqualityEngine() const;
+ //-------------------------------------- end equality information
+ //------------------------------------------ conflicts
+ /**
+ * Set that the current state of the solver is in conflict. This should be
+ * called immediately after a call to conflict(...) on the output channel of
+ * the theory of strings.
+ */
+ void setConflict();
+ /** Are we currently in conflict? */
+ bool isInConflict() const;
+ /** set pending conflict
+ *
+ * If conf is non-null, this is called when conf is a conjunction of literals
+ * that hold in the current context that are unsatisfiable. It is set as the
+ * "pending conflict" to be processed as a conflict lemma on the output
+ * channel of this class. It is not sent out immediately since it may require
+ * explanation from the equality engine, and may be called at any time, e.g.
+ * during a merge operation, when the equality engine is not in a state to
+ * provide explanations.
+ */
+ void setPendingConflictWhen(Node conf);
+ /** get the pending conflict, or null if none exist */
+ Node getPendingConflict() const;
+ //------------------------------------------ end conflicts
+ /** get length with explanation
+ *
+ * If possible, this returns an arithmetic term that exists in the current
+ * context that is equal to the length of te, or otherwise returns the
+ * length of t. It adds to exp literals that hold in the current context that
+ * explain why that term is equal to the length of t. For example, if
+ * we have assertions:
+ * len( x ) = 5 ^ z = x ^ x = y,
+ * then getLengthExp( z, exp, y ) returns len( x ) and adds { z = x } to
+ * exp. On the other hand, getLengthExp( z, exp, x ) returns len( x ) and
+ * adds nothing to exp.
+ */
+ Node getLengthExp(Node t, std::vector<Node>& exp, Node te);
+ /** shorthand for getLengthExp(t, exp, t) */
+ Node getLength(Node t, std::vector<Node>& exp);
+ /**
+ * Get the above information for equivalence class eqc. If doMake is true,
+ * we construct a new information class if one does not exist. The term eqc
+ * should currently be a representative of the equality engine of this class.
+ */
+ EqcInfo* getOrMakeEqcInfo(Node eqc, bool doMake = true);
+
+ /** add endpoints to eqc info
+ *
+ * This method is called when term t is the explanation for why equivalence
+ * class eqc may have a constant endpoint due to a concatentation term concat.
+ * For example, we may call this method on:
+ * t := (str.++ x y), concat := (str.++ x y), eqc
+ * for some eqc that is currently equal to t. Another example is:
+ * t := (str.in.re z (re.++ r s)), concat := (re.++ r s), eqc
+ * for some eqc that is currently equal to z.
+ */
+ void addEndpointsToEqcInfo(Node t, Node concat, Node eqc);
+
+ private:
+ /** Pointer to the SAT context object used by the theory of strings. */
+ context::Context* d_context;
+ /** Reference to equality engine of the theory of strings. */
+ eq::EqualityEngine& d_ee;
+ /** Are we in conflict? */
+ context::CDO<bool> d_conflict;
+ /** The pending conflict if one exists */
+ context::CDO<Node> d_pendingConflict;
+ /** Map from representatives to their equivalence class information */
+ std::map<Node, EqcInfo*> d_eqcInfo;
+}; /* class TheoryStrings */
+
+} // namespace strings
+} // namespace theory
+} // namespace CVC4
+
+#endif /* CVC4__THEORY__STRINGS__THEORY_STRINGS_H */
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index caaded4c3..b0681b1ff 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -61,7 +61,12 @@ std::ostream& operator<<(std::ostream& out, InferStep s)
return out;
}
-Node TheoryStrings::TermIndex::add( TNode n, unsigned index, TheoryStrings* t, Node er, std::vector< Node >& c ) {
+Node TheoryStrings::TermIndex::add(TNode n,
+ unsigned index,
+ const SolverState& s,
+ Node er,
+ std::vector<Node>& c)
+{
if( index==n.getNumChildren() ){
if( d_data.isNull() ){
d_data = n;
@@ -69,13 +74,13 @@ Node TheoryStrings::TermIndex::add( TNode n, unsigned index, TheoryStrings* t, N
return d_data;
}else{
Assert( index<n.getNumChildren() );
- TNode nir = t->getRepresentative( n[index] );
+ TNode nir = s.getRepresentative(n[index]);
//if it is empty, and doing CONCAT, ignore
if( nir==er && n.getKind()==kind::STRING_CONCAT ){
- return add( n, index+1, t, er, c );
+ return add(n, index + 1, s, er, c);
}else{
c.push_back( nir );
- return d_children[nir].add( n, index+1, t, er, c );
+ return d_children[nir].add(n, index + 1, s, er, c);
}
}
}
@@ -88,16 +93,15 @@ TheoryStrings::TheoryStrings(context::Context* c,
: Theory(THEORY_STRINGS, c, u, out, valuation, logicInfo),
d_notify(*this),
d_equalityEngine(d_notify, c, "theory::strings", true),
- d_im(*this, c, u, d_equalityEngine, out),
+ d_state(c, d_equalityEngine),
+ d_im(*this, c, u, d_state, out),
d_conflict(c, false),
- d_pendingConflict(c),
d_nf_pairs(c),
d_pregistered_terms_cache(u),
d_registered_terms_cache(u),
d_length_lemma_terms_cache(u),
d_preproc(&d_sk_cache, u),
d_extf_infer_cache(c),
- d_extf_infer_cache_u(u),
d_ee_disequalities(c),
d_congruent(c),
d_proxy_var(u),
@@ -105,7 +109,7 @@ TheoryStrings::TheoryStrings(context::Context* c,
d_functionsTerms(c),
d_has_extf(c, false),
d_has_str_code(false),
- d_regexp_solver(*this, d_im, c, u),
+ d_regexp_solver(*this, d_state, d_im, c, u),
d_input_vars(u),
d_input_var_lsum(u),
d_cardinality_lits(u),
@@ -156,47 +160,7 @@ TheoryStrings::TheoryStrings(context::Context* c,
}
TheoryStrings::~TheoryStrings() {
- for( std::map< Node, EqcInfo* >::iterator it = d_eqc_info.begin(); it != d_eqc_info.end(); ++it ){
- delete it->second;
- }
-}
-
-Node TheoryStrings::getRepresentative( Node t ) {
- if( d_equalityEngine.hasTerm( t ) ){
- return d_equalityEngine.getRepresentative( t );
- }else{
- return t;
- }
-}
-bool TheoryStrings::hasTerm( Node a ){
- return d_equalityEngine.hasTerm( a );
-}
-
-bool TheoryStrings::areEqual( Node a, Node b ){
- if( a==b ){
- return true;
- }else if( hasTerm( a ) && hasTerm( b ) ){
- return d_equalityEngine.areEqual( a, b );
- }else{
- return false;
- }
-}
-
-bool TheoryStrings::areDisequal( Node a, Node b ){
- if( a==b ){
- return false;
- }else{
- if( hasTerm( a ) && hasTerm( b ) ) {
- Node ar = d_equalityEngine.getRepresentative( a );
- Node br = d_equalityEngine.getRepresentative( b );
- return ( ar!=br && ar.isConst() && br.isConst() ) || d_equalityEngine.areDisequal( ar, br, false );
- }else{
- Node ar = getRepresentative( a );
- Node br = getRepresentative( b );
- return ar!=br && ar.isConst() && br.isConst();
- }
- }
}
bool TheoryStrings::areCareDisequal( TNode x, TNode y ) {
@@ -213,41 +177,18 @@ bool TheoryStrings::areCareDisequal( TNode x, TNode y ) {
return false;
}
-Node TheoryStrings::getLengthExp( Node t, std::vector< Node >& exp, Node te ){
- Assert( areEqual( t, te ) );
- Node lt = mkLength( te );
- if( hasTerm( lt ) ){
- // use own length if it exists, leads to shorter explanation
- return lt;
- }else{
- EqcInfo * ei = getOrMakeEqcInfo( t, false );
- Node length_term = ei ? ei->d_length_term : Node::null();
- if( length_term.isNull() ){
- //typically shouldnt be necessary
- length_term = t;
- }
- Debug("strings") << "TheoryStrings::getLengthTerm " << t << " is " << length_term << std::endl;
- addToExplanation( length_term, te, exp );
- return Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, length_term ) );
- }
-}
-
-Node TheoryStrings::getLength( Node t, std::vector< Node >& exp ) {
- return getLengthExp( t, exp, t );
-}
-
Node TheoryStrings::getNormalString(Node x, std::vector<Node>& nf_exp)
{
if (!x.isConst())
{
- Node xr = getRepresentative(x);
+ Node xr = d_state.getRepresentative(x);
std::map<Node, NormalForm>::iterator it = d_normal_form.find(xr);
if (it != d_normal_form.end())
{
NormalForm& nf = it->second;
- Node ret = mkConcat(nf.d_nf);
+ Node ret = utils::mkNConcat(nf.d_nf);
nf_exp.insert(nf_exp.end(), nf.d_exp.begin(), nf.d_exp.end());
- addToExplanation(x, nf.d_base, nf_exp);
+ d_im.addToExplanation(x, nf.d_base, nf_exp);
Trace("strings-debug")
<< "Term: " << x << " has a normal form " << ret << std::endl;
return ret;
@@ -263,7 +204,7 @@ Node TheoryStrings::getNormalString(Node x, std::vector<Node>& nf_exp)
Node nc = getNormalString(x[i], nf_exp);
vec_nodes.push_back(nc);
}
- return mkConcat(vec_nodes);
+ return utils::mkNConcat(vec_nodes);
}
}
return x;
@@ -326,8 +267,8 @@ void TheoryStrings::explain(TNode literal, std::vector<TNode>& assumptions) {
std::vector< TNode > tassumptions;
if (atom.getKind() == kind::EQUAL) {
if( atom[0]!=atom[1] ){
- Assert( hasTerm( atom[0] ) );
- Assert( hasTerm( atom[1] ) );
+ Assert(d_equalityEngine.hasTerm(atom[0]));
+ Assert(d_equalityEngine.hasTerm(atom[1]));
d_equalityEngine.explainEquality(atom[0], atom[1], polarity, tassumptions);
}
} else {
@@ -385,7 +326,7 @@ Node TheoryStrings::getCurrentSubstitutionFor(int effort,
Trace("strings-subs") << " model val : " << mv << std::endl;
return mv;
}
- Node nr = getRepresentative(n);
+ Node nr = d_state.getRepresentative(n);
std::map<Node, Node>::iterator itc = d_eqc_to_const.find(nr);
if (itc != d_eqc_to_const.end())
{
@@ -399,7 +340,7 @@ Node TheoryStrings::getCurrentSubstitutionFor(int effort,
}
if (!d_eqc_to_const_base[nr].isNull())
{
- addToExplanation(n, d_eqc_to_const_base[nr], exp);
+ d_im.addToExplanation(n, d_eqc_to_const_base[nr], exp);
}
return itc->second;
}
@@ -413,7 +354,7 @@ Node TheoryStrings::getCurrentSubstitutionFor(int effort,
<< " " << nr << std::endl;
if (!nfnr.d_base.isNull())
{
- addToExplanation(n, nfnr.d_base, exp);
+ d_im.addToExplanation(n, nfnr.d_base, exp);
}
return ns;
}
@@ -451,9 +392,9 @@ bool TheoryStrings::doReduction(int effort, Node n, bool& isCd)
Node x = n[0];
Node s = n[1];
std::vector<Node> lexp;
- Node lenx = getLength(x, lexp);
- Node lens = getLength(s, lexp);
- if (areEqual(lenx, lens))
+ Node lenx = d_state.getLength(x, lexp);
+ Node lens = d_state.getLength(s, lexp);
+ if (d_state.areEqual(lenx, lens))
{
Trace("strings-extf-debug")
<< " resolve extf : " << n
@@ -461,7 +402,7 @@ bool TheoryStrings::doReduction(int effort, Node n, bool& isCd)
// We can reduce negative contains to a disequality when lengths are
// equal. In other words, len( x ) = len( s ) implies
// ~contains( x, s ) reduces to x != s.
- if (!areDisequal(x, s))
+ if (!d_state.areDisequal(x, s))
{
// len( x ) = len( s ) ^ ~contains( x, s ) => x != s
lexp.push_back(lenx.eqNode(lens));
@@ -509,7 +450,7 @@ bool TheoryStrings::doReduction(int effort, Node n, bool& isCd)
d_sk_cache.mkSkolemCached(x, s, SkolemCache::SK_FIRST_CTN_PRE, "sc1");
Node sk2 =
d_sk_cache.mkSkolemCached(x, s, SkolemCache::SK_FIRST_CTN_POST, "sc2");
- Node eq = Rewriter::rewrite(x.eqNode(mkConcat(sk1, s, sk2)));
+ Node eq = Rewriter::rewrite(x.eqNode(utils::mkNConcat(sk1, s, sk2)));
std::vector<Node> exp_vec;
exp_vec.push_back(n);
d_im.sendInference(d_empty_vec, exp_vec, eq, "POS-CTN", true);
@@ -607,7 +548,7 @@ bool TheoryStrings::collectModelInfo(TheoryModel* m)
{
if (s.getType().isString())
{
- Node r = getRepresentative(s);
+ Node r = d_state.getRepresentative(s);
repSet.insert(r);
}
}
@@ -682,11 +623,11 @@ bool TheoryStrings::collectModelInfo(TheoryModel* m)
// one?
if (d_has_str_code && lts_values[i] == d_one)
{
- EqcInfo* eip = getOrMakeEqcInfo(eqc, false);
- if (eip && !eip->d_code_term.get().isNull())
+ EqcInfo* eip = d_state.getOrMakeEqcInfo(eqc, false);
+ if (eip && !eip->d_codeTerm.get().isNull())
{
// its value must be equal to its code
- Node ct = nm->mkNode(kind::STRING_CODE, eip->d_code_term.get());
+ Node ct = nm->mkNode(kind::STRING_CODE, eip->d_codeTerm.get());
Node ctv = d_valuation.getModelValue(ct);
unsigned cvalue =
ctv.getConst<Rational>().getNumerator().toUnsignedInt();
@@ -812,7 +753,7 @@ bool TheoryStrings::collectModelInfo(TheoryModel* m)
Trace("strings-model") << " ++ ";
}
Trace("strings-model") << n;
- Node r = getRepresentative(n);
+ Node r = d_state.getRepresentative(n);
if (!r.isConst() && processed.find(r) == processed.end())
{
Trace("strings-model") << "(UNPROCESSED)";
@@ -823,11 +764,11 @@ bool TheoryStrings::collectModelInfo(TheoryModel* m)
std::vector< Node > nc;
for (const Node& n : nf.d_nf)
{
- Node r = getRepresentative(n);
+ Node r = d_state.getRepresentative(n);
Assert( r.isConst() || processed.find( r )!=processed.end() );
nc.push_back(r.isConst() ? r : processed[r]);
}
- Node cc = mkConcat( nc );
+ Node cc = utils::mkNConcat(nc);
Assert( cc.getKind()==kind::CONST_STRING );
Trace("strings-model") << "*** Determined constant " << cc << " for " << nodes[i] << std::endl;
processed[nodes[i]] = cc;
@@ -956,7 +897,8 @@ void TheoryStrings::check(Effort e) {
bool polarity;
TNode atom;
- if( !done() && !hasTerm( d_emptyString ) ) {
+ if (!done() && !d_equalityEngine.hasTerm(d_emptyString))
+ {
preRegisterTerm( d_emptyString );
}
@@ -1001,11 +943,16 @@ void TheoryStrings::check(Effort e) {
++eqc2_i;
}
Trace("strings-eqc") << " } " << std::endl;
- EqcInfo * ei = getOrMakeEqcInfo( eqc, false );
+ EqcInfo* ei = d_state.getOrMakeEqcInfo(eqc, false);
if( ei ){
- Trace("strings-eqc-debug") << "* Length term : " << ei->d_length_term.get() << std::endl;
- Trace("strings-eqc-debug") << "* Cardinality lemma k : " << ei->d_cardinality_lem_k.get() << std::endl;
- Trace("strings-eqc-debug") << "* Normalization length lemma : " << ei->d_normalized_length.get() << std::endl;
+ Trace("strings-eqc-debug")
+ << "* Length term : " << ei->d_lengthTerm.get() << std::endl;
+ Trace("strings-eqc-debug")
+ << "* Cardinality lemma k : " << ei->d_cardinalityLemK.get()
+ << std::endl;
+ Trace("strings-eqc-debug")
+ << "* Normalization length lemma : "
+ << ei->d_normalizedLength.get() << std::endl;
}
}
++eqcs2_i;
@@ -1097,7 +1044,7 @@ void TheoryStrings::checkMemberships()
bool pol = d_extf_info_tmp[n].d_const.getConst<bool>();
Trace("strings-process-debug")
<< " add membership : " << n << ", pol = " << pol << std::endl;
- Node r = getRepresentative(n[0]);
+ Node r = d_state.getRepresentative(n[0]);
assertedMems[r].push_back(pol ? n : n.negate());
}
else
@@ -1109,136 +1056,6 @@ void TheoryStrings::checkMemberships()
d_regexp_solver.check(assertedMems);
}
-TheoryStrings::EqcInfo::EqcInfo(context::Context* c)
- : d_length_term(c),
- d_code_term(c),
- d_cardinality_lem_k(c),
- d_normalized_length(c),
- d_prefixC(c),
- d_suffixC(c)
-{
-}
-
-Node TheoryStrings::EqcInfo::addEndpointConst(Node t, Node c, bool isSuf)
-{
- // check conflict
- Node prev = isSuf ? d_suffixC : d_prefixC;
- if (!prev.isNull())
- {
- Trace("strings-eager-pconf-debug") << "Check conflict " << prev << ", " << t
- << " post=" << isSuf << std::endl;
- Node prevC = utils::getConstantEndpoint(prev, isSuf);
- Assert(!prevC.isNull());
- Assert(prevC.getKind() == CONST_STRING);
- if (c.isNull())
- {
- c = utils::getConstantEndpoint(t, isSuf);
- Assert(!c.isNull());
- }
- Assert(c.getKind() == CONST_STRING);
- bool conflict = false;
- // if the constant prefixes are different
- if (c != prevC)
- {
- // conflicts between constants should be handled by equality engine
- Assert(!t.isConst() || !prev.isConst());
- Trace("strings-eager-pconf-debug")
- << "Check conflict constants " << prevC << ", " << c << std::endl;
- const String& ps = prevC.getConst<String>();
- const String& cs = c.getConst<String>();
- unsigned pvs = ps.size();
- unsigned cvs = cs.size();
- if (pvs == cvs || (pvs > cvs && t.isConst())
- || (cvs > pvs && prev.isConst()))
- {
- // If equal length, cannot be equal due to node check above.
- // If one is fully constant and has less length than the other, then the
- // other will not fit and we are in conflict.
- conflict = true;
- }
- else
- {
- const String& larges = pvs > cvs ? ps : cs;
- const String& smalls = pvs > cvs ? cs : ps;
- if (isSuf)
- {
- conflict = !larges.hasSuffix(smalls);
- }
- else
- {
- conflict = !larges.hasPrefix(smalls);
- }
- }
- if (!conflict && (pvs > cvs || prev.isConst()))
- {
- // current is subsumed, either shorter prefix or the other is a full
- // constant
- return Node::null();
- }
- }
- else if (!t.isConst())
- {
- // current is subsumed since the other may be a full constant
- return Node::null();
- }
- if (conflict)
- {
- Trace("strings-eager-pconf")
- << "Conflict for " << prevC << ", " << c << std::endl;
- std::vector<Node> ccs;
- Node r[2];
- for (unsigned i = 0; i < 2; i++)
- {
- Node tp = i == 0 ? t : prev;
- if (tp.getKind() == STRING_IN_REGEXP)
- {
- ccs.push_back(tp);
- r[i] = tp[0];
- }
- else
- {
- r[i] = tp;
- }
- }
- if (r[0] != r[1])
- {
- ccs.push_back(r[0].eqNode(r[1]));
- }
- Assert(!ccs.empty());
- Node ret =
- ccs.size() == 1 ? ccs[0] : NodeManager::currentNM()->mkNode(AND, ccs);
- Trace("strings-eager-pconf")
- << "String: eager prefix conflict: " << ret << std::endl;
- return ret;
- }
- }
- if (isSuf)
- {
- d_suffixC = t;
- }
- else
- {
- d_prefixC = t;
- }
- return Node::null();
-}
-
-TheoryStrings::EqcInfo * TheoryStrings::getOrMakeEqcInfo( Node eqc, bool doMake ) {
- std::map< Node, EqcInfo* >::iterator eqc_i = d_eqc_info.find( eqc );
- if( eqc_i==d_eqc_info.end() ){
- if( doMake ){
- EqcInfo* ei = new EqcInfo( getSatContext() );
- d_eqc_info[eqc] = ei;
- return ei;
- }else{
- return NULL;
- }
- }else{
- return (*eqc_i).second;
- }
-}
-
-
/** Conflict when merging two constants */
void TheoryStrings::conflict(TNode a, TNode b){
if( !d_conflict ){
@@ -1258,14 +1075,14 @@ void TheoryStrings::eqNotifyNewClass(TNode t){
{
Trace("strings-debug") << "New length eqc : " << t << std::endl;
Node r = d_equalityEngine.getRepresentative(t[0]);
- EqcInfo* ei = getOrMakeEqcInfo(r);
+ EqcInfo* ei = d_state.getOrMakeEqcInfo(r);
if (k == kind::STRING_LENGTH)
{
- ei->d_length_term = t[0];
+ ei->d_lengthTerm = t[0];
}
else
{
- ei->d_code_term = t[0];
+ ei->d_codeTerm = t[0];
}
//we care about the length of this string
registerTerm( t[0], 1 );
@@ -1273,69 +1090,48 @@ void TheoryStrings::eqNotifyNewClass(TNode t){
}
else if (k == CONST_STRING)
{
- EqcInfo* ei = getOrMakeEqcInfo(t);
+ EqcInfo* ei = d_state.getOrMakeEqcInfo(t);
ei->d_prefixC = t;
ei->d_suffixC = t;
return;
}
else if (k == STRING_CONCAT)
{
- addEndpointsToEqcInfo(t, t, t);
- }
-}
-
-void TheoryStrings::addEndpointsToEqcInfo(Node t, Node concat, Node eqc)
-{
- Assert(concat.getKind() == STRING_CONCAT
- || concat.getKind() == REGEXP_CONCAT);
- EqcInfo* ei = nullptr;
- // check each side
- for (unsigned r = 0; r < 2; r++)
- {
- unsigned index = r == 0 ? 0 : concat.getNumChildren() - 1;
- Node c = utils::getConstantComponent(concat[index]);
- if (!c.isNull())
- {
- if (ei == nullptr)
- {
- ei = getOrMakeEqcInfo(eqc);
- }
- Trace("strings-eager-pconf-debug")
- << "New term: " << concat << " for " << t << " with prefix " << c
- << " (" << (r == 1) << ")" << std::endl;
- setPendingConflictWhen(ei->addEndpointConst(t, c, r == 1));
- }
+ d_state.addEndpointsToEqcInfo(t, t, t);
}
}
/** called when two equivalance classes will merge */
void TheoryStrings::eqNotifyPreMerge(TNode t1, TNode t2){
- EqcInfo * e2 = getOrMakeEqcInfo(t2, false);
+ EqcInfo* e2 = d_state.getOrMakeEqcInfo(t2, false);
if( e2 ){
- EqcInfo * e1 = getOrMakeEqcInfo( t1 );
+ EqcInfo* e1 = d_state.getOrMakeEqcInfo(t1);
//add information from e2 to e1
- if( !e2->d_length_term.get().isNull() ){
- e1->d_length_term.set( e2->d_length_term );
+ if (!e2->d_lengthTerm.get().isNull())
+ {
+ e1->d_lengthTerm.set(e2->d_lengthTerm);
}
- if (!e2->d_code_term.get().isNull())
+ if (!e2->d_codeTerm.get().isNull())
{
- e1->d_code_term.set(e2->d_code_term);
+ e1->d_codeTerm.set(e2->d_codeTerm);
}
if (!e2->d_prefixC.get().isNull())
{
- setPendingConflictWhen(
+ d_state.setPendingConflictWhen(
e1->addEndpointConst(e2->d_prefixC, Node::null(), false));
}
if (!e2->d_suffixC.get().isNull())
{
- setPendingConflictWhen(
+ d_state.setPendingConflictWhen(
e1->addEndpointConst(e2->d_suffixC, Node::null(), true));
}
- if( e2->d_cardinality_lem_k.get()>e1->d_cardinality_lem_k.get() ) {
- e1->d_cardinality_lem_k.set( e2->d_cardinality_lem_k );
+ if (e2->d_cardinalityLemK.get() > e1->d_cardinalityLemK.get())
+ {
+ e1->d_cardinalityLemK.set(e2->d_cardinalityLemK);
}
- if( !e2->d_normalized_length.get().isNull() ){
- e1->d_normalized_length.set( e2->d_normalized_length );
+ if (!e2->d_normalizedLength.get().isNull())
+ {
+ e1->d_normalizedLength.set(e2->d_normalizedLength);
}
}
}
@@ -1481,19 +1277,20 @@ void TheoryStrings::assertPendingFact(Node atom, bool polarity, Node exp) {
if (polarity && atom[1].getKind() == REGEXP_CONCAT)
{
Node eqc = d_equalityEngine.getRepresentative(atom[0]);
- addEndpointsToEqcInfo(atom, atom[1], eqc);
+ d_state.addEndpointsToEqcInfo(atom, atom[1], eqc);
}
}
}
// process the conflict
if (!d_conflict)
{
- if (!d_pendingConflict.get().isNull())
+ Node pc = d_state.getPendingConflict();
+ if (!pc.isNull())
{
std::vector<Node> a;
- a.push_back(d_pendingConflict.get());
- Trace("strings-pending") << "Process pending conflict "
- << d_pendingConflict.get() << std::endl;
+ a.push_back(pc);
+ Trace("strings-pending")
+ << "Process pending conflict " << pc << std::endl;
Node conflictNode = mkExplain(a);
d_conflict = true;
Trace("strings-conflict")
@@ -1509,28 +1306,6 @@ void TheoryStrings::assertPendingFact(Node atom, bool polarity, Node exp) {
Trace("strings-pending-debug") << " Finished collect terms" << std::endl;
}
-void TheoryStrings::setPendingConflictWhen(Node conf)
-{
- if (!conf.isNull() && d_pendingConflict.get().isNull())
- {
- d_pendingConflict = conf;
- }
-}
-
-void TheoryStrings::addToExplanation( Node a, Node b, std::vector< Node >& exp ) {
- if( a!=b ){
- Debug("strings-explain") << "Add to explanation : " << a << " == " << b << std::endl;
- Assert( areEqual( a, b ) );
- exp.push_back( a.eqNode( b ) );
- }
-}
-
-void TheoryStrings::addToExplanation( Node lit, std::vector< Node >& exp ) {
- if( !lit.isNull() ){
- exp.push_back( lit );
- }
-}
-
void TheoryStrings::checkInit() {
//build term index
d_eqc_to_const.clear();
@@ -1542,7 +1317,7 @@ void TheoryStrings::checkInit() {
std::map< Kind, unsigned > ncongruent;
std::map< Kind, unsigned > congruent;
- d_emptyString_r = getRepresentative( d_emptyString );
+ d_emptyString_r = d_state.getRepresentative(d_emptyString);
eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine );
while( !eqcs_i.isFinished() ){
Node eqc = (*eqcs_i);
@@ -1561,7 +1336,7 @@ void TheoryStrings::checkInit() {
d_eqc_to_const_exp[eqc] = Node::null();
}else if( tn.isInteger() ){
if( n.getKind()==kind::STRING_LENGTH ){
- Node nr = getRepresentative( n[0] );
+ Node nr = d_state.getRepresentative(n[0]);
d_eqc_to_len_term[nr] = n[0];
}
}else if( n.getNumChildren()>0 ){
@@ -1569,18 +1344,23 @@ void TheoryStrings::checkInit() {
if( k!=kind::EQUAL ){
if( d_congruent.find( n )==d_congruent.end() ){
std::vector< Node > c;
- Node nc = d_term_index[k].add( n, 0, this, d_emptyString_r, c );
+ Node nc = d_term_index[k].add(n, 0, d_state, d_emptyString_r, c);
if( nc!=n ){
//check if we have inferred a new equality by removal of empty components
- if( n.getKind()==kind::STRING_CONCAT && !areEqual( nc, n ) ){
+ if (n.getKind() == kind::STRING_CONCAT
+ && !d_state.areEqual(nc, n))
+ {
std::vector< Node > exp;
unsigned count[2] = { 0, 0 };
while( count[0]<nc.getNumChildren() || count[1]<n.getNumChildren() ){
//explain empty prefixes
for( unsigned t=0; t<2; t++ ){
Node nn = t==0 ? nc : n;
- while( count[t]<nn.getNumChildren() &&
- ( nn[count[t]]==d_emptyString || areEqual( nn[count[t]], d_emptyString ) ) ){
+ while (
+ count[t] < nn.getNumChildren()
+ && (nn[count[t]] == d_emptyString
+ || d_state.areEqual(nn[count[t]], d_emptyString)))
+ {
if( nn[count[t]]!=d_emptyString ){
exp.push_back( nn[count[t]].eqNode( d_emptyString ) );
}
@@ -1599,7 +1379,9 @@ void TheoryStrings::checkInit() {
}
//infer the equality
d_im.sendInference(exp, n.eqNode(nc), "I_Norm");
- }else if( getExtTheory()->hasFunctionKind( n.getKind() ) ){
+ }
+ else if (getExtTheory()->hasFunctionKind(n.getKind()))
+ {
//mark as congruent : only process if neither has been reduced
getExtTheory()->markCongruent( nc, n );
}
@@ -1612,17 +1394,21 @@ void TheoryStrings::checkInit() {
}else if( k==kind::STRING_CONCAT && c.size()==1 ){
Trace("strings-process-debug") << " congruent term by singular : " << n << " " << c[0] << std::endl;
//singular case
- if( !areEqual( c[0], n ) ){
+ if (!d_state.areEqual(c[0], n))
+ {
Node ns;
std::vector< Node > exp;
//explain empty components
bool foundNEmpty = false;
for( unsigned i=0; i<n.getNumChildren(); i++ ){
- if( areEqual( n[i], d_emptyString ) ){
+ if (d_state.areEqual(n[i], d_emptyString))
+ {
if( n[i]!=d_emptyString ){
exp.push_back( n[i].eqNode( d_emptyString ) );
}
- }else{
+ }
+ else
+ {
Assert( !foundNEmpty );
ns = n[i];
foundNEmpty = true;
@@ -1682,8 +1468,9 @@ void TheoryStrings::checkConstantEquivalenceClasses( TermIndex* ti, std::vector<
Node n = ti->d_data;
if( !n.isNull() ){
//construct the constant
- Node c = mkConcat( vecc );
- if( !areEqual( n, c ) ){
+ Node c = utils::mkNConcat(vecc);
+ if (!d_state.areEqual(n, c))
+ {
Trace("strings-debug") << "Constant eqc : " << c << " for " << n << std::endl;
Trace("strings-debug") << " ";
for( unsigned i=0; i<vecc.size(); i++ ){
@@ -1694,19 +1481,24 @@ void TheoryStrings::checkConstantEquivalenceClasses( TermIndex* ti, std::vector<
unsigned countc = 0;
std::vector< Node > exp;
while( count<n.getNumChildren() ){
- while( count<n.getNumChildren() && areEqual( n[count], d_emptyString ) ){
- addToExplanation( n[count], d_emptyString, exp );
+ while (count < n.getNumChildren()
+ && d_state.areEqual(n[count], d_emptyString))
+ {
+ d_im.addToExplanation(n[count], d_emptyString, exp);
count++;
}
if( count<n.getNumChildren() ){
Trace("strings-debug") << "...explain " << n[count] << " " << vecc[countc] << std::endl;
- if( !areEqual( n[count], vecc[countc] ) ){
- Node nrr = getRepresentative( n[count] );
+ if (!d_state.areEqual(n[count], vecc[countc]))
+ {
+ Node nrr = d_state.getRepresentative(n[count]);
Assert( !d_eqc_to_const_exp[nrr].isNull() );
- addToExplanation( n[count], d_eqc_to_const_base[nrr], exp );
+ d_im.addToExplanation(n[count], d_eqc_to_const_base[nrr], exp);
exp.push_back( d_eqc_to_const_exp[nrr] );
- }else{
- addToExplanation( n[count], vecc[countc], exp );
+ }
+ else
+ {
+ d_im.addToExplanation(n[count], vecc[countc], exp);
}
countc++;
count++;
@@ -1714,13 +1506,14 @@ void TheoryStrings::checkConstantEquivalenceClasses( TermIndex* ti, std::vector<
}
//exp contains an explanation of n==c
Assert( countc==vecc.size() );
- if( hasTerm( c ) ){
+ if (d_state.hasTerm(c))
+ {
d_im.sendInference(exp, n.eqNode(c), "I_CONST_MERGE");
return;
}
else if (!d_im.hasProcessed())
{
- Node nr = getRepresentative( n );
+ Node nr = d_state.getRepresentative(n);
std::map< Node, Node >::iterator it = d_eqc_to_const.find( nr );
if( it==d_eqc_to_const.end() ){
Trace("strings-debug") << "Set eqc const " << n << " to " << c << std::endl;
@@ -1732,11 +1525,11 @@ void TheoryStrings::checkConstantEquivalenceClasses( TermIndex* ti, std::vector<
Trace("strings-debug") << "Conflict, other constant was " << it->second << ", this constant was " << c << std::endl;
if( d_eqc_to_const_exp[nr].isNull() ){
// n==c ^ n == c' => false
- addToExplanation( n, it->second, exp );
+ d_im.addToExplanation(n, it->second, exp);
}else{
// n==c ^ n == d_eqc_to_const_base[nr] == c' => false
exp.push_back( d_eqc_to_const_exp[nr] );
- addToExplanation( n, d_eqc_to_const_base[nr], exp );
+ d_im.addToExplanation(n, d_eqc_to_const_base[nr], exp);
}
d_im.sendInference(exp, d_false, "I_CONST_CONFLICT");
return;
@@ -1770,7 +1563,7 @@ void TheoryStrings::checkExtfEval( int effort ) {
{
// Setup information about n, including if it is equal to a constant.
ExtfInfoTmp& einfo = d_extf_info_tmp[n];
- Node r = getRepresentative(n);
+ Node r = d_state.getRepresentative(n);
std::map<Node, Node>::iterator itcit = d_eqc_to_const.find(r);
if (itcit != d_eqc_to_const.end())
{
@@ -1853,7 +1646,8 @@ void TheoryStrings::checkExtfEval( int effort ) {
Node conc;
if( !nrs.isNull() ){
Trace("strings-extf-debug") << " symbolic def : " << nrs << std::endl;
- if( !areEqual( nrs, nrc ) ){
+ if (!d_state.areEqual(nrs, nrc))
+ {
//infer symbolic unit
if( n.getType().isBoolean() ){
conc = nrc==d_true ? nrs : nrs.negate();
@@ -1863,12 +1657,16 @@ void TheoryStrings::checkExtfEval( int effort ) {
einfo.d_exp.clear();
}
}else{
- if( !areEqual( n, nrc ) ){
+ if (!d_state.areEqual(n, nrc))
+ {
if( n.getType().isBoolean() ){
- if( areEqual( n, nrc==d_true ? d_false : d_true ) ){
+ if (d_state.areEqual(n, nrc == d_true ? d_false : d_true))
+ {
einfo.d_exp.push_back(nrc == d_true ? n.negate() : n);
conc = d_false;
- }else{
+ }
+ else
+ {
conc = nrc==d_true ? n : n.negate();
}
}else{
@@ -1887,7 +1685,8 @@ void TheoryStrings::checkExtfEval( int effort ) {
}
}else{
//check if it is already equal, if so, mark as reduced. Otherwise, do nothing.
- if( areEqual( n, nrc ) ){
+ if (d_state.areEqual(n, nrc))
+ {
Trace("strings-extf") << " resolved extf, since satisfied by model: " << n << std::endl;
einfo.d_model_active = false;
}
@@ -1966,13 +1765,13 @@ void TheoryStrings::checkExtfInference( Node n, Node nr, ExtfInfoTmp& in, int ef
else
{
// otherwise, must explain via base node
- Node r = getRepresentative(n);
+ Node r = d_state.getRepresentative(n);
// we have that:
// d_eqc_to_const_exp[r] => d_eqc_to_const_base[r] = in.d_const
// thus:
// n = d_eqc_to_const_base[r] ^ d_eqc_to_const_exp[r] => n = in.d_const
Assert(d_eqc_to_const_base.find(r) != d_eqc_to_const_base.end());
- addToExplanation(n, d_eqc_to_const_base[r], in.d_exp);
+ d_im.addToExplanation(n, d_eqc_to_const_base[r], in.d_exp);
Assert(d_eqc_to_const_exp.find(r) != d_eqc_to_const_exp.end());
in.d_exp.insert(in.d_exp.end(),
d_eqc_to_const_exp[r].begin(),
@@ -2016,9 +1815,9 @@ void TheoryStrings::checkExtfInference( Node n, Node nr, ExtfInfoTmp& in, int ef
Node conc = nm->mkNode(STRING_STRCTN, children);
conc = Rewriter::rewrite(pol ? conc : conc.negate());
// check if it already (does not) hold
- if (hasTerm(conc))
+ if (d_state.hasTerm(conc))
{
- if (areEqual(conc, d_false))
+ if (d_state.areEqual(conc, d_false))
{
// we are in conflict
d_im.sendInference(in.d_exp, conc, "CTN_Decompose");
@@ -2082,12 +1881,12 @@ void TheoryStrings::checkExtfInference( Node n, Node nr, ExtfInfoTmp& in, int ef
Node lit = pol ? conc : conc[0];
if (lit.getKind() == EQUAL)
{
- do_infer = pol ? !areEqual(lit[0], lit[1])
- : !areDisequal(lit[0], lit[1]);
+ do_infer = pol ? !d_state.areEqual(lit[0], lit[1])
+ : !d_state.areDisequal(lit[0], lit[1]);
}
else
{
- do_infer = !areEqual(lit, pol ? d_true : d_false);
+ do_infer = !d_state.areEqual(lit, pol ? d_true : d_false);
}
if (do_infer)
{
@@ -2231,9 +2030,6 @@ void TheoryStrings::debugPrintFlatForms( const char * tc ){
Trace( tc ) << std::endl;
}
-void TheoryStrings::debugPrintNormalForms( const char * tc ) {
-}
-
struct sortConstLength {
std::map< Node, unsigned > d_const_length;
bool operator() (Node i, Node j) {
@@ -2324,7 +2120,7 @@ void TheoryStrings::checkFlatForms()
// of ( n = f[n] )
std::vector<Node> exp;
Assert(d_eqc_to_const_base.find(eqc) != d_eqc_to_const_base.end());
- addToExplanation(n, d_eqc_to_const_base[eqc], exp);
+ d_im.addToExplanation(n, d_eqc_to_const_base[eqc], exp);
Assert(d_eqc_to_const_exp.find(eqc) != d_eqc_to_const_exp.end());
if (!d_eqc_to_const_exp[eqc].isNull())
{
@@ -2337,7 +2133,7 @@ void TheoryStrings::checkFlatForms()
Assert(e >= 0 && e < (int)d_flat_form_index[n].size());
Assert(d_flat_form_index[n][e] >= 0
&& d_flat_form_index[n][e] < (int)n.getNumChildren());
- addToExplanation(
+ d_im.addToExplanation(
d_flat_form[n][e], n[d_flat_form_index[n][e]], exp);
}
}
@@ -2435,7 +2231,7 @@ void TheoryStrings::checkFlatForm(std::vector<Node>& eqc,
Node curr_c = getConstantEqc(curr);
Node ac = a[d_flat_form_index[a][count]];
std::vector<Node> lexp;
- Node lcurr = getLength(ac, lexp);
+ Node lcurr = d_state.getLength(ac, lexp);
for (unsigned i = 1; i < eqc_size; i++)
{
b = eqc[i];
@@ -2467,7 +2263,7 @@ void TheoryStrings::checkFlatForm(std::vector<Node>& eqc,
{
Node bc = b[d_flat_form_index[b][count]];
inelig.push_back(b);
- Assert(!areEqual(curr, cc));
+ Assert(!d_state.areEqual(curr, cc));
Node cc_c = getConstantEqc(cc);
if (!curr_c.isNull() && !cc_c.isNull())
{
@@ -2477,10 +2273,10 @@ void TheoryStrings::checkFlatForm(std::vector<Node>& eqc,
cc_c, curr_c, index, isRev);
if (s.isNull())
{
- addToExplanation(ac, d_eqc_to_const_base[curr], exp);
- addToExplanation(d_eqc_to_const_exp[curr], exp);
- addToExplanation(bc, d_eqc_to_const_base[cc], exp);
- addToExplanation(d_eqc_to_const_exp[cc], exp);
+ d_im.addToExplanation(ac, d_eqc_to_const_base[curr], exp);
+ d_im.addToExplanation(d_eqc_to_const_exp[curr], exp);
+ d_im.addToExplanation(bc, d_eqc_to_const_base[cc], exp);
+ d_im.addToExplanation(d_eqc_to_const_exp[cc], exp);
conc = d_false;
inf_type = 0;
break;
@@ -2497,8 +2293,8 @@ void TheoryStrings::checkFlatForm(std::vector<Node>& eqc,
{
// if lengths are the same, apply LengthEq
std::vector<Node> lexp2;
- Node lcc = getLength(bc, lexp2);
- if (areEqual(lcurr, lcc))
+ Node lcc = d_state.getLength(bc, lexp2);
+ if (d_state.areEqual(lcurr, lcc))
{
Trace("strings-ff-debug") << "Infer " << ac << " == " << bc
<< " since " << lcurr
@@ -2519,7 +2315,7 @@ void TheoryStrings::checkFlatForm(std::vector<Node>& eqc,
}
exp.insert(exp.end(), lexp.begin(), lexp.end());
exp.insert(exp.end(), lexp2.begin(), lexp2.end());
- addToExplanation(lcurr, lcc, exp);
+ d_im.addToExplanation(lcurr, lcc, exp);
conc = ac.eqNode(bc);
inf_type = 1;
break;
@@ -2535,13 +2331,13 @@ void TheoryStrings::checkFlatForm(std::vector<Node>& eqc,
Trace("strings-ff-debug")
<< "Found inference : " << conc << " based on equality " << a
<< " == " << b << ", " << isRev << " " << inf_type << std::endl;
- addToExplanation(a, b, exp);
+ d_im.addToExplanation(a, b, exp);
// explain why prefixes up to now were the same
for (unsigned j = 0; j < count; j++)
{
Trace("strings-ff-debug") << "Add at " << d_flat_form_index[a][j] << " "
<< d_flat_form_index[b][j] << std::endl;
- addToExplanation(
+ d_im.addToExplanation(
a[d_flat_form_index[a][j]], b[d_flat_form_index[b][j]], exp);
}
// explain why other components up to now are empty
@@ -2564,9 +2360,9 @@ void TheoryStrings::checkFlatForm(std::vector<Node>& eqc,
int endj = isRev ? c.getNumChildren() : jj;
for (int j = startj; j < endj; j++)
{
- if (areEqual(c[j], d_emptyString))
+ if (d_state.areEqual(c[j], d_emptyString))
{
- addToExplanation(c[j], d_emptyString, exp);
+ d_im.addToExplanation(c[j], d_emptyString, exp);
}
}
}
@@ -2615,7 +2411,7 @@ Node TheoryStrings::checkCycles( Node eqc, std::vector< Node >& curr, std::vecto
d_eqc[eqc].push_back( n );
}
for( unsigned i=0; i<n.getNumChildren(); i++ ){
- Node nr = getRepresentative( n[i] );
+ Node nr = d_state.getRepresentative(n[i]);
if( eqc==d_emptyString_r ){
//for empty eqc, ensure all components are empty
if( nr!=d_emptyString_r ){
@@ -2634,13 +2430,14 @@ Node TheoryStrings::checkCycles( Node eqc, std::vector< Node >& curr, std::vecto
Node ncy = checkCycles( nr, curr, exp );
if( !ncy.isNull() ){
Trace("strings-cycle") << eqc << " cycle: " << ncy << " at " << n << "[" << i << "] : " << n[i] << std::endl;
- addToExplanation( n, eqc, exp );
- addToExplanation( nr, n[i], exp );
+ d_im.addToExplanation(n, eqc, exp);
+ d_im.addToExplanation(nr, n[i], exp);
if( ncy==eqc ){
//can infer all other components must be empty
for( unsigned j=0; j<n.getNumChildren(); j++ ){
//take first non-empty
- if( j!=i && !areEqual( n[j], d_emptyString ) ){
+ if (j != i && !d_state.areEqual(n[j], d_emptyString))
+ {
d_im.sendInference(
exp, n[j].eqNode(d_emptyString), "I_CYCLE");
return Node::null();
@@ -2710,7 +2507,7 @@ void TheoryStrings::checkNormalFormsEq()
return;
}
NormalForm& nfe = getNormalForm(eqc);
- Node nf_term = mkConcat(nfe.d_nf);
+ Node nf_term = utils::mkNConcat(nfe.d_nf);
std::map<Node, Node>::iterator itn = nf_to_eqc.find(nf_term);
if (itn != nf_to_eqc.end())
{
@@ -2778,7 +2575,7 @@ void TheoryStrings::checkCodes()
Node cp = getProxyVariableFor(c);
AlwaysAssert(!cp.isNull());
Node vc = nm->mkNode(STRING_CODE, cp);
- if (!areEqual(cc, vc))
+ if (!d_state.areEqual(cc, vc))
{
d_im.sendInference(d_empty_vec, cc.eqNode(vc), "Code_Proxy");
}
@@ -2786,10 +2583,10 @@ void TheoryStrings::checkCodes()
}
else
{
- EqcInfo* ei = getOrMakeEqcInfo(eqc, false);
- if (ei && !ei->d_code_term.get().isNull())
+ EqcInfo* ei = d_state.getOrMakeEqcInfo(eqc, false);
+ if (ei && !ei->d_codeTerm.get().isNull())
{
- Node vc = nm->mkNode(kind::STRING_CODE, ei->d_code_term.get());
+ Node vc = nm->mkNode(kind::STRING_CODE, ei->d_codeTerm.get());
nconst_codes.push_back(vc);
}
}
@@ -2810,7 +2607,7 @@ void TheoryStrings::checkCodes()
{
Trace("strings-code-debug")
<< "Compare codes : " << c1 << " " << c2 << std::endl;
- if (!areDisequal(c1, c2) && !areEqual(c1, d_neg_one))
+ if (!d_state.areDisequal(c1, c2) && !d_state.areEqual(c1, d_neg_one))
{
Node eq_no = c1.eqNode(d_neg_one);
Node deq = c1.eqNode(c2).negate();
@@ -2828,19 +2625,22 @@ void TheoryStrings::checkCodes()
//compute d_normal_forms_(base,exp,exp_depend)[eqc]
void TheoryStrings::normalizeEquivalenceClass( Node eqc ) {
Trace("strings-process-debug") << "Process equivalence class " << eqc << std::endl;
- if( areEqual( eqc, d_emptyString ) ) {
+ if (d_state.areEqual(eqc, d_emptyString))
+ {
#ifdef CVC4_ASSERTIONS
for( unsigned j=0; j<d_eqc[eqc].size(); j++ ){
Node n = d_eqc[eqc][j];
for( unsigned i=0; i<n.getNumChildren(); i++ ){
- Assert( areEqual( n[i], d_emptyString ) );
+ Assert(d_state.areEqual(n[i], d_emptyString));
}
}
#endif
//do nothing
Trace("strings-process-debug") << "Return process equivalence class " << eqc << " : empty." << std::endl;
d_normal_form[eqc].init(d_emptyString);
- } else {
+ }
+ else
+ {
// should not have computed the normal form of this equivalence class yet
Assert(d_normal_form.find(eqc) == d_normal_form.end());
// Normal forms for the relevant terms in the equivalence class of eqc
@@ -2859,7 +2659,6 @@ void TheoryStrings::normalizeEquivalenceClass( Node eqc ) {
{
return;
}
- // debugPrintNormalForms( "strings-solve", eqc, normal_forms );
//construct the normal form
Assert( !normal_forms.empty() );
@@ -3007,7 +2806,7 @@ void TheoryStrings::getNormalForms(Node eqc,
printConcat(currv, "strings-error");
Trace("strings-error") << "..." << currv[i] << std::endl;
}
- Assert(!areEqual(currv[i], n));
+ Assert(!d_state.areEqual(currv[i], n));
}
}
}
@@ -3016,7 +2815,7 @@ void TheoryStrings::getNormalForms(Node eqc,
}else{
//this was redundant: combination of self + empty string(s)
Node nn = currv.size() == 0 ? d_emptyString : currv[0];
- Assert( areEqual( nn, eqc ) );
+ Assert(d_state.areEqual(nn, eqc));
}
}else{
eqc_non_c = n;
@@ -3103,7 +2902,7 @@ void TheoryStrings::getNormalForms(Node eqc,
//conflict, explanation is n = base ^ base = c ^ relevant porition of ( n = N[n] )
std::vector< Node > exp;
Assert( d_eqc_to_const_base.find( eqc )!=d_eqc_to_const_base.end() );
- addToExplanation( n, d_eqc_to_const_base[eqc], exp );
+ d_im.addToExplanation(n, d_eqc_to_const_base[eqc], exp);
Assert( d_eqc_to_const_exp.find( eqc )!=d_eqc_to_const_exp.end() );
if( !d_eqc_to_const_exp[eqc].isNull() ){
exp.push_back( d_eqc_to_const_exp[eqc] );
@@ -3251,7 +3050,7 @@ void TheoryStrings::processSimpleNEq(NormalForm& nfi,
//can infer that this string must be empty
Node eq = nfkv[index_k].eqNode(d_emptyString);
//Trace("strings-lemma") << "Strings: Infer " << eq << " from " << eq_exp << std::endl;
- Assert(!areEqual(d_emptyString, nfkv[index_k]));
+ Assert(!d_state.areEqual(d_emptyString, nfkv[index_k]));
d_im.sendInference(curr_exp, eq, "N_EndpointEmp");
index_k++;
}
@@ -3265,12 +3064,13 @@ void TheoryStrings::processSimpleNEq(NormalForm& nfi,
index++;
success = true;
}else{
- Assert(!areEqual(nfiv[index], nfjv[index]));
+ Assert(!d_state.areEqual(nfiv[index], nfjv[index]));
std::vector< Node > temp_exp;
- Node length_term_i = getLength(nfiv[index], temp_exp);
- Node length_term_j = getLength(nfjv[index], temp_exp);
+ Node length_term_i = d_state.getLength(nfiv[index], temp_exp);
+ Node length_term_j = d_state.getLength(nfjv[index], temp_exp);
// check length(nfiv[index]) == length(nfjv[index])
- if( areEqual( length_term_i, length_term_j ) ){
+ if (d_state.areEqual(length_term_i, length_term_j))
+ {
Trace("strings-solve-debug") << "Simple Case 2 : string lengths are equal" << std::endl;
Node eq = nfiv[index].eqNode(nfjv[index]);
//eq = Rewriter::rewrite( eq );
@@ -3306,13 +3106,16 @@ void TheoryStrings::processSimpleNEq(NormalForm& nfi,
eqnc.push_back(nfkv[index_l]);
}
}
- eqn.push_back( mkConcat( eqnc ) );
+ eqn.push_back(utils::mkNConcat(eqnc));
}
- if( !areEqual( eqn[0], eqn[1] ) ){
+ if (!d_state.areEqual(eqn[0], eqn[1]))
+ {
d_im.sendInference(
antec, eqn[0].eqNode(eqn[1]), "N_EndpointEq", true);
return;
- }else{
+ }
+ else
+ {
Assert(nfiv.size() == nfjv.size());
index = nfiv.size() - rproc;
}
@@ -3367,11 +3170,11 @@ void TheoryStrings::processSimpleNEq(NormalForm& nfi,
bool info_valid = false;
Assert(index < nfiv.size() - rproc && index < nfjv.size() - rproc);
std::vector< Node > lexp;
- Node length_term_i = getLength(nfiv[index], lexp);
- Node length_term_j = getLength(nfjv[index], lexp);
+ Node length_term_i = d_state.getLength(nfiv[index], lexp);
+ Node length_term_j = d_state.getLength(nfjv[index], lexp);
//split on equality between string lengths (note that splitting on equality between strings is worse since it is harder to process)
- if (!areDisequal(length_term_i, length_term_j)
- && !areEqual(length_term_i, length_term_j)
+ if (!d_state.areDisequal(length_term_i, length_term_j)
+ && !d_state.areEqual(length_term_i, length_term_j)
&& !nfiv[index].isConst() && !nfjv[index].isConst())
{ // AJR: remove the latter 2 conditions?
Trace("strings-solve-debug") << "Non-simple Case 1 : string lengths neither equal nor disequal" << std::endl;
@@ -3494,7 +3297,9 @@ void TheoryStrings::processSimpleNEq(NormalForm& nfi,
"c_spt");
Trace("strings-csp") << "Const Split: " << prea << " is removed from " << stra << " due to " << strb << ", p=" << p << std::endl;
//set info
- info.d_conc = other_str.eqNode( isRev ? mkConcat( sk, prea ) : mkConcat(prea, sk) );
+ info.d_conc = other_str.eqNode(
+ isRev ? utils::mkNConcat(sk, prea)
+ : utils::mkNConcat(prea, sk));
info.d_new_skolem[LENGTH_SPLIT].push_back(sk);
info.d_id = INFER_SSPLIT_CST_PROP;
info_valid = true;
@@ -3517,10 +3322,17 @@ void TheoryStrings::processSimpleNEq(NormalForm& nfi,
: SkolemCache::SK_ID_VC_BIN_SPT,
"cb_spt");
Trace("strings-csp") << "Const Split: " << c_firstHalf << " is removed from " << const_str << " (binary) " << std::endl;
- info.d_conc = NodeManager::currentNM()->mkNode( kind::OR, other_str.eqNode( isRev ? mkConcat( sk, c_firstHalf ) : mkConcat( c_firstHalf, sk ) ),
- NodeManager::currentNM()->mkNode( kind::AND,
- sk.eqNode( d_emptyString ).negate(),
- c_firstHalf.eqNode( isRev ? mkConcat( sk, other_str ) : mkConcat( other_str, sk ) ) ) );
+ info.d_conc = nm->mkNode(
+ OR,
+ other_str.eqNode(
+ isRev ? utils::mkNConcat(sk, c_firstHalf)
+ : utils::mkNConcat(c_firstHalf, sk)),
+ nm->mkNode(
+ AND,
+ sk.eqNode(d_emptyString).negate(),
+ c_firstHalf.eqNode(
+ isRev ? utils::mkNConcat(sk, other_str)
+ : utils::mkNConcat(other_str, sk))));
info.d_new_skolem[LENGTH_SPLIT].push_back(sk);
info.d_id = INFER_SSPLIT_CST_BINARY;
info_valid = true;
@@ -3533,7 +3345,9 @@ void TheoryStrings::processSimpleNEq(NormalForm& nfi,
: SkolemCache::SK_ID_VC_SPT,
"c_spt");
Trace("strings-csp") << "Const Split: " << firstChar << " is removed from " << const_str << " (serial) " << std::endl;
- info.d_conc = other_str.eqNode( isRev ? mkConcat( sk, firstChar ) : mkConcat(firstChar, sk) );
+ info.d_conc = other_str.eqNode(
+ isRev ? utils::mkNConcat(sk, firstChar)
+ : utils::mkNConcat(firstChar, sk));
info.d_new_skolem[LENGTH_SPLIT].push_back(sk);
info.d_id = INFER_SSPLIT_CST;
info_valid = true;
@@ -3585,12 +3399,12 @@ void TheoryStrings::processSimpleNEq(NormalForm& nfi,
"v_spt");
// must add length requirement
info.d_new_skolem[LENGTH_GEQ_ONE].push_back(sk);
- Node eq1 =
- nfiv[index].eqNode(isRev ? mkConcat(sk, nfjv[index])
- : mkConcat(nfjv[index], sk));
- Node eq2 =
- nfjv[index].eqNode(isRev ? mkConcat(sk, nfiv[index])
- : mkConcat(nfiv[index], sk));
+ Node eq1 = nfiv[index].eqNode(
+ isRev ? utils::mkNConcat(sk, nfjv[index])
+ : utils::mkNConcat(nfjv[index], sk));
+ Node eq2 = nfjv[index].eqNode(
+ isRev ? utils::mkNConcat(sk, nfiv[index])
+ : utils::mkNConcat(nfiv[index], sk));
if( lentTestSuccess!=-1 ){
info.d_antn.push_back( lentTestExp );
@@ -3686,15 +3500,15 @@ TheoryStrings::ProcessLoopResult TheoryStrings::processLoop(NormalForm& nfi,
Trace("strings-loop") << " ... (X)= " << vecoi[index] << std::endl;
Trace("strings-loop") << " ... T(Y.Z)= ";
std::vector<Node> vec_t(veci.begin() + index, veci.begin() + loop_index);
- Node t_yz = mkConcat(vec_t);
+ Node t_yz = utils::mkNConcat(vec_t);
Trace("strings-loop") << " (" << t_yz << ")" << std::endl;
Trace("strings-loop") << " ... S(Z.Y)= ";
std::vector<Node> vec_s(vecoi.begin() + index + 1, vecoi.end());
- Node s_zy = mkConcat(vec_s);
+ Node s_zy = utils::mkNConcat(vec_s);
Trace("strings-loop") << s_zy << std::endl;
Trace("strings-loop") << " ... R= ";
std::vector<Node> vec_r(veci.begin() + loop_index + 1, veci.end());
- Node r = mkConcat(vec_r);
+ Node r = utils::mkNConcat(vec_r);
Trace("strings-loop") << r << std::endl;
if (s_zy.isConst() && r.isConst() && r != d_emptyString)
@@ -3731,7 +3545,7 @@ TheoryStrings::ProcessLoopResult TheoryStrings::processLoop(NormalForm& nfi,
// the equality could rewrite to false
if (!split_eqr.isConst())
{
- if (!areDisequal(t, d_emptyString))
+ if (!d_state.areDisequal(t, d_emptyString))
{
// try to make t equal to empty to avoid loop
info.d_conc = nm->mkNode(kind::OR, split_eq, split_eq.negate());
@@ -3786,12 +3600,12 @@ TheoryStrings::ProcessLoopResult TheoryStrings::processLoop(NormalForm& nfi,
std::vector<Node> v2(vec_r);
v2.insert(v2.begin(), y);
v2.insert(v2.begin(), z);
- restr = mkConcat(z, y);
- cc = Rewriter::rewrite(s_zy.eqNode(mkConcat(v2)));
+ restr = utils::mkNConcat(z, y);
+ cc = Rewriter::rewrite(s_zy.eqNode(utils::mkNConcat(v2)));
}
else
{
- cc = Rewriter::rewrite(s_zy.eqNode(mkConcat(z, y)));
+ cc = Rewriter::rewrite(s_zy.eqNode(utils::mkNConcat(z, y)));
}
if (cc == d_false)
{
@@ -3831,13 +3645,13 @@ TheoryStrings::ProcessLoopResult TheoryStrings::processLoop(NormalForm& nfi,
registerLength(sk_y, LENGTH_GEQ_ONE);
Node sk_z = d_sk_cache.mkSkolem("z_loop");
// t1 * ... * tn = y * z
- Node conc1 = t_yz.eqNode(mkConcat(sk_y, sk_z));
+ Node conc1 = t_yz.eqNode(utils::mkNConcat(sk_y, sk_z));
// s1 * ... * sk = z * y * r
vec_r.insert(vec_r.begin(), sk_y);
vec_r.insert(vec_r.begin(), sk_z);
- Node conc2 = s_zy.eqNode(mkConcat(vec_r));
- Node conc3 = vecoi[index].eqNode(mkConcat(sk_y, sk_w));
- Node restr = r == d_emptyString ? s_zy : mkConcat(sk_z, sk_y);
+ Node conc2 = s_zy.eqNode(utils::mkNConcat(vec_r));
+ Node conc3 = vecoi[index].eqNode(utils::mkNConcat(sk_y, sk_w));
+ Node restr = r == d_emptyString ? s_zy : utils::mkNConcat(sk_z, sk_y);
str_in_re =
nm->mkNode(kind::STRING_IN_REGEXP,
sk_w,
@@ -3864,7 +3678,6 @@ TheoryStrings::ProcessLoopResult TheoryStrings::processLoop(NormalForm& nfi,
//return true for lemma, false if we succeed
void TheoryStrings::processDeq( Node ni, Node nj ) {
NodeManager* nm = NodeManager::currentNM();
- //Assert( areDisequal( ni, nj ) );
NormalForm& nfni = getNormalForm(ni);
NormalForm& nfnj = getNormalForm(nj);
if (nfni.d_nf.size() > 1 || nfnj.d_nf.size() > 1)
@@ -3894,12 +3707,14 @@ void TheoryStrings::processDeq( Node ni, Node nj ) {
Node i = nfi[index];
Node j = nfj[index];
Trace("strings-solve-debug") << "...Processing(DEQ) " << i << " " << j << std::endl;
- if( !areEqual( i, j ) ){
+ if (!d_state.areEqual(i, j))
+ {
Assert( i.getKind()!=kind::CONST_STRING || j.getKind()!=kind::CONST_STRING );
std::vector< Node > lexp;
- Node li = getLength( i, lexp );
- Node lj = getLength( j, lexp );
- if( areDisequal( li, lj ) ){
+ Node li = d_state.getLength(i, lexp);
+ Node lj = d_state.getLength(j, lexp);
+ if (d_state.areDisequal(li, lj))
+ {
if( i.getKind()==kind::CONST_STRING || j.getKind()==kind::CONST_STRING ){
//check if empty
Node const_k = i.getKind() == kind::CONST_STRING ? i : j;
@@ -3914,10 +3729,14 @@ void TheoryStrings::processDeq( Node ni, Node nj ) {
//split on first character
CVC4::String str = const_k.getConst<String>();
Node firstChar = str.size() == 1 ? const_k : NodeManager::currentNM()->mkConst( str.prefix( 1 ) );
- if( areEqual( lnck, d_one ) ){
- if( areDisequal( firstChar, nconst_k ) ){
+ if (d_state.areEqual(lnck, d_one))
+ {
+ if (d_state.areDisequal(firstChar, nconst_k))
+ {
return;
- }else if( !areEqual( firstChar, nconst_k ) ){
+ }
+ else if (!d_state.areEqual(firstChar, nconst_k))
+ {
//splitting on demand : try to make them disequal
if (d_im.sendSplit(
firstChar, nconst_k, "S-Split(DEQL-Const)", false))
@@ -3925,7 +3744,9 @@ void TheoryStrings::processDeq( Node ni, Node nj ) {
return;
}
}
- }else{
+ }
+ else
+ {
Node sk = d_sk_cache.mkSkolemCached(
nconst_k, SkolemCache::SK_ID_DC_SPT, "dc_spt");
registerLength(sk, LENGTH_ONE);
@@ -3961,9 +3782,12 @@ void TheoryStrings::processDeq( Node ni, Node nj ) {
antec.insert(antec.end(), nfni.d_exp.begin(), nfni.d_exp.end());
antec.insert(antec.end(), nfnj.d_exp.begin(), nfnj.d_exp.end());
//check disequal
- if( areDisequal( ni, nj ) ){
+ if (d_state.areDisequal(ni, nj))
+ {
antec.push_back( ni.eqNode( nj ).negate() );
- }else{
+ }
+ else
+ {
antec_new_lits.push_back( ni.eqNode( nj ).negate() );
}
antec_new_lits.push_back( li.eqNode( lj ).negate() );
@@ -3977,24 +3801,30 @@ void TheoryStrings::processDeq( Node ni, Node nj ) {
registerLength(sk3, LENGTH_GEQ_ONE);
//Node nemp = sk3.eqNode(d_emptyString).negate();
//conc.push_back(nemp);
- Node lsk1 = mkLength( sk1 );
+ Node lsk1 = utils::mkNLength(sk1);
conc.push_back( lsk1.eqNode( li ) );
- Node lsk2 = mkLength( sk2 );
+ Node lsk2 = utils::mkNLength(sk2);
conc.push_back( lsk2.eqNode( lj ) );
- conc.push_back( NodeManager::currentNM()->mkNode( kind::OR, j.eqNode( mkConcat( sk1, sk3 ) ), i.eqNode( mkConcat( sk2, sk3 ) ) ) );
+ conc.push_back(nm->mkNode(OR,
+ j.eqNode(utils::mkNConcat(sk1, sk3)),
+ i.eqNode(utils::mkNConcat(sk2, sk3))));
d_im.sendInference(
antec, antec_new_lits, nm->mkNode(AND, conc), "D-DISL-Split");
++(d_statistics.d_deq_splits);
return;
}
- }else if( areEqual( li, lj ) ){
- Assert( !areDisequal( i, j ) );
+ }
+ else if (d_state.areEqual(li, lj))
+ {
+ Assert(!d_state.areDisequal(i, j));
//splitting on demand : try to make them disequal
if (d_im.sendSplit(i, j, "S-Split(DEQL)", false))
{
return;
}
- }else{
+ }
+ else
+ {
//splitting on demand : try to make lengths equal
if (d_im.sendSplit(li, lj, "D-Split"))
{
@@ -4054,8 +3884,8 @@ int TheoryStrings::processSimpleDeq( std::vector< Node >& nfi, std::vector< Node
Trace("strings-solve-debug") << "Disequality normalize empty" << std::endl;
std::vector< Node > ant;
//we have a conflict : because the lengths are equal, the remainder needs to be empty, which will lead to a conflict
- Node lni = getLengthExp(ni, ant, nfni.d_base);
- Node lnj = getLengthExp(nj, ant, nfnj.d_base);
+ Node lni = d_state.getLengthExp(ni, ant, nfni.d_base);
+ Node lnj = d_state.getLengthExp(nj, ant, nfnj.d_base);
ant.push_back( lni.eqNode( lnj ) );
ant.insert(ant.end(), nfni.d_exp.begin(), nfni.d_exp.end());
ant.insert(ant.end(), nfnj.d_exp.begin(), nfnj.d_exp.end());
@@ -4072,7 +3902,8 @@ int TheoryStrings::processSimpleDeq( std::vector< Node >& nfi, std::vector< Node
Node i = nfi[index];
Node j = nfj[index];
Trace("strings-solve-debug") << "...Processing(QED) " << i << " " << j << std::endl;
- if( !areEqual( i, j ) ) {
+ if (!d_state.areEqual(i, j))
+ {
if( i.getKind()==kind::CONST_STRING && j.getKind()==kind::CONST_STRING ) {
unsigned int len_short = i.getConst<String>().size() < j.getConst<String>().size() ? i.getConst<String>().size() : j.getConst<String>().size();
bool isSameFix = isRev ? i.getConst<String>().rstrncmp(j.getConst<String>(), len_short): i.getConst<String>().strncmp(j.getConst<String>(), len_short);
@@ -4102,13 +3933,16 @@ int TheoryStrings::processSimpleDeq( std::vector< Node >& nfi, std::vector< Node
}
}else{
std::vector< Node > lexp;
- Node li = getLength( i, lexp );
- Node lj = getLength( j, lexp );
- if( areEqual( li, lj ) && areDisequal( i, j ) ){
+ Node li = d_state.getLength(i, lexp);
+ Node lj = d_state.getLength(j, lexp);
+ if (d_state.areEqual(li, lj) && d_state.areDisequal(i, j))
+ {
Trace("strings-solve") << "Simple Case 2 : found equal length disequal sub strings " << i << " " << j << std::endl;
//we are done: D-Remove
return 1;
- }else{
+ }
+ else
+ {
return 0;
}
}
@@ -4256,7 +4090,7 @@ void TheoryStrings::registerTerm( Node n, int effort ) {
{
d_has_str_code = true;
// ite( str.len(s)==1, 0 <= str.code(s) < num_codes, str.code(s)=-1 )
- Node code_len = mkLength(n[0]).eqNode(d_one);
+ Node code_len = utils::mkNLength(n[0]).eqNode(d_one);
Node code_eq_neg1 = n.eqNode(d_neg_one);
Node code_range = nm->mkNode(
AND,
@@ -4269,7 +4103,7 @@ void TheoryStrings::registerTerm( Node n, int effort ) {
}
else if (n.getKind() == STRING_STRIDOF)
{
- Node len = mkLength(n[0]);
+ Node len = utils::mkNLength(n[0]);
Node lem = nm->mkNode(AND,
nm->mkNode(GEQ, n, nm->mkConst(Rational(-1))),
nm->mkNode(LT, n, len));
@@ -4358,22 +4192,6 @@ void TheoryStrings::registerLength(Node n, LengthStatus s)
}
}
-Node TheoryStrings::mkConcat( Node n1, Node n2 ) {
- return Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, n1, n2 ) );
-}
-
-Node TheoryStrings::mkConcat( Node n1, Node n2, Node n3 ) {
- return Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, n1, n2, n3 ) );
-}
-
-Node TheoryStrings::mkConcat( const std::vector< Node >& c ) {
- return Rewriter::rewrite( c.size()>1 ? NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, c ) : ( c.size()==1 ? c[0] : d_emptyString ) );
-}
-
-Node TheoryStrings::mkLength( Node t ) {
- return Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, t ) );
-}
-
Node TheoryStrings::mkExplain(const std::vector<Node>& a)
{
std::vector< Node > an;
@@ -4396,8 +4214,8 @@ Node TheoryStrings::mkExplain(const std::vector<Node>& a,
Debug("strings-explain") << "Add to explanation " << apc << std::endl;
if (apc.getKind() == NOT && apc[0].getKind() == EQUAL)
{
- Assert(hasTerm(apc[0][0]));
- Assert(hasTerm(apc[0][1]));
+ Assert(d_equalityEngine.hasTerm(apc[0][0]));
+ Assert(d_equalityEngine.hasTerm(apc[0][1]));
// ensure that we are ready to explain the disequality
AlwaysAssert(d_equalityEngine.areDisequal(apc[0][0], apc[0][1], true));
}
@@ -4442,14 +4260,15 @@ void TheoryStrings::checkNormalFormsDeq()
processed[n[0]][n[1]] = true;
Node lt[2];
for( unsigned i=0; i<2; i++ ){
- EqcInfo* ei = getOrMakeEqcInfo( n[i], false );
- lt[i] = ei ? ei->d_length_term : Node::null();
+ EqcInfo* ei = d_state.getOrMakeEqcInfo(n[i], false);
+ lt[i] = ei ? ei->d_lengthTerm : Node::null();
if( lt[i].isNull() ){
lt[i] = eq[i];
}
lt[i] = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, lt[i] );
}
- if( !areEqual( lt[0], lt[1] ) && !areDisequal( lt[0], lt[1] ) ){
+ if (!d_state.areEqual(lt[0], lt[1]) && !d_state.areDisequal(lt[0], lt[1]))
+ {
d_im.sendSplit(lt[0], lt[1], "DEQ-LENGTH-SP");
}
}
@@ -4480,7 +4299,7 @@ void TheoryStrings::checkNormalFormsDeq()
}
else
{
- if (areDisequal(cols[i][j], cols[i][k]))
+ if (d_state.areDisequal(cols[i][j], cols[i][k]))
{
Assert(!d_conflict);
if (Trace.isOn("strings-solve"))
@@ -4511,13 +4330,14 @@ void TheoryStrings::checkLengthsEqc() {
NormalForm& nfi = getNormalForm(d_strings_eqc[i]);
Trace("strings-process-debug") << "Process length constraints for " << d_strings_eqc[i] << std::endl;
//check if there is a length term for this equivalence class
- EqcInfo* ei = getOrMakeEqcInfo( d_strings_eqc[i], false );
- Node lt = ei ? ei->d_length_term : Node::null();
+ EqcInfo* ei = d_state.getOrMakeEqcInfo(d_strings_eqc[i], false);
+ Node lt = ei ? ei->d_lengthTerm : Node::null();
if( !lt.isNull() ) {
Node llt = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, lt );
//now, check if length normalization has occurred
- if( ei->d_normalized_length.get().isNull() ) {
- Node nf = mkConcat(nfi.d_nf);
+ if (ei->d_normalizedLength.get().isNull())
+ {
+ Node nf = utils::mkNConcat(nfi.d_nf);
if( Trace.isOn("strings-process-debug") ){
Trace("strings-process-debug")
<< " normal form is " << nf << " from base " << nfi.d_base
@@ -4536,17 +4356,17 @@ void TheoryStrings::checkLengthsEqc() {
Node lc = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, nf );
Node lcr = Rewriter::rewrite( lc );
Trace("strings-process-debug") << "Rewrote length " << lc << " to " << lcr << std::endl;
- if (!areEqual(llt, lcr))
+ if (!d_state.areEqual(llt, lcr))
{
Node eq = llt.eqNode(lcr);
- ei->d_normalized_length.set( eq );
+ ei->d_normalizedLength.set(eq);
d_im.sendInference(ant, eq, "LEN-NORM", true);
}
}
}else{
Trace("strings-process-debug") << "No length term for eqc " << d_strings_eqc[i] << " " << d_eqc_to_len_term[d_strings_eqc[i]] << std::endl;
if( !options::stringEagerLen() ){
- Node c = mkConcat(nfi.d_nf);
+ Node c = utils::mkNConcat(nfi.d_nf);
registerTerm( c, 3 );
}
}
@@ -4594,9 +4414,12 @@ void TheoryStrings::checkCardinality() {
bool success = true;
while( r<card_need && success ){
Node rr = NodeManager::currentNM()->mkConst<Rational>( Rational(r) );
- if( areDisequal( rr, lr ) ){
+ if (d_state.areDisequal(rr, lr))
+ {
r++;
- }else{
+ }
+ else
+ {
success = false;
}
}
@@ -4612,7 +4435,8 @@ void TheoryStrings::checkCardinality() {
itr1 != cols[i].end(); ++itr1) {
for( std::vector< Node >::iterator itr2 = itr1 + 1;
itr2 != cols[i].end(); ++itr2) {
- if(!areDisequal( *itr1, *itr2 )) {
+ if (!d_state.areDisequal(*itr1, *itr2))
+ {
// add split lemma
if (d_im.sendSplit(*itr1, *itr2, "CARD-SP"))
{
@@ -4621,9 +4445,12 @@ void TheoryStrings::checkCardinality() {
}
}
}
- EqcInfo* ei = getOrMakeEqcInfo( lr, true );
- Trace("strings-card") << "Previous cardinality used for " << lr << " is " << ((int)ei->d_cardinality_lem_k.get()-1) << std::endl;
- if( int_k+1 > ei->d_cardinality_lem_k.get() ){
+ EqcInfo* ei = d_state.getOrMakeEqcInfo(lr, true);
+ Trace("strings-card")
+ << "Previous cardinality used for " << lr << " is "
+ << ((int)ei->d_cardinalityLemK.get() - 1) << std::endl;
+ if (int_k + 1 > ei->d_cardinalityLemK.get())
+ {
Node k_node = NodeManager::currentNM()->mkConst( ::CVC4::Rational( int_k ) );
//add cardinality lemma
Node dist = NodeManager::currentNM()->mkNode( kind::DISTINCT, cols[i] );
@@ -4640,7 +4467,7 @@ void TheoryStrings::checkCardinality() {
Node len = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, cols[i][0] );
Node cons = NodeManager::currentNM()->mkNode( kind::GEQ, len, k_node );
cons = Rewriter::rewrite( cons );
- ei->d_cardinality_lem_k.set( int_k+1 );
+ ei->d_cardinalityLemK.set(int_k + 1);
if( cons!=d_true ){
d_im.sendInference(
d_empty_vec, vec_node, cons, "CARDINALITY", true);
@@ -4653,18 +4480,6 @@ void TheoryStrings::checkCardinality() {
Trace("strings-card") << "...end check cardinality" << std::endl;
}
-void TheoryStrings::getEquivalenceClasses( std::vector< Node >& eqcs ) {
- eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine );
- while( !eqcs_i.isFinished() ) {
- Node eqc = (*eqcs_i);
- //if eqc.getType is string
- if (eqc.getType().isString()) {
- eqcs.push_back( eqc );
- }
- ++eqcs_i;
- }
-}
-
void TheoryStrings::separateByLength(std::vector< Node >& n,
std::vector< std::vector< Node > >& cols,
std::vector< Node >& lts ) {
@@ -4675,8 +4490,8 @@ void TheoryStrings::separateByLength(std::vector< Node >& n,
for( unsigned i=0; i<n.size(); i++ ) {
Node eqc = n[i];
Assert( d_equalityEngine.getRepresentative(eqc)==eqc );
- EqcInfo* ei = getOrMakeEqcInfo( eqc, false );
- Node lt = ei ? ei->d_length_term : Node::null();
+ EqcInfo* ei = d_state.getOrMakeEqcInfo(eqc, false);
+ Node lt = ei ? ei->d_lengthTerm : Node::null();
if( !lt.isNull() ){
lt = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, lt );
Node r = d_equalityEngine.getRepresentative( lt );
diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h
index 94811636c..9db40f8fe 100644
--- a/src/theory/strings/theory_strings.h
+++ b/src/theory/strings/theory_strings.h
@@ -31,6 +31,7 @@
#include "theory/strings/regexp_operation.h"
#include "theory/strings/regexp_solver.h"
#include "theory/strings/skolem_cache.h"
+#include "theory/strings/solver_state.h"
#include "theory/strings/theory_strings_preprocess.h"
#include "theory/theory.h"
#include "theory/uf/equality_engine.h"
@@ -191,42 +192,7 @@ class TheoryStrings : public Theory {
}
};/* class TheoryStrings::NotifyClass */
- //--------------------------- equality engine
- /**
- * Get the representative of t in the equality engine of this class, or t
- * itself if it is not registered as a term.
- */
- Node getRepresentative(Node t);
- /** Is t registered as a term in the equality engine of this class? */
- bool hasTerm(Node a);
- /**
- * Are a and b equal according to the equality engine of this class? Also
- * returns true if a and b are identical.
- */
- bool areEqual(Node a, Node b);
- /**
- * Are a and b disequal according to the equality engine of this class? Also
- * returns true if the representative of a and b are distinct constants.
- */
- bool areDisequal(Node a, Node b);
- //--------------------------- end equality engine
-
//--------------------------- helper functions
- /** get length with explanation
- *
- * If possible, this returns an arithmetic term that exists in the current
- * context that is equal to the length of te, or otherwise returns the
- * length of t. It adds to exp literals that hold in the current context that
- * explain why that term is equal to the length of t. For example, if
- * we have assertions:
- * len( x ) = 5 ^ z = x ^ x = y,
- * then getLengthExp( z, exp, y ) returns len( x ) and adds { z = x } to
- * exp. On the other hand, getLengthExp( z, exp, x ) returns len( x ) and
- * adds nothing to exp.
- */
- Node getLengthExp(Node t, std::vector<Node>& exp, Node te);
- /** shorthand for getLengthExp(t, exp, t) */
- Node getLength(Node t, std::vector<Node>& exp);
/** get normal string
*
* This method returns the node that is equivalent to the normal form of x,
@@ -252,12 +218,12 @@ class TheoryStrings : public Theory {
NotifyClass d_notify;
/** Equaltity engine */
eq::EqualityEngine d_equalityEngine;
+ /** The solver state object */
+ SolverState d_state;
/** The (custom) output channel of the theory of strings */
InferenceManager d_im;
/** Are we in conflict */
context::CDO<bool> d_conflict;
- /** Pending conflict */
- context::CDO<Node> d_pendingConflict;
/** map from terms to their normal forms */
std::map<Node, NormalForm> d_normal_form;
/** get normal form */
@@ -276,7 +242,6 @@ class TheoryStrings : public Theory {
StringsPreprocess d_preproc;
// extended functions inferences cache
NodeSet d_extf_infer_cache;
- NodeSet d_extf_infer_cache_u;
std::vector< Node > d_empty_vec;
//
NodeList d_ee_disequalities;
@@ -327,7 +292,11 @@ private:
public:
Node d_data;
std::map< TNode, TermIndex > d_children;
- Node add( TNode n, unsigned index, TheoryStrings* t, Node er, std::vector< Node >& c );
+ Node add(TNode n,
+ unsigned index,
+ const SolverState& s,
+ Node er,
+ std::vector<Node>& c);
void clear(){ d_children.clear(); }
};
std::map< Kind, TermIndex > d_term_index;
@@ -337,7 +306,6 @@ private:
std::map< Node, std::vector< int > > d_flat_form_index;
void debugPrintFlatForms( const char * tc );
- void debugPrintNormalForms( const char * tc );
/////////////////////////////////////////////////////////////////////////////
// MODEL GENERATION
/////////////////////////////////////////////////////////////////////////////
@@ -359,55 +327,6 @@ private:
EqualityStatus getEqualityStatus(TNode a, TNode b) override;
private:
- /** SAT-context-dependent information about an equivalence class */
- class EqcInfo {
- public:
- EqcInfo( context::Context* c );
- ~EqcInfo(){}
- /**
- * If non-null, this is a term x from this eq class such that str.len( x )
- * occurs as a term in this SAT context.
- */
- context::CDO< Node > d_length_term;
- /**
- * If non-null, this is a term x from this eq class such that str.code( x )
- * occurs as a term in this SAT context.
- */
- context::CDO<Node> d_code_term;
- context::CDO< unsigned > d_cardinality_lem_k;
- context::CDO< Node > d_normalized_length;
- /**
- * A node that explains the longest constant prefix known of this
- * equivalence class. This can either be:
- * (1) A term from this equivalence class, including a constant "ABC" or
- * concatenation term (str.++ "ABC" ...), or
- * (2) A membership of the form (str.in.re x R) where x is in this
- * equivalence class and R is a regular expression of the form
- * (str.to.re "ABC") or (re.++ (str.to.re "ABC") ...).
- */
- context::CDO<Node> d_prefixC;
- /** same as above, for suffix. */
- context::CDO<Node> d_suffixC;
- /** add prefix constant
- *
- * This informs this equivalence class info that a term t in its
- * equivalence class has a constant prefix (if isSuf=true) or suffix
- * (if isSuf=false). The constant c (if non-null) is the value of that
- * constant, if it has been computed already.
- *
- * If this method returns a non-null node ret, then ret is a conjunction
- * corresponding to a conflict that holds in the current context.
- */
- Node addEndpointConst(Node t, Node c, bool isSuf);
- };
- /** map from representatives to information necessary for equivalence classes */
- std::map< Node, EqcInfo* > d_eqc_info;
- /**
- * Get the above information for equivalence class eqc. If doMake is true,
- * we construct a new information class if one does not exist. The term eqc
- * should currently be a representative of the equality engine of this class.
- */
- EqcInfo * getOrMakeEqcInfo( Node eqc, bool doMake = true );
/**
* Map string terms to their "proxy variables". Proxy variables are used are
* intermediate variables so that length information can be communicated for
@@ -643,15 +562,6 @@ private:
int processSimpleDeq( std::vector< Node >& nfi, std::vector< Node >& nfj, Node ni, Node nj, unsigned& index, bool isRev );
//--------------------------end for checkNormalFormsDeq
- //--------------------------------for checkMemberships
- // check membership constraints
- Node mkRegExpAntec(Node atom, Node ant);
- bool checkPDerivative( Node x, Node r, Node atom, bool &addedLemma, std::vector< Node > &nf_exp);
- //check contains
- void checkPosContains( std::vector< Node >& posContains );
- void checkNegContains( std::vector< Node >& negContains );
- //--------------------------------end for checkMemberships
-
private:
void addCarePairs(TNodeTrie* t1,
TNodeTrie* t2,
@@ -698,41 +608,12 @@ private:
* of atom, including calls to registerTerm.
*/
void assertPendingFact(Node atom, bool polarity, Node exp);
- /** add endpoints to eqc info
- *
- * This method is called when term t is the explanation for why equivalence
- * class eqc may have a constant endpoint due to a concatentation term concat.
- * For example, we may call this method on:
- * t := (str.++ x y), concat := (str.++ x y), eqc
- * for some eqc that is currently equal to t. Another example is:
- * t := (str.in.re z (re.++ r s)), concat := (re.++ r s), eqc
- * for some eqc that is currently equal to z.
- */
- void addEndpointsToEqcInfo(Node t, Node concat, Node eqc);
- /** set pending conflict
- *
- * If conf is non-null, this is called when conf is a conjunction of literals
- * that hold in the current context that are unsatisfiable. It is set as the
- * "pending conflict" to be processed as a conflict lemma on the output
- * channel of this class. It is not sent out immediately since it may require
- * explanation from the equality engine, and may be called at any time, e.g.
- * during a merge operation, when the equality engine is not in a state to
- * provide explanations.
- */
- void setPendingConflictWhen(Node conf);
/**
* This processes the infer info ii as an inference. In more detail, it calls
* the inference manager to process the inference, it introduces Skolems, and
* updates the set of normal form pairs.
*/
void doInferInfo(const InferInfo& ii);
- /**
- * Adds equality a = b to the vector exp if a and b are distinct terms. It
- * must be the case that areEqual( a, b ) holds in this context.
- */
- void addToExplanation(Node a, Node b, std::vector<Node>& exp);
- /** Adds lit to the vector exp if it is non-null */
- void addToExplanation(Node lit, std::vector<Node>& exp);
/** Register term
*
@@ -754,18 +635,6 @@ private:
*/
void registerTerm(Node n, int effort);
- /**
- * Are we in conflict? This returns true if this theory has called its output
- * channel's conflict method in the current SAT context.
- */
- bool inConflict() const { return d_conflict; }
-
- /** mkConcat **/
- inline Node mkConcat(Node n1, Node n2);
- inline Node mkConcat(Node n1, Node n2, Node n3);
- inline Node mkConcat(const std::vector<Node>& c);
- inline Node mkLength(Node n);
-
/** make explanation
*
* This returns a node corresponding to the explanation of formulas in a,
@@ -778,18 +647,6 @@ private:
protected:
- /** get equivalence classes
- *
- * This adds the representative of all equivalence classes to eqcs
- */
- void getEquivalenceClasses(std::vector<Node>& eqcs);
- /** get relevant equivalence classes
- *
- * This adds the representative of all equivalence classes that contain at
- * least one term in termSet.
- */
- void getRelevantEquivalenceClasses(std::vector<Node>& eqcs,
- std::set<Node>& termSet);
// separate into collections with equal length
void separateByLength(std::vector<Node>& n,
diff --git a/src/theory/strings/theory_strings_utils.cpp b/src/theory/strings/theory_strings_utils.cpp
index d764b87c1..03c2419c4 100644
--- a/src/theory/strings/theory_strings_utils.cpp
+++ b/src/theory/strings/theory_strings_utils.cpp
@@ -16,6 +16,8 @@
#include "theory/strings/theory_strings_utils.h"
+#include "theory/rewriter.h"
+
using namespace CVC4::kind;
namespace CVC4 {
@@ -101,7 +103,7 @@ void getConcat(Node n, std::vector<Node>& c)
}
}
-Node mkConcat(Kind k, std::vector<Node>& c)
+Node mkConcat(Kind k, const std::vector<Node>& c)
{
Assert(!c.empty() || k == STRING_CONCAT);
NodeManager* nm = NodeManager::currentNM();
@@ -109,6 +111,28 @@ Node mkConcat(Kind k, std::vector<Node>& c)
: (c.size() == 1 ? c[0] : nm->mkConst(String("")));
}
+Node mkNConcat(Node n1, Node n2)
+{
+ return Rewriter::rewrite(
+ NodeManager::currentNM()->mkNode(STRING_CONCAT, n1, n2));
+}
+
+Node mkNConcat(Node n1, Node n2, Node n3)
+{
+ return Rewriter::rewrite(
+ NodeManager::currentNM()->mkNode(STRING_CONCAT, n1, n2, n3));
+}
+
+Node mkNConcat(const std::vector<Node>& c)
+{
+ return Rewriter::rewrite(mkConcat(STRING_CONCAT, c));
+}
+
+Node mkNLength(Node t)
+{
+ return Rewriter::rewrite(NodeManager::currentNM()->mkNode(STRING_LENGTH, t));
+}
+
Node getConstantComponent(Node t)
{
Kind tk = t.getKind();
diff --git a/src/theory/strings/theory_strings_utils.h b/src/theory/strings/theory_strings_utils.h
index cadc98df3..2c84bd516 100644
--- a/src/theory/strings/theory_strings_utils.h
+++ b/src/theory/strings/theory_strings_utils.h
@@ -56,7 +56,27 @@ void getConcat(Node n, std::vector<Node>& c);
* Make the concatentation from vector c
* The kind k is either STRING_CONCAT or REGEXP_CONCAT.
*/
-Node mkConcat(Kind k, std::vector<Node>& c);
+Node mkConcat(Kind k, const std::vector<Node>& c);
+
+/**
+ * Returns the rewritten form of the string concatenation of n1 and n2.
+ */
+Node mkNConcat(Node n1, Node n2);
+
+/**
+ * Returns the rewritten form of the string concatenation of n1, n2 and n3.
+ */
+Node mkNConcat(Node n1, Node n2, Node n3);
+
+/**
+ * Returns the rewritten form of the string concatenation of nodes in c.
+ */
+Node mkNConcat(const std::vector<Node>& c);
+
+/**
+ * Returns the rewritten form of the length of string term t.
+ */
+Node mkNLength(Node t);
/**
* Get constant component. Returns the string constant represented by the
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback