Miscellaneous changes from proof-new (#7042)

diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 04d8c34c40bc294adbfd1cbb4cf65ed3ae17f0e9..ba03a4fe8bd1751c13e521fa56d60f78b6930c01 100644 (file)
--- 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<BitVectorBitOf>().d_bitIndex
+        << ") ";
+    stillNeedToPrintParams = false;
+    break;
 
   // sets
   case kind::SINGLETON:

diff --git a/src/proof/print_expr.h b/src/proof/print_expr.h
index 15a8bb6c298c8ad0aa8e1b7167b6777f6da2208f..409b95e490c0bc3a931facbf20fbd16d66ed62db 100644 (file)
--- 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<PExpr>& stream,
               Node tt = Node::null(),
               Node ff = Node::null());

diff --git a/src/proof/proof_checker.cpp b/src/proof/proof_checker.cpp
index 6a9979f750f6e7e0c1fdf5bb03859b9387a51bac..1d5aa61b4fb19a47bb2a687bd4346b2cf5193bfe 100644 (file)
--- 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 f1f10eedb96a8951bbe6cfc044811af698bd9159..6092a193272427ccdfedf5ac59946249125b01d5 100644 (file)
--- 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 7e1cdf8d34b1436846d54738d74ecfd3e49614e8..008b0dc6f45f40dd6275ff60b19ebd789f36a33b 100644 (file)
--- 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 6c5de13c7e09655cd0187d2313ea7eb0f41a1383..ce991758418e5922afb3b9682fbe3dfb01147f29 100644 (file)
--- 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 8971df1d1bb49327836a6c86c40dd1e32e4d9233..ae3e81d7893a8789cf323cb7b942b120af3930eb 100644 (file)
--- 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 5511800a13340cba87c34468229145ccf656d3e0..1eea6286b2606666efb8810d2adfe737b57b9100 100644 (file)
--- a/src/smt/preprocess_proof_generator.cpp
+++ b/src/smt/preprocess_proof_generator.cpp
@@ -19,9 +19,11 @@
 #include <sstream>
 
 #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<ProofNode> 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;
           }
         }