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) 20092021 by the authors listed in the file AUTHORS 
8 

** in the toplevel source directory and their institutional affiliations. 
9 

** All rights reserved. See the file COPYING in the toplevel 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 
8994 
~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 topmost 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 divisionbyzero semantics. Needed to deal with partial 
79 

* division function ("/"), 
80 

* (2) Uninterpreted intdivisionbyzero semantics. Needed to deal with 
81 

* partial function "div", 
82 

* (3) Uninterpreted modzero 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 

* functionness 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 nonlinear 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 