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,
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)
{
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)
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()
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
* 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.
* 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 */
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. */
projects / cvc5.git / commitdiff