src/theory/theory_rewriter.cpp

   1 /******************************************************************************
   2  * Top contributors (to current version):
   3  *   Andrew Reynolds
   4  *
   5  * This file is part of the cvc5 project.
   6  *
   7  * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
   8  * in the top-level source directory and their institutional affiliations.
   9  * All rights reserved.  See the file COPYING in the top-level source
  10  * directory for licensing information.
  11  * ****************************************************************************
  12  *
  13  * The TheoryRewriter class.
  14  *
  15  * The interface that theory rewriters implement.
  16  */
  17
  18 #include "theory/theory_rewriter.h"
  19
  20 namespace cvc5 {
  21 namespace theory {
  22
  23 TrustRewriteResponse::TrustRewriteResponse(RewriteStatus status,
  24                                            Node n,
  25                                            Node nr,
  26                                            ProofGenerator* pg)
  27     : d_status(status)
  28 {
  29   // we always make non-null, regardless of whether n = nr
  30   d_node = TrustNode::mkTrustRewrite(n, nr, pg);
  31 }
  32
  33 TrustRewriteResponse TheoryRewriter::postRewriteWithProof(TNode node)
  34 {
  35   RewriteResponse response = postRewrite(node);
  36   // by default, we return a trust rewrite response with no proof generator
  37   return TrustRewriteResponse(
  38       response.d_status, node, response.d_node, nullptr);
  39 }
  40
  41 TrustRewriteResponse TheoryRewriter::preRewriteWithProof(TNode node)
  42 {
  43   RewriteResponse response = preRewrite(node);
  44   // by default, we return a trust rewrite response with no proof generator
  45   return TrustRewriteResponse(
  46       response.d_status, node, response.d_node, nullptr);
  47 }
  48
  49 Node TheoryRewriter::rewriteEqualityExt(Node node) { return node; }
  50
  51 TrustNode TheoryRewriter::rewriteEqualityExtWithProof(Node node)
  52 {
  53   Node nodeRew = rewriteEqualityExt(node);
  54   if (nodeRew != node)
  55   {
  56     // by default, we return a trust rewrite response with no proof generator
  57     return TrustNode::mkTrustRewrite(node, nodeRew, nullptr);
  58   }
  59   // no rewrite
  60   return TrustNode::null();
  61 }
  62
  63 TrustNode TheoryRewriter::expandDefinition(Node node)
  64 {
  65   // no expansion
  66   return TrustNode::null();
  67 }
  68
  69 }  // namespace theory
  70 }  // namespace cvc5