From fe655f21e7cea33e9057c46fc8b2573314cbf302 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 23 Aug 2021 19:00:16 -0500 Subject: [PATCH] Miscellaneous changes from proof-new (#7042) --- src/printer/smt2/smt2_printer.cpp | 5 +++++ src/proof/print_expr.h | 10 +++++----- src/proof/proof_checker.cpp | 4 ++-- src/proof/proof_checker.h | 8 ++++---- src/proof/proof_rule.cpp | 1 + src/proof/trust_node.cpp | 6 ++++++ src/proof/trust_node.h | 3 +++ src/smt/preprocess_proof_generator.cpp | 11 ++++++++--- 8 files changed, 34 insertions(+), 14 deletions(-) diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 04d8c34c4..ba03a4fe8 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -686,6 +686,11 @@ void Smt2Printer::toStream(std::ostream& out, out << ' '; stillNeedToPrintParams = false; break; + case kind::BITVECTOR_BITOF: + out << "(_ bitOf " << n.getOperator().getConst().d_bitIndex + << ") "; + stillNeedToPrintParams = false; + break; // sets case kind::SINGLETON: diff --git a/src/proof/print_expr.h b/src/proof/print_expr.h index 15a8bb6c2..409b95e49 100644 --- a/src/proof/print_expr.h +++ b/src/proof/print_expr.h @@ -27,7 +27,7 @@ namespace cvc5 { namespace proof { -/** +/** * A term, type or a proof. This class is used for printing combinations of * proofs terms and types. */ @@ -54,10 +54,10 @@ class PExpr class PExprStream { public: - /** - * Takes a reference to a stream (vector of p-expressions), and the - * representation true/false (tt/ff). - */ + /** + * Takes a reference to a stream (vector of p-expressions), and the + * representation true/false (tt/ff). + */ PExprStream(std::vector& stream, Node tt = Node::null(), Node ff = Node::null()); diff --git a/src/proof/proof_checker.cpp b/src/proof/proof_checker.cpp index 6a9979f75..1d5aa61b4 100644 --- a/src/proof/proof_checker.cpp +++ b/src/proof/proof_checker.cpp @@ -85,7 +85,7 @@ ProofCheckerStatistics::ProofCheckerStatistics() { } -ProofChecker::ProofChecker(uint32_t pclevel, theory::RewriteDb* rdb) +ProofChecker::ProofChecker(uint32_t pclevel, rewriter::RewriteDb* rdb) : d_pclevel(pclevel), d_rdb(rdb) { } @@ -308,7 +308,7 @@ ProofRuleChecker* ProofChecker::getCheckerFor(PfRule id) return it->second; } -theory::RewriteDb* ProofChecker::getRewriteDatabase() { return d_rdb; } +rewriter::RewriteDb* ProofChecker::getRewriteDatabase() { return d_rdb; } uint32_t ProofChecker::getPedanticLevel(PfRule id) const { diff --git a/src/proof/proof_checker.h b/src/proof/proof_checker.h index f1f10eedb..6092a1932 100644 --- a/src/proof/proof_checker.h +++ b/src/proof/proof_checker.h @@ -29,7 +29,7 @@ namespace cvc5 { class ProofChecker; class ProofNode; -namespace theory { +namespace rewriter { class RewriteDb; } @@ -105,7 +105,7 @@ class ProofCheckerStatistics class ProofChecker { public: - ProofChecker(uint32_t pclevel = 0, theory::RewriteDb* rdb = nullptr); + ProofChecker(uint32_t pclevel = 0, rewriter::RewriteDb* rdb = nullptr); ~ProofChecker() {} /** * Return the formula that is proven by proof node pn, or null if pn is not @@ -167,7 +167,7 @@ class ProofChecker /** get checker for */ ProofRuleChecker* getCheckerFor(PfRule id); /** get the rewrite database */ - theory::RewriteDb* getRewriteDatabase(); + rewriter::RewriteDb* getRewriteDatabase(); /** * Get the pedantic level for id if it has been assigned a pedantic * level via registerTrustedChecker above, or zero otherwise. @@ -192,7 +192,7 @@ class ProofChecker /** The pedantic level of this checker */ uint32_t d_pclevel; /** Pointer to the rewrite database */ - theory::RewriteDb* d_rdb; + rewriter::RewriteDb* d_rdb; /** * Check internal. This is used by check and checkDebug above. It writes * checking errors on out when enableOutput is true. We treat trusted checkers diff --git a/src/proof/proof_rule.cpp b/src/proof/proof_rule.cpp index 7e1cdf8d3..008b0dc6f 100644 --- a/src/proof/proof_rule.cpp +++ b/src/proof/proof_rule.cpp @@ -48,6 +48,7 @@ const char* toString(PfRule id) case PfRule::TRUST_SUBS_MAP: return "TRUST_SUBS_MAP"; case PfRule::TRUST_SUBS_EQ: return "TRUST_SUBS_EQ"; case PfRule::THEORY_INFERENCE: return "THEORY_INFERENCE"; + case PfRule::SAT_REFUTATION: return "SAT_REFUTATION"; //================================================= Boolean rules case PfRule::RESOLUTION: return "RESOLUTION"; case PfRule::CHAIN_RESOLUTION: return "CHAIN_RESOLUTION"; diff --git a/src/proof/trust_node.cpp b/src/proof/trust_node.cpp index 6c5de13c7..ce9917584 100644 --- a/src/proof/trust_node.cpp +++ b/src/proof/trust_node.cpp @@ -68,6 +68,12 @@ TrustNode TrustNode::mkTrustRewrite(TNode n, Node nr, ProofGenerator* g) return TrustNode(TrustNodeKind::REWRITE, rkey, g); } +TrustNode TrustNode::mkReplaceGenTrustNode(const TrustNode& orig, + ProofGenerator* g) +{ + return TrustNode(orig.getKind(), orig.getProven(), g); +} + TrustNode TrustNode::null() { return TrustNode(TrustNodeKind::INVALID, Node::null()); diff --git a/src/proof/trust_node.h b/src/proof/trust_node.h index 8971df1d1..ae3e81d78 100644 --- a/src/proof/trust_node.h +++ b/src/proof/trust_node.h @@ -92,6 +92,9 @@ class TrustNode static TrustNode mkTrustRewrite(TNode n, Node nr, ProofGenerator* g = nullptr); + /** Make a trust node, replacing the original generator */ + static TrustNode mkReplaceGenTrustNode(const TrustNode& orig, + ProofGenerator* g); /** The null proven node */ static TrustNode null(); ~TrustNode() {} diff --git a/src/smt/preprocess_proof_generator.cpp b/src/smt/preprocess_proof_generator.cpp index 5511800a1..1eea6286b 100644 --- a/src/smt/preprocess_proof_generator.cpp +++ b/src/smt/preprocess_proof_generator.cpp @@ -19,9 +19,11 @@ #include #include "options/proof_options.h" +#include "proof/method_id.h" #include "proof/proof.h" #include "proof/proof_checker.h" #include "proof/proof_node.h" +#include "theory/quantifiers/extended_rewrite.h" #include "theory/rewriter.h" namespace cvc5 { @@ -177,11 +179,14 @@ std::shared_ptr PreprocessProofGenerator::getProofFor(Node f) Assert(proven.getKind() == kind::EQUAL); if (!proofStepProcessed) { - // maybe its just a simple rewrite? - if (proven[1] == theory::Rewriter::rewrite(proven[0])) + // maybe its just an (extended) rewrite? + theory::quantifiers::ExtendedRewriter extr(true); + Node pr = extr.extendedRewrite(proven[0]); + if (proven[1] == pr) { + Node idr = mkMethodId(MethodId::RW_EXT_REWRITE); Trace("smt-pppg-debug") << "...add simple rewrite" << std::endl; - cdp.addStep(proven, PfRule::REWRITE, {}, {proven[0]}); + cdp.addStep(proven, PfRule::REWRITE, {}, {proven[0], idr}); proofStepProcessed = true; } } -- 2.30.2