summaryrefslogtreecommitdiff
path: root/src/theory
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory')
-rw-r--r--src/theory/strings/infer_proof_cons.cpp107
-rw-r--r--src/theory/strings/infer_proof_cons.h74
-rw-r--r--src/theory/strings/proof_checker.cpp7
-rw-r--r--src/theory/strings/sequences_stats.cpp2
-rw-r--r--src/theory/strings/sequences_stats.h7
5 files changed, 140 insertions, 57 deletions
diff --git a/src/theory/strings/infer_proof_cons.cpp b/src/theory/strings/infer_proof_cons.cpp
index f48d29416..e9a6da104 100644
--- a/src/theory/strings/infer_proof_cons.cpp
+++ b/src/theory/strings/infer_proof_cons.cpp
@@ -59,6 +59,69 @@ void InferProofCons::notifyFact(const InferInfo& ii)
d_lazyFactMap.insert(ii.d_conc, iic);
}
+bool InferProofCons::addProofTo(CDProof* pf,
+ Node conc,
+ InferenceId infer,
+ bool isRev,
+ const std::vector<Node>& exp)
+{
+ // now go back and convert it to proof steps and add to proof
+ bool useBuffer = false;
+ ProofStep ps;
+ TheoryProofStepBuffer psb(pf->getManager()->getChecker());
+ // run the conversion
+ convert(infer, isRev, conc, exp, ps, psb, useBuffer);
+ // make the proof based on the step or the buffer
+ if (useBuffer)
+ {
+ if (!pf->addSteps(psb))
+ {
+ return false;
+ }
+ }
+ else
+ {
+ if (!pf->addStep(conc, ps))
+ {
+ return false;
+ }
+ }
+ return true;
+}
+
+void InferProofCons::packArgs(Node conc,
+ InferenceId infer,
+ bool isRev,
+ const std::vector<Node>& exp,
+ std::vector<Node>& args)
+{
+ args.push_back(conc);
+ args.push_back(mkInferenceIdNode(infer));
+ args.push_back(NodeManager::currentNM()->mkConst(isRev));
+ // The vector exp is stored as arguments; its flatten form are premises. We
+ // need both since the grouping of exp is important, e.g. { (and a b), c }
+ // is different from { a, b, c } in the convert routine, since positions
+ // of formulas in exp have special meaning.
+ args.insert(args.end(), exp.begin(), exp.end());
+}
+
+bool InferProofCons::unpackArgs(const std::vector<Node>& args,
+ Node& conc,
+ InferenceId& infer,
+ bool& isRev,
+ std::vector<Node>& exp)
+{
+ Assert(args.size() >= 3);
+ conc = args[0];
+ if (!getInferenceId(args[1], infer))
+ {
+ return false;
+ }
+ isRev = args[2].getConst<bool>();
+ exp.insert(exp.end(), args.begin() + 3, args.end());
+ return true;
+}
+
void InferProofCons::convert(InferenceId infer,
bool isRev,
Node conc,
@@ -134,7 +197,7 @@ void InferProofCons::convert(InferenceId infer,
useBuffer = true;
}
}
- if (!useBuffer)
+ else
{
// use the predicate version?
ps.d_args.push_back(conc);
@@ -933,8 +996,6 @@ void InferProofCons::convert(InferenceId infer,
ps.d_args.push_back(t);
// use the trust rule
ps.d_rule = PfRule::THEORY_INFERENCE;
- // add to stats
- d_statistics.d_inferencesNoPf << infer;
}
if (Trace.isOn("strings-ipc-debug"))
{
@@ -1023,8 +1084,6 @@ Node InferProofCons::convertTrans(Node eqa,
std::shared_ptr<ProofNode> InferProofCons::getProofFor(Node fact)
{
- // temporary proof
- CDProof pf(d_pnm);
// get the inference
NodeInferInfoMap::iterator it = d_lazyFactMap.find(fact);
if (it == d_lazyFactMap.end())
@@ -1038,28 +1097,20 @@ std::shared_ptr<ProofNode> InferProofCons::getProofFor(Node fact)
}
}
AlwaysAssert(it != d_lazyFactMap.end());
- // now go back and convert it to proof steps and add to proof
- bool useBuffer = false;
- ProofStep ps;
- TheoryProofStepBuffer psb(d_pnm->getChecker());
std::shared_ptr<InferInfo> ii = (*it).second;
- // run the conversion
- convert(ii->getId(), ii->d_idRev, ii->d_conc, ii->d_premises, ps, psb, useBuffer);
- // make the proof based on the step or the buffer
- if (useBuffer)
- {
- if (!pf.addSteps(psb))
- {
- return nullptr;
- }
- }
- else
+ Assert(ii->d_conc == fact);
+ // make a placeholder proof using STRINGS_INFERENCE, which is reconstructed
+ // during post-process
+ CDProof pf(d_pnm);
+ std::vector<Node> args;
+ packArgs(ii->d_conc, ii->getId(), ii->d_idRev, ii->d_premises, args);
+ // must flatten
+ std::vector<Node> exp;
+ for (const Node& ec : ii->d_premises)
{
- if (!pf.addStep(fact, ps))
- {
- return nullptr;
- }
+ utils::flattenOp(AND, ec, exp);
}
+ pf.addStep(fact, PfRule::STRING_INFERENCE, exp, args);
return pf.getProofFor(fact);
}
@@ -1071,7 +1122,7 @@ std::string InferProofCons::identify() const
bool InferProofCons::purifyCoreSubstitution(Node& tgt,
std::vector<Node>& children,
TheoryProofStepBuffer& psb,
- bool concludeTgtNew) const
+ bool concludeTgtNew)
{
// collect the terms to purify, which are the LHS of the substitution
std::unordered_set<Node> termsToPurify;
@@ -1106,7 +1157,7 @@ Node InferProofCons::purifyCorePredicate(
Node lit,
bool concludeNew,
TheoryProofStepBuffer& psb,
- std::unordered_set<Node>& termsToPurify) const
+ std::unordered_set<Node>& termsToPurify)
{
bool pol = lit.getKind() != NOT;
Node atom = pol ? lit : lit[0];
@@ -1145,8 +1196,8 @@ Node InferProofCons::purifyCorePredicate(
return newLit;
}
-Node InferProofCons::purifyCoreTerm(
- Node n, std::unordered_set<Node>& termsToPurify) const
+Node InferProofCons::purifyCoreTerm(Node n,
+ std::unordered_set<Node>& termsToPurify)
{
Assert(n.getType().isStringLike());
if (n.getNumChildren() == 0)
diff --git a/src/theory/strings/infer_proof_cons.h b/src/theory/strings/infer_proof_cons.h
index 6bc64a085..110d231cf 100644
--- a/src/theory/strings/infer_proof_cons.h
+++ b/src/theory/strings/infer_proof_cons.h
@@ -42,6 +42,10 @@ namespace strings {
*
* The main (private) method of this class is convert below, which is
* called when we need to construct a proof node from an InferInfo.
+ *
+ * This class uses lazy proof reconstruction. Namely, the getProofFor method
+ * returns applications of the rule STRING_INFERENCE, which store the arguments
+ * to the proof conversion routine "convert" below.
*/
class InferProofCons : public ProofGenerator
{
@@ -72,10 +76,40 @@ class InferProofCons : public ProofGenerator
*
* It should be the case that a call was made to notifyFact(ii) where
* ii.d_conc is fact in this SAT context.
+ *
+ * This returns the appropriate application of STRING_INFERENCE so that it
+ * can be reconstructed if necessary during proof post-processing.
*/
std::shared_ptr<ProofNode> getProofFor(Node fact) override;
/** Identify this generator (for debugging, etc..) */
virtual std::string identify() const override;
+ /**
+ * Add proof of running convert on the given arguments to CDProof pf. This is
+ * called lazily during proof post-processing.
+ */
+ static bool addProofTo(CDProof* pf,
+ Node conc,
+ InferenceId infer,
+ bool isRev,
+ const std::vector<Node>& exp);
+ /**
+ * Pack arguments of a STRING_INFERENCE rule application in args. This proof
+ * rule stores the arguments to the convert method of this class below.
+ */
+ static void packArgs(Node conc,
+ InferenceId infer,
+ bool isRev,
+ const std::vector<Node>& exp,
+ std::vector<Node>& args);
+ /**
+ * Inverse of the above method, which recovers the arguments that were packed
+ * into the vector args.
+ */
+ static bool unpackArgs(const std::vector<Node>& args,
+ Node& conc,
+ InferenceId& infer,
+ bool& isRev,
+ std::vector<Node>& exp);
private:
/** convert
@@ -100,26 +134,26 @@ class InferProofCons : public ProofGenerator
* In particular, psb will contain a set of steps that form a proof
* whose conclusion is ii.d_conc and whose free assumptions are ii.d_ant.
*/
- void convert(InferenceId infer,
- bool isRev,
- Node conc,
- const std::vector<Node>& exp,
- ProofStep& ps,
- TheoryProofStepBuffer& psb,
- bool& useBuffer);
+ static void convert(InferenceId infer,
+ bool isRev,
+ Node conc,
+ const std::vector<Node>& exp,
+ ProofStep& ps,
+ TheoryProofStepBuffer& psb,
+ bool& useBuffer);
/**
* Convert length proof. If this method returns true, it adds proof step(s)
* to the buffer psb that conclude lenReq from premises lenExp.
*/
- bool convertLengthPf(Node lenReq,
- const std::vector<Node>& lenExp,
- TheoryProofStepBuffer& psb);
+ static bool convertLengthPf(Node lenReq,
+ const std::vector<Node>& lenExp,
+ TheoryProofStepBuffer& psb);
/**
* Helper method, adds the proof of (TRANS eqa eqb) into the proof step
* buffer psb, where eqa and eqb are flipped as needed. Returns the
* conclusion, or null if we were not able to construct a TRANS step.
*/
- Node convertTrans(Node eqa, Node eqb, TheoryProofStepBuffer& psb);
+ static Node convertTrans(Node eqa, Node eqb, TheoryProofStepBuffer& psb);
/**
* Purify core substitution.
*
@@ -159,10 +193,10 @@ class InferProofCons : public ProofGenerator
* children'[i] from children[i] for all i, and tgt' from tgt (or vice versa
* based on concludeTgtNew).
*/
- bool purifyCoreSubstitution(Node& tgt,
- std::vector<Node>& children,
- TheoryProofStepBuffer& psb,
- bool concludeTgtNew = false) const;
+ static bool purifyCoreSubstitution(Node& tgt,
+ std::vector<Node>& children,
+ TheoryProofStepBuffer& psb,
+ bool concludeTgtNew = false);
/**
* Return the purified form of the predicate lit with respect to a set of
* terms to purify, call the returned literal lit'.
@@ -171,17 +205,17 @@ class InferProofCons : public ProofGenerator
* Note that string predicates that require purification are string
* (dis)equalities only.
*/
- Node purifyCorePredicate(Node lit,
- bool concludeNew,
- TheoryProofStepBuffer& psb,
- std::unordered_set<Node>& termsToPurify) const;
+ static Node purifyCorePredicate(Node lit,
+ bool concludeNew,
+ TheoryProofStepBuffer& psb,
+ std::unordered_set<Node>& termsToPurify);
/**
* Purify term with respect to a set of terms to purify. This replaces
* all terms to purify with their purification variables that occur in
* positions that are relevant for the core calculus of strings (direct
* children of concat or equal).
*/
- Node purifyCoreTerm(Node n, std::unordered_set<Node>& termsToPurify) const;
+ static Node purifyCoreTerm(Node n, std::unordered_set<Node>& termsToPurify);
/** the proof node manager */
ProofNodeManager* d_pnm;
/** The lazy fact map */
diff --git a/src/theory/strings/proof_checker.cpp b/src/theory/strings/proof_checker.cpp
index 5a4008724..f566a4f39 100644
--- a/src/theory/strings/proof_checker.cpp
+++ b/src/theory/strings/proof_checker.cpp
@@ -53,6 +53,8 @@ void StringProofRuleChecker::registerTo(ProofChecker* pc)
pc->registerChecker(PfRule::RE_ELIM, this);
pc->registerChecker(PfRule::STRING_CODE_INJ, this);
pc->registerChecker(PfRule::STRING_SEQ_UNIT_INJ, this);
+ // trusted rule
+ pc->registerTrustedChecker(PfRule::STRING_INFERENCE, this, 2);
}
Node StringProofRuleChecker::checkInternal(PfRule id,
@@ -504,6 +506,11 @@ Node StringProofRuleChecker::checkInternal(PfRule id,
AlwaysAssert(t[0].getType() == t[1].getType());
return t[0].eqNode(t[1]);
}
+ else if (id == PfRule::STRING_INFERENCE)
+ {
+ Assert(args.size() >= 3);
+ return args[0];
+ }
return Node::null();
}
diff --git a/src/theory/strings/sequences_stats.cpp b/src/theory/strings/sequences_stats.cpp
index 2c4834de2..85939d75f 100644
--- a/src/theory/strings/sequences_stats.cpp
+++ b/src/theory/strings/sequences_stats.cpp
@@ -26,8 +26,6 @@ SequencesStatistics::SequencesStatistics()
smtStatisticsRegistry().registerInt("theory::strings::checkRuns")),
d_strategyRuns(
smtStatisticsRegistry().registerInt("theory::strings::strategyRuns")),
- d_inferencesNoPf(smtStatisticsRegistry().registerHistogram<InferenceId>(
- "theory::strings::inferencesNoPf")),
d_cdSimplifications(smtStatisticsRegistry().registerHistogram<Kind>(
"theory::strings::cdSimplifications")),
d_reductions(smtStatisticsRegistry().registerHistogram<Kind>(
diff --git a/src/theory/strings/sequences_stats.h b/src/theory/strings/sequences_stats.h
index 398b8894d..9ec9d3434 100644
--- a/src/theory/strings/sequences_stats.h
+++ b/src/theory/strings/sequences_stats.h
@@ -58,13 +58,6 @@ class SequencesStatistics
IntStat d_strategyRuns;
//--------------- inferences
/**
- * Counts the number of applications of each type of inference that were not
- * processed as a proof step. This is a subset of the statistics in
- * TheoryInferenceManager, i.e.
- * (theory::strings::inferences{Facts,Lemmas,Conflicts}).
- */
- HistogramStat<InferenceId> d_inferencesNoPf;
- /**
* Counts the number of applications of each type of context-dependent
* simplification. The sum of this map is equal to the number of EXTF or
* EXTF_N inferences.
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback