diff options
| -rw-r--r-- | src/expr/proof_node_manager.cpp | 19 | ||||
| -rw-r--r-- | src/expr/proof_node_manager.h | 3 |
2 files changed, 20 insertions, 2 deletions
diff --git a/src/expr/proof_node_manager.cpp b/src/expr/proof_node_manager.cpp index 54315ee05..66a8197d8 100644 --- a/src/expr/proof_node_manager.cpp +++ b/src/expr/proof_node_manager.cpp @@ -22,7 +22,11 @@ using namespace CVC4::kind; namespace CVC4 { -ProofNodeManager::ProofNodeManager(ProofChecker* pc) : d_checker(pc) {} +ProofNodeManager::ProofNodeManager(ProofChecker* pc) + : d_checker(pc) +{ + d_true = NodeManager::currentNM()->mkConst(true); +} std::shared_ptr<ProofNode> ProofNodeManager::mkNode( PfRule id, @@ -88,6 +92,19 @@ std::shared_ptr<ProofNode> ProofNodeManager::mkScope( acu.insert(a); continue; } + // trivial assumption + if (a == d_true) + { + Trace("pnm-scope") << "- justify trivial True assumption\n"; + for (std::shared_ptr<ProofNode> pfs : fa.second) + { + Assert(pfs->getResult() == a); + updateNode(pfs.get(), PfRule::MACRO_SR_PRED_INTRO, {}, {a}); + } + Trace("pnm-scope") << "...finished" << std::endl; + acu.insert(a); + continue; + } Trace("pnm-scope") << "- try matching free assumption " << a << "\n"; // otherwise it may be due to symmetry? Node aeqSym = CDProof::getSymmFact(a); diff --git a/src/expr/proof_node_manager.h b/src/expr/proof_node_manager.h index 774177d66..799a50f2e 100644 --- a/src/expr/proof_node_manager.h +++ b/src/expr/proof_node_manager.h @@ -118,7 +118,6 @@ class ProofNodeManager bool ensureClosed = true, bool doMinimize = false, Node expected = Node::null()); - /** * This method updates pn to be a proof of the form <id>( children, args ), * while maintaining its d_proven field. This method returns false if this @@ -150,6 +149,8 @@ class ProofNodeManager private: /** The (optional) proof checker */ ProofChecker* d_checker; + /** the true node */ + Node d_true; /** Check internal * * This returns the result of proof checking a ProofNode with the provided |