From: Andrew Reynolds Date: Sat, 6 Jul 2019 01:40:49 +0000 (-0500) Subject: Refactor strings to use an inference manager object (#3076) X-Git-Tag: cvc5-1.0.0~4094 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=1e71ddfb9ac9e368c9f99d351ae7954fb502663e;p=cvc5.git Refactor strings to use an inference manager object (#3076) --- diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 885b26078..cc13dec6d 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -628,6 +628,8 @@ libcvc4_add_sources( 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 @@ -645,6 +647,8 @@ libcvc4_add_sources( 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 diff --git a/src/theory/strings/inference_manager.cpp b/src/theory/strings/inference_manager.cpp new file mode 100644 index 000000000..ec144aa6d --- /dev/null +++ b/src/theory/strings/inference_manager.cpp @@ -0,0 +1,407 @@ +/********************* */ +/*! \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& 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()) + { + 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& exp, + std::vector& 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 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& exp, + Node eq, + const char* c, + bool asLemma) +{ + std::vector 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 vars; + std::vector subs; + std::vector 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& 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& vars, + std::vector& subs, + std::vector& 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 diff --git a/src/theory/strings/inference_manager.h b/src/theory/strings/inference_manager.h new file mode 100644 index 000000000..71651f7df --- /dev/null +++ b/src/theory/strings/inference_manager.h @@ -0,0 +1,292 @@ +/********************* */ +/*! \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 +#include + +#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 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& 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& exp, + std::vector& exp_n, + Node eq, + const char* c, + bool asLemma = false); + /** same as above, but where exp_n is empty */ + void sendInference(std::vector& 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 d_pending; + /** A map from the literals in the above vector to their explanation */ + std::map d_pendingExp; + /** A map from literals to their pending phase requirement */ + std::map d_pendingReqPhase; + /** A list of pending lemmas to be sent on the output channel. */ + std::vector 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& vars, + std::vector& subs, + std::vector& unproc) const; +}; + +} // namespace strings +} // namespace theory +} // namespace CVC4 + +#endif diff --git a/src/theory/strings/regexp_solver.cpp b/src/theory/strings/regexp_solver.cpp index bf3a170df..5079806ac 100644 --- a/src/theory/strings/regexp_solver.cpp +++ b/src/theory/strings/regexp_solver.cpp @@ -32,9 +32,11 @@ namespace theory { 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), @@ -147,17 +149,17 @@ void RegExpSolver::check() 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; @@ -235,7 +237,7 @@ void RegExpSolver::check() std::vector 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; } @@ -280,7 +282,7 @@ void RegExpSolver::check() 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) { @@ -298,7 +300,7 @@ void RegExpSolver::check() repUnfold.insert(x); } } - if (d_parent.inConflict()) + if (d_im.hasConflict()) { break; } @@ -307,7 +309,7 @@ void RegExpSolver::check() } if (addedLemma) { - if (!d_parent.inConflict()) + if (!d_im.hasConflict()) { for (unsigned i = 0; i < processed.size(); i++) { @@ -338,7 +340,7 @@ bool RegExpSolver::checkPDerivative( std::vector 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; @@ -354,7 +356,7 @@ bool RegExpSolver::checkPDerivative( 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; @@ -444,7 +446,7 @@ bool RegExpSolver::deriveRegExp(Node x, } std::vector 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; diff --git a/src/theory/strings/regexp_solver.h b/src/theory/strings/regexp_solver.h index 13b66557a..ec74d98cd 100644 --- a/src/theory/strings/regexp_solver.h +++ b/src/theory/strings/regexp_solver.h @@ -23,6 +23,7 @@ #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" @@ -42,7 +43,10 @@ class RegExpSolver typedef context::CDHashSet 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 @@ -69,6 +73,8 @@ class RegExpSolver 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( diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 7b6bbdc99..ac6c0c102 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -26,6 +26,7 @@ #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" @@ -104,9 +105,8 @@ 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_conflict(c, false), - d_infer(c), - d_infer_exp(c), d_nf_pairs(c), d_pregistered_terms_cache(u), d_registered_terms_cache(u), @@ -121,7 +121,7 @@ TheoryStrings::TheoryStrings(context::Context* c, 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), @@ -468,7 +468,7 @@ bool TheoryStrings::doReduction(int effort, Node n, bool& isCd) 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. @@ -513,7 +513,7 @@ bool TheoryStrings::doReduction(int effort, Node n, bool& isCd) Node eq = Rewriter::rewrite(x.eqNode(mkConcat(sk1, s, sk2))); std::vector 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; @@ -538,7 +538,7 @@ bool TheoryStrings::doReduction(int effort, Node n, bool& isCd) 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; @@ -970,7 +970,7 @@ void TheoryStrings::check(Effort e) { //assert pending fact assertPendingFact( atom, polarity, fact ); } - doPendingFacts(); + d_im.doPendingFacts(); Assert(d_strategy_init); std::map >::iterator itsr = @@ -1016,18 +1016,18 @@ void TheoryStrings::check(Effort e) { 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() { @@ -1056,7 +1056,7 @@ void TheoryStrings::checkExtfReductions( int effort ) { if (ret) { getExtTheory()->markReduced(extf[i], isCd); - if (hasProcessed()) + if (d_im.hasProcessed()) { return; } @@ -1329,47 +1329,6 @@ void TheoryStrings::assertPendingFact(Node atom, bool polarity, Node exp) { Trace("strings-pending-debug") << " Finished collect terms" << std::endl; } -void TheoryStrings::doPendingFacts() { - size_t i=0; - while( !d_conflict && ilemma( 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; @@ -1451,7 +1410,7 @@ void TheoryStrings::checkInit() { } } //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 ); @@ -1481,7 +1440,7 @@ void TheoryStrings::checkInit() { } 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]++; @@ -1526,7 +1485,7 @@ void TheoryStrings::checkConstantEquivalenceClasses() << 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 ) { @@ -1566,16 +1525,18 @@ void TheoryStrings::checkConstantEquivalenceClasses( TermIndex* ti, std::vector< //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; @@ -1587,7 +1548,7 @@ void TheoryStrings::checkConstantEquivalenceClasses( TermIndex* ti, std::vector< 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; @@ -1601,7 +1562,8 @@ void TheoryStrings::checkConstantEquivalenceClasses( TermIndex* ti, std::vector< vecc.push_back( itc->second ); checkConstantEquivalenceClasses( &it->second, vecc ); vecc.pop_back(); - if( hasProcessed() ){ + if (d_im.hasProcessed()) + { break; } } @@ -1698,7 +1660,7 @@ void TheoryStrings::checkExtfEval( int effort ) { } 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; @@ -1731,7 +1693,7 @@ void TheoryStrings::checkExtfEval( int effort ) { // 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; @@ -1839,7 +1801,7 @@ void TheoryStrings::checkExtfInference( Node n, Node nr, ExtfInfoTmp& in, int ef 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())) { @@ -1912,7 +1874,7 @@ void TheoryStrings::checkExtfInference( Node n, Node nr, ExtfInfoTmp& in, int ef 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"); } } } @@ -1945,23 +1907,34 @@ void TheoryStrings::checkExtfInference( Node n, Node nr, ExtfInfoTmp& in, int ef 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& 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) { @@ -2082,7 +2055,8 @@ void TheoryStrings::checkCycles() std::vector< Node > curr; std::vector< Node > exp; checkCycles( eqc[i], curr, exp ); - if( hasProcessed() ){ + if (d_im.hasProcessed()) + { return; } } @@ -2143,7 +2117,7 @@ void TheoryStrings::checkFlatForms() } } Node conc = d_false; - sendInference(exp, conc, "F_NCTN"); + d_im.sendInference(exp, conc, "F_NCTN"); return; } } @@ -2212,7 +2186,7 @@ void TheoryStrings::checkFlatForm(std::vector& eqc, 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 @@ -2248,7 +2222,7 @@ void TheoryStrings::checkFlatForm(std::vector& eqc, 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--; @@ -2368,13 +2342,13 @@ void TheoryStrings::checkFlatForm(std::vector& eqc, // 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; @@ -2414,7 +2388,8 @@ Node TheoryStrings::checkCycles( Node eqc, std::vector< Node >& curr, std::vecto 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{ @@ -2433,7 +2408,8 @@ Node TheoryStrings::checkCycles( Node eqc, std::vector< Node >& curr, std::vecto for( unsigned j=0; j& curr, std::vecto return ncy; } }else{ - if( hasProcessed() ){ + if (d_im.hasProcessed()) + { return Node::null(); } } @@ -2479,7 +2456,7 @@ void TheoryStrings::checkNormalFormsEq() } } - if (hasProcessed()) + if (d_im.hasProcessed()) { return; } @@ -2495,7 +2472,7 @@ void TheoryStrings::checkNormalFormsEq() << eqc << std::endl; normalizeEquivalenceClass(eqc); Trace("strings-debug") << "Finished normalizing eqc..." << std::endl; - if (hasProcessed()) + if (d_im.hasProcessed()) { return; } @@ -2507,11 +2484,12 @@ void TheoryStrings::checkNormalFormsEq() NormalForm& nfe_eq = getNormalForm(itn->second); // two equivalence classes have same normal form, merge std::vector 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; } } @@ -2519,7 +2497,7 @@ void TheoryStrings::checkNormalFormsEq() { 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; @@ -2564,12 +2542,12 @@ void TheoryStrings::checkCodes() 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); } @@ -2583,7 +2561,7 @@ void TheoryStrings::checkCodes() } } } - if (hasProcessed()) + if (d_im.hasProcessed()) { return; } @@ -2606,7 +2584,7 @@ void TheoryStrings::checkCodes() 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"); } } } @@ -2637,12 +2615,14 @@ void TheoryStrings::normalizeEquivalenceClass( Node eqc ) { std::map 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 ); @@ -2897,7 +2877,7 @@ void TheoryStrings::getNormalForms(Node eqc, //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"); } } } @@ -2927,9 +2907,12 @@ void TheoryStrings::processNEqc(std::vector& normal_forms) 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 @@ -2937,9 +2920,12 @@ void TheoryStrings::processNEqc(std::vector& normal_forms) 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; } } @@ -2980,11 +2966,11 @@ void TheoryStrings::processNEqc(std::vector& normal_forms) } 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. @@ -3027,7 +3013,6 @@ void TheoryStrings::processSimpleNEq(NormalForm& nfi, NormalForm& nfk = index == (nfiv.size() - rproc) ? nfj : nfi; std::vector& 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)) @@ -3036,7 +3021,7 @@ void TheoryStrings::processSimpleNEq(NormalForm& nfi, 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++; } } @@ -3063,7 +3048,7 @@ void TheoryStrings::processSimpleNEq(NormalForm& nfi, 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 @@ -3093,7 +3078,8 @@ void TheoryStrings::processSimpleNEq(NormalForm& nfi, 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()); @@ -3136,7 +3122,7 @@ void TheoryStrings::processSimpleNEq(NormalForm& nfi, 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{ @@ -3477,7 +3463,7 @@ TheoryStrings::ProcessLoopResult TheoryStrings::processLoop(NormalForm& nfi, { 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; } } @@ -3623,6 +3609,7 @@ 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); @@ -3667,7 +3654,7 @@ void TheoryStrings::processDeq( Node ni, Node 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 @@ -3678,7 +3665,7 @@ void TheoryStrings::processDeq( Node ni, Node nj ) { 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; @@ -3701,9 +3688,14 @@ void TheoryStrings::processDeq( Node ni, Node nj ) { 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; } } @@ -3736,20 +3728,21 @@ void TheoryStrings::processDeq( Node ni, Node nj ) { 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; } @@ -3819,7 +3812,7 @@ int TheoryStrings::processSimpleDeq( std::vector< Node >& nfi, std::vector< Node } 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]; @@ -4030,179 +4023,6 @@ void TheoryStrings::registerTerm( Node n, int effort ) { } } -bool TheoryStrings::sendInternalInference(std::vector& 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()) - { - 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 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 " << subs[i] << std::endl; - } - sendLemma( d_true, eqs, c ); - return; - }else{ - for( unsigned i=0; i " << 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()) @@ -4284,59 +4104,6 @@ void TheoryStrings::registerLength(Node n, LengthStatus s) } } -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; imkNode( kind::STRING_CONCAT, n1, n2 ) ); } @@ -4411,22 +4178,6 @@ Node TheoryStrings::mkExplain( std::vector< Node >& a, std::vector< Node >& an ) return ant; } -Node TheoryStrings::mkAnd( std::vector< Node >& a ) { - std::vector< Node > au; - for( unsigned i=0; imkNode( kind::AND, au ); - } -} - void TheoryStrings::checkNormalFormsDeq() { std::vector< std::vector< Node > > cols; @@ -4452,15 +4203,17 @@ void TheoryStrings::checkNormalFormsDeq() 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; i1 && 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 " @@ -4492,7 +4245,7 @@ void TheoryStrings::checkNormalFormsDeq() Trace("strings-solve") << "..." << std::endl; } processDeq(cols[i][j], cols[i][k]); - if (hasProcessed()) + if (d_im.hasProcessed()) { return; } @@ -4540,7 +4293,7 @@ void TheoryStrings::checkLengthsEqc() { { 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{ @@ -4548,18 +4301,6 @@ void TheoryStrings::checkLengthsEqc() { 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 { @@ -4626,7 +4367,7 @@ void TheoryStrings::checkCardinality() { 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; } @@ -4654,7 +4395,8 @@ void TheoryStrings::checkCardinality() { 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; } } @@ -4841,8 +4583,8 @@ void TheoryStrings::runInferStep(InferStep s, int effort) 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; } @@ -4944,7 +4686,7 @@ void TheoryStrings::runStrategy(unsigned sbegin, unsigned send) InferStep curr = d_infer_steps[i]; if (curr == BREAK) { - if (hasProcessed()) + if (d_im.hasProcessed()) { break; } diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h index 8371a27ea..a83a6ad12 100644 --- a/src/theory/strings/theory_strings.h +++ b/src/theory/strings/theory_strings.h @@ -24,6 +24,7 @@ #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" @@ -135,6 +136,7 @@ struct StringsProxyVarAttributeId {}; typedef expr::Attribute< StringsProxyVarAttributeId, bool > StringsProxyVarAttribute; class TheoryStrings : public Theory { + friend class InferenceManager; typedef context::CDList NodeList; typedef context::CDHashMap NodeBoolMap; typedef context::CDHashMap NodeIntMap; @@ -298,16 +300,10 @@ class TheoryStrings : public Theory { 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 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 d_normal_form; /** get normal form */ @@ -421,8 +417,21 @@ private: * 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 d_functionsTerms; @@ -492,7 +501,23 @@ private: 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& exp) const; //--------------------------for checkExtfEval /** @@ -704,11 +729,15 @@ private: */ 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. @@ -736,98 +765,13 @@ private: * 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& 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& exp, - std::vector& exp_n, - Node eq, - const char* c, - bool asLemma = false); - /** same as above, but where exp_n is empty */ - void sendInference(std::vector& 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); @@ -839,8 +783,6 @@ private: Node mkExplain(std::vector& a, std::vector& an); protected: - /** mkAnd **/ - Node mkAnd(std::vector& a); /** get equivalence classes * @@ -861,11 +803,6 @@ private: std::vector& lts); void printConcat(std::vector& n, const char* c); - void inferSubstitutionProxyVars(Node n, - std::vector& vars, - std::vector& subs, - std::vector& unproc); - // Symbolic Regular Expression private: /** regular expression solver module */ diff --git a/src/theory/strings/theory_strings_utils.cpp b/src/theory/strings/theory_strings_utils.cpp new file mode 100644 index 000000000..42a8af5a1 --- /dev/null +++ b/src/theory/strings/theory_strings_utils.cpp @@ -0,0 +1,50 @@ +/********************* */ +/*! \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& a) +{ + std::vector 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 diff --git a/src/theory/strings/theory_strings_utils.h b/src/theory/strings/theory_strings_utils.h new file mode 100644 index 000000000..9e0779e16 --- /dev/null +++ b/src/theory/strings/theory_strings_utils.h @@ -0,0 +1,42 @@ +/********************* */ +/*! \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 + +#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& a); + +} // namespace utils +} // namespace strings +} // namespace theory +} // namespace CVC4 + +#endif