Move first order model for full model check to own file (#5918)

[cvc5.git] / src / theory / rewriter.h

diff --git a/src/theory/rewriter.h b/src/theory/rewriter.h
index f7298e1fb00a99e3d9dfe7fb3daffefaa6e23e77..572662483d19aa38280070961802ff31fa1fb181 100644 (file)
--- a/src/theory/rewriter.h
+++ b/src/theory/rewriter.h
@@ -2,10 +2,10 @@
 /*! \file rewriter.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Morgan Deters, Dejan Jovanovic, Tim King
+ **   Andres Noetzli, Andrew Reynolds, Dejan Jovanovic
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** in the top-level source directory and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **
@@ -19,12 +19,18 @@
 #pragma once
 
 #include "expr/node.h"
+#include "expr/term_conversion_proof_generator.h"
 #include "theory/theory_rewriter.h"
+#include "theory/trust_node.h"
 #include "util/unsafe_interrupt_exception.h"
 
 namespace CVC4 {
 namespace theory {
 
+namespace builtin {
+class BuiltinProofRuleChecker;
+}
+
 class RewriterInitializer;
 
 /**
@@ -48,6 +54,8 @@ RewriteResponse identityRewrite(RewriteEnvironment* re, TNode n);
  * The main rewriter class.
  */
 class Rewriter {
+  friend builtin::BuiltinProofRuleChecker;
+
  public:
   Rewriter();
 
@@ -57,11 +65,50 @@ class Rewriter {
    */
   static Node rewrite(TNode node);
 
+  /**
+   * Rewrites the equality node using theoryOf() to determine which rewriter to
+   * use on the node corresponding to an equality s = t.
+   *
+   * Specifically, this method performs rewrites whose conclusion is not
+   * necessarily one of { s = t, t = s, true, false }, which is an invariant
+   * guaranted by the above method. This invariant is motivated by theory
+   * combination, which needs to guarantee that equalities between terms
+   * can be communicated for all pairs of terms.
+   */
+  static Node rewriteEqualityExt(TNode node);
+
+  /**
+   * Rewrite with proof production, which is managed by the term conversion
+   * proof generator managed by this class (d_tpg). This method requires a call
+   * to setProofNodeManager prior to this call.
+   *
+   * @param node The node to rewrite.
+   * @param isExtEq Whether node is an equality which we are applying
+   * rewriteEqualityExt on.
+   * @return The trust node of kind TrustNodeKind::REWRITE that contains the
+   * rewritten form of node.
+   */
+  TrustNode rewriteWithProof(TNode node,
+                             bool isExtEq = false);
+
+  /** Set proof node manager */
+  void setProofNodeManager(ProofNodeManager* pnm);
+
   /**
    * Garbage collects the rewrite caches.
    */
   static void clearCaches();
 
+  /**
+   * Registers a theory rewriter with this rewriter. The rewriter does not own
+   * the theory rewriters.
+   *
+   * @param tid The theory that the theory rewriter should be associated with.
+   * @param trew The theory rewriter to register.
+   */
+  static void registerTheoryRewriter(theory::TheoryId tid,
+                                     TheoryRewriter* trew);
+
   /**
    * Register a prerewrite for a given kind.
    *
@@ -102,11 +149,12 @@ class Rewriter {
 
  private:
   /**
-   * Get the (singleton) instance of the rewriter.
+   * Get the rewriter associated with the SmtEngine in scope.
    *
-   * TODO(#3468): Get rid of this singleton
+   * TODO(#3468): Get rid of this function (it relies on there being an
+   * singleton with the current SmtEngine in scope)
    */
-  static Rewriter& getInstance();
+  static Rewriter* getInstance();
 
   /** Returns the appropriate cache for a node */
   Node getPreRewriteCache(theory::TheoryId theoryId, TNode node);
@@ -123,13 +171,25 @@ class Rewriter {
   /**
    * Rewrites the node using the given theory rewriter.
    */
-  Node rewriteTo(theory::TheoryId theoryId, Node node);
+  Node rewriteTo(theory::TheoryId theoryId,
+                 Node node,
+                 TConvProofGenerator* tcpg = nullptr);
 
   /** Calls the pre-rewriter for the given theory */
-  RewriteResponse preRewrite(theory::TheoryId theoryId, TNode n);
+  RewriteResponse preRewrite(theory::TheoryId theoryId,
+                             TNode n,
+                             TConvProofGenerator* tcpg = nullptr);
 
   /** Calls the post-rewriter for the given theory */
-  RewriteResponse postRewrite(theory::TheoryId theoryId, TNode n);
+  RewriteResponse postRewrite(theory::TheoryId theoryId,
+                              TNode n,
+                              TConvProofGenerator* tcpg = nullptr);
+  /** processes a trust rewrite response */
+  RewriteResponse processTrustRewriteResponse(
+      theory::TheoryId theoryId,
+      const TrustRewriteResponse& tresponse,
+      bool isPre,
+      TConvProofGenerator* tcpg);
 
   /**
    * Calls the equality-rewriter for the given theory.
@@ -138,10 +198,8 @@ class Rewriter {
 
   void clearCachesInternal();
 
-  /** Theory rewriters managed by this rewriter instance */
-  std::unique_ptr<TheoryRewriter> d_theoryRewriters[theory::THEORY_LAST];
-
-  unsigned long d_iterationCount = 0;
+  /** Theory rewriters used by this rewriter instance */
+  TheoryRewriter* d_theoryRewriters[theory::THEORY_LAST];
 
   /** Rewriter table for prewrites. Maps kinds to rewriter function. */
   std::function<RewriteResponse(RewriteEnvironment*, TNode)>
@@ -164,6 +222,8 @@ class Rewriter {
 
   RewriteEnvironment d_re;
 
+  /** The proof generator */
+  std::unique_ptr<TConvProofGenerator> d_tpg;
 #ifdef CVC4_ASSERTIONS
   std::unique_ptr<std::unordered_set<Node, NodeHashFunction>> d_rewriteStack =
       nullptr;