theory/shared_terms_database.h
theory/sort_inference.cpp
theory/sort_inference.h
+ theory/strings/inference_manager.cpp
+ theory/strings/inference_manager.h
theory/strings/normal_form.cpp
theory/strings/normal_form.h
theory/strings/regexp_elim.cpp
theory/strings/theory_strings_rewriter.cpp
theory/strings/theory_strings_rewriter.h
theory/strings/theory_strings_type_rules.h
+ theory/strings/theory_strings_utils.cpp
+ theory/strings/theory_strings_utils.h
theory/strings/type_enumerator.h
theory/subs_minimize.cpp
theory/subs_minimize.h
--- /dev/null
+/********************* */
+/*! \file inference_manager.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 inference manager for the theory of strings.
+ **/
+
+#include "theory/strings/inference_manager.h"
+
+#include "expr/kind.h"
+#include "options/strings_options.h"
+#include "theory/rewriter.h"
+#include "theory/strings/theory_strings.h"
+#include "theory/strings/theory_strings_rewriter.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 {
+
+InferenceManager::InferenceManager(TheoryStrings& p,
+ context::Context* c,
+ context::UserContext* u,
+ eq::EqualityEngine& ee,
+ OutputChannel& out)
+ : d_parent(p), d_ee(ee), d_out(out), d_keep(c)
+{
+ d_true = NodeManager::currentNM()->mkConst(true);
+ d_false = NodeManager::currentNM()->mkConst(false);
+}
+
+bool InferenceManager::sendInternalInference(std::vector<Node>& exp,
+ Node conc,
+ const char* c)
+{
+ if (conc.getKind() == AND
+ || (conc.getKind() == NOT && conc[0].getKind() == OR))
+ {
+ Node conj = conc.getKind() == AND ? conc : conc[0];
+ bool pol = conc.getKind() == AND;
+ bool ret = true;
+ for (const Node& cc : conj)
+ {
+ bool retc = sendInternalInference(exp, pol ? cc : cc.negate(), c);
+ ret = ret && retc;
+ }
+ return ret;
+ }
+ bool pol = conc.getKind() != NOT;
+ Node lit = pol ? conc : conc[0];
+ if (lit.getKind() == EQUAL)
+ {
+ for (unsigned i = 0; i < 2; i++)
+ {
+ if (!lit[i].isConst() && !d_parent.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]))
+ {
+ return true;
+ }
+ }
+ else if (lit.isConst())
+ {
+ if (lit.getConst<bool>())
+ {
+ Assert(pol);
+ // trivially holds
+ return true;
+ }
+ }
+ else if (!d_parent.hasTerm(lit))
+ {
+ // introduces a new non-constant term, do not infer
+ return false;
+ }
+ else if (d_parent.areEqual(lit, pol ? d_true : d_false))
+ {
+ // already holds
+ return true;
+ }
+ sendInference(exp, conc, c);
+ return true;
+}
+
+void InferenceManager::sendInference(std::vector<Node>& exp,
+ std::vector<Node>& exp_n,
+ Node eq,
+ const char* c,
+ bool asLemma)
+{
+ eq = eq.isNull() ? d_false : Rewriter::rewrite(eq);
+ if (eq == d_true)
+ {
+ return;
+ }
+ if (Trace.isOn("strings-infer-debug"))
+ {
+ Trace("strings-infer-debug")
+ << "By " << c << ", infer : " << eq << " from: " << std::endl;
+ for (unsigned i = 0; i < exp.size(); i++)
+ {
+ Trace("strings-infer-debug") << " " << exp[i] << std::endl;
+ }
+ for (unsigned i = 0; i < exp_n.size(); i++)
+ {
+ Trace("strings-infer-debug") << " N:" << exp_n[i] << std::endl;
+ }
+ }
+ // check if we should send a lemma or an inference
+ if (asLemma || eq == d_false || eq.getKind() == OR || !exp_n.empty()
+ || options::stringInferAsLemmas())
+ {
+ Node eq_exp;
+ if (options::stringRExplainLemmas())
+ {
+ eq_exp = d_parent.mkExplain(exp, exp_n);
+ }
+ else
+ {
+ if (exp.empty())
+ {
+ eq_exp = utils::mkAnd(exp_n);
+ }
+ else if (exp_n.empty())
+ {
+ eq_exp = utils::mkAnd(exp);
+ }
+ else
+ {
+ std::vector<Node> ev;
+ ev.insert(ev.end(), exp.begin(), exp.end());
+ ev.insert(ev.end(), exp_n.begin(), exp_n.end());
+ eq_exp = NodeManager::currentNM()->mkNode(AND, ev);
+ }
+ }
+ // if we have unexplained literals, this lemma is not a conflict
+ if (eq == d_false && !exp_n.empty())
+ {
+ eq = eq_exp.negate();
+ eq_exp = d_true;
+ }
+ sendLemma(eq_exp, eq, c);
+ }
+ else
+ {
+ sendInfer(utils::mkAnd(exp), eq, c);
+ }
+}
+
+void InferenceManager::sendInference(std::vector<Node>& exp,
+ Node eq,
+ const char* c,
+ bool asLemma)
+{
+ std::vector<Node> exp_n;
+ sendInference(exp, exp_n, eq, c, asLemma);
+}
+
+void InferenceManager::sendLemma(Node ant, Node conc, const char* c)
+{
+ if (conc.isNull() || conc == d_false)
+ {
+ Trace("strings-conflict")
+ << "Strings::Conflict : " << c << " : " << ant << std::endl;
+ Trace("strings-lemma") << "Strings::Conflict : " << c << " : " << ant
+ << std::endl;
+ Trace("strings-assert")
+ << "(assert (not " << ant << ")) ; conflict " << c << std::endl;
+ d_out.conflict(ant);
+ d_parent.d_conflict = true;
+ return;
+ }
+ Node lem;
+ if (ant == d_true)
+ {
+ lem = conc;
+ }
+ else
+ {
+ lem = NodeManager::currentNM()->mkNode(IMPLIES, ant, conc);
+ }
+ Trace("strings-lemma") << "Strings::Lemma " << c << " : " << lem << std::endl;
+ Trace("strings-assert") << "(assert " << lem << ") ; lemma " << c
+ << std::endl;
+ d_pendingLem.push_back(lem);
+}
+
+void InferenceManager::sendInfer(Node eq_exp, Node eq, const char* c)
+{
+ if (options::stringInferSym())
+ {
+ std::vector<Node> vars;
+ std::vector<Node> subs;
+ std::vector<Node> unproc;
+ inferSubstitutionProxyVars(eq_exp, vars, subs, unproc);
+ if (unproc.empty())
+ {
+ Node eqs =
+ eq.substitute(vars.begin(), vars.end(), subs.begin(), subs.end());
+ if (Trace.isOn("strings-lemma-debug"))
+ {
+ Trace("strings-lemma-debug") << "Strings::Infer " << eq << " from "
+ << eq_exp << " by " << c << std::endl;
+ Trace("strings-lemma-debug")
+ << "Strings::Infer Alternate : " << eqs << std::endl;
+ for (unsigned i = 0, nvars = vars.size(); i < nvars; i++)
+ {
+ Trace("strings-lemma-debug")
+ << " " << vars[i] << " -> " << subs[i] << std::endl;
+ }
+ }
+ sendLemma(d_true, eqs, c);
+ return;
+ }
+ if (Trace.isOn("strings-lemma-debug"))
+ {
+ for (const Node& u : unproc)
+ {
+ Trace("strings-lemma-debug")
+ << " non-trivial exp : " << u << std::endl;
+ }
+ }
+ }
+ Trace("strings-lemma") << "Strings::Infer " << eq << " from " << eq_exp
+ << " by " << c << std::endl;
+ Trace("strings-assert") << "(assert (=> " << eq_exp << " " << eq
+ << ")) ; infer " << c << std::endl;
+ d_pending.push_back(eq);
+ d_pendingExp[eq] = eq_exp;
+ d_keep.insert(eq);
+ d_keep.insert(eq_exp);
+}
+
+bool InferenceManager::sendSplit(Node a, Node b, const char* c, bool preq)
+{
+ Node eq = a.eqNode(b);
+ eq = Rewriter::rewrite(eq);
+ if (eq.isConst())
+ {
+ return false;
+ }
+ NodeManager* nm = NodeManager::currentNM();
+ Node lemma_or = nm->mkNode(OR, eq, nm->mkNode(NOT, eq));
+ Trace("strings-lemma") << "Strings::Lemma " << c << " SPLIT : " << lemma_or
+ << std::endl;
+ d_pendingLem.push_back(lemma_or);
+ sendPhaseRequirement(eq, preq);
+ return true;
+}
+
+void InferenceManager::sendPhaseRequirement(Node lit, bool pol)
+{
+ d_pendingReqPhase[lit] = pol;
+}
+
+void InferenceManager::doPendingFacts()
+{
+ size_t i = 0;
+ while (!hasConflict() && i < d_pending.size())
+ {
+ Node fact = d_pending[i];
+ Node exp = d_pendingExp[fact];
+ if (fact.getKind() == AND)
+ {
+ for (const Node& lit : fact)
+ {
+ bool polarity = lit.getKind() != NOT;
+ TNode atom = polarity ? lit : lit[0];
+ d_parent.assertPendingFact(atom, polarity, exp);
+ }
+ }
+ else
+ {
+ bool polarity = fact.getKind() != NOT;
+ TNode atom = polarity ? fact : fact[0];
+ d_parent.assertPendingFact(atom, polarity, exp);
+ }
+ i++;
+ }
+ d_pending.clear();
+ d_pendingExp.clear();
+}
+
+void InferenceManager::doPendingLemmas()
+{
+ if (!hasConflict())
+ {
+ for (const Node& lc : d_pendingLem)
+ {
+ Trace("strings-pending") << "Process pending lemma : " << lc << std::endl;
+ d_out.lemma(lc);
+ }
+ for (const std::pair<const Node, bool>& prp : d_pendingReqPhase)
+ {
+ Trace("strings-pending") << "Require phase : " << prp.first
+ << ", polarity = " << prp.second << std::endl;
+ d_out.requirePhase(prp.first, prp.second);
+ }
+ }
+ d_pendingLem.clear();
+ d_pendingReqPhase.clear();
+}
+
+bool InferenceManager::hasConflict() const { return d_parent.d_conflict; }
+
+void InferenceManager::inferSubstitutionProxyVars(
+ Node n,
+ std::vector<Node>& vars,
+ std::vector<Node>& subs,
+ std::vector<Node>& unproc) const
+{
+ if (n.getKind() == AND)
+ {
+ for (const Node& nc : n)
+ {
+ inferSubstitutionProxyVars(nc, vars, subs, unproc);
+ }
+ return;
+ }
+ if (n.getKind() == EQUAL)
+ {
+ Node ns = n.substitute(vars.begin(), vars.end(), subs.begin(), subs.end());
+ ns = Rewriter::rewrite(ns);
+ if (ns.getKind() == EQUAL)
+ {
+ Node s;
+ Node v;
+ for (unsigned i = 0; i < 2; i++)
+ {
+ Node ss;
+ // determine whether this side has a proxy variable
+ if (ns[i].getAttribute(StringsProxyVarAttribute()))
+ {
+ // it is a proxy variable
+ ss = ns[i];
+ }
+ else if (ns[i].isConst())
+ {
+ ss = d_parent.getProxyVariableFor(ns[i]);
+ }
+ if (!ss.isNull())
+ {
+ v = ns[1 - i];
+ // if the other side is a constant or variable
+ if (v.getNumChildren() == 0)
+ {
+ if (s.isNull())
+ {
+ s = ss;
+ }
+ else
+ {
+ // both sides of the equality correspond to a proxy variable
+ if (ss == s)
+ {
+ // it is a trivial equality, e.g. between a proxy variable
+ // and its definition
+ return;
+ }
+ else
+ {
+ // equality between proxy variables, non-trivial
+ s = Node::null();
+ }
+ }
+ }
+ }
+ }
+ if (!s.isNull())
+ {
+ // the equality can be turned into a substitution
+ subs.push_back(s);
+ vars.push_back(v);
+ return;
+ }
+ }
+ else
+ {
+ n = ns;
+ }
+ }
+ if (n != d_true)
+ {
+ unproc.push_back(n);
+ }
+}
+
+} // namespace strings
+} // namespace theory
+} // namespace CVC4
--- /dev/null
+/********************* */
+/*! \file inference_manager.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 Customized inference manager for the theory of strings
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__THEORY__STRINGS__INFERENCE_MANAGER_H
+#define CVC4__THEORY__STRINGS__INFERENCE_MANAGER_H
+
+#include <map>
+#include <vector>
+
+#include "context/cdhashset.h"
+#include "context/context.h"
+#include "expr/node.h"
+#include "theory/output_channel.h"
+#include "theory/uf/equality_engine.h"
+
+namespace CVC4 {
+namespace theory {
+namespace strings {
+
+class TheoryStrings;
+
+/** Inference Manager
+ *
+ * The purpose of this class is to process inference steps for strategies
+ * in the theory of strings.
+ *
+ * In particular, inferences are given to this class via calls to functions:
+ *
+ * sendInternalInference, sendInference, sendSplit
+ *
+ * This class decides how the conclusion of these calls will be processed.
+ * It primarily has to decide whether the conclusions will be processed:
+ *
+ * (1) Internally in the strings solver, via calls to equality engine's
+ * assertLiteral and assertPredicate commands. We refer to these literals as
+ * "facts",
+ * (2) Externally on the output channel of theory of strings as "lemmas",
+ * (3) External on the output channel as "conflicts" (when a conclusion of an
+ * inference is false).
+ *
+ * It buffers facts and lemmas in vectors d_pending and d_pending_lem
+ * respectively.
+ *
+ * When applicable, facts can be flushed to the equality engine via a call to
+ * doPendingFacts, and lemmas can be flushed to the output channel via a call
+ * to doPendingLemmas.
+ *
+ * It also manages other kinds of interaction with the output channel of the
+ * theory of strings, e.g. sendPhaseRequirement.
+ */
+class InferenceManager
+{
+ typedef context::CDHashSet<Node, NodeHashFunction> NodeSet;
+
+ public:
+ InferenceManager(TheoryStrings& p,
+ context::Context* c,
+ context::UserContext* u,
+ eq::EqualityEngine& ee,
+ OutputChannel& out);
+ ~InferenceManager() {}
+
+ /** send internal inferences
+ *
+ * This is called when we have inferred exp => conc, where exp is a set
+ * of equalities and disequalities that hold in the current equality engine.
+ * This method adds equalities and disequalities ~( s = t ) via
+ * sendInference such that both s and t are either constants or terms
+ * that already occur in the equality engine, and ~( s = t ) is a consequence
+ * of conc. This function can be seen as a "conservative" version of
+ * sendInference below in that it does not introduce any new non-constant
+ * terms to the state.
+ *
+ * The argument c is a string identifying the reason for the inference.
+ * This string is used for debugging purposes.
+ *
+ * Return true if the inference is complete, in the sense that we infer
+ * inferences that are equivalent to conc. This returns false e.g. if conc
+ * (or one of its conjuncts if it is a conjunction) was not inferred due
+ * to the criteria mentioned above.
+ */
+ bool sendInternalInference(std::vector<Node>& exp, Node conc, const char* c);
+ /** send inference
+ *
+ * This function should be called when ( exp ^ exp_n ) => eq. The set exp
+ * contains literals that are explainable, i.e. those that hold in the
+ * equality engine of the theory of strings. On the other hand, the set
+ * exp_n ("explanations new") contain nodes that are not explainable by the
+ * theory of strings. This method may call sendInfer or sendLemma. Overall,
+ * the result of this method is one of the following:
+ *
+ * [1] (No-op) Do nothing if eq is true,
+ *
+ * [2] (Infer) Indicate that eq should be added to the equality engine of this
+ * class with explanation EXPLAIN(exp), where EXPLAIN returns the
+ * explanation of the node in exp in terms of the literals asserted to the
+ * theory of strings,
+ *
+ * [3] (Lemma) Indicate that the lemma ( EXPLAIN(exp) ^ exp_n ) => eq should
+ * be sent on the output channel of the theory of strings, or
+ *
+ * [4] (Conflict) Immediately report a conflict EXPLAIN(exp) on the output
+ * channel of the theory of strings.
+ *
+ * Determining which case to apply depends on the form of eq and whether
+ * exp_n is empty. In particular, lemmas must be used whenever exp_n is
+ * non-empty, conflicts are used when exp_n is empty and eq is false.
+ *
+ * The argument c is a string identifying the reason for inference, used for
+ * debugging.
+ *
+ * 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,
+ Node eq,
+ const char* c,
+ bool asLemma = false);
+ /** same as above, but where exp_n is empty */
+ void sendInference(std::vector<Node>& exp,
+ Node eq,
+ const char* c,
+ bool asLemma = false);
+ /** Send split
+ *
+ * This requests that ( a = b V a != b ) is sent on the output channel as a
+ * lemma. We additionally request a phase requirement for the equality a=b
+ * with polarity preq.
+ *
+ * The argument c is a string identifying the reason for inference, used for
+ * debugging.
+ *
+ * This method returns true if the split was non-trivial, and false
+ * otherwise. A split is trivial if a=b rewrites to a constant.
+ */
+ bool sendSplit(Node a, Node b, const char* c, bool preq = true);
+ /** Send phase requirement
+ *
+ * This method is called to indicate this class should send a phase
+ * requirement request to the output channel for literal lit to be
+ * decided with polarity pol.
+ */
+ void sendPhaseRequirement(Node lit, bool pol);
+ /** Do pending facts
+ *
+ * This method asserts pending facts (d_pending) with explanations
+ * (d_pendingExp) to the equality engine of the theory of strings via calls
+ * to assertPendingFact in the theory of strings.
+ *
+ * It terminates early if a conflict is encountered, for instance, by
+ * equality reasoning within the equality engine.
+ *
+ * Regardless of whether a conflict is encountered, the vector d_pending
+ * and map d_pendingExp are cleared.
+ */
+ void doPendingFacts();
+ /** Do pending lemmas
+ *
+ * This method flushes all pending lemmas (d_pending_lem) to the output
+ * channel of theory of strings.
+ *
+ * Like doPendingFacts, this function will terminate early if a conflict
+ * has already been encountered by the theory of strings. The vector
+ * d_pending_lem is cleared regardless of whether a conflict is discovered.
+ *
+ * Notice that as a result of the above design, some lemmas may be "dropped"
+ * if a conflict is discovered in between when a lemma is added to the
+ * pending vector of this class (via a sendInference call). Lemmas
+ * e.g. those that are required for initialization should not be sent via
+ * this class, since they should never be dropped.
+ */
+ void doPendingLemmas();
+ /**
+ * Have we processed an inference during this call to check? In particular,
+ * 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();
+ }
+ /** 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:
+ /**
+ * Indicates that ant => conc should be sent on the output channel of this
+ * class. This will either trigger an immediate call to the conflict
+ * method of the output channel of this class of conc is false, or adds the
+ * above lemma to the lemma cache d_pending_lem, which may be flushed
+ * later within the current call to TheoryStrings::check.
+ *
+ * The argument c is a string identifying the reason for inference, used for
+ * debugging.
+ */
+ void sendLemma(Node ant, Node conc, const char* c);
+ /**
+ * Indicates that conc should be added to the equality engine of this class
+ * with explanation eq_exp. It must be the case that eq_exp is a (conjunction
+ * of) literals that each are explainable, i.e. they already hold in the
+ * equality engine of this class.
+ */
+ void sendInfer(Node eq_exp, Node eq, const char* c);
+
+ /** 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.
+ */
+ eq::EqualityEngine& d_ee;
+ /** the output channel
+ *
+ * This is a reference to the output channel of the theory of strings.
+ */
+ OutputChannel& d_out;
+ /** Common constants */
+ Node d_true;
+ Node d_false;
+ /** The list of pending literals to assert to the equality engine */
+ std::vector<Node> d_pending;
+ /** A map from the literals in the above vector to their explanation */
+ std::map<Node, Node> d_pendingExp;
+ /** A map from literals to their pending phase requirement */
+ std::map<Node, bool> d_pendingReqPhase;
+ /** A list of pending lemmas to be sent on the output channel. */
+ std::vector<Node> d_pendingLem;
+ /**
+ * The keep set of this class. This set is maintained to ensure that
+ * facts and their explanations are ref-counted. Since facts and their
+ * explanations are SAT-context-dependent, this set is also
+ * SAT-context-dependent.
+ */
+ NodeSet d_keep;
+ /** infer substitution proxy vars
+ *
+ * This method attempts to (partially) convert the formula n into a
+ * substitution of the form:
+ * v1 -> s1, ..., vn -> sn
+ * where s1 ... sn are proxy variables and v1 ... vn are either variables
+ * or constants.
+ *
+ * This method ensures that P ^ v1 = s1 ^ ... ^ vn = sn ^ unproc is equivalent
+ * to P ^ n, where P is the conjunction of equalities corresponding to the
+ * definition of all proxy variables introduced by the theory of strings.
+ *
+ * For example, say that v1 was introduced as a proxy variable for "ABC", and
+ * v2 was introduced as a proxy variable for "AA".
+ *
+ * Given the input n := v1 = "ABC" ^ v2 = x ^ x = "AA", this method sets:
+ * vars = { x },
+ * subs = { v2 },
+ * unproc = {}.
+ * In particular, this says that the information content of n is essentially
+ * x = v2. The first and third conjunctions can be dropped from the
+ * explanation since these equalities simply correspond to definitions
+ * of proxy variables.
+ *
+ * This method is used as a performance heuristic. It can infer when the
+ * explanation of a fact depends only trivially on equalities corresponding
+ * to definitions of proxy variables, which can be omitted since they are
+ * assumed to hold globally.
+ */
+ void inferSubstitutionProxyVars(Node n,
+ std::vector<Node>& vars,
+ std::vector<Node>& subs,
+ std::vector<Node>& unproc) const;
+};
+
+} // namespace strings
+} // namespace theory
+} // namespace CVC4
+
+#endif
namespace strings {
RegExpSolver::RegExpSolver(TheoryStrings& p,
+ InferenceManager& im,
context::Context* c,
context::UserContext* u)
: d_parent(p),
+ d_im(im),
d_regexp_memberships(c),
d_regexp_ucached(u),
d_regexp_ccached(c),
vec_nodes.push_back(n);
}
Node conc;
- d_parent.sendInference(vec_nodes, conc, "INTERSECT CONFLICT", true);
+ d_im.sendInference(vec_nodes, conc, "INTERSECT CONFLICT", true);
addedLemma = true;
break;
}
- if (d_parent.inConflict())
+ if (d_im.hasConflict())
{
break;
}
}
// updates
- if (!d_parent.inConflict() && !spflag)
+ if (!d_im.hasConflict() && !spflag)
{
d_inter_cache[x] = r;
d_inter_index[x] = (int)n_pmem;
std::vector<Node> exp_n;
exp_n.push_back(assertion);
Node conc = Node::null();
- d_parent.sendInference(rnfexp, exp_n, conc, "REGEXP NF Conflict");
+ d_im.sendInference(rnfexp, exp_n, conc, "REGEXP NF Conflict");
addedLemma = true;
break;
}
exp_n.push_back(assertion);
Node conc = nvec.size() == 1 ? nvec[0] : nm->mkNode(AND, nvec);
conc = Rewriter::rewrite(conc);
- d_parent.sendInference(rnfexp, exp_n, conc, "REGEXP_Unfold");
+ d_im.sendInference(rnfexp, exp_n, conc, "REGEXP_Unfold");
addedLemma = true;
if (changed)
{
repUnfold.insert(x);
}
}
- if (d_parent.inConflict())
+ if (d_im.hasConflict())
{
break;
}
}
if (addedLemma)
{
- if (!d_parent.inConflict())
+ if (!d_im.hasConflict())
{
for (unsigned i = 0; i < processed.size(); i++)
{
std::vector<Node> exp_n;
exp_n.push_back(atom);
exp_n.push_back(x.eqNode(d_emptyString));
- d_parent.sendInference(nf_exp, exp_n, exp, "RegExp Delta");
+ d_im.sendInference(nf_exp, exp_n, exp, "RegExp Delta");
addedLemma = true;
d_regexp_ccached.insert(atom);
return false;
exp_n.push_back(atom);
exp_n.push_back(x.eqNode(d_emptyString));
Node conc;
- d_parent.sendInference(nf_exp, exp_n, conc, "RegExp Delta CONFLICT");
+ d_im.sendInference(nf_exp, exp_n, conc, "RegExp Delta CONFLICT");
addedLemma = true;
d_regexp_ccached.insert(atom);
return false;
}
std::vector<Node> exp_n;
exp_n.push_back(atom);
- d_parent.sendInference(ant, exp_n, conc, "RegExp-Derive");
+ d_im.sendInference(ant, exp_n, conc, "RegExp-Derive");
return true;
}
return false;
#include "context/cdlist.h"
#include "context/context.h"
#include "expr/node.h"
+#include "theory/strings/inference_manager.h"
#include "theory/strings/regexp_operation.h"
#include "util/regexp.h"
typedef context::CDHashSet<Node, NodeHashFunction> NodeSet;
public:
- RegExpSolver(TheoryStrings& p, context::Context* c, context::UserContext* u);
+ RegExpSolver(TheoryStrings& p,
+ InferenceManager& im,
+ context::Context* c,
+ context::UserContext* u);
~RegExpSolver() {}
/** add membership
Node d_false;
/** the parent of this object */
TheoryStrings& d_parent;
+ /** the output channel of the parent of this object */
+ InferenceManager& d_im;
// check membership constraints
Node mkAnd(Node c1, Node c2);
bool checkPDerivative(
#include "theory/ext_theory.h"
#include "theory/rewriter.h"
#include "theory/strings/theory_strings_rewriter.h"
+#include "theory/strings/theory_strings_utils.h"
#include "theory/strings/type_enumerator.h"
#include "theory/theory_model.h"
#include "theory/valuation.h"
: 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_conflict(c, false),
- d_infer(c),
- d_infer_exp(c),
d_nf_pairs(c),
d_pregistered_terms_cache(u),
d_registered_terms_cache(u),
d_functionsTerms(c),
d_has_extf(c, false),
d_has_str_code(false),
- d_regexp_solver(*this, c, u),
+ d_regexp_solver(*this, d_im, c, u),
d_input_vars(u),
d_input_var_lsum(u),
d_cardinality_lits(u),
lexp.push_back(lenx.eqNode(lens));
lexp.push_back(n.negate());
Node xneqs = x.eqNode(s).negate();
- sendInference(lexp, xneqs, "NEG-CTN-EQL", true);
+ d_im.sendInference(lexp, xneqs, "NEG-CTN-EQL", true);
}
// this depends on the current assertions, so we set that this
// inference is context-dependent.
Node eq = Rewriter::rewrite(x.eqNode(mkConcat(sk1, s, sk2)));
std::vector<Node> exp_vec;
exp_vec.push_back(n);
- sendInference(d_empty_vec, exp_vec, eq, "POS-CTN", true);
+ d_im.sendInference(d_empty_vec, exp_vec, eq, "POS-CTN", true);
Trace("strings-extf-debug")
<< " resolve extf : " << n << " based on positive contain reduction."
<< std::endl;
Trace("strings-red-lemma")
<< "Reduction_" << effort << " lemma : " << nnlem << std::endl;
Trace("strings-red-lemma") << "...from " << n << std::endl;
- sendInference(d_empty_vec, nnlem, "Reduction", true);
+ d_im.sendInference(d_empty_vec, nnlem, "Reduction", true);
Trace("strings-extf-debug")
<< " resolve extf : " << n << " based on reduction." << std::endl;
isCd = false;
//assert pending fact
assertPendingFact( atom, polarity, fact );
}
- doPendingFacts();
+ d_im.doPendingFacts();
Assert(d_strategy_init);
std::map<Effort, std::pair<unsigned, unsigned> >::iterator itsr =
do{
runStrategy(sbegin, send);
// flush the facts
- addedFact = !d_pending.empty();
- addedLemma = !d_lemma_cache.empty();
- doPendingFacts();
- doPendingLemmas();
+ addedFact = d_im.hasPendingFact();
+ addedLemma = d_im.hasPendingLemma();
+ d_im.doPendingFacts();
+ d_im.doPendingLemmas();
// repeat if we did not add a lemma or conflict
}while( !d_conflict && !addedLemma && addedFact );
Trace("strings-check") << "Theory of strings done full effort check " << addedLemma << " " << d_conflict << std::endl;
}
Trace("strings-check") << "Theory of strings, done check : " << e << std::endl;
- Assert( d_pending.empty() );
- Assert( d_lemma_cache.empty() );
+ Assert(!d_im.hasPendingFact());
+ Assert(!d_im.hasPendingLemma());
}
bool TheoryStrings::needsCheckLastEffort() {
if (ret)
{
getExtTheory()->markReduced(extf[i], isCd);
- if (hasProcessed())
+ if (d_im.hasProcessed())
{
return;
}
Trace("strings-pending-debug") << " Finished collect terms" << std::endl;
}
-void TheoryStrings::doPendingFacts() {
- size_t i=0;
- while( !d_conflict && i<d_pending.size() ) {
- Node fact = d_pending[i];
- Node exp = d_pending_exp[ fact ];
- if(fact.getKind() == kind::AND) {
- for(size_t j=0; j<fact.getNumChildren(); j++) {
- bool polarity = fact[j].getKind() != kind::NOT;
- TNode atom = polarity ? fact[j] : fact[j][0];
- assertPendingFact(atom, polarity, exp);
- }
- } else {
- bool polarity = fact.getKind() != kind::NOT;
- TNode atom = polarity ? fact : fact[0];
- assertPendingFact(atom, polarity, exp);
- }
- i++;
- }
- d_pending.clear();
- d_pending_exp.clear();
-}
-
-void TheoryStrings::doPendingLemmas() {
- if( !d_conflict && !d_lemma_cache.empty() ){
- for( unsigned i=0; i<d_lemma_cache.size(); i++ ){
- Trace("strings-pending") << "Process pending lemma : " << d_lemma_cache[i] << std::endl;
- d_out->lemma( d_lemma_cache[i] );
- }
- for( std::map< Node, bool >::iterator it = d_pending_req_phase.begin(); it != d_pending_req_phase.end(); ++it ){
- Trace("strings-pending") << "Require phase : " << it->first << ", polarity = " << it->second << std::endl;
- d_out->requirePhase( it->first, it->second );
- }
- }
- d_lemma_cache.clear();
- d_pending_req_phase.clear();
-}
-
-bool TheoryStrings::hasProcessed() {
- return d_conflict || !d_lemma_cache.empty() || !d_pending.empty();
-}
-
void TheoryStrings::addToExplanation( Node a, Node b, std::vector< Node >& exp ) {
if( a!=b ){
Debug("strings-explain") << "Add to explanation : " << a << " == " << b << std::endl;
}
}
//infer the equality
- sendInference( exp, n.eqNode( nc ), "I_Norm" );
+ d_im.sendInference(exp, n.eqNode(nc), "I_Norm");
}else if( getExtTheory()->hasFunctionKind( n.getKind() ) ){
//mark as congruent : only process if neither has been reduced
getExtTheory()->markCongruent( nc, n );
}
AlwaysAssert( foundNEmpty );
//infer the equality
- sendInference(exp, n.eqNode(ns), "I_Norm_S");
+ d_im.sendInference(exp, n.eqNode(ns), "I_Norm_S");
}
d_congruent.insert( n );
congruent[k]++;
<< std::endl;
prevSize = d_eqc_to_const.size();
checkConstantEquivalenceClasses(&d_term_index[kind::STRING_CONCAT], vecc);
- } while (!hasProcessed() && d_eqc_to_const.size() > prevSize);
+ } while (!d_im.hasProcessed() && d_eqc_to_const.size() > prevSize);
}
void TheoryStrings::checkConstantEquivalenceClasses( TermIndex* ti, std::vector< Node >& vecc ) {
//exp contains an explanation of n==c
Assert( countc==vecc.size() );
if( hasTerm( c ) ){
- sendInference( exp, n.eqNode( c ), "I_CONST_MERGE" );
+ d_im.sendInference(exp, n.eqNode(c), "I_CONST_MERGE");
return;
- }else if( !hasProcessed() ){
+ }
+ else if (!d_im.hasProcessed())
+ {
Node nr = 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;
d_eqc_to_const[nr] = c;
d_eqc_to_const_base[nr] = n;
- d_eqc_to_const_exp[nr] = mkAnd( exp );
+ d_eqc_to_const_exp[nr] = utils::mkAnd(exp);
}else if( c!=it->second ){
//conflict
Trace("strings-debug") << "Conflict, other constant was " << it->second << ", this constant was " << c << std::endl;
exp.push_back( d_eqc_to_const_exp[nr] );
addToExplanation( n, d_eqc_to_const_base[nr], exp );
}
- sendInference( exp, d_false, "I_CONST_CONFLICT" );
+ d_im.sendInference(exp, d_false, "I_CONST_CONFLICT");
return;
}else{
Trace("strings-debug") << "Duplicate constant." << std::endl;
vecc.push_back( itc->second );
checkConstantEquivalenceClasses( &it->second, vecc );
vecc.pop_back();
- if( hasProcessed() ){
+ if (d_im.hasProcessed())
+ {
break;
}
}
}
if( !conc.isNull() ){
Trace("strings-extf") << " resolve extf : " << sn << " -> " << nrc << std::endl;
- sendInference(
+ d_im.sendInference(
einfo.d_exp, conc, effort == 0 ? "EXTF" : "EXTF-N", true);
if( d_conflict ){
Trace("strings-extf-debug") << " conflict, return." << std::endl;
// reduced since this argument may be circular: we may infer than n
// can be reduced to something else, but that thing may argue that it
// can be reduced to n, in theory.
- sendInternalInference(
+ d_im.sendInternalInference(
einfo.d_exp, nrcAssert, effort == 0 ? "EXTF_d" : "EXTF_d-N");
}
to_reduce = nrc;
if (areEqual(conc, d_false))
{
// we are in conflict
- sendInference(in.d_exp, conc, "CTN_Decompose");
+ d_im.sendInference(in.d_exp, conc, "CTN_Decompose");
}
else if (getExtTheory()->hasFunctionKind(conc.getKind()))
{
exp_c.insert(exp_c.end(),
d_extf_info_tmp[ofrom].d_exp.begin(),
d_extf_info_tmp[ofrom].d_exp.end());
- sendInference(exp_c, conc, "CTN_Trans");
+ d_im.sendInference(exp_c, conc, "CTN_Trans");
}
}
}
inferEqrr = Rewriter::rewrite(inferEqrr);
Trace("strings-extf-infer") << "checkExtfInference: " << inferEq
<< " ...reduces to " << inferEqrr << std::endl;
- sendInternalInference(in.d_exp, inferEqrr, "EXTF_equality_rew");
+ d_im.sendInternalInference(in.d_exp, inferEqrr, "EXTF_equality_rew");
}
}
-Node TheoryStrings::getSymbolicDefinition( Node n, std::vector< Node >& exp ) {
+Node TheoryStrings::getProxyVariableFor(Node n) const
+{
+ NodeNodeMap::const_iterator it = d_proxy_var.find(n);
+ if (it != d_proxy_var.end())
+ {
+ return (*it).second;
+ }
+ return Node::null();
+}
+Node TheoryStrings::getSymbolicDefinition(Node n, std::vector<Node>& exp) const
+{
if( n.getNumChildren()==0 ){
- NodeNodeMap::const_iterator it = d_proxy_var.find( n );
- if( it==d_proxy_var.end() ){
+ Node pn = getProxyVariableFor(n);
+ if (pn.isNull())
+ {
return Node::null();
- }else{
- Node eq = n.eqNode( (*it).second );
- eq = Rewriter::rewrite( eq );
- if( std::find( exp.begin(), exp.end(), eq )==exp.end() ){
- exp.push_back( eq );
- }
- return (*it).second;
}
+ Node eq = n.eqNode(pn);
+ eq = Rewriter::rewrite(eq);
+ if (std::find(exp.begin(), exp.end(), eq) == exp.end())
+ {
+ exp.push_back(eq);
+ }
+ return pn;
}else{
std::vector< Node > children;
if (n.getMetaKind() == kind::metakind::PARAMETERIZED) {
std::vector< Node > curr;
std::vector< Node > exp;
checkCycles( eqc[i], curr, exp );
- if( hasProcessed() ){
+ if (d_im.hasProcessed())
+ {
return;
}
}
}
}
Node conc = d_false;
- sendInference(exp, conc, "F_NCTN");
+ d_im.sendInference(exp, conc, "F_NCTN");
return;
}
}
b[d_flat_form_index[b][j]].eqNode(d_emptyString));
}
Assert(!conc_c.empty());
- conc = mkAnd(conc_c);
+ conc = utils::mkAnd(conc_c);
inf_type = 2;
Assert(count > 0);
// swap, will enforce is empty past current
a[d_flat_form_index[a][j]].eqNode(d_emptyString));
}
Assert(!conc_c.empty());
- conc = mkAnd(conc_c);
+ conc = utils::mkAnd(conc_c);
inf_type = 2;
Assert(count > 0);
count--;
// strict prefix equality ( a.b = a ) where a,b non-empty
// is conflicting by arithmetic len(a.b)=len(a)+len(b)!=len(a)
// when len(b)!=0.
- sendInference(
+ d_im.sendInference(
exp,
conc,
- inf_type == 0
- ? "F_Const"
- : (inf_type == 1 ? "F_Unify" : (inf_type == 2 ? "F_EndpointEmp"
- : "F_EndpointEq")));
+ inf_type == 0 ? "F_Const"
+ : (inf_type == 1 ? "F_Unify"
+ : (inf_type == 2 ? "F_EndpointEmp"
+ : "F_EndpointEq")));
if (d_conflict)
{
return;
if( nr!=d_emptyString_r ){
std::vector< Node > exp;
exp.push_back( n.eqNode( d_emptyString ) );
- sendInference( exp, n[i].eqNode( d_emptyString ), "I_CYCLE_E" );
+ d_im.sendInference(
+ exp, n[i].eqNode(d_emptyString), "I_CYCLE_E");
return Node::null();
}
}else{
for( unsigned j=0; j<n.getNumChildren(); j++ ){
//take first non-empty
if( j!=i && !areEqual( n[j], d_emptyString ) ){
- sendInference( exp, n[j].eqNode( d_emptyString ), "I_CYCLE" );
+ d_im.sendInference(
+ exp, n[j].eqNode(d_emptyString), "I_CYCLE");
return Node::null();
}
}
return ncy;
}
}else{
- if( hasProcessed() ){
+ if (d_im.hasProcessed())
+ {
return Node::null();
}
}
}
}
- if (hasProcessed())
+ if (d_im.hasProcessed())
{
return;
}
<< eqc << std::endl;
normalizeEquivalenceClass(eqc);
Trace("strings-debug") << "Finished normalizing eqc..." << std::endl;
- if (hasProcessed())
+ if (d_im.hasProcessed())
{
return;
}
NormalForm& nfe_eq = getNormalForm(itn->second);
// two equivalence classes have same normal form, merge
std::vector<Node> nf_exp;
- nf_exp.push_back(mkAnd(nfe.d_exp));
+ nf_exp.push_back(utils::mkAnd(nfe.d_exp));
nf_exp.push_back(eqc_to_exp[itn->second]);
Node eq = nfe.d_base.eqNode(nfe_eq.d_base);
- sendInference(nf_exp, eq, "Normal_Form");
- if( hasProcessed() ){
+ d_im.sendInference(nf_exp, eq, "Normal_Form");
+ if (d_im.hasProcessed())
+ {
return;
}
}
{
nf_to_eqc[nf_term] = eqc;
eqc_to_nf[eqc] = nf_term;
- eqc_to_exp[eqc] = mkAnd(nfe.d_exp);
+ eqc_to_exp[eqc] = utils::mkAnd(nfe.d_exp);
}
Trace("strings-process-debug")
<< "Done verifying normal forms are the same for " << eqc << std::endl;
Node cc = nm->mkNode(kind::STRING_CODE, c);
cc = Rewriter::rewrite(cc);
Assert(cc.isConst());
- NodeNodeMap::const_iterator it = d_proxy_var.find(c);
- AlwaysAssert(it != d_proxy_var.end());
- Node vc = nm->mkNode(kind::STRING_CODE, (*it).second);
+ Node cp = getProxyVariableFor(c);
+ AlwaysAssert(!cp.isNull());
+ Node vc = nm->mkNode(STRING_CODE, cp);
if (!areEqual(cc, vc))
{
- sendInference(d_empty_vec, cc.eqNode(vc), "Code_Proxy");
+ d_im.sendInference(d_empty_vec, cc.eqNode(vc), "Code_Proxy");
}
const_codes.push_back(vc);
}
}
}
}
- if (hasProcessed())
+ if (d_im.hasProcessed())
{
return;
}
Node eqn = c1[0].eqNode(c2[0]);
// str.code(x)==-1 V str.code(x)!=str.code(y) V x==y
Node inj_lem = nm->mkNode(kind::OR, eq_no, deq, eqn);
- sendInference(d_empty_vec, inj_lem, "Code_Inj");
+ d_im.sendInference(d_empty_vec, inj_lem, "Code_Inj");
}
}
}
std::map<Node, unsigned> term_to_nf_index;
// get the normal forms
getNormalForms(eqc, normal_forms, term_to_nf_index);
- if( hasProcessed() ){
+ if (d_im.hasProcessed())
+ {
return;
}
// process the normal forms
processNEqc(normal_forms);
- if( hasProcessed() ){
+ if (d_im.hasProcessed())
+ {
return;
}
// debugPrintNormalForms( "strings-solve", eqc, normal_forms );
//TODO: this can be minimized based on firstc/lastc, normal_forms_exp_depend
exp.insert(exp.end(), nf.d_exp.begin(), nf.d_exp.end());
Node conc = d_false;
- sendInference( exp, conc, "N_NCTN" );
+ d_im.sendInference(exp, conc, "N_NCTN");
}
}
}
processSimpleNEq(nfi, nfj, rindex, true, 0, pinfer);
nfi.reverse();
nfj.reverse();
- if( hasProcessed() ){
+ if (d_im.hasProcessed())
+ {
return;
- }else if( !pinfer.empty() && pinfer.back().d_id==1 ){
+ }
+ else if (!pinfer.empty() && pinfer.back().d_id == 1)
+ {
break;
}
//AJR: for less aggressive endpoint inference
unsigned index = 0;
processSimpleNEq(nfi, nfj, index, false, rindex, pinfer);
- if( hasProcessed() ){
+ if (d_im.hasProcessed())
+ {
return;
- }else if( !pinfer.empty() && pinfer.back().d_id==1 ){
+ }
+ else if (!pinfer.empty() && pinfer.back().d_id == 1)
+ {
break;
}
}
}
std::stringstream ssi;
ssi << pinfer[use_index].d_id;
- sendInference(pinfer[use_index].d_ant,
- pinfer[use_index].d_antn,
- pinfer[use_index].d_conc,
- ssi.str().c_str(),
- pinfer[use_index].sendAsLemma());
+ 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());
// 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.
NormalForm& nfk = index == (nfiv.size() - rproc) ? nfj : nfi;
std::vector<Node>& nfkv = nfk.d_nf;
unsigned index_k = index;
- //Node eq_exp = mkAnd( curr_exp );
std::vector< Node > curr_exp;
NormalForm::getExplanationForPrefixEq(nfi, nfj, -1, -1, curr_exp);
while (!d_conflict && index_k < (nfkv.size() - rproc))
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]));
- sendInference( curr_exp, eq, "N_EndpointEmp" );
+ d_im.sendInference(curr_exp, eq, "N_EndpointEmp");
index_k++;
}
}
NormalForm::getExplanationForPrefixEq(
nfi, nfj, index, index, temp_exp);
temp_exp.push_back(length_eq);
- sendInference( temp_exp, eq, "N_Unify" );
+ d_im.sendInference(temp_exp, eq, "N_Unify");
return;
}
else if ((nfiv[index].getKind() != CONST_STRING
eqn.push_back( mkConcat( eqnc ) );
}
if( !areEqual( eqn[0], eqn[1] ) ){
- sendInference( antec, eqn[0].eqNode( eqn[1] ), "N_EndpointEq", true );
+ d_im.sendInference(
+ antec, eqn[0].eqNode(eqn[1]), "N_EndpointEq", true);
return;
}else{
Assert(nfiv.size() == nfjv.size());
std::vector< Node > antec;
NormalForm::getExplanationForPrefixEq(
nfi, nfj, index, index, antec);
- sendInference( antec, d_false, "N_Const", true );
+ d_im.sendInference(antec, d_false, "N_Const", true);
return;
}
}else{
{
Trace("strings-loop") << "Strings::Loop: tails are different."
<< std::endl;
- sendInference(info.d_ant, conc, "Loop Conflict", true);
+ d_im.sendInference(info.d_ant, conc, "Loop Conflict", true);
return ProcessLoopResult::CONFLICT;
}
}
//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( !d_equalityEngine.areDisequal( nconst_k, d_emptyString, true ) ){
Node eq = nconst_k.eqNode( d_emptyString );
Node conc = NodeManager::currentNM()->mkNode( kind::OR, eq, eq.negate() );
- sendInference( d_empty_vec, conc, "D-DISL-Emp-Split" );
+ d_im.sendInference(d_empty_vec, conc, "D-DISL-Emp-Split");
return;
}else{
//split on first character
return;
}else if( !areEqual( firstChar, nconst_k ) ){
//splitting on demand : try to make them disequal
- if (sendSplit(
+ if (d_im.sendSplit(
firstChar, nconst_k, "S-Split(DEQL-Const)", false))
{
return;
antec.insert(
antec.end(), nfnj.d_exp.begin(), nfnj.d_exp.end());
antec.push_back( nconst_k.eqNode( d_emptyString ).negate() );
- sendInference( antec, NodeManager::currentNM()->mkNode( kind::OR,
- NodeManager::currentNM()->mkNode( kind::AND, eq1, sk.eqNode( firstChar ).negate() ), eq2 ), "D-DISL-CSplit" );
- d_pending_req_phase[ eq1 ] = true;
+ d_im.sendInference(
+ antec,
+ nm->mkNode(
+ OR,
+ nm->mkNode(AND, eq1, sk.eqNode(firstChar).negate()),
+ eq2),
+ "D-DISL-CSplit");
+ d_im.sendPhaseRequirement(eq1, true);
return;
}
}
Node lsk2 = mkLength( 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 ) ) ) );
- sendInference( antec, antec_new_lits, NodeManager::currentNM()->mkNode( kind::AND, conc ), "D-DISL-Split" );
+ 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 ) );
//splitting on demand : try to make them disequal
- if (sendSplit(i, j, "S-Split(DEQL)", false))
+ if (d_im.sendSplit(i, j, "S-Split(DEQL)", false))
{
return;
}
}else{
//splitting on demand : try to make lengths equal
- if (sendSplit(li, lj, "D-Split"))
+ if (d_im.sendSplit(li, lj, "D-Split"))
{
return;
}
}
Node conc = cc.size()==1 ? cc[0] : NodeManager::currentNM()->mkNode( kind::AND, cc );
conc = Rewriter::rewrite( conc );
- sendInference( ant, conc, "Disequality Normalize Empty", true);
+ d_im.sendInference(ant, conc, "Disequality Normalize Empty", true);
return -1;
}else{
Node i = nfi[index];
}
}
-bool TheoryStrings::sendInternalInference(std::vector<Node>& exp,
- Node conc,
- const char* c)
-{
- if (conc.getKind() == AND
- || (conc.getKind() == NOT && conc[0].getKind() == OR))
- {
- Node conj = conc.getKind() == AND ? conc : conc[0];
- bool pol = conc.getKind() == AND;
- bool ret = true;
- for (const Node& cc : conj)
- {
- bool retc = sendInternalInference(exp, pol ? cc : cc.negate(), c);
- ret = ret && retc;
- }
- return ret;
- }
- bool pol = conc.getKind() != NOT;
- Node lit = pol ? conc : conc[0];
- if (lit.getKind() == EQUAL)
- {
- for (unsigned i = 0; i < 2; i++)
- {
- if (!lit[i].isConst() && !hasTerm(lit[i]))
- {
- // introduces a new non-constant term, do not infer
- return false;
- }
- }
- // does it already hold?
- if (pol ? areEqual(lit[0], lit[1]) : areDisequal(lit[0], lit[1]))
- {
- return true;
- }
- }
- else if (lit.isConst())
- {
- if (lit.getConst<bool>())
- {
- Assert(pol);
- // trivially holds
- return true;
- }
- }
- else if (!hasTerm(lit))
- {
- // introduces a new non-constant term, do not infer
- return false;
- }
- else if (areEqual(lit, pol ? d_true : d_false))
- {
- // already holds
- return true;
- }
- sendInference(exp, conc, c);
- return true;
-}
-
-void TheoryStrings::sendInference( std::vector< Node >& exp, std::vector< Node >& exp_n, Node eq, const char * c, bool asLemma ) {
- eq = eq.isNull() ? d_false : Rewriter::rewrite( eq );
- if( eq!=d_true ){
- if( Trace.isOn("strings-infer-debug") ){
- Trace("strings-infer-debug") << "By " << c << ", infer : " << eq << " from: " << std::endl;
- for( unsigned i=0; i<exp.size(); i++ ){
- Trace("strings-infer-debug") << " " << exp[i] << std::endl;
- }
- for( unsigned i=0; i<exp_n.size(); i++ ){
- Trace("strings-infer-debug") << " N:" << exp_n[i] << std::endl;
- }
- //Trace("strings-infer-debug") << "as lemma : " << asLemma << std::endl;
- }
- //check if we should send a lemma or an inference
- if( asLemma || eq==d_false || eq.getKind()==kind::OR || !exp_n.empty() || options::stringInferAsLemmas() ){
- Node eq_exp;
- if( options::stringRExplainLemmas() ){
- eq_exp = mkExplain( exp, exp_n );
- }else{
- if( exp.empty() ){
- eq_exp = mkAnd( exp_n );
- }else if( exp_n.empty() ){
- eq_exp = mkAnd( exp );
- }else{
- std::vector< Node > ev;
- ev.insert( ev.end(), exp.begin(), exp.end() );
- ev.insert( ev.end(), exp_n.begin(), exp_n.end() );
- eq_exp = NodeManager::currentNM()->mkNode( kind::AND, ev );
- }
- }
- // if we have unexplained literals, this lemma is not a conflict
- if (eq == d_false && !exp_n.empty())
- {
- eq = eq_exp.negate();
- eq_exp = d_true;
- }
- sendLemma( eq_exp, eq, c );
- }else{
- sendInfer( mkAnd( exp ), eq, c );
- }
- }
-}
-
-void TheoryStrings::sendInference( std::vector< Node >& exp, Node eq, const char * c, bool asLemma ) {
- std::vector< Node > exp_n;
- sendInference( exp, exp_n, eq, c, asLemma );
-}
-
-void TheoryStrings::sendLemma( Node ant, Node conc, const char * c ) {
- if( conc.isNull() || conc == d_false ) {
- Trace("strings-conflict") << "Strings::Conflict : " << c << " : " << ant << std::endl;
- Trace("strings-lemma") << "Strings::Conflict : " << c << " : " << ant << std::endl;
- Trace("strings-assert") << "(assert (not " << ant << ")) ; conflict " << c << std::endl;
- d_out->conflict(ant);
- d_conflict = true;
- } else {
- Node lem;
- if( ant == d_true ) {
- lem = conc;
- }else{
- lem = NodeManager::currentNM()->mkNode( kind::IMPLIES, ant, conc );
- }
- Trace("strings-lemma") << "Strings::Lemma " << c << " : " << lem << std::endl;
- Trace("strings-assert") << "(assert " << lem << ") ; lemma " << c << std::endl;
- d_lemma_cache.push_back( lem );
- }
-}
-
-void TheoryStrings::sendInfer( Node eq_exp, Node eq, const char * c ) {
- if( options::stringInferSym() ){
- std::vector< Node > vars;
- std::vector< Node > subs;
- std::vector< Node > unproc;
- inferSubstitutionProxyVars( eq_exp, vars, subs, unproc );
- if( unproc.empty() ){
- Trace("strings-lemma-debug") << "Strings::Infer " << eq << " from " << eq_exp << " by " << c << std::endl;
- Node eqs = eq.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() );
- Trace("strings-lemma-debug") << "Strings::Infer Alternate : " << eqs << std::endl;
- for( unsigned i=0; i<vars.size(); i++ ){
- Trace("strings-lemma-debug") << " " << vars[i] << " -> " << subs[i] << std::endl;
- }
- sendLemma( d_true, eqs, c );
- return;
- }else{
- for( unsigned i=0; i<unproc.size(); i++ ){
- Trace("strings-lemma-debug") << " non-trivial exp : " << unproc[i] << std::endl;
- }
- }
- }
- Trace("strings-lemma") << "Strings::Infer " << eq << " from " << eq_exp << " by " << c << std::endl;
- Trace("strings-assert") << "(assert (=> " << eq_exp << " " << eq << ")) ; infer " << c << std::endl;
- d_pending.push_back( eq );
- d_pending_exp[eq] = eq_exp;
- d_infer.push_back( eq );
- d_infer_exp.push_back( eq_exp );
-}
-
-bool TheoryStrings::sendSplit(Node a, Node b, const char* c, bool preq)
-{
- Node eq = a.eqNode( b );
- eq = Rewriter::rewrite( eq );
- if (!eq.isConst())
- {
- Node neq = NodeManager::currentNM()->mkNode(kind::NOT, eq);
- Node lemma_or = NodeManager::currentNM()->mkNode(kind::OR, eq, neq);
- Trace("strings-lemma") << "Strings::Lemma " << c << " SPLIT : " << lemma_or
- << std::endl;
- d_lemma_cache.push_back(lemma_or);
- d_pending_req_phase[eq] = preq;
- ++(d_statistics.d_splits);
- return true;
- }
- return false;
-}
-
void TheoryStrings::registerLength(Node n, LengthStatus s)
{
if (d_length_lemma_terms_cache.find(n) != d_length_lemma_terms_cache.end())
}
}
-void TheoryStrings::inferSubstitutionProxyVars( Node n, std::vector< Node >& vars, std::vector< Node >& subs, std::vector< Node >& unproc ) {
- if( n.getKind()==kind::AND ){
- for( unsigned i=0; i<n.getNumChildren(); i++ ){
- inferSubstitutionProxyVars( n[i], vars, subs, unproc );
- }
- return;
- }else if( n.getKind()==kind::EQUAL ){
- Node ns = n.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() );
- ns = Rewriter::rewrite( ns );
- if( ns.getKind()==kind::EQUAL ){
- Node s;
- Node v;
- for( unsigned i=0; i<2; i++ ){
- Node ss;
- if( ns[i].getAttribute(StringsProxyVarAttribute()) ){
- ss = ns[i];
- }else if( ns[i].isConst() ){
- NodeNodeMap::const_iterator it = d_proxy_var.find( ns[i] );
- if( it!=d_proxy_var.end() ){
- ss = (*it).second;
- }
- }
- if( !ss.isNull() ){
- v = ns[1-i];
- if( v.getNumChildren()==0 ){
- if( s.isNull() ){
- s = ss;
- }else{
- //both sides involved in proxy var
- if( ss==s ){
- return;
- }else{
- s = Node::null();
- }
- }
- }
- }
- }
- if( !s.isNull() ){
- subs.push_back( s );
- vars.push_back( v );
- return;
- }
- }else{
- n = ns;
- }
- }
- if( n!=d_true ){
- unproc.push_back( n );
- }
-}
-
-
Node TheoryStrings::mkConcat( Node n1, Node n2 ) {
return Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, n1, n2 ) );
}
return ant;
}
-Node TheoryStrings::mkAnd( std::vector< Node >& a ) {
- std::vector< Node > au;
- for( unsigned i=0; i<a.size(); i++ ){
- if( std::find( au.begin(), au.end(), a[i] )==au.end() ){
- au.push_back( a[i] );
- }
- }
- if( au.empty() ) {
- return d_true;
- } else if( au.size() == 1 ) {
- return au[0];
- } else {
- return NodeManager::currentNM()->mkNode( kind::AND, au );
- }
-}
-
void TheoryStrings::checkNormalFormsDeq()
{
std::vector< std::vector< Node > > cols;
lt[i] = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, lt[i] );
}
if( !areEqual( lt[0], lt[1] ) && !areDisequal( lt[0], lt[1] ) ){
- sendSplit( lt[0], lt[1], "DEQ-LENGTH-SP" );
+ d_im.sendSplit(lt[0], lt[1], "DEQ-LENGTH-SP");
}
}
}
-
- if( !hasProcessed() ){
+
+ if (!d_im.hasProcessed())
+ {
separateByLength( d_strings_eqc, cols, lts );
for( unsigned i=0; i<cols.size(); i++ ){
- if( cols[i].size()>1 && d_lemma_cache.empty() ){
+ if (cols[i].size() > 1 && !d_im.hasPendingLemma())
+ {
if (Trace.isOn("strings-solve"))
{
Trace("strings-solve") << "- Verify disequalities are processed for "
Trace("strings-solve") << "..." << std::endl;
}
processDeq(cols[i][j], cols[i][k]);
- if (hasProcessed())
+ if (d_im.hasProcessed())
{
return;
}
{
Node eq = llt.eqNode(lcr);
ei->d_normalized_length.set( eq );
- sendInference( ant, eq, "LEN-NORM", true );
+ d_im.sendInference(ant, eq, "LEN-NORM", true);
}
}
}else{
if( !options::stringEagerLen() ){
Node c = mkConcat(nfi.d_nf);
registerTerm( c, 3 );
- /*
- if( !c.isConst() ){
- NodeNodeMap::const_iterator it = d_proxy_var.find( c );
- if( it!=d_proxy_var.end() ){
- Node pv = (*it).second;
- Assert( d_proxy_var_to_length.find( pv )!=d_proxy_var_to_length.end() );
- Node pvl = d_proxy_var_to_length[pv];
- Node ceq = Rewriter::rewrite( mkLength( pv ).eqNode( pvl ) );
- sendInference( d_empty_vec, ceq, "LEN-NORM-I", true );
- }
- }
- */
}
}
//} else {
itr2 != cols[i].end(); ++itr2) {
if(!areDisequal( *itr1, *itr2 )) {
// add split lemma
- if (sendSplit(*itr1, *itr2, "CARD-SP"))
+ if (d_im.sendSplit(*itr1, *itr2, "CARD-SP"))
{
return;
}
cons = Rewriter::rewrite( cons );
ei->d_cardinality_lem_k.set( int_k+1 );
if( cons!=d_true ){
- sendInference( d_empty_vec, vec_node, cons, "CARDINALITY", true );
+ d_im.sendInference(
+ d_empty_vec, vec_node, cons, "CARDINALITY", true);
return;
}
}
default: Unreachable(); break;
}
Trace("strings-process") << "Done " << s
- << ", addedFact = " << !d_pending.empty() << " "
- << !d_lemma_cache.empty()
+ << ", addedFact = " << d_im.hasPendingFact()
+ << ", addedLemma = " << d_im.hasPendingLemma()
<< ", d_conflict = " << d_conflict << std::endl;
}
InferStep curr = d_infer_steps[i];
if (curr == BREAK)
{
- if (hasProcessed())
+ if (d_im.hasProcessed())
{
break;
}
#include "expr/attribute.h"
#include "expr/node_trie.h"
#include "theory/decision_manager.h"
+#include "theory/strings/inference_manager.h"
#include "theory/strings/normal_form.h"
#include "theory/strings/regexp_elim.h"
#include "theory/strings/regexp_operation.h"
typedef expr::Attribute< StringsProxyVarAttributeId, bool > StringsProxyVarAttribute;
class TheoryStrings : public Theory {
+ friend class InferenceManager;
typedef context::CDList<Node> NodeList;
typedef context::CDHashMap<Node, bool, NodeHashFunction> NodeBoolMap;
typedef context::CDHashMap<Node, int, NodeHashFunction> NodeIntMap;
NotifyClass d_notify;
/** Equaltity engine */
eq::EqualityEngine d_equalityEngine;
+ /** The (custom) output channel of the theory of strings */
+ InferenceManager d_im;
/** Are we in conflict */
context::CDO<bool> d_conflict;
- //list of pairs of nodes to merge
- std::map< Node, Node > d_pending_exp;
- std::vector< Node > d_pending;
- std::vector< Node > d_lemma_cache;
- std::map< Node, bool > d_pending_req_phase;
- /** inferences: maintained to ensure ref count for internally introduced nodes */
- NodeList d_infer;
- NodeList d_infer_exp;
/** map from terms to their normal forms */
std::map<Node, NormalForm> d_normal_form;
/** get normal form */
* should currently be a representative of the equality engine of this class.
*/
EqcInfo * getOrMakeEqcInfo( Node eqc, bool doMake = true );
- //maintain which concat terms have the length lemma instantiated
+ /**
+ * Map string terms to their "proxy variables". Proxy variables are used are
+ * intermediate variables so that length information can be communicated for
+ * constants. For example, to communicate that "ABC" has length 3, we
+ * introduce a proxy variable v_{"ABC"} for "ABC", and assert:
+ * v_{"ABC"} = "ABC" ^ len( v_{"ABC"} ) = 3
+ * Notice this is required since we cannot directly write len( "ABC" ) = 3,
+ * which rewrites to 3 = 3.
+ * In the above example, we store "ABC" -> v_{"ABC"} in this map.
+ */
NodeNodeMap d_proxy_var;
+ /**
+ * Map from proxy variables to their normalized length. In the above example,
+ * we store "ABC" -> 3.
+ */
NodeNodeMap d_proxy_var_to_length;
/** All the function terms that the theory has seen */
context::CDList<TNode> d_functionsTerms;
SkolemCache d_sk_cache;
void checkConstantEquivalenceClasses( TermIndex* ti, std::vector< Node >& vecc );
- Node getSymbolicDefinition( Node n, std::vector< Node >& exp );
+ /** Get proxy variable
+ *
+ * If this method returns the proxy variable for (string) term n if one
+ * exists, otherwise it returns null.
+ */
+ Node getProxyVariableFor(Node n) const;
+ /** Get symbolic definition
+ *
+ * This method returns the "symbolic definition" of n, call it n', and
+ * populates the vector exp with an explanation such that exp => n = n'.
+ *
+ * The symbolic definition of n is the term where (maximal) subterms of n
+ * are replaced by their proxy variables. For example, if we introduced
+ * proxy variable v for x ++ y, then given input x ++ y = w, this method
+ * returns v = w and adds v = x ++ y to exp.
+ */
+ Node getSymbolicDefinition(Node n, std::vector<Node>& exp) const;
//--------------------------for checkExtfEval
/**
*/
bool areCareDisequal(TNode x, TNode y);
- // do pending merges
+ /** assert pending fact
+ *
+ * This asserts atom with polarity to the equality engine of this class,
+ * where exp is the explanation of why (~) atom holds.
+ *
+ * This call may trigger further initialization steps involving the terms
+ * of atom, including calls to registerTerm.
+ */
void assertPendingFact(Node atom, bool polarity, Node exp);
- void doPendingFacts();
- void doPendingLemmas();
- bool hasProcessed();
/**
* 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.
* effort, the call to this method does nothing.
*/
void registerTerm(Node n, int effort);
- //-------------------------------------send inferences
- public:
- /** send internal inferences
- *
- * This is called when we have inferred exp => conc, where exp is a set
- * of equalities and disequalities that hold in the current equality engine.
- * This method adds equalities and disequalities ~( s = t ) via
- * sendInference such that both s and t are either constants or terms
- * that already occur in the equality engine, and ~( s = t ) is a consequence
- * of conc. This function can be seen as a "conservative" version of
- * sendInference below in that it does not introduce any new non-constant
- * terms to the state.
- *
- * The argument c is a string identifying the reason for the inference.
- * This string is used for debugging purposes.
- *
- * Return true if the inference is complete, in the sense that we infer
- * inferences that are equivalent to conc. This returns false e.g. if conc
- * (or one of its conjuncts if it is a conjunction) was not inferred due
- * to the criteria mentioned above.
- */
- bool sendInternalInference(std::vector<Node>& exp, Node conc, const char* c);
- /** send inference
- *
- * This function should be called when ( exp ^ exp_n ) => eq. The set exp
- * contains literals that are explainable by this class, i.e. those that
- * hold in the equality engine of this class. On the other hand, the set
- * exp_n ("explanations new") contain nodes that are not explainable by this
- * class. This method may call sendInfer or sendLemma. Overall, the result
- * of this method is one of the following:
- *
- * [1] (No-op) Do nothing if eq is true,
- *
- * [2] (Infer) Indicate that eq should be added to the equality engine of this
- * class with explanation EXPLAIN(exp), where EXPLAIN returns the
- * explanation of the node in exp in terms of the literals asserted to this
- * class,
- *
- * [3] (Lemma) Indicate that the lemma ( EXPLAIN(exp) ^ exp_n ) => eq should
- * be sent on the output channel of this class, or
- *
- * [4] (Conflict) Immediately report a conflict EXPLAIN(exp) on the output
- * channel of this class.
- *
- * Determining which case to apply depends on the form of eq and whether
- * exp_n is empty. In particular, lemmas must be used whenever exp_n is
- * non-empty, conflicts are used when exp_n is empty and eq is false.
- *
- * The argument c is a string identifying the reason for inference, used for
- * debugging.
- *
- * 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,
- Node eq,
- const char* c,
- bool asLemma = false);
- /** same as above, but where exp_n is empty */
- void sendInference(std::vector<Node>& exp,
- Node eq,
- const char* c,
- bool asLemma = false);
+
/**
* 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; }
- protected:
- /**
- * Indicates that ant => conc should be sent on the output channel of this
- * class. This will either trigger an immediate call to the conflict
- * method of the output channel of this class of conc is false, or adds the
- * above lemma to the lemma cache d_lemma_cache, which may be flushed
- * later within the current call to TheoryStrings::check.
- *
- * The argument c is a string identifying the reason for inference, used for
- * debugging.
- */
- void sendLemma(Node ant, Node conc, const char* c);
- /**
- * Indicates that conc should be added to the equality engine of this class
- * with explanation eq_exp. It must be the case that eq_exp is a (conjunction
- * of) literals that each are explainable, i.e. they already hold in the
- * equality engine of this class.
- */
- void sendInfer(Node eq_exp, Node eq, const char* c);
- bool sendSplit(Node a, Node b, const char* c, bool preq = true);
- //-------------------------------------end send inferences
-
/** mkConcat **/
inline Node mkConcat(Node n1, Node n2);
inline Node mkConcat(Node n1, Node n2, Node n3);
Node mkExplain(std::vector<Node>& a, std::vector<Node>& an);
protected:
- /** mkAnd **/
- Node mkAnd(std::vector<Node>& a);
/** get equivalence classes
*
std::vector<Node>& lts);
void printConcat(std::vector<Node>& n, const char* c);
- void inferSubstitutionProxyVars(Node n,
- std::vector<Node>& vars,
- std::vector<Node>& subs,
- std::vector<Node>& unproc);
-
// Symbolic Regular Expression
private:
/** regular expression solver module */
--- /dev/null
+/********************* */
+/*! \file theory_strings_utils.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 Util functions for theory strings.
+ **
+ ** Util functions for theory strings.
+ **/
+
+#include "theory/strings/theory_strings_utils.h"
+
+using namespace CVC4::kind;
+
+namespace CVC4 {
+namespace theory {
+namespace strings {
+namespace utils {
+
+Node mkAnd(std::vector<Node>& a)
+{
+ std::vector<Node> au;
+ for (const Node& ai : a)
+ {
+ if (std::find(au.begin(), au.end(), ai) == au.end())
+ {
+ au.push_back(ai);
+ }
+ }
+ if (au.empty())
+ {
+ return NodeManager::currentNM()->mkConst(true);
+ }
+ else if (au.size() == 1)
+ {
+ return au[0];
+ }
+ return NodeManager::currentNM()->mkNode(AND, au);
+}
+
+} // namespace utils
+} // namespace strings
+} // namespace theory
+} // namespace CVC4
--- /dev/null
+/********************* */
+/*! \file theory_strings_utils.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 Util functions for theory strings.
+ **
+ ** Util functions for theory strings.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__THEORY__STRINGS__THEORY_STRINGS_UTILS_H
+#define CVC4__THEORY__STRINGS__THEORY_STRINGS_UTILS_H
+
+#include <vector>
+
+#include "expr/node.h"
+
+namespace CVC4 {
+namespace theory {
+namespace strings {
+namespace utils {
+
+/**
+ * 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);
+
+} // namespace utils
+} // namespace strings
+} // namespace theory
+} // namespace CVC4
+
+#endif
projects / cvc5.git / commitdiff