summaryrefslogtreecommitdiff
path: root/src/theory/strings/inference_manager.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/strings/inference_manager.cpp')
-rw-r--r--src/theory/strings/inference_manager.cpp279
1 files changed, 141 insertions, 138 deletions
diff --git a/src/theory/strings/inference_manager.cpp b/src/theory/strings/inference_manager.cpp
index 2a559faac..8e68913ac 100644
--- a/src/theory/strings/inference_manager.cpp
+++ b/src/theory/strings/inference_manager.cpp
@@ -117,83 +117,86 @@ bool InferenceManager::sendInternalInference(std::vector<Node>& exp,
}
void InferenceManager::sendInference(const std::vector<Node>& exp,
- const std::vector<Node>& exp_n,
+ const std::vector<Node>& expn,
Node eq,
Inference infer,
bool asLemma)
{
eq = eq.isNull() ? d_false : Rewriter::rewrite(eq);
- if (Trace.isOn("strings-infer-debug"))
- {
- Trace("strings-infer-debug")
- << "By " << infer << ", 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;
- }
- }
if (eq == d_true)
{
return;
}
- // only keep stats if not trivial conclusion
- d_statistics.d_inferences << infer;
- Node atom = eq.getKind() == NOT ? eq[0] : eq;
- // check if we should send a lemma or an inference
- if (asLemma || atom == d_false || atom.getKind() == OR || !exp_n.empty()
- || options::stringInferAsLemmas())
+ // wrap in infer info and send below
+ InferInfo ii;
+ ii.d_id = infer;
+ ii.d_conc = eq;
+ ii.d_ant = exp;
+ ii.d_antn = expn;
+ sendInference(ii, asLemma);
+}
+
+void InferenceManager::sendInference(const std::vector<Node>& exp,
+ Node eq,
+ Inference infer,
+ bool asLemma)
+{
+ std::vector<Node> expn;
+ sendInference(exp, expn, eq, infer, asLemma);
+}
+
+void InferenceManager::sendInference(const InferInfo& ii, bool asLemma)
+{
+ Assert(!ii.isTrivial());
+ Trace("strings-infer-debug")
+ << "sendInference: " << ii << ", asLemma = " << asLemma << std::endl;
+ // check if we should send a conflict, lemma or a fact
+ if (asLemma || options::stringInferAsLemmas() || !ii.isFact())
{
- Node eq_exp;
- if (options::stringRExplainLemmas())
+ if (ii.isConflict())
{
- eq_exp = 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;
+ Trace("strings-infer-debug") << "...as conflict" << std::endl;
+ Trace("strings-lemma") << "Strings::Conflict: " << ii.d_ant << " by "
+ << ii.d_id << std::endl;
+ Trace("strings-conflict") << "CONFLICT: inference conflict " << ii.d_ant
+ << " by " << ii.d_id << std::endl;
+ // we must fully explain it
+ Node conf = mkExplain(ii.d_ant);
+ Trace("strings-assert") << "(assert (not " << conf << ")) ; conflict "
+ << ii.d_id << std::endl;
+ ++(d_statistics.d_conflictsInfer);
+ // only keep stats if we process it here
+ d_statistics.d_inferences << ii.d_id;
+ d_out.conflict(conf);
+ d_state.setConflict();
+ return;
}
- sendLemma(eq_exp, eq, infer);
+ Trace("strings-infer-debug") << "...as lemma" << std::endl;
+ d_pendingLem.push_back(ii);
return;
}
- Node eqExp = utils::mkAnd(exp);
if (options::stringInferSym())
{
std::vector<Node> vars;
std::vector<Node> subs;
std::vector<Node> unproc;
- d_termReg.inferSubstitutionProxyVars(eqExp, vars, subs, unproc);
+ for (const Node& ac : ii.d_ant)
+ {
+ d_termReg.inferSubstitutionProxyVars(ac, vars, subs, unproc);
+ }
if (unproc.empty())
{
- Node eqs =
- eq.substitute(vars.begin(), vars.end(), subs.begin(), subs.end());
+ Node eqs = ii.d_conc.substitute(
+ vars.begin(), vars.end(), subs.begin(), subs.end());
+ InferInfo iiSubsLem;
+ // keep the same id for now, since we are transforming the form of the
+ // inference, not the root reason.
+ iiSubsLem.d_id = ii.d_id;
+ iiSubsLem.d_conc = eqs;
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 " << iiSubsLem << std::endl;
Trace("strings-lemma-debug")
<< "Strings::Infer Alternate : " << eqs << std::endl;
for (unsigned i = 0, nvars = vars.size(); i < nvars; i++)
@@ -202,7 +205,8 @@ void InferenceManager::sendInference(const std::vector<Node>& exp,
<< " " << vars[i] << " -> " << subs[i] << std::endl;
}
}
- sendLemma(d_true, eqs, infer);
+ Trace("strings-infer-debug") << "...as symbolic lemma" << std::endl;
+ d_pendingLem.push_back(iiSubsLem);
return;
}
if (Trace.isOn("strings-lemma-debug"))
@@ -214,59 +218,11 @@ void InferenceManager::sendInference(const std::vector<Node>& exp,
}
}
}
- 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,
- Node eq,
- Inference infer,
- bool asLemma)
-{
- std::vector<Node> exp_n;
- sendInference(exp, exp_n, eq, infer, asLemma);
-}
-
-void InferenceManager::sendInference(const InferInfo& i)
-{
- sendInference(i.d_ant, i.d_antn, i.d_conc, i.d_id, true);
-}
-
-void InferenceManager::sendLemma(Node ant, Node conc, Inference infer)
-{
- if (conc.isNull() || conc == d_false)
- {
- Trace("strings-conflict")
- << "Strings::Conflict : " << infer << " : " << ant << std::endl;
- Trace("strings-lemma") << "Strings::Conflict : " << infer << " : " << ant
- << std::endl;
- Trace("strings-assert")
- << "(assert (not " << ant << ")) ; conflict " << infer << std::endl;
- ++(d_statistics.d_conflictsInfer);
- d_out.conflict(ant);
- d_state.setConflict();
- return;
- }
- Node lem;
- if (ant == d_true)
- {
- lem = conc;
- }
- else
- {
- lem = NodeManager::currentNM()->mkNode(IMPLIES, ant, conc);
- }
- Trace("strings-lemma") << "Strings::Lemma " << infer << " : " << lem
- << std::endl;
- Trace("strings-assert") << "(assert " << lem << ") ; lemma " << infer
- << std::endl;
- d_pendingLem.push_back(lem);
+ Trace("strings-infer-debug") << "...as fact" << std::endl;
+ // add to pending, to be processed as a fact
+ d_pending.push_back(ii);
}
-
bool InferenceManager::sendSplit(Node a, Node b, Inference infer, bool preq)
{
Node eq = a.eqNode(b);
@@ -275,14 +231,12 @@ bool InferenceManager::sendSplit(Node a, Node b, Inference infer, bool preq)
{
return false;
}
- // update statistics
- d_statistics.d_inferences << infer;
NodeManager* nm = NodeManager::currentNM();
- Node lemma_or = nm->mkNode(OR, eq, nm->mkNode(NOT, eq));
- Trace("strings-lemma") << "Strings::Lemma " << infer
- << " SPLIT : " << lemma_or << std::endl;
- d_pendingLem.push_back(lemma_or);
+ InferInfo iiSplit;
+ iiSplit.d_id = infer;
+ iiSplit.d_conc = nm->mkNode(OR, eq, nm->mkNode(NOT, eq));
sendPhaseRequirement(eq, preq);
+ d_pendingLem.push_back(iiSplit);
return true;
}
@@ -320,23 +274,25 @@ void InferenceManager::doPendingFacts()
size_t i = 0;
while (!d_state.isInConflict() && i < d_pending.size())
{
- Node fact = d_pending[i].d_fact;
- Node exp = d_pending[i].d_exp;
- if (fact.getKind() == AND)
- {
- for (const Node& lit : fact)
- {
- bool polarity = lit.getKind() != NOT;
- TNode atom = polarity ? lit : lit[0];
- assertPendingFact(atom, polarity, exp);
- }
- }
- else
- {
- bool polarity = fact.getKind() != NOT;
- TNode atom = polarity ? fact : fact[0];
- assertPendingFact(atom, polarity, exp);
- }
+ InferInfo& ii = d_pending[i];
+ // At this point, ii should be a "fact", i.e. something whose conclusion
+ // should be added as a normal equality or predicate to the equality engine
+ // with no new external assumptions (ii.d_antn).
+ Assert(ii.isFact());
+ Node fact = ii.d_conc;
+ Node exp = utils::mkAnd(ii.d_ant);
+ Trace("strings-assert") << "(assert (=> " << exp << " " << fact
+ << ")) ; fact " << ii.d_id << std::endl;
+ // only keep stats if we process it here
+ Trace("strings-lemma") << "Strings::Fact: " << fact << " from " << exp
+ << " by " << ii.d_id << std::endl;
+ d_statistics.d_inferences << ii.d_id;
+ // assert it as a pending fact
+ bool polarity = fact.getKind() != NOT;
+ TNode atom = polarity ? fact : fact[0];
+ // no double negation or double (conjunctive) conclusions
+ Assert(atom.getKind() != NOT && atom.getKind() != AND);
+ 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.
@@ -349,21 +305,68 @@ void InferenceManager::doPendingFacts()
void InferenceManager::doPendingLemmas()
{
- if (!d_state.isInConflict())
+ if (d_state.isInConflict())
+ {
+ // just clear the pending vectors, nothing else to do
+ d_pendingLem.clear();
+ d_pendingReqPhase.clear();
+ return;
+ }
+ NodeManager* nm = NodeManager::currentNM();
+ for (unsigned i = 0, psize = d_pendingLem.size(); i < psize; i++)
{
- for (const Node& lc : d_pendingLem)
+ InferInfo& ii = d_pendingLem[i];
+ Assert(!ii.isTrivial());
+ Assert(!ii.isConflict());
+ // get the explanation
+ Node eqExp;
+ if (options::stringRExplainLemmas())
+ {
+ eqExp = mkExplain(ii.d_ant, ii.d_antn);
+ }
+ else
+ {
+ std::vector<Node> ev;
+ ev.insert(ev.end(), ii.d_ant.begin(), ii.d_ant.end());
+ ev.insert(ev.end(), ii.d_antn.begin(), ii.d_antn.end());
+ eqExp = utils::mkAnd(ev);
+ }
+ // make the lemma node
+ Node lem = ii.d_conc;
+ if (eqExp != d_true)
{
- Trace("strings-pending") << "Process pending lemma : " << lc << std::endl;
- ++(d_statistics.d_lemmasInfer);
- d_out.lemma(lc);
+ lem = nm->mkNode(IMPLIES, eqExp, lem);
}
- for (const std::pair<const Node, bool>& prp : d_pendingReqPhase)
+ Trace("strings-pending") << "Process pending lemma : " << lem << std::endl;
+ Trace("strings-assert")
+ << "(assert " << lem << ") ; lemma " << ii.d_id << std::endl;
+ Trace("strings-lemma") << "Strings::Lemma: " << lem << " by " << ii.d_id
+ << std::endl;
+ // only keep stats if we process it here
+ d_statistics.d_inferences << ii.d_id;
+ ++(d_statistics.d_lemmasInfer);
+ d_out.lemma(lem);
+
+ // Process the side effects of the inference info.
+ // Register the new skolems from this inference. We register them here
+ // (lazily), since this is the moment when we have decided to process the
+ // inference.
+ for (const std::pair<const LengthStatus, std::vector<Node> >& sks :
+ ii.d_new_skolem)
{
- Trace("strings-pending") << "Require phase : " << prp.first
- << ", polarity = " << prp.second << std::endl;
- d_out.requirePhase(prp.first, prp.second);
+ for (const Node& n : sks.second)
+ {
+ d_termReg.registerTermAtomic(n, sks.first);
+ }
}
}
+ // process the pending require phase calls
+ 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();
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback