diff options
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/strings/infer_proof_cons.cpp | 107 | ||||
-rw-r--r-- | src/theory/strings/infer_proof_cons.h | 74 | ||||
-rw-r--r-- | src/theory/strings/proof_checker.cpp | 7 | ||||
-rw-r--r-- | src/theory/strings/sequences_stats.cpp | 2 | ||||
-rw-r--r-- | src/theory/strings/sequences_stats.h | 7 |
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. |