theory/shared_terms_database.h
theory/sort_inference.cpp
theory/sort_inference.h
+ theory/strings/infer_info.cpp
+ theory/strings/infer_info.h
theory/strings/inference_manager.cpp
theory/strings/inference_manager.h
theory/strings/normal_form.cpp
--- /dev/null
+/********************* */
+/*! \file infer_info.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 inference information utility.
+ **/
+
+#include "theory/strings/infer_info.h"
+
+using namespace CVC4::kind;
+
+namespace CVC4 {
+namespace theory {
+namespace strings {
+
+std::ostream& operator<<(std::ostream& out, Inference i)
+{
+ switch (i)
+ {
+ case INFER_SSPLIT_CST_PROP: out << "S-Split(CST-P)-prop"; break;
+ case INFER_SSPLIT_VAR_PROP: out << "S-Split(VAR)-prop"; break;
+ case INFER_LEN_SPLIT: out << "Len-Split(Len)"; break;
+ case INFER_LEN_SPLIT_EMP: out << "Len-Split(Emp)"; break;
+ case INFER_SSPLIT_CST_BINARY: out << "S-Split(CST-P)-binary"; break;
+ case INFER_SSPLIT_CST: out << "S-Split(CST-P)"; break;
+ case INFER_SSPLIT_VAR: out << "S-Split(VAR)"; break;
+ case INFER_FLOOP: out << "F-Loop"; break;
+ default: out << "?"; break;
+ }
+ return out;
+}
+
+InferInfo::InferInfo() : d_id(INFER_NONE), d_index(0), d_rev(false) {}
+
+} // namespace strings
+} // namespace theory
+} // namespace CVC4
--- /dev/null
+/********************* */
+/*! \file infer_info.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 Inference information utility
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__THEORY__STRINGS__INFER_INFO_H
+#define CVC4__THEORY__STRINGS__INFER_INFO_H
+
+#include <map>
+#include <vector>
+#include "expr/node.h"
+
+namespace CVC4 {
+namespace theory {
+namespace strings {
+
+/** Types of inferences used in the procedure
+ *
+ * These are variants of the inference rules in Figures 3-5 of Liang et al.
+ * "A DPLL(T) Solver for a Theory of Strings and Regular Expressions", CAV 2014.
+ */
+enum Inference
+{
+ INFER_NONE = 0,
+ // string split constant propagation, for example:
+ // x = y, x = "abc", y = y1 ++ "b" ++ y2
+ // implies y1 = "a" ++ y1'
+ INFER_SSPLIT_CST_PROP = 1,
+ // string split variable propagation, for example:
+ // x = y, x = x1 ++ x2, y = y1 ++ y2, len( x1 ) >= len( y1 )
+ // implies x1 = y1 ++ x1'
+ // This is inspired by Zheng et al CAV 2015.
+ INFER_SSPLIT_VAR_PROP,
+ // length split, for example:
+ // len( x1 ) = len( y1 ) V len( x1 ) != len( y1 )
+ // This is inferred when e.g. x = y, x = x1 ++ x2, y = y1 ++ y2.
+ INFER_LEN_SPLIT,
+ // length split empty, for example:
+ // z = "" V z != ""
+ // This is inferred when, e.g. x = y, x = z ++ x1, y = y1 ++ z
+ INFER_LEN_SPLIT_EMP,
+ // string split constant binary, for example:
+ // x1 = "aaaa" ++ x1' V "aaaa" = x1 ++ x1'
+ // This is inferred when, e.g. x = y, x = x1 ++ x2, y = "aaaaaaaa" ++ y2.
+ // This inference is disabled by default and is enabled by stringBinaryCsp().
+ INFER_SSPLIT_CST_BINARY,
+ // string split constant
+ // x = y, x = "c" ++ x2, y = y1 ++ y2, y1 != ""
+ // implies y1 = "c" ++ y1'
+ // This is a special case of F-Split in Figure 5 of Liang et al CAV 2014.
+ INFER_SSPLIT_CST,
+ // string split variable, for example:
+ // x = y, x = x1 ++ x2, y = y1 ++ y2
+ // implies x1 = y1 ++ x1' V y1 = x1 ++ y1'
+ // This is rule F-Split in Figure 5 of Liang et al CAV 2014.
+ INFER_SSPLIT_VAR,
+ // flat form loop, for example:
+ // x = y, x = x1 ++ z, y = z ++ y2
+ // implies z = u2 ++ u1, u in ( u1 ++ u2 )*, x1 = u2 ++ u, y2 = u ++ u1
+ // for fresh u, u1, u2.
+ // This is the rule F-Loop from Figure 5 of Liang et al CAV 2014.
+ INFER_FLOOP,
+};
+std::ostream& operator<<(std::ostream& out, Inference i);
+
+/**
+ * Length status, used for indicating the length constraints for Skolems
+ * introduced by the theory of strings.
+ */
+enum LengthStatus
+{
+ // The length of the Skolem is not specified, and should be split on.
+ LENGTH_SPLIT,
+ // The length of the Skolem is exactly one.
+ LENGTH_ONE,
+ // The length of the Skolem is greater than or equal to one.
+ LENGTH_GEQ_ONE
+};
+
+/**
+ * This data structure encapsulates an inference for strings. This includes
+ * the form of the inference, as well as the side effects it generates.
+ */
+class InferInfo
+{
+ public:
+ InferInfo();
+ /**
+ * The identifier for the inference, indicating the kind of reasoning used
+ * for this conclusion.
+ */
+ Inference d_id;
+ /** The conclusion of the inference */
+ Node d_conc;
+ /**
+ * The antecedant(s) of the inference, interpreted conjunctively. These are
+ * literals that currently hold in the equality engine.
+ */
+ std::vector<Node> d_ant;
+ /**
+ * The "new literal" antecedant(s) of the inference, interpreted
+ * conjunctively. These are literals that were needed to show the conclusion
+ * but do not currently hold in the equality engine.
+ */
+ std::vector<Node> d_antn;
+ /**
+ * A list of new skolems introduced as a result of this inference. They
+ * are mapped to by a length status, indicating the length constraint that
+ * can be assumed for them.
+ */
+ std::map<LengthStatus, std::vector<Node> > d_new_skolem;
+ /**
+ * The pending phase requirements, see InferenceManager::sendPhaseRequirement.
+ */
+ std::map<Node, bool> d_pending_phase;
+ /**
+ * The index in the normal forms under which this inference is addressing.
+ * For example, if the inference is inferring x = y from |x|=|y| and
+ * w ++ x ++ ... = w ++ y ++ ...
+ * then d_index is 1, since x and y are at index 1 in these concat terms.
+ */
+ unsigned d_index;
+ /**
+ * The normal form pair that is cached as a result of this inference.
+ */
+ Node d_nf_pair[2];
+ /** for debugging
+ *
+ * The base pair of strings d_i/d_j that led to the inference, and whether
+ * (d_rev) we were processing the normal forms of these strings in reverse
+ * direction.
+ */
+ Node d_i;
+ Node d_j;
+ bool d_rev;
+};
+
+} // namespace strings
+} // namespace theory
+} // namespace CVC4
+
+#endif /* CVC4__THEORY__STRINGS__THEORY_STRINGS_H */
return true;
}
-void InferenceManager::sendInference(std::vector<Node>& exp,
- std::vector<Node>& exp_n,
+void InferenceManager::sendInference(const std::vector<Node>& exp,
+ const std::vector<Node>& exp_n,
Node eq,
const char* c,
bool asLemma)
}
}
-void InferenceManager::sendInference(std::vector<Node>& exp,
+void InferenceManager::sendInference(const std::vector<Node>& exp,
Node eq,
const char* c,
bool asLemma)
sendInference(exp, exp_n, eq, c, asLemma);
}
+void InferenceManager::sendInference(const InferInfo& i)
+{
+ std::stringstream ssi;
+ ssi << i.d_id;
+ sendInference(i.d_ant, i.d_antn, i.d_conc, ssi.str().c_str(), true);
+}
+
void InferenceManager::sendLemma(Node ant, Node conc, const char* c)
{
if (conc.isNull() || conc == d_false)
#include "context/context.h"
#include "expr/node.h"
#include "theory/output_channel.h"
+#include "theory/strings/infer_info.h"
#include "theory/uf/equality_engine.h"
namespace CVC4 {
* If the flag asLemma is true, then this method will send a lemma instead
* of an inference whenever applicable.
*/
- void sendInference(std::vector<Node>& exp,
- std::vector<Node>& exp_n,
+ void sendInference(const std::vector<Node>& exp,
+ const std::vector<Node>& exp_n,
Node eq,
const char* c,
bool asLemma = false);
/** same as above, but where exp_n is empty */
- void sendInference(std::vector<Node>& exp,
+ void sendInference(const std::vector<Node>& exp,
Node eq,
const char* c,
bool asLemma = false);
+ /** Send inference
+ *
+ * Makes the appropriate call to send inference based on the infer info
+ * data structure (see sendInference documentation above).
+ */
+ void sendInference(const InferInfo& i);
/** Send split
*
* This requests that ( a = b V a != b ) is sent on the output channel as a
namespace theory {
namespace strings {
-std::ostream& operator<<(std::ostream& out, Inference i)
-{
- switch (i)
- {
- case INFER_SSPLIT_CST_PROP: out << "S-Split(CST-P)-prop"; break;
- case INFER_SSPLIT_VAR_PROP: out << "S-Split(VAR)-prop"; break;
- case INFER_LEN_SPLIT: out << "Len-Split(Len)"; break;
- case INFER_LEN_SPLIT_EMP: out << "Len-Split(Emp)"; break;
- case INFER_SSPLIT_CST_BINARY: out << "S-Split(CST-P)-binary"; break;
- case INFER_SSPLIT_CST: out << "S-Split(CST-P)"; break;
- case INFER_SSPLIT_VAR: out << "S-Split(VAR)"; break;
- case INFER_FLOOP: out << "F-Loop"; break;
- default: out << "?"; break;
- }
- return out;
-}
-
std::ostream& operator<<(std::ostream& out, InferStep s)
{
switch (s)
set_use_index = true;
}
}
+ doInferInfo(pinfer[use_index]);
+}
+
+void TheoryStrings::doInferInfo(const InferInfo& ii)
+{
// send the inference
- if (!pinfer[use_index].d_nf_pair[0].isNull())
+ if (!ii.d_nf_pair[0].isNull())
{
- Assert(!pinfer[use_index].d_nf_pair[1].isNull());
- addNormalFormPair(pinfer[use_index].d_nf_pair[0],
- pinfer[use_index].d_nf_pair[1]);
- }
- std::stringstream ssi;
- ssi << pinfer[use_index].d_id;
- d_im.sendInference(pinfer[use_index].d_ant,
- pinfer[use_index].d_antn,
- pinfer[use_index].d_conc,
- ssi.str().c_str(),
- pinfer[use_index].sendAsLemma());
+ Assert(!ii.d_nf_pair[1].isNull());
+ addNormalFormPair(ii.d_nf_pair[0], ii.d_nf_pair[1]);
+ }
+ // send the inference
+ d_im.sendInference(ii);
// Register the new skolems from this inference. We register them here
// (lazily), since the code above has now decided to use the inference
// at use_index that involves them.
for (const std::pair<const LengthStatus, std::vector<Node> >& sks :
- pinfer[use_index].d_new_skolem)
+ ii.d_new_skolem)
{
for (const Node& n : sks.second)
{
}
}
-bool TheoryStrings::InferInfo::sendAsLemma() {
- return true;
-}
-
void TheoryStrings::processSimpleNEq(NormalForm& nfi,
NormalForm& nfj,
unsigned& index,
return Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, t ) );
}
-Node TheoryStrings::mkExplain( std::vector< Node >& a ) {
+Node TheoryStrings::mkExplain(const std::vector<Node>& a)
+{
std::vector< Node > an;
return mkExplain( a, an );
}
-Node TheoryStrings::mkExplain( std::vector< Node >& a, std::vector< Node >& an ) {
+Node TheoryStrings::mkExplain(const std::vector<Node>& a,
+ const std::vector<Node>& an)
+{
std::vector< TNode > antec_exp;
- for( unsigned i=0; i<a.size(); i++ ) {
- if( std::find( a.begin(), a.begin() + i, a[i] )==a.begin() + i ) {
- bool exp = true;
- Debug("strings-explain") << "Ask for explanation of " << a[i] << std::endl;
- //assert
- if(a[i].getKind() == kind::EQUAL) {
- //Assert( hasTerm(a[i][0]) );
- //Assert( hasTerm(a[i][1]) );
- Assert( areEqual(a[i][0], a[i][1]) );
- if( a[i][0]==a[i][1] ){
- exp = false;
- }
- } else if( a[i].getKind()==kind::NOT && a[i][0].getKind()==kind::EQUAL ) {
- Assert( hasTerm(a[i][0][0]) );
- Assert( hasTerm(a[i][0][1]) );
- AlwaysAssert( d_equalityEngine.areDisequal(a[i][0][0], a[i][0][1], true) );
- }else if( a[i].getKind() == kind::AND ){
- for( unsigned j=0; j<a[i].getNumChildren(); j++ ){
- a.push_back( a[i][j] );
- }
- exp = false;
- }
- if( exp ) {
- unsigned ps = antec_exp.size();
- explain(a[i], antec_exp);
- Debug("strings-explain") << "Done, explanation was : " << std::endl;
- for( unsigned j=ps; j<antec_exp.size(); j++ ) {
- Debug("strings-explain") << " " << antec_exp[j] << std::endl;
- }
- Debug("strings-explain") << std::endl;
- }
+ // copy to processing vector
+ std::vector<Node> aconj;
+ for (const Node& ac : a)
+ {
+ utils::flattenOp(AND, ac, aconj);
+ }
+ for (const Node& apc : aconj)
+ {
+ Assert(apc.getKind() != AND);
+ 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]));
+ // ensure that we are ready to explain the disequality
+ AlwaysAssert(d_equalityEngine.areDisequal(apc[0][0], apc[0][1], true));
}
+ Assert(apc.getKind() != EQUAL || d_equalityEngine.areEqual(apc[0], apc[1]));
+ // now, explain
+ explain(apc, antec_exp);
}
- for( unsigned i=0; i<an.size(); i++ ) {
- if( std::find( an.begin(), an.begin() + i, an[i] )==an.begin() + i ){
- Debug("strings-explain") << "Add to explanation (new literal) " << an[i] << std::endl;
- antec_exp.push_back(an[i]);
+ for (const Node& anc : an)
+ {
+ if (std::find(antec_exp.begin(), antec_exp.end(), anc) == antec_exp.end())
+ {
+ Debug("strings-explain")
+ << "Add to explanation (new literal) " << anc << std::endl;
+ antec_exp.push_back(anc);
}
}
Node ant;
} else {
ant = NodeManager::currentNM()->mkNode( kind::AND, antec_exp );
}
- //ant = Rewriter::rewrite( ant );
return ant;
}
#include "expr/attribute.h"
#include "expr/node_trie.h"
#include "theory/decision_manager.h"
+#include "theory/strings/infer_info.h"
#include "theory/strings/inference_manager.h"
#include "theory/strings/normal_form.h"
#include "theory/strings/regexp_elim.h"
*
*/
-/** Types of inferences used in the procedure
- *
- * These are variants of the inference rules in Figures 3-5 of Liang et al.
- * "A DPLL(T) Solver for a Theory of Strings and Regular Expressions", CAV 2014.
- */
-enum Inference
-{
- INFER_NONE,
- // string split constant propagation, for example:
- // x = y, x = "abc", y = y1 ++ "b" ++ y2
- // implies y1 = "a" ++ y1'
- INFER_SSPLIT_CST_PROP,
- // string split variable propagation, for example:
- // x = y, x = x1 ++ x2, y = y1 ++ y2, len( x1 ) >= len( y1 )
- // implies x1 = y1 ++ x1'
- // This is inspired by Zheng et al CAV 2015.
- INFER_SSPLIT_VAR_PROP,
- // length split, for example:
- // len( x1 ) = len( y1 ) V len( x1 ) != len( y1 )
- // This is inferred when e.g. x = y, x = x1 ++ x2, y = y1 ++ y2.
- INFER_LEN_SPLIT,
- // length split empty, for example:
- // z = "" V z != ""
- // This is inferred when, e.g. x = y, x = z ++ x1, y = y1 ++ z
- INFER_LEN_SPLIT_EMP,
- // string split constant binary, for example:
- // x1 = "aaaa" ++ x1' V "aaaa" = x1 ++ x1'
- // This is inferred when, e.g. x = y, x = x1 ++ x2, y = "aaaaaaaa" ++ y2.
- // This inference is disabled by default and is enabled by stringBinaryCsp().
- INFER_SSPLIT_CST_BINARY,
- // string split constant
- // x = y, x = "c" ++ x2, y = y1 ++ y2, y1 != ""
- // implies y1 = "c" ++ y1'
- // This is a special case of F-Split in Figure 5 of Liang et al CAV 2014.
- INFER_SSPLIT_CST,
- // string split variable, for example:
- // x = y, x = x1 ++ x2, y = y1 ++ y2
- // implies x1 = y1 ++ x1' V y1 = x1 ++ y1'
- // This is rule F-Split in Figure 5 of Liang et al CAV 2014.
- INFER_SSPLIT_VAR,
- // flat form loop, for example:
- // x = y, x = x1 ++ z, y = z ++ y2
- // implies z = u2 ++ u1, u in ( u1 ++ u2 )*, x1 = u2 ++ u, y2 = u ++ u1
- // for fresh u, u1, u2.
- // This is the rule F-Loop from Figure 5 of Liang et al CAV 2014.
- INFER_FLOOP,
-};
-std::ostream& operator<<(std::ostream& out, Inference i);
-
/** inference steps
*
* Corresponds to a step in the overall strategy of the strings solver. For
};
private:
- /** Length status, used for the registerLength function below */
- enum LengthStatus
- {
- LENGTH_SPLIT,
- LENGTH_ONE,
- LENGTH_GEQ_ONE
- };
/** register length
*
*/
void registerLength(Node n, LengthStatus s);
- //------------------------- candidate inferences
- class InferInfo
- {
- public:
- /** for debugging
- *
- * The base pair of strings d_i/d_j that led to the inference, and whether
- * (d_rev) we were processing the normal forms of these strings in reverse
- * direction.
- */
- Node d_i;
- Node d_j;
- bool d_rev;
- std::vector<Node> d_ant;
- std::vector<Node> d_antn;
- std::map<LengthStatus, std::vector<Node> > d_new_skolem;
- Node d_conc;
- Inference d_id;
- std::map<Node, bool> d_pending_phase;
- unsigned d_index;
- Node d_nf_pair[2];
- bool sendAsLemma();
- };
- //------------------------- end candidate inferences
/** cache of all skolems */
SkolemCache d_sk_cache;
* of atom, including calls to registerTerm.
*/
void assertPendingFact(Node atom, bool polarity, Node exp);
+ /**
+ * 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.
inline Node mkConcat(const std::vector<Node>& c);
inline Node mkLength(Node n);
- /** mkExplain **/
- Node mkExplain(std::vector<Node>& a);
- Node mkExplain(std::vector<Node>& a, std::vector<Node>& an);
+ /** make explanation
+ *
+ * This returns a node corresponding to the explanation of formulas in a,
+ * interpreted conjunctively. The returned node is a conjunction of literals
+ * that have been asserted to the equality engine.
+ */
+ Node mkExplain(const std::vector<Node>& a);
+ /** Same as above, but the new literals an are append to the result */
+ Node mkExplain(const std::vector<Node>& a, const std::vector<Node>& an);
protected:
namespace strings {
namespace utils {
-Node mkAnd(std::vector<Node>& a)
+Node mkAnd(const std::vector<Node>& a)
{
std::vector<Node> au;
for (const Node& ai : a)
return NodeManager::currentNM()->mkNode(AND, au);
}
+void flattenOp(Kind k, Node n, std::vector<Node>& conj)
+{
+ if (n.getKind() != k)
+ {
+ // easy case, just add to conj if non-duplicate
+ if (std::find(conj.begin(), conj.end(), n) == conj.end())
+ {
+ conj.push_back(n);
+ }
+ return;
+ }
+ // otherwise, traverse
+ std::unordered_set<TNode, TNodeHashFunction> visited;
+ std::unordered_set<TNode, TNodeHashFunction>::iterator it;
+ std::vector<TNode> visit;
+ TNode cur;
+ visit.push_back(n);
+ do
+ {
+ cur = visit.back();
+ visit.pop_back();
+ it = visited.find(cur);
+
+ if (it == visited.end())
+ {
+ visited.insert(cur);
+ if (cur.getKind() == k)
+ {
+ for (const Node& cn : cur)
+ {
+ visit.push_back(cn);
+ }
+ }
+ else if (std::find(conj.begin(), conj.end(), cur) == conj.end())
+ {
+ conj.push_back(cur);
+ }
+ }
+ } while (!visit.empty());
+}
+
void getConcat(Node n, std::vector<Node>& c)
{
Kind k = n.getKind();
* Make the conjunction of nodes in a. Removes duplicate conjuncts, returns
* true if a is empty, and a single literal if a has size 1.
*/
-Node mkAnd(std::vector<Node>& a);
+Node mkAnd(const std::vector<Node>& a);
+
+/**
+ * Adds all (non-duplicate) children of <k> applications from n to conj. For
+ * example, given (<k> (<k> A B) C A), we add { A, B, C } to conj.
+ */
+void flattenOp(Kind k, Node n, std::vector<Node>& conj);
/**
* Gets the "vector form" of term n, adds it to c.
projects / cvc5.git / commitdiff