diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2020-05-18 11:15:55 -0500 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2020-05-18 11:15:55 -0500 |
commit | 1ee18ab1b0e6648fdd614742c841128079e6ec27 (patch) | |
tree | 41acf592ea277f23a3f790d4fd78149e13f8be56 | |
parent | 30bc3db1f7dee1f89baea8706e5966cb13b8948c (diff) |
More
-rw-r--r-- | src/expr/proof.cpp | 7 | ||||
-rw-r--r-- | src/expr/proof.h | 6 | ||||
-rw-r--r-- | src/theory/builtin/proof_checker.cpp | 2 | ||||
-rw-r--r-- | src/theory/strings/infer_proof_cons.cpp | 13 | ||||
-rw-r--r-- | src/theory/strings/infer_proof_cons.h | 2 | ||||
-rw-r--r-- | src/theory/theory_engine.cpp | 37 |
6 files changed, 39 insertions, 28 deletions
diff --git a/src/expr/proof.cpp b/src/expr/proof.cpp index 8ec55d1f5..dda2ccd2d 100644 --- a/src/expr/proof.cpp +++ b/src/expr/proof.cpp @@ -381,4 +381,11 @@ bool CDProof::isAssumption(ProofNode* pn) return false; } +bool CDProof::isSame(TNode f, TNode g) +{ + return f == g + || (f.getKind() == EQUAL && g.getKind() == EQUAL + && f[0] == g[1] && f[1] == g[0]); +} + } // namespace CVC4 diff --git a/src/expr/proof.h b/src/expr/proof.h index e5b2775d9..20bbb4996 100644 --- a/src/expr/proof.h +++ b/src/expr/proof.h @@ -206,6 +206,12 @@ class CDProof /** Get the proof manager for this proof */ ProofNodeManager* getManager() const; + /** + * Is same? Returns true if f and g are the same formula, or if they are + * symmetric equalities. If two nodes f and g are the same, then a proof for + * f suffices as a proof for g according to this class. + */ + static bool isSame(TNode f, TNode g); protected: typedef context::CDHashMap<Node, std::shared_ptr<ProofNode>, NodeHashFunction> NodeProofNodeMap; diff --git a/src/theory/builtin/proof_checker.cpp b/src/theory/builtin/proof_checker.cpp index b05dbf7e7..8c47bc060 100644 --- a/src/theory/builtin/proof_checker.cpp +++ b/src/theory/builtin/proof_checker.cpp @@ -369,7 +369,7 @@ bool BuiltinProofRuleChecker::getMethodIds(const std::vector<Node>& args, return false; } } - if (args.size() >= index + 1) + if (args.size() > index + 1) { if (!getMethodId(args[index + 1], idr)) { diff --git a/src/theory/strings/infer_proof_cons.cpp b/src/theory/strings/infer_proof_cons.cpp index 281b1abff..49a697592 100644 --- a/src/theory/strings/infer_proof_cons.cpp +++ b/src/theory/strings/infer_proof_cons.cpp @@ -261,7 +261,7 @@ Node InferProofCons::convert(Inference infer, ps.d_children.begin() + mainEqIndex); Node mainEqSRew = d_psb.tryStep(PfRule::MACRO_SR_PRED_ELIM, childrenSRew, emptyVec); - if (isSymm(mainEqSRew, mainEq)) + if (CDProof::isSame(mainEqSRew, mainEq)) { Trace("strings-ipc-core") << "...undo step" << std::endl; // not necessary @@ -909,7 +909,7 @@ bool InferProofCons::convertPredTransform(Node src, MethodId idr) { // symmetric equalities - if (isSymm(src, tgt)) + if (CDProof::isSame(src, tgt)) { return true; } @@ -962,7 +962,7 @@ Node InferProofCons::convertPredElim(Node src, std::vector<Node> args; addMethodIds(args, ids, idr); Node srcRew = d_psb.tryStep(PfRule::MACRO_SR_PRED_ELIM, children, args); - if (isSymm(src, srcRew)) + if (CDProof::isSame(src, srcRew)) { d_psb.popStep(); return src; @@ -1010,13 +1010,6 @@ Node InferProofCons::convertTrans(Node eqa, Node eqb) return Node::null(); } -bool InferProofCons::isSymm(Node src, Node tgt) -{ - return src == tgt - || (src.getKind() == EQUAL && tgt.getKind() == EQUAL - && src[0] == tgt[1] && src[1] == tgt[0]); -} - ProofStepBuffer* InferProofCons::getBuffer() { return &d_psb; } std::shared_ptr<ProofNode> InferProofCons::getProofFor(Node fact) diff --git a/src/theory/strings/infer_proof_cons.h b/src/theory/strings/infer_proof_cons.h index ed38fdb96..18f2d0b61 100644 --- a/src/theory/strings/infer_proof_cons.h +++ b/src/theory/strings/infer_proof_cons.h @@ -145,8 +145,6 @@ class InferProofCons : public ProofGenerator /** */ Node convertTrans(Node eqa, Node eqb); - /** Is symm */ - static bool isSymm(Node src, Node tgt); /** the proof node manager */ ProofNodeManager* d_pnm; /** The lazy fact map */ diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 3b1c5bfaa..965cd4e72 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -2013,7 +2013,7 @@ theory::TrustNode TheoryEngine::getExplanation( if (d_lazyProof != nullptr) { // FIXME - // lcp.reset(new LazyCDProof(d_pNodeManager.get())); + //lcp.reset(new LazyCDProof(d_pNodeManager.get())); } unsigned i = 0; // Index of the current literal we are processing unsigned j = 0; // Index of the last literal we are keeping @@ -2061,6 +2061,7 @@ theory::TrustNode TheoryEngine::getExplanation( { Debug("theory::explain") << "\tLiteral came from THEORY_SAT_SOLVER. Kepping it." << endl; explanationVector[j++] = explanationVector[i++]; + // it will be a free assumption in the proof continue; } @@ -2080,7 +2081,7 @@ theory::TrustNode TheoryEngine::getExplanation( if (lcp != nullptr) { // toExplain.d_node[0] ... toExplain.d_node[n] - // --------------------------------------------MACRO_BSR_PRED_INTRO + // --------------------------------------------MACRO_SR_PRED_INTRO // toExplain.d_node std::vector<Node> children; for (size_t k = 0; k < nchild; ++k) @@ -2089,6 +2090,7 @@ theory::TrustNode TheoryEngine::getExplanation( } std::vector<Node> args; args.push_back(toExplain.d_node); + args.push_back(mkMethodId(MethodId::SB_PREDICATE)); lcp->addStep( toExplain.d_node, PfRule::MACRO_SR_PRED_INTRO, children, args); } @@ -2150,19 +2152,24 @@ theory::TrustNode TheoryEngine::getExplanation( } if (lcp != nullptr) { - // ----------- Via theory - // exp => lit exp - // ---------------------------------MACRO_BSR_PRED_TRANSFORM - // lit - Node proven = texplanation.getProven(); - lcp->addLazyStep(proven, texplanation.getGenerator()); - std::vector<Node> children; - children.push_back(proven); - children.push_back(texplanation.getNode()); - std::vector<Node> args; - args.push_back(toExplain.d_node); - lcp->addStep( - toExplain.d_node, PfRule::MACRO_SR_PRED_TRANSFORM, children, args); + // if not a trivial explanation + if (!CDProof::isSame(texplanation.getNode(), toExplain.d_node)) + { + // ----------- Via theory + // exp => lit exp + // ---------------------------------MACRO_SR_PRED_TRANSFORM + // lit + Node proven = texplanation.getProven(); + lcp->addLazyStep(proven, texplanation.getGenerator()); + std::vector<Node> children; + children.push_back(proven); + children.push_back(texplanation.getNode()); + std::vector<Node> args; + args.push_back(toExplain.d_node); + args.push_back(mkMethodId(MethodId::SB_PREDICATE)); + lcp->addStep( + toExplain.d_node, PfRule::MACRO_SR_PRED_TRANSFORM, children, args); + } } Node explanation = texplanation.getNode(); |