GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/theory_rewriter.cpp Lines: 18 20 90.0 %
Date: 2021-08-11 Branches: 23 48 47.9 %

Line Exec Source
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
819865
TrustRewriteResponse::TrustRewriteResponse(RewriteStatus status,
24
                                           Node n,
25
                                           Node nr,
26
819865
                                           ProofGenerator* pg)
27
819865
    : d_status(status)
28
{
29
  // we always make non-null, regardless of whether n = nr
30
819865
  d_node = TrustNode::mkTrustRewrite(n, nr, pg);
31
819865
}
32
33
346415
TrustRewriteResponse TheoryRewriter::postRewriteWithProof(TNode node)
34
{
35
692830
  RewriteResponse response = postRewrite(node);
36
  // by default, we return a trust rewrite response with no proof generator
37
  return TrustRewriteResponse(
38
692830
      response.d_status, node, response.d_node, nullptr);
39
}
40
41
473450
TrustRewriteResponse TheoryRewriter::preRewriteWithProof(TNode node)
42
{
43
946900
  RewriteResponse response = preRewrite(node);
44
  // by default, we return a trust rewrite response with no proof generator
45
  return TrustRewriteResponse(
46
946900
      response.d_status, node, response.d_node, nullptr);
47
}
48
49
Node TheoryRewriter::rewriteEqualityExt(Node node) { return node; }
50
51
29
TrustNode TheoryRewriter::rewriteEqualityExtWithProof(Node node)
52
{
53
58
  Node nodeRew = rewriteEqualityExt(node);
54
29
  if (nodeRew != node)
55
  {
56
    // by default, we return a trust rewrite response with no proof generator
57
29
    return TrustNode::mkTrustRewrite(node, nodeRew, nullptr);
58
  }
59
  // no rewrite
60
  return TrustNode::null();
61
}
62
63
7932
TrustNode TheoryRewriter::expandDefinition(Node node)
64
{
65
  // no expansion
66
7932
  return TrustNode::null();
67
}
68
69
}  // namespace theory
70
29337
}  // namespace cvc5