Miscellaneous changes from proof-new (#7042)

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<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 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<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 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 <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;
           }
         }