GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/builtin/theory_builtin_rewriter.h Lines: 2 2 100.0 %
Date: 2021-03-22 Branches: 1 2 50.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file theory_builtin_rewriter.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Andres Noetzli, Mathias Preiner
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 [[ Add one-line brief description here ]]
13
 **
14
 ** [[ Add lengthier description here ]]
15
 ** \todo document this file
16
 **/
17
18
#include "cvc4_private.h"
19
20
#ifndef CVC4__THEORY__BUILTIN__THEORY_BUILTIN_REWRITER_H
21
#define CVC4__THEORY__BUILTIN__THEORY_BUILTIN_REWRITER_H
22
23
#include "theory/theory_rewriter.h"
24
25
namespace CVC4 {
26
namespace theory {
27
namespace builtin {
28
29
17987
class TheoryBuiltinRewriter : public TheoryRewriter
30
{
31
  static Node blastDistinct(TNode node);
32
33
 public:
34
35
  RewriteResponse postRewrite(TNode node) override;
36
37
389416
  RewriteResponse preRewrite(TNode node) override { return doRewrite(node); }
38
39
  // conversions between lambdas and arrays
40
 private:
41
  /** recursive helper for getLambdaForArrayRepresentation */
42
  static Node getLambdaForArrayRepresentationRec( TNode a, TNode bvl, unsigned bvlIndex,
43
                                                  std::unordered_map< TNode, Node, TNodeHashFunction >& visited );
44
  /** recursive helper for getArrayRepresentationForLambda */
45
  static Node getArrayRepresentationForLambdaRec(TNode n, TypeNode retType);
46
47
 public:
48
  /**
49
   * The default rewriter for rewrites that occur at both pre and post rewrite.
50
   */
51
  static RewriteResponse doRewrite(TNode node);
52
  /**
53
   * Main entry point for rewriting terms of the form (witness ((x T)) (P x)).
54
   * Returns the rewritten form of node.
55
   */
56
  static Node rewriteWitness(TNode node);
57
  /** Get function type for array type
58
   *
59
   * This returns the function type of terms returned by the function
60
   * getLambdaForArrayRepresentation( t, bvl ),
61
   * where t.getType()=atn.
62
   *
63
   * bvl should be a bound variable list whose variables correspond in-order
64
   * to the index types of the (curried) Array type. For example, a bound
65
   * variable list bvl whose variables have types (Int, Real) can be given as
66
   * input when paired with atn = (Array Int (Array Real Bool)), or (Array Int
67
   * (Array Real (Array Bool Bool))). This function returns (-> Int Real Bool)
68
   * and (-> Int Real (Array Bool Bool)) respectively in these cases.
69
   * On the other hand, the above bvl is not a proper input for
70
   * atn = (Array Int (Array Bool Bool)) or (Array Int Int).
71
   * If the types of bvl and atn do not match, we throw an assertion failure.
72
   */
73
  static TypeNode getFunctionTypeForArrayType(TypeNode atn, Node bvl);
74
  /** Get array type for function type
75
   *
76
   * This returns the array type of terms returned by
77
   * getArrayRepresentationForLambda( t ), where t.getType()=ftn.
78
   */
79
  static TypeNode getArrayTypeForFunctionType(TypeNode ftn);
80
  /**
81
   * Given an array constant a, returns a lambda expression that it corresponds
82
   * to, with bound variable list bvl.
83
   * Examples:
84
   *
85
   * (store (storeall (Array Int Int) 2) 0 1)
86
   * becomes
87
   * ((lambda x. (ite (= x 0) 1 2))
88
   *
89
   * (store (storeall (Array Int (Array Int Int)) (storeall (Array Int Int) 4))
90
   * 0 (store (storeall (Array Int Int) 3) 1 2)) becomes (lambda xy. (ite (= x
91
   * 0) (ite (= x 1) 2 3) 4))
92
   *
93
   * (store (store (storeall (Array Int Bool) false) 2 true) 1 true)
94
   * becomes
95
   * (lambda x. (ite (= x 1) true (ite (= x 2) true false)))
96
   *
97
   * Notice that the return body of the lambda is rewritten to ensure that the
98
   * representation is canonical. Hence the last
99
   * example will in fact be returned as:
100
   * (lambda x. (ite (= x 1) true (= x 2)))
101
   */
102
  static Node getLambdaForArrayRepresentation(TNode a, TNode bvl);
103
  /**
104
   * Given a lambda expression n, returns an array term that corresponds to n.
105
   * This does the opposite direction of the examples described above.
106
   *
107
   * We limit the return values of this method to be almost constant functions,
108
   * that is, arrays of the form:
109
   *   (store ... (store (storeall _ b) i1 e1) ... in en)
110
   * where b, i1, e1, ..., in, en are constants.
111
   * Notice however that the return value of this form need not be a (canonical)
112
   * array constant.
113
   *
114
   * If it is not possible to construct an array of this form that corresponds
115
   * to n, this method returns null.
116
   */
117
  static Node getArrayRepresentationForLambda(TNode n);
118
}; /* class TheoryBuiltinRewriter */
119
120
}/* CVC4::theory::builtin namespace */
121
}/* CVC4::theory namespace */
122
}/* CVC4 namespace */
123
124
#endif /* CVC4__THEORY__BUILTIN__THEORY_BUILTIN_REWRITER_H */