GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/theory_rewriter.cpp Lines: 16 18 88.9 %
Date: 2021-03-22 Branches: 23 50 46.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file theory_rewriter.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds
6
 ** This file is part of the CVC4 project.
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.\endverbatim
11
 **
12
 ** \brief The TheoryRewriter class
13
 **
14
 ** The TheoryRewriter class is the interface that theory rewriters implement.
15
 **/
16
17
#include "theory/theory_rewriter.h"
18
19
namespace CVC4 {
20
namespace theory {
21
22
694350
TrustRewriteResponse::TrustRewriteResponse(RewriteStatus status,
23
                                           Node n,
24
                                           Node nr,
25
694350
                                           ProofGenerator* pg)
26
694350
    : d_status(status)
27
{
28
  // we always make non-null, regardless of whether n = nr
29
694350
  d_node = TrustNode::mkTrustRewrite(n, nr, pg);
30
694350
}
31
32
294900
TrustRewriteResponse TheoryRewriter::postRewriteWithProof(TNode node)
33
{
34
589800
  RewriteResponse response = postRewrite(node);
35
  // by default, we return a trust rewrite response with no proof generator
36
  return TrustRewriteResponse(
37
589800
      response.d_status, node, response.d_node, nullptr);
38
}
39
40
399450
TrustRewriteResponse TheoryRewriter::preRewriteWithProof(TNode node)
41
{
42
798900
  RewriteResponse response = preRewrite(node);
43
  // by default, we return a trust rewrite response with no proof generator
44
  return TrustRewriteResponse(
45
798900
      response.d_status, node, response.d_node, nullptr);
46
}
47
48
Node TheoryRewriter::rewriteEqualityExt(Node node) { return node; }
49
50
6
TrustNode TheoryRewriter::rewriteEqualityExtWithProof(Node node)
51
{
52
12
  Node nodeRew = rewriteEqualityExt(node);
53
6
  if (nodeRew != node)
54
  {
55
    // by default, we return a trust rewrite response with no proof generator
56
6
    return TrustNode::mkTrustRewrite(node, nodeRew, nullptr);
57
  }
58
  // no rewrite
59
  return TrustNode::null();
60
}
61
62
}  // namespace theory
63
26676
}  // namespace CVC4