GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/arith/operator_elim.h Lines: 1 1 100.0 %
Date: 2021-03-22 Branches: 0 0 0.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file operator_elim.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Andres Noetzli, Martin Brain
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 Operator elimination for arithmetic
13
 **/
14
15
#pragma once
16
17
#include <map>
18
19
#include "expr/node.h"
20
#include "theory/eager_proof_generator.h"
21
#include "theory/logic_info.h"
22
#include "theory/skolem_lemma.h"
23
24
namespace CVC4 {
25
26
class TConvProofGenerator;
27
28
namespace theory {
29
namespace arith {
30
31
class OperatorElim : public EagerProofGenerator
32
{
33
 public:
34
  OperatorElim(ProofNodeManager* pnm, const LogicInfo& info);
35
8992
  ~OperatorElim() {}
36
  /** Eliminate operators in this term.
37
   *
38
   * Eliminate operators in term n. If n has top symbol that is not a core
39
   * one (including division, int division, mod, to_int, is_int, syntactic sugar
40
   * transcendental functions), then we replace it by a form that eliminates
41
   * that operator. This may involve the introduction of witness terms.
42
   *
43
   * @param n The node to eliminate
44
   * @param lems The lemmas that we wish to add concerning n. It is the
45
   * responsbility of the caller to process these lemmas.
46
   * @param partialOnly Whether we only want to eliminate partial operators.
47
   * @return the trust node of kind REWRITE encapsulating the eliminated form
48
   * of n and a proof generator for proving this equivalence.
49
   */
50
  TrustNode eliminate(Node n,
51
                      std::vector<SkolemLemma>& lems,
52
                      bool partialOnly = false);
53
  /**
54
   * Get axiom for term n. This returns the axiom that this class uses to
55
   * eliminate the term n, which is determined by its top-most symbol.
56
   */
57
  static Node getAxiomFor(Node n);
58
59
 private:
60
  /** Logic info of the owner of this class */
61
  const LogicInfo& d_info;
62
63
  /** Arithmetic skolem identifier */
64
  enum class ArithSkolemId
65
  {
66
    /* an uninterpreted function f s.t. f(x) = x / 0.0 (real division) */
67
    DIV_BY_ZERO,
68
    /* an uninterpreted function f s.t. f(x) = x / 0 (integer division) */
69
    INT_DIV_BY_ZERO,
70
    /* an uninterpreted function f s.t. f(x) = x mod 0 */
71
    MOD_BY_ZERO,
72
    /* an uninterpreted function f s.t. f(x) = sqrt(x) */
73
    SQRT,
74
  };
75
76
  /**
77
   * Function symbols used to implement:
78
   * (1) Uninterpreted division-by-zero semantics.  Needed to deal with partial
79
   * division function ("/"),
80
   * (2) Uninterpreted int-division-by-zero semantics.  Needed to deal with
81
   * partial function "div",
82
   * (3) Uninterpreted mod-zero semantics.  Needed to deal with partial
83
   * function "mod".
84
   *
85
   * If the option arithNoPartialFun() is enabled, then the range of this map
86
   * stores Skolem constants instead of Skolem functions, meaning that the
87
   * function-ness of e.g. division by zero is ignored.
88
   */
89
  std::map<ArithSkolemId, Node> d_arith_skolem;
90
  /**
91
   * Eliminate operators in term n. If n has top symbol that is not a core
92
   * one (including division, int division, mod, to_int, is_int, syntactic sugar
93
   * transcendental functions), then we replace it by a form that eliminates
94
   * that operator. This may involve the introduction of witness terms.
95
   *
96
   * One exception to the above rule is that we may leave certain applications
97
   * like (/ 4 1) unchanged, since replacing this by 4 changes its type from
98
   * real to int. This is important for some subtyping issues during
99
   * expandDefinition. Moreover, applications like this can be eliminated
100
   * trivially later by rewriting.
101
   *
102
   * This method is called both during expandDefinition and during ppRewrite.
103
   *
104
   * @param n The node to eliminate operators from.
105
   * @return The (single step) eliminated form of n.
106
   */
107
  Node eliminateOperators(Node n,
108
                          std::vector<SkolemLemma>& lems,
109
                          TConvProofGenerator* tg,
110
                          bool partialOnly);
111
  /** get arithmetic skolem
112
   *
113
   * Returns the Skolem in the above map for the given id, creating it if it
114
   * does not already exist.
115
   */
116
  Node getArithSkolem(ArithSkolemId asi);
117
  /**
118
   * Make the witness term, which creates a witness term based on the skolem
119
   * manager with this class as a proof generator.
120
   */
121
  Node mkWitnessTerm(Node v,
122
                     Node pred,
123
                     const std::string& prefix,
124
                     const std::string& comment,
125
                     std::vector<SkolemLemma>& lems);
126
  /** get arithmetic skolem application
127
   *
128
   * By default, this returns the term f( n ), where f is the Skolem function
129
   * for the identifier asi.
130
   *
131
   * If the option arithNoPartialFun is enabled, this returns f, where f is
132
   * the Skolem constant for the identifier asi.
133
   */
134
  Node getArithSkolemApp(Node n, ArithSkolemId asi);
135
136
  /**
137
   * Called when a non-linear term n is given to this class. Throw an exception
138
   * if the logic is linear.
139
   */
140
  void checkNonLinearLogic(Node term);
141
};
142
143
}  // namespace arith
144
}  // namespace theory
145
}  // namespace CVC4