// send phase requirements
for (const std::pair<const Node, bool> pp : cii.d_pendingPhase)
{
- d_im.sendPhaseRequirement(pp.first, pp.second);
+ Node ppr = Rewriter::rewrite(pp.first);
+ d_im.addPendingPhaseRequirement(ppr, pp.second);
}
// send the inference, which is a lemma
#include "theory/strings/infer_info.h"
+#include "theory/strings/inference_manager.h"
#include "theory/strings/theory_strings_utils.h"
namespace CVC4 {
return out;
}
-InferInfo::InferInfo() : d_id(Inference::NONE), d_idRev(false) {}
+InferInfo::InferInfo() : d_sim(nullptr), d_id(Inference::NONE), d_idRev(false)
+{
+}
+
+bool InferInfo::process(TheoryInferenceManager* im, bool asLemma)
+{
+ if (asLemma)
+ {
+ return d_sim->processLemma(*this);
+ }
+ return d_sim->processFact(*this);
+}
bool InferInfo::isTrivial() const
{
#include <vector>
#include "expr/node.h"
+#include "theory/theory_inference.h"
#include "util/safe_print.h"
namespace CVC4 {
LENGTH_GEQ_ONE
};
+class InferenceManager;
+
/**
* An inference. This is a class to track an unprocessed call to either
* send a fact, lemma, or conflict that is waiting to be asserted to the
* - (main equality) x ++ y ++ v1 = z ++ w ++ v2,
* - (length constraint) len(y) = len(w).
*/
-class InferInfo
+class InferInfo : public TheoryInference
{
public:
InferInfo();
~InferInfo() {}
+ /** Process this inference */
+ bool process(TheoryInferenceManager* im, bool asLemma) override;
+ /** Pointer to the class used for processing this info */
+ InferenceManager* d_sim;
/** The inference identifier */
Inference d_id;
/** Whether it is the reverse form of the above id */
ExtTheory& e,
SequencesStatistics& statistics,
ProofNodeManager* pnm)
- : TheoryInferenceManager(t, s, pnm),
+ : InferenceManagerBuffered(t, s, pnm),
d_state(s),
d_termReg(tr),
d_extt(e),
- d_statistics(statistics)
+ d_statistics(statistics),
+ d_ipc(pnm ? new InferProofCons(d_state.getSatContext(), pnm, d_statistics)
+ : nullptr)
{
NodeManager* nm = NodeManager::currentNM();
d_zero = nm->mkConst(Rational(0));
d_false = nm->mkConst(false);
}
+void InferenceManager::doPending()
+{
+ doPendingFacts();
+ if (d_state.isInConflict())
+ {
+ // just clear the pending vectors, nothing else to do
+ clearPendingLemmas();
+ clearPendingPhaseRequirements();
+ return;
+ }
+ doPendingLemmas();
+ doPendingPhaseRequirements();
+}
+
bool InferenceManager::sendInternalInference(std::vector<Node>& exp,
Node conc,
Inference infer)
return true;
}
-void InferenceManager::sendInference(const std::vector<Node>& exp,
+bool InferenceManager::sendInference(const std::vector<Node>& exp,
const std::vector<Node>& noExplain,
Node eq,
Inference infer,
bool isRev,
bool asLemma)
{
- eq = eq.isNull() ? d_false : Rewriter::rewrite(eq);
- if (eq == d_true)
+ if (eq.isNull())
{
- return;
+ eq = d_false;
+ }
+ else if (Rewriter::rewrite(eq) == d_true)
+ {
+ // if trivial, return
+ return false;
}
// wrap in infer info and send below
InferInfo ii;
ii.d_ant = exp;
ii.d_noExplain = noExplain;
sendInference(ii, asLemma);
+ return true;
}
-void InferenceManager::sendInference(const std::vector<Node>& exp,
+bool InferenceManager::sendInference(const std::vector<Node>& exp,
Node eq,
Inference infer,
bool isRev,
bool asLemma)
{
std::vector<Node> noExplain;
- sendInference(exp, noExplain, eq, infer, isRev, asLemma);
+ return sendInference(exp, noExplain, eq, infer, isRev, asLemma);
}
-void InferenceManager::sendInference(const InferInfo& ii, bool asLemma)
+void InferenceManager::sendInference(InferInfo& ii, bool asLemma)
{
Assert(!ii.isTrivial());
+ // set that this inference manager will be processing this inference
+ ii.d_sim = this;
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())
+ if (ii.isConflict())
+ {
+ 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;
+ ++(d_statistics.d_conflictsInfer);
+ // process the conflict immediately
+ processConflict(ii);
+ return;
+ }
+ else if (asLemma || options::stringInferAsLemmas() || !ii.isFact())
{
- if (ii.isConflict())
- {
- 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.notifyInConflict();
- return;
- }
Trace("strings-infer-debug") << "...as lemma" << std::endl;
- d_pendingLem.push_back(ii);
+ addPendingLemma(std::unique_ptr<InferInfo>(new InferInfo(ii)));
return;
}
if (options::stringInferSym())
Node eqs = ii.d_conc.substitute(
vars.begin(), vars.end(), subs.begin(), subs.end());
InferInfo iiSubsLem;
+ iiSubsLem.d_sim = this;
// 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;
}
}
Trace("strings-infer-debug") << "...as symbolic lemma" << std::endl;
- d_pendingLem.push_back(iiSubsLem);
+ addPendingLemma(std::unique_ptr<InferInfo>(new InferInfo(iiSubsLem)));
return;
}
if (Trace.isOn("strings-lemma-debug"))
for (const Node& u : unproc)
{
Trace("strings-lemma-debug")
- << " non-trivial exp : " << u << std::endl;
+ << " non-trivial explanation : " << u << std::endl;
}
}
}
Trace("strings-infer-debug") << "...as fact" << std::endl;
- // add to pending, to be processed as a fact
- d_pending.push_back(ii);
+ // add to pending to be processed as a fact
+ addPendingFact(std::unique_ptr<InferInfo>(new InferInfo(ii)));
}
bool InferenceManager::sendSplit(Node a, Node b, Inference infer, bool preq)
}
NodeManager* nm = NodeManager::currentNM();
InferInfo iiSplit;
+ iiSplit.d_sim = this;
iiSplit.d_id = infer;
iiSplit.d_conc = nm->mkNode(OR, eq, nm->mkNode(NOT, eq));
- sendPhaseRequirement(eq, preq);
- d_pendingLem.push_back(iiSplit);
+ eq = Rewriter::rewrite(eq);
+ addPendingPhaseRequirement(eq, preq);
+ addPendingLemma(std::unique_ptr<InferInfo>(new InferInfo(iiSplit)));
return true;
}
-void InferenceManager::sendPhaseRequirement(Node lit, bool pol)
-{
- lit = Rewriter::rewrite(lit);
- d_pendingReqPhase[lit] = pol;
-}
-
void InferenceManager::setIncomplete() { d_out.setIncomplete(); }
void InferenceManager::addToExplanation(Node a,
{
if (!lit.isNull())
{
+ Assert(!lit.isConst());
exp.push_back(lit);
}
}
-void InferenceManager::doPendingFacts()
+bool InferenceManager::hasProcessed() const
{
- size_t i = 0;
- while (!d_state.isInConflict() && i < d_pending.size())
- {
- 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_noExplain).
- Assert(ii.isFact());
- Node facts = ii.d_conc;
- Node exp = utils::mkAnd(ii.d_ant);
- Trace("strings-assert") << "(assert (=> " << exp << " " << facts
- << ")) ; fact " << ii.d_id << std::endl;
- // only keep stats if we process it here
- Trace("strings-lemma") << "Strings::Fact: " << facts << " from " << exp
- << " by " << ii.d_id << std::endl;
- d_statistics.d_inferences << ii.d_id;
- // assert it as a pending fact
- if (facts.getKind() == AND)
- {
- for (const Node& fact : facts)
- {
- 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);
- assertInternalFact(atom, polarity, exp);
- }
- }
- else
- {
- bool polarity = facts.getKind() != NOT;
- TNode atom = polarity ? facts : facts[0];
- // no double negation or double (conjunctive) conclusions
- Assert(atom.getKind() != NOT && atom.getKind() != AND);
- assertInternalFact(atom, polarity, exp);
- }
- i++;
- }
- d_pending.clear();
+ return d_state.isInConflict() || hasPending();
}
-void InferenceManager::doPendingLemmas()
+void InferenceManager::markCongruent(Node a, Node b)
{
- 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++)
- {
- 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_noExplain);
- }
- else
- {
- std::vector<Node> ev;
- ev.insert(ev.end(), ii.d_ant.begin(), ii.d_ant.end());
- eqExp = utils::mkAnd(ev);
- }
- // make the lemma node
- Node lem = ii.d_conc;
- if (eqExp != d_true)
- {
- lem = nm->mkNode(IMPLIES, eqExp, lem);
- }
- 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);
-
- // 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)
- {
- for (const Node& n : sks.second)
- {
- d_termReg.registerTermAtomic(n, sks.first);
- }
- }
- LemmaProperty p = LemmaProperty::NONE;
- if (ii.d_id == Inference::REDUCTION)
- {
- p |= LemmaProperty::NEEDS_JUSTIFY;
- }
- d_out.lemma(lem, p);
- }
- // process the pending require phase calls
- for (const std::pair<const Node, bool>& prp : d_pendingReqPhase)
+ Assert(a.getKind() == b.getKind());
+ if (d_extt.hasFunctionKind(a.getKind()))
{
- Trace("strings-pending") << "Require phase : " << prp.first
- << ", polarity = " << prp.second << std::endl;
- d_out.requirePhase(prp.first, prp.second);
+ d_extt.markCongruent(a, b);
}
- d_pendingLem.clear();
- d_pendingReqPhase.clear();
}
-bool InferenceManager::hasProcessed() const
+void InferenceManager::markReduced(Node n, bool contextDepend)
{
- return d_state.isInConflict() || !d_pendingLem.empty() || !d_pending.empty();
+ d_extt.markReduced(n, contextDepend);
}
-Node InferenceManager::mkExplain(const std::vector<Node>& a) const
+void InferenceManager::processConflict(const InferInfo& ii)
{
- std::vector<Node> noExplain;
- return mkExplain(a, noExplain);
+ Assert(!d_state.isInConflict());
+ // setup the fact to reproduce the proof in the call below
+ d_statistics.d_inferences << ii.d_id;
+ if (d_ipc != nullptr)
+ {
+ d_ipc->notifyFact(ii);
+ }
+ // make the trust node
+ TrustNode tconf = mkConflictExp(ii.d_ant, d_ipc.get());
+ Assert(tconf.getKind() == TrustNodeKind::CONFLICT);
+ Trace("strings-assert") << "(assert (not " << tconf.getNode()
+ << ")) ; conflict " << ii.d_id << std::endl;
+ // send the trusted conflict
+ trustedConflict(tconf);
}
-Node InferenceManager::mkExplain(const std::vector<Node>& a,
- const std::vector<Node>& noExplain) const
+bool InferenceManager::processFact(InferInfo& ii)
{
- std::vector<TNode> antec_exp;
- // copy to processing vector
- std::vector<Node> aconj;
- for (const Node& ac : a)
- {
- utils::flattenOp(AND, ac, aconj);
- }
- for (const Node& apc : aconj)
+ // Get the fact(s). There are multiple facts if the conclusion is an AND
+ std::vector<Node> facts;
+ if (ii.d_conc.getKind() == AND)
{
- if (std::find(noExplain.begin(), noExplain.end(), apc) != noExplain.end())
+ for (const Node& cc : ii.d_conc)
{
- if (std::find(antec_exp.begin(), antec_exp.end(), apc) == antec_exp.end())
- {
- Debug("strings-explain")
- << "Add to explanation (new literal) " << apc << std::endl;
- antec_exp.push_back(apc);
- }
- continue;
+ facts.push_back(cc);
}
- Assert(apc.getKind() != AND);
- Debug("strings-explain") << "Add to explanation " << apc << std::endl;
- if (apc.getKind() == NOT && apc[0].getKind() == EQUAL)
- {
- Assert(d_ee->hasTerm(apc[0][0]));
- Assert(d_ee->hasTerm(apc[0][1]));
- // ensure that we are ready to explain the disequality
- AlwaysAssert(d_ee->areDisequal(apc[0][0], apc[0][1], true));
- }
- Assert(apc.getKind() != EQUAL || d_ee->areEqual(apc[0], apc[1]));
- // now, explain
- explain(apc, antec_exp);
}
- Node ant;
- if (antec_exp.empty())
+ else
{
- ant = d_true;
+ facts.push_back(ii.d_conc);
}
- else if (antec_exp.size() == 1)
+ Trace("strings-assert") << "(assert (=> " << ii.getAntecedant() << " "
+ << ii.d_conc << ")) ; fact " << ii.d_id << std::endl;
+ Trace("strings-lemma") << "Strings::Fact: " << ii.d_conc << " from "
+ << ii.getAntecedant() << " by " << ii.d_id
+ << std::endl;
+ std::vector<Node> exp;
+ for (const Node& ec : ii.d_ant)
{
- ant = antec_exp[0];
+ utils::flattenOp(AND, ec, exp);
}
- else
+ bool ret = false;
+ // convert for each fact
+ for (const Node& fact : facts)
{
- ant = NodeManager::currentNM()->mkNode(AND, antec_exp);
+ ii.d_conc = fact;
+ d_statistics.d_inferences << ii.d_id;
+ bool polarity = fact.getKind() != NOT;
+ TNode atom = polarity ? fact : fact[0];
+ bool curRet = false;
+ if (d_ipc != nullptr)
+ {
+ // ensure the proof generator is ready to explain this fact in the
+ // current SAT context
+ d_ipc->notifyFact(ii);
+ // now, assert the internal fact with d_ipc as proof generator
+ curRet = assertInternalFact(atom, polarity, exp, d_ipc.get());
+ }
+ else
+ {
+ Node cexp = utils::mkAnd(exp);
+ // without proof generator
+ curRet = assertInternalFact(atom, polarity, cexp);
+ }
+ ret = ret || curRet;
+ // may be in conflict
+ if (d_state.isInConflict())
+ {
+ break;
+ }
}
- return ant;
+ return ret;
}
-void InferenceManager::explain(TNode literal,
- std::vector<TNode>& assumptions) const
+bool InferenceManager::processLemma(InferInfo& ii)
{
- Debug("strings-explain") << "Explain " << literal << " "
- << d_state.isInConflict() << std::endl;
- bool polarity = literal.getKind() != NOT;
- TNode atom = polarity ? literal : literal[0];
- std::vector<TNode> tassumptions;
- if (atom.getKind() == EQUAL)
+ Assert(!ii.isTrivial());
+ Assert(!ii.isConflict());
+ // set up the explanation and no-explanation
+ std::vector<Node> exp;
+ for (const Node& ec : ii.d_ant)
{
- if (atom[0] != atom[1])
- {
- Assert(d_ee->hasTerm(atom[0]));
- Assert(d_ee->hasTerm(atom[1]));
- d_ee->explainEquality(atom[0], atom[1], polarity, tassumptions);
- }
+ utils::flattenOp(AND, ec, exp);
}
- else
+ std::vector<Node> noExplain;
+ if (!options::stringRExplainLemmas())
{
- d_ee->explainPredicate(atom, polarity, tassumptions);
+ // if we aren't regressing the explanation, we add all literals to
+ // noExplain and ignore ii.d_ant.
+ noExplain.insert(noExplain.end(), exp.begin(), exp.end());
}
- for (const TNode a : tassumptions)
+ else
{
- if (std::find(assumptions.begin(), assumptions.end(), a)
- == assumptions.end())
+ // otherwise, the no-explain literals are those provided
+ for (const Node& ecn : ii.d_noExplain)
{
- assumptions.push_back(a);
+ utils::flattenOp(AND, ecn, noExplain);
}
}
- if (Debug.isOn("strings-explain-debug"))
+ // ensure that the proof generator is ready to explain the final conclusion
+ // of the lemma (ii.d_conc).
+ d_statistics.d_inferences << ii.d_id;
+ if (d_ipc != nullptr)
+ {
+ d_ipc->notifyFact(ii);
+ }
+ TrustNode tlem = mkLemmaExp(ii.d_conc, exp, noExplain, d_ipc.get());
+ Trace("strings-pending") << "Process pending lemma : " << tlem.getNode()
+ << std::endl;
+
+ // 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)
{
- Debug("strings-explain-debug")
- << "Explanation for " << literal << " was " << std::endl;
- for (const TNode a : tassumptions)
+ for (const Node& n : sks.second)
{
- Debug("strings-explain-debug") << " " << a << std::endl;
+ d_termReg.registerTermAtomic(n, sks.first);
}
}
-}
-
-void InferenceManager::markCongruent(Node a, Node b)
-{
- Assert(a.getKind() == b.getKind());
- if (d_extt.hasFunctionKind(a.getKind()))
+ LemmaProperty p = LemmaProperty::NONE;
+ if (ii.d_id == Inference::REDUCTION)
{
- d_extt.markCongruent(a, b);
+ p |= LemmaProperty::NEEDS_JUSTIFY;
}
-}
+ Trace("strings-assert") << "(assert " << tlem.getNode() << ") ; lemma "
+ << ii.d_id << std::endl;
+ Trace("strings-lemma") << "Strings::Lemma: " << tlem.getNode() << " by "
+ << ii.d_id << std::endl;
+ ++(d_statistics.d_lemmasInfer);
-void InferenceManager::markReduced(Node n, bool contextDepend)
-{
- d_extt.markReduced(n, contextDepend);
+ // call the trusted lemma, without caching
+ return trustedLemma(tlem, p, false);
}
} // namespace strings
#include "context/cdhashset.h"
#include "context/context.h"
#include "expr/node.h"
+#include "expr/proof_node_manager.h"
#include "theory/ext_theory.h"
+#include "theory/inference_manager_buffered.h"
#include "theory/output_channel.h"
#include "theory/strings/infer_info.h"
+#include "theory/strings/infer_proof_cons.h"
#include "theory/strings/sequences_stats.h"
#include "theory/strings/solver_state.h"
#include "theory/strings/term_registry.h"
* theory of strings, e.g. sendPhaseRequirement, setIncomplete, and
* with the extended theory object e.g. markCongruent.
*/
-class InferenceManager : public TheoryInferenceManager
+class InferenceManager : public InferenceManagerBuffered
{
typedef context::CDHashSet<Node, NodeHashFunction> NodeSet;
typedef context::CDHashMap<Node, Node, NodeHashFunction> NodeNodeMap;
+ friend class InferInfo;
public:
InferenceManager(Theory& t,
ProofNodeManager* pnm);
~InferenceManager() {}
+ /**
+ * Do pending method. This processes all pending facts, lemmas and pending
+ * phase requests based on the policy of this manager. This means that
+ * we process the pending facts first and abort if in conflict. Otherwise, we
+ * process the pending lemmas and then the pending phase requirements.
+ * Notice that we process the pending lemmas even if there were facts.
+ */
+ void doPending();
+
/** send internal inferences
*
* This is called when we have inferred exp => conc, where exp is a set
* is used as a hint for proof reconstruction.
* @param asLemma If true, then this method will send a lemma instead
* of a fact whenever applicable.
+ * @return true if the inference was not trivial (e.g. its conclusion did
+ * not rewrite to true).
*/
- void sendInference(const std::vector<Node>& exp,
+ bool sendInference(const std::vector<Node>& exp,
const std::vector<Node>& noExplain,
Node eq,
Inference infer,
bool isRev = false,
bool asLemma = false);
/** same as above, but where noExplain is empty */
- void sendInference(const std::vector<Node>& exp,
+ bool sendInference(const std::vector<Node>& exp,
Node eq,
Inference infer,
bool isRev = false,
* If the flag asLemma is true, then this method will send a lemma instead
* of a fact whenever applicable.
*/
- void sendInference(const InferInfo& ii, bool asLemma = false);
+ void sendInference(InferInfo& ii, bool asLemma = false);
/** Send split
*
* This requests that ( a = b V a != b ) is sent on the output channel as a
* otherwise. A split is trivial if a=b rewrites to a constant.
*/
bool sendSplit(Node a, Node b, Inference infer, 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. This requirement is processed at the same time
- * lemmas are sent on the output channel of this class during this call to
- * check. This means if the current lemmas of this class are abandoned (due
- * to a conflict), the phase requirement is not processed.
- */
- void sendPhaseRequirement(Node lit, bool pol);
/**
* Set that we are incomplete for the current set of assertions (in other
* words, we must answer "unknown" instead of "sat"); this calls the output
/** Adds lit to the vector exp if it is non-null */
void addToExplanation(Node lit, std::vector<Node>& exp) const;
//----------------------------end constructing antecedants
- /** 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.
- *
- * 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;
- /** 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(); }
- /** make explanation
- *
- * This returns a node corresponding to the explanation of formulas in a,
- * interpreted conjunctively. The returned node is a conjunction of literals
- * that have been asserted to the equality engine.
- */
- Node mkExplain(const std::vector<Node>& a) const;
- /** Same as above, but with a subset noExplain that should not be explained */
- Node mkExplain(const std::vector<Node>& a,
- const std::vector<Node>& noExplain) const;
- /**
- * Explain literal l, add conjuncts to assumptions vector instead of making
- * the node corresponding to their conjunction.
- */
- void explain(TNode literal, std::vector<TNode>& assumptions) const;
// ------------------------------------------------- extended theory
/**
* Mark that terms a and b are congruent in the current context.
void markReduced(Node n, bool contextDepend = true);
// ------------------------------------------------- end extended theory
+ /**
+ * Called when ii is ready to be processed as a conflict. This makes a
+ * trusted node whose generator is the underlying proof equality engine
+ * (if it exists), and sends it on the output channel.
+ */
+ void processConflict(const InferInfo& ii);
+
private:
+ /** Called when ii is ready to be processed as a fact */
+ bool processFact(InferInfo& ii);
+ /** Called when ii is ready to be processed as a lemma */
+ bool processLemma(InferInfo& ii);
/** Reference to the solver state of the theory of strings. */
SolverState& d_state;
/** Reference to the term registry of theory of strings */
ExtTheory& d_extt;
/** Reference to the statistics for the theory of strings/sequences. */
SequencesStatistics& d_statistics;
-
+ /** Conversion from inferences to proofs */
+ std::unique_ptr<InferProofCons> d_ipc;
/** Common constants */
Node d_true;
Node d_false;
Node d_zero;
Node d_one;
- /**
- * The list of pending literals to assert to the equality engine along with
- * their explanation.
- */
- std::vector<InferInfo> 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. */
- std::vector<InferInfo> d_pendingLem;
};
} // namespace strings
d_regexpUnfoldingsNeg("theory::strings::regexpUnfoldingsNeg"),
d_rewrites("theory::strings::rewrites"),
d_conflictsEqEngine("theory::strings::conflictsEqEngine", 0),
- d_conflictsEagerPrefix("theory::strings::conflictsEagerPrefix", 0),
+ d_conflictsEager("theory::strings::conflictsEager", 0),
d_conflictsInfer("theory::strings::conflictsInfer", 0),
d_lemmasEagerPreproc("theory::strings::lemmasEagerPreproc", 0),
d_lemmasCmiSplit("theory::strings::lemmasCmiSplit", 0),
smtStatisticsRegistry()->registerStat(&d_regexpUnfoldingsNeg);
smtStatisticsRegistry()->registerStat(&d_rewrites);
smtStatisticsRegistry()->registerStat(&d_conflictsEqEngine);
- smtStatisticsRegistry()->registerStat(&d_conflictsEagerPrefix);
+ smtStatisticsRegistry()->registerStat(&d_conflictsEager);
smtStatisticsRegistry()->registerStat(&d_conflictsInfer);
smtStatisticsRegistry()->registerStat(&d_lemmasEagerPreproc);
smtStatisticsRegistry()->registerStat(&d_lemmasCmiSplit);
smtStatisticsRegistry()->unregisterStat(&d_regexpUnfoldingsNeg);
smtStatisticsRegistry()->unregisterStat(&d_rewrites);
smtStatisticsRegistry()->unregisterStat(&d_conflictsEqEngine);
- smtStatisticsRegistry()->unregisterStat(&d_conflictsEagerPrefix);
+ smtStatisticsRegistry()->unregisterStat(&d_conflictsEager);
smtStatisticsRegistry()->unregisterStat(&d_conflictsInfer);
smtStatisticsRegistry()->unregisterStat(&d_lemmasEagerPreproc);
smtStatisticsRegistry()->unregisterStat(&d_lemmasCmiSplit);
//--------------- conflicts, partition of calls to OutputChannel::conflict
/** Number of equality engine conflicts */
IntStat d_conflictsEqEngine;
- /** Number of eager prefix conflicts */
- IntStat d_conflictsEagerPrefix;
+ /** Number of eager conflicts */
+ IntStat d_conflictsEager;
/** Number of inference conflicts */
IntStat d_conflictsInfer;
//--------------- end of conflicts
SolverState::SolverState(context::Context* c,
context::UserContext* u,
Valuation& v)
- : TheoryState(c, u, v), d_eeDisequalities(c), d_pendingConflict(c)
+ : TheoryState(c, u, v), d_eeDisequalities(c), d_pendingConflictSet(c, false)
{
d_zero = NodeManager::currentNM()->mkConst(Rational(0));
+ d_false = NodeManager::currentNM()->mkConst(false);
}
SolverState::~SolverState()
}
if (!e2->d_prefixC.get().isNull())
{
- setPendingConflictWhen(
+ setPendingPrefixConflictWhen(
e1->addEndpointConst(e2->d_prefixC, Node::null(), false));
}
if (!e2->d_suffixC.get().isNull())
{
- setPendingConflictWhen(
+ setPendingPrefixConflictWhen(
e1->addEndpointConst(e2->d_suffixC, Node::null(), true));
}
if (e2->d_cardinalityLemK.get() > e1->d_cardinalityLemK.get())
Trace("strings-eager-pconf-debug")
<< "New term: " << concat << " for " << t << " with prefix " << c
<< " (" << (r == 1) << ")" << std::endl;
- setPendingConflictWhen(ei->addEndpointConst(t, c, r == 1));
+ setPendingPrefixConflictWhen(ei->addEndpointConst(t, c, r == 1));
}
}
}
return false;
}
-void SolverState::setPendingConflictWhen(Node conf)
+void SolverState::setPendingPrefixConflictWhen(Node conf)
{
- if (!conf.isNull() && d_pendingConflict.get().isNull())
+ if (conf.isNull() || d_pendingConflictSet.get())
{
- d_pendingConflict = conf;
+ return;
}
+ InferInfo iiPrefixConf;
+ iiPrefixConf.d_id = Inference::PREFIX_CONFLICT;
+ iiPrefixConf.d_conc = d_false;
+ utils::flattenOp(AND, conf, iiPrefixConf.d_ant);
+ setPendingConflict(iiPrefixConf);
}
-Node SolverState::getPendingConflict() const { return d_pendingConflict; }
+void SolverState::setPendingConflict(InferInfo& ii)
+{
+ if (!d_pendingConflictSet.get())
+ {
+ d_pendingConflict = ii;
+ }
+}
+
+bool SolverState::hasPendingConflict() const { return d_pendingConflictSet; }
+
+bool SolverState::getPendingConflict(InferInfo& ii) const
+{
+ if (d_pendingConflictSet)
+ {
+ ii = d_pendingConflict;
+ return true;
+ }
+ return false;
+}
std::pair<bool, Node> SolverState::entailmentCheck(options::TheoryOfMode mode,
TNode lit)
#include "context/context.h"
#include "expr/node.h"
#include "theory/strings/eqc_info.h"
+#include "theory/strings/infer_info.h"
#include "theory/theory_model.h"
#include "theory/theory_state.h"
#include "theory/uf/equality_engine.h"
void eqNotifyDisequal(TNode t1, TNode t2, TNode reason);
//-------------------------------------- end notifications for equalities
//------------------------------------------ conflicts
- /** set pending conflict
+ /** set pending prefix conflict
*
* If conf is non-null, this is called when conf is a conjunction of literals
* that hold in the current context that are unsatisfiable. It is set as the
* during a merge operation, when the equality engine is not in a state to
* provide explanations.
*/
- void setPendingConflictWhen(Node conf);
+ void setPendingPrefixConflictWhen(Node conf);
+ /**
+ * Set pending conflict, infer info version. Called when we are in conflict
+ * based on the inference ii. This generalizes the above method.
+ */
+ void setPendingConflict(InferInfo& ii);
+ /** return true if we have a pending conflict */
+ bool hasPendingConflict() const;
/** get the pending conflict, or null if none exist */
- Node getPendingConflict() const;
+ bool getPendingConflict(InferInfo& ii) const;
//------------------------------------------ end conflicts
/** get length with explanation
*
private:
/** Common constants */
Node d_zero;
+ Node d_false;
/**
* The (SAT-context-dependent) list of disequalities that have been asserted
* to the equality engine above.
*/
NodeList d_eeDisequalities;
/** The pending conflict if one exists */
- context::CDO<Node> d_pendingConflict;
+ context::CDO<bool> d_pendingConflictSet;
+ /** The pending conflict, valid if the above flag is true */
+ InferInfo d_pendingConflict;
/** Map from representatives to their equivalence class information */
std::map<Node, EqcInfo*> d_eqcInfo;
}; /* class TheoryStrings */
#include "theory/strings/theory_strings.h"
#include "expr/kind.h"
+#include "options/smt_options.h"
#include "options/strings_options.h"
#include "options/theory_options.h"
#include "smt/logic_exception.h"
d_notify(*this),
d_statistics(),
d_state(c, u, d_valuation),
- d_termReg(d_state, out, d_statistics, nullptr),
+ d_termReg(d_state, out, d_statistics, pnm),
d_extTheoryCb(),
d_extTheory(d_extTheoryCb, c, u, out),
d_im(*this, d_state, d_termReg, d_extTheory, d_statistics, pnm),
TrustNode TheoryStrings::explain(TNode literal)
{
Debug("strings-explain") << "explain called on " << literal << std::endl;
- std::vector< TNode > assumptions;
- d_im.explain(literal, assumptions);
- Node ret;
- if( assumptions.empty() ){
- ret = d_true;
- }else if( assumptions.size()==1 ){
- ret = assumptions[0];
- }else{
- ret = NodeManager::currentNM()->mkNode(kind::AND, assumptions);
- }
- return TrustNode::mkTrustPropExp(literal, ret, nullptr);
+ return d_im.explainLit(literal);
}
void TheoryStrings::presolve() {
}
}
// process pending conflicts due to reasoning about endpoints
- if (!d_state.isInConflict())
+ if (!d_state.isInConflict() && d_state.hasPendingConflict())
{
- Node pc = d_state.getPendingConflict();
- if (!pc.isNull())
- {
- std::vector<Node> a;
- a.push_back(pc);
- Trace("strings-pending")
- << "Process pending conflict " << pc << std::endl;
- Node conflictNode = d_im.mkExplain(a);
- Trace("strings-conflict")
- << "CONFLICT: Eager prefix : " << conflictNode << std::endl;
- ++(d_statistics.d_conflictsEagerPrefix);
- d_im.conflict(conflictNode);
- return;
- }
+ InferInfo iiPendingConf;
+ d_state.getPendingConflict(iiPendingConf);
+ Trace("strings-pending")
+ << "Process pending conflict " << iiPendingConf.d_ant << std::endl;
+ Trace("strings-conflict")
+ << "CONFLICT: Eager : " << iiPendingConf.d_ant << std::endl;
+ ++(d_statistics.d_conflictsEager);
+ // call the inference manager to send the conflict
+ d_im.processConflict(iiPendingConf);
+ return;
}
Trace("strings-pending-debug") << " Now collect terms" << std::endl;
// Collect extended function terms in the atom. Notice that we must register
Trace("strings-eqc") << std::endl;
}
++(d_statistics.d_checkRuns);
- bool addedLemma = false;
- bool addedFact;
+ bool sentLemma = false;
+ bool hadPending = false;
Trace("strings-check") << "Full effort check..." << std::endl;
do{
+ d_im.reset();
++(d_statistics.d_strategyRuns);
Trace("strings-check") << " * Run strategy..." << std::endl;
runStrategy(e);
+ // remember if we had pending facts or lemmas
+ hadPending = d_im.hasPending();
// Send the facts *and* the lemmas. We send lemmas regardless of whether
// we send facts since some lemmas cannot be dropped. Other lemmas are
// otherwise avoided by aborting the strategy when a fact is ready.
- addedFact = d_im.hasPendingFact();
- addedLemma = d_im.hasPendingLemma();
- d_im.doPendingFacts();
- d_im.doPendingLemmas();
+ d_im.doPending();
+ // Did we successfully send a lemma? Notice that if hasPending = true
+ // and sentLemma = false, then the above call may have:
+ // (1) had no pending lemmas, but successfully processed pending facts,
+ // (2) unsuccessfully processed pending lemmas.
+ // In either case, we repeat the strategy if we are not in conflict.
+ sentLemma = d_im.hasSentLemma();
if (Trace.isOn("strings-check"))
{
Trace("strings-check") << " ...finish run strategy: ";
- Trace("strings-check") << (addedFact ? "addedFact " : "");
- Trace("strings-check") << (addedLemma ? "addedLemma " : "");
+ Trace("strings-check") << (hadPending ? "hadPending " : "");
+ Trace("strings-check") << (sentLemma ? "sentLemma " : "");
Trace("strings-check") << (d_state.isInConflict() ? "conflict " : "");
- if (!addedFact && !addedLemma && !d_state.isInConflict())
+ if (!hadPending && !sentLemma && !d_state.isInConflict())
{
Trace("strings-check") << "(none)";
}
Trace("strings-check") << std::endl;
}
- // repeat if we did not add a lemma or conflict
- } while (!d_state.isInConflict() && !addedLemma && addedFact);
+ // repeat if we did not add a lemma or conflict, and we had pending
+ // facts or lemmas.
+ } while (!d_state.isInConflict() && !sentLemma && hadPending);
}
Trace("strings-check") << "Theory of strings, done check : " << e << std::endl;
Assert(!d_im.hasPendingFact());
/** Conflict when merging two constants */
void TheoryStrings::conflict(TNode a, TNode b){
- if (!d_state.isInConflict())
+ if (d_state.isInConflict())
{
- Debug("strings-conflict") << "Making conflict..." << std::endl;
- d_state.notifyInConflict();
- TrustNode conflictNode = explain(a.eqNode(b));
- Trace("strings-conflict")
- << "CONFLICT: Eq engine conflict : " << conflictNode.getNode()
- << std::endl;
- ++(d_statistics.d_conflictsEqEngine);
- d_out->conflict(conflictNode.getNode());
+ // already in conflict
+ return;
}
+ d_im.conflictEqConstantMerge(a, b);
+ Trace("strings-conflict") << "CONFLICT: Eq engine conflict" << std::endl;
+ ++(d_statistics.d_conflictsEqEngine);
}
void TheoryStrings::eqNotifyNewClass(TNode t){
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);
- d_im.sendPhaseRequirement(deq, false);
+ deq = Rewriter::rewrite(deq);
+ d_im.addPendingPhaseRequirement(deq, false);
std::vector<Node> emptyVec;
d_im.sendInference(emptyVec, inj_lem, Inference::CODE_INJ);
}
projects / cvc5.git / commitdiff