diff options
| -rw-r--r-- | src/theory/strings/inference_manager.cpp | 96 | ||||
| -rw-r--r-- | src/theory/strings/inference_manager.h | 55 |
2 files changed, 84 insertions, 67 deletions
diff --git a/src/theory/strings/inference_manager.cpp b/src/theory/strings/inference_manager.cpp index 9d1c6fac4..2a559faac 100644 --- a/src/theory/strings/inference_manager.cpp +++ b/src/theory/strings/inference_manager.cpp @@ -177,11 +177,48 @@ void InferenceManager::sendInference(const std::vector<Node>& exp, eq_exp = d_true; } sendLemma(eq_exp, eq, infer); + return; } - else + Node eqExp = utils::mkAnd(exp); + if (options::stringInferSym()) { - sendInfer(utils::mkAnd(exp), eq, infer); + std::vector<Node> vars; + std::vector<Node> subs; + std::vector<Node> unproc; + d_termReg.inferSubstitutionProxyVars(eqExp, 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 " + << eqExp << " by " << infer << 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, infer); + 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 " << eqExp + << " by " << infer << std::endl; + Trace("strings-assert") << "(assert (=> " << eqExp << " " << eq + << ")) ; infer " << infer << std::endl; + d_pending.push_back(PendingInfer(infer, eq, eqExp)); } void InferenceManager::sendInference(const std::vector<Node>& exp, @@ -229,51 +266,6 @@ void InferenceManager::sendLemma(Node ant, Node conc, Inference infer) d_pendingLem.push_back(lem); } -void InferenceManager::sendInfer(Node eq_exp, Node eq, Inference infer) -{ - if (options::stringInferSym()) - { - std::vector<Node> vars; - std::vector<Node> subs; - std::vector<Node> unproc; - d_termReg.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 " << infer << 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, infer); - 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 " << infer << std::endl; - Trace("strings-assert") << "(assert (=> " << eq_exp << " " << eq - << ")) ; infer " << infer << 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, Inference infer, bool preq) { @@ -328,8 +320,8 @@ void InferenceManager::doPendingFacts() size_t i = 0; while (!d_state.isInConflict() && i < d_pending.size()) { - Node fact = d_pending[i]; - Node exp = d_pendingExp[fact]; + Node fact = d_pending[i].d_fact; + Node exp = d_pending[i].d_exp; if (fact.getKind() == AND) { for (const Node& lit : fact) @@ -345,10 +337,14 @@ void InferenceManager::doPendingFacts() TNode atom = polarity ? fact : fact[0]; assertPendingFact(atom, polarity, exp); } + // Must reference count the equality and its explanation, which is not done + // by the equality engine. Notice that we do not need to do this for + // external assertions, which enter as facts through sendAssumption. + d_keep.insert(fact); + d_keep.insert(exp); i++; } d_pending.clear(); - d_pendingExp.clear(); } void InferenceManager::doPendingLemmas() diff --git a/src/theory/strings/inference_manager.h b/src/theory/strings/inference_manager.h index 041724d8d..6e11bf85e 100644 --- a/src/theory/strings/inference_manager.h +++ b/src/theory/strings/inference_manager.h @@ -35,6 +35,29 @@ namespace CVC4 { namespace theory { namespace strings { +/** + * A pending inference. This is a helper class to track an unprocessed call to + * InferenceManager::sendInference that is waiting to be asserted as a fact to + * the equality engine. + */ +struct PendingInfer +{ + PendingInfer(Inference i, Node fact, Node exp) + : d_infer(i), d_fact(fact), d_exp(exp) + { + } + ~PendingInfer() {} + /** The inference identifier */ + Inference d_infer; + /** The conclusion */ + Node d_fact; + /** + * Its explanation. This is a conjunction of literals that hold in the + * equality engine in the current context. + */ + Node d_exp; +}; + /** Inference Manager * * The purpose of this class is to process inference steps for strategies @@ -115,18 +138,22 @@ class InferenceManager * 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: + * theory of strings. This method may call sendLemma or otherwise add a + * PendingInfer to d_pending, indicating a fact should be asserted to the + * equality engine. 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, + * class with explanation exp, where exp is a set of literals that currently + * hold in the equality engine. We add this to the pending vector d_pending. * * [3] (Lemma) Indicate that the lemma ( EXPLAIN(exp) ^ exp_n ) => eq should - * be sent on the output channel of the theory of strings, or + * be sent on the output channel of the theory of strings, where EXPLAIN + * returns the explanation of the node in exp in terms of the literals + * asserted to the theory of strings, as computed by the equality engine. + * This is also added to a pending vector, d_pendingLem. * * [4] (Conflict) Immediately report a conflict EXPLAIN(exp) on the output * channel of the theory of strings. @@ -288,13 +315,6 @@ class InferenceManager * debugging. */ void sendLemma(Node ant, Node conc, Inference infer); - /** - * 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, Inference infer); /** Reference to the solver state of the theory of strings. */ SolverState& d_state; /** Reference to the term registry of theory of strings */ @@ -311,10 +331,11 @@ class InferenceManager Node d_false; Node d_zero; Node d_one; - /** 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; + /** + * The list of pending literals to assert to the equality engine along with + * their explanation. + */ + std::vector<PendingInfer> d_pending; /** 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. */ |