summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/expr/proof.cpp7
-rw-r--r--src/expr/proof.h6
-rw-r--r--src/theory/builtin/proof_checker.cpp2
-rw-r--r--src/theory/strings/infer_proof_cons.cpp13
-rw-r--r--src/theory/strings/infer_proof_cons.h2
-rw-r--r--src/theory/theory_engine.cpp37
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();
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback