Head

GCC Code Coverage Report

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


/******************************************************************************
 * Top contributors (to current version):
 *   Andrew Reynolds
 *
 * This file is part of the cvc5 project.
 *
 * Copyright (c) 2009-2021 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.
 * ****************************************************************************
 *
 * The TheoryRewriter class.
 *
 * The interface that theory rewriters implement.
 */

#include "theory/theory_rewriter.h"

namespace cvc5 {
namespace theory {

TrustRewriteResponse::TrustRewriteResponse(RewriteStatus status,
                                           Node n,
                                           Node nr,
                                           ProofGenerator* pg)
    : d_status(status)
{
  // we always make non-null, regardless of whether n = nr
  d_node = TrustNode::mkTrustRewrite(n, nr, pg);
}

TrustRewriteResponse TheoryRewriter::postRewriteWithProof(TNode node)
{
  RewriteResponse response = postRewrite(node);
  // by default, we return a trust rewrite response with no proof generator
  return TrustRewriteResponse(
      response.d_status, node, response.d_node, nullptr);
}

TrustRewriteResponse TheoryRewriter::preRewriteWithProof(TNode node)
{
  RewriteResponse response = preRewrite(node);
  // by default, we return a trust rewrite response with no proof generator
  return TrustRewriteResponse(
      response.d_status, node, response.d_node, nullptr);
}

Node TheoryRewriter::rewriteEqualityExt(Node node) { return node; }

TrustNode TheoryRewriter::rewriteEqualityExtWithProof(Node node)
{
  Node nodeRew = rewriteEqualityExt(node);
  if (nodeRew != node)
  {
    // by default, we return a trust rewrite response with no proof generator
    return TrustNode::mkTrustRewrite(node, nodeRew, nullptr);
  }
  // no rewrite
  return TrustNode::null();
}

TrustNode TheoryRewriter::expandDefinition(Node node)
{
  // no expansion
  return TrustNode::null();
}

}  // namespace theory
}  // namespace cvc5


Generated by: GCOVR (Version 3.2)

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	29340	} // namespace cvc5