clang  9.0.0svn
SMTSolver.h
Go to the documentation of this file.
1 //== SMTSolver.h ------------------------------------------------*- C++ -*--==//
2 //
3 // Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
4 // See https://llvm.org/LICENSE.txt for license information.
5 // SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
6 //
7 //===----------------------------------------------------------------------===//
8 //
9 // This file defines a SMT generic Solver API, which will be the base class
10 // for every SMT solver specific class.
11 //
12 //===----------------------------------------------------------------------===//
13 
14 #ifndef LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SMTSOLVER_H
15 #define LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SMTSOLVER_H
16 
19 #include "llvm/ADT/APSInt.h"
20 
21 namespace clang {
22 namespace ento {
23 
24 /// Generic base class for SMT Solvers
25 ///
26 /// This class is responsible for wrapping all sorts and expression generation,
27 /// through the mk* methods. It also provides methods to create SMT expressions
28 /// straight from clang's AST, through the from* methods.
29 class SMTSolver {
30 public:
31  SMTSolver() = default;
32  virtual ~SMTSolver() = default;
33 
34  LLVM_DUMP_METHOD void dump() const { print(llvm::errs()); }
35 
36  // Returns an appropriate floating-point sort for the given bitwidth.
37  SMTSortRef getFloatSort(unsigned BitWidth) {
38  switch (BitWidth) {
39  case 16:
40  return getFloat16Sort();
41  case 32:
42  return getFloat32Sort();
43  case 64:
44  return getFloat64Sort();
45  case 128:
46  return getFloat128Sort();
47  default:;
48  }
49  llvm_unreachable("Unsupported floating-point bitwidth!");
50  }
51 
52  // Returns a boolean sort.
53  virtual SMTSortRef getBoolSort() = 0;
54 
55  // Returns an appropriate bitvector sort for the given bitwidth.
56  virtual SMTSortRef getBitvectorSort(const unsigned BitWidth) = 0;
57 
58  // Returns a floating-point sort of width 16
59  virtual SMTSortRef getFloat16Sort() = 0;
60 
61  // Returns a floating-point sort of width 32
62  virtual SMTSortRef getFloat32Sort() = 0;
63 
64  // Returns a floating-point sort of width 64
65  virtual SMTSortRef getFloat64Sort() = 0;
66 
67  // Returns a floating-point sort of width 128
68  virtual SMTSortRef getFloat128Sort() = 0;
69 
70  // Returns an appropriate sort for the given AST.
71  virtual SMTSortRef getSort(const SMTExprRef &AST) = 0;
72 
73  // Returns a new SMTExprRef from an SMTExpr
74  virtual SMTExprRef newExprRef(const SMTExpr &E) const = 0;
75 
76  /// Given a constraint, adds it to the solver
77  virtual void addConstraint(const SMTExprRef &Exp) const = 0;
78 
79  /// Creates a bitvector addition operation
80  virtual SMTExprRef mkBVAdd(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
81 
82  /// Creates a bitvector subtraction operation
83  virtual SMTExprRef mkBVSub(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
84 
85  /// Creates a bitvector multiplication operation
86  virtual SMTExprRef mkBVMul(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
87 
88  /// Creates a bitvector signed modulus operation
89  virtual SMTExprRef mkBVSRem(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
90 
91  /// Creates a bitvector unsigned modulus operation
92  virtual SMTExprRef mkBVURem(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
93 
94  /// Creates a bitvector signed division operation
95  virtual SMTExprRef mkBVSDiv(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
96 
97  /// Creates a bitvector unsigned division operation
98  virtual SMTExprRef mkBVUDiv(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
99 
100  /// Creates a bitvector logical shift left operation
101  virtual SMTExprRef mkBVShl(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
102 
103  /// Creates a bitvector arithmetic shift right operation
104  virtual SMTExprRef mkBVAshr(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
105 
106  /// Creates a bitvector logical shift right operation
107  virtual SMTExprRef mkBVLshr(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
108 
109  /// Creates a bitvector negation operation
110  virtual SMTExprRef mkBVNeg(const SMTExprRef &Exp) = 0;
111 
112  /// Creates a bitvector not operation
113  virtual SMTExprRef mkBVNot(const SMTExprRef &Exp) = 0;
114 
115  /// Creates a bitvector xor operation
116  virtual SMTExprRef mkBVXor(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
117 
118  /// Creates a bitvector or operation
119  virtual SMTExprRef mkBVOr(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
120 
121  /// Creates a bitvector and operation
122  virtual SMTExprRef mkBVAnd(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
123 
124  /// Creates a bitvector unsigned less-than operation
125  virtual SMTExprRef mkBVUlt(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
126 
127  /// Creates a bitvector signed less-than operation
128  virtual SMTExprRef mkBVSlt(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
129 
130  /// Creates a bitvector unsigned greater-than operation
131  virtual SMTExprRef mkBVUgt(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
132 
133  /// Creates a bitvector signed greater-than operation
134  virtual SMTExprRef mkBVSgt(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
135 
136  /// Creates a bitvector unsigned less-equal-than operation
137  virtual SMTExprRef mkBVUle(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
138 
139  /// Creates a bitvector signed less-equal-than operation
140  virtual SMTExprRef mkBVSle(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
141 
142  /// Creates a bitvector unsigned greater-equal-than operation
143  virtual SMTExprRef mkBVUge(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
144 
145  /// Creates a bitvector signed greater-equal-than operation
146  virtual SMTExprRef mkBVSge(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
147 
148  /// Creates a boolean not operation
149  virtual SMTExprRef mkNot(const SMTExprRef &Exp) = 0;
150 
151  /// Creates a boolean equality operation
152  virtual SMTExprRef mkEqual(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
153 
154  /// Creates a boolean and operation
155  virtual SMTExprRef mkAnd(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
156 
157  /// Creates a boolean or operation
158  virtual SMTExprRef mkOr(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
159 
160  /// Creates a boolean ite operation
161  virtual SMTExprRef mkIte(const SMTExprRef &Cond, const SMTExprRef &T,
162  const SMTExprRef &F) = 0;
163 
164  /// Creates a bitvector sign extension operation
165  virtual SMTExprRef mkBVSignExt(unsigned i, const SMTExprRef &Exp) = 0;
166 
167  /// Creates a bitvector zero extension operation
168  virtual SMTExprRef mkBVZeroExt(unsigned i, const SMTExprRef &Exp) = 0;
169 
170  /// Creates a bitvector extract operation
171  virtual SMTExprRef mkBVExtract(unsigned High, unsigned Low,
172  const SMTExprRef &Exp) = 0;
173 
174  /// Creates a bitvector concat operation
175  virtual SMTExprRef mkBVConcat(const SMTExprRef &LHS,
176  const SMTExprRef &RHS) = 0;
177 
178  /// Creates a floating-point negation operation
179  virtual SMTExprRef mkFPNeg(const SMTExprRef &Exp) = 0;
180 
181  /// Creates a floating-point isInfinite operation
182  virtual SMTExprRef mkFPIsInfinite(const SMTExprRef &Exp) = 0;
183 
184  /// Creates a floating-point isNaN operation
185  virtual SMTExprRef mkFPIsNaN(const SMTExprRef &Exp) = 0;
186 
187  /// Creates a floating-point isNormal operation
188  virtual SMTExprRef mkFPIsNormal(const SMTExprRef &Exp) = 0;
189 
190  /// Creates a floating-point isZero operation
191  virtual SMTExprRef mkFPIsZero(const SMTExprRef &Exp) = 0;
192 
193  /// Creates a floating-point multiplication operation
194  virtual SMTExprRef mkFPMul(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
195 
196  /// Creates a floating-point division operation
197  virtual SMTExprRef mkFPDiv(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
198 
199  /// Creates a floating-point remainder operation
200  virtual SMTExprRef mkFPRem(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
201 
202  /// Creates a floating-point addition operation
203  virtual SMTExprRef mkFPAdd(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
204 
205  /// Creates a floating-point subtraction operation
206  virtual SMTExprRef mkFPSub(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
207 
208  /// Creates a floating-point less-than operation
209  virtual SMTExprRef mkFPLt(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
210 
211  /// Creates a floating-point greater-than operation
212  virtual SMTExprRef mkFPGt(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
213 
214  /// Creates a floating-point less-than-or-equal operation
215  virtual SMTExprRef mkFPLe(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
216 
217  /// Creates a floating-point greater-than-or-equal operation
218  virtual SMTExprRef mkFPGe(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
219 
220  /// Creates a floating-point equality operation
221  virtual SMTExprRef mkFPEqual(const SMTExprRef &LHS,
222  const SMTExprRef &RHS) = 0;
223 
224  /// Creates a floating-point conversion from floatint-point to floating-point
225  /// operation
226  virtual SMTExprRef mkFPtoFP(const SMTExprRef &From, const SMTSortRef &To) = 0;
227 
228  /// Creates a floating-point conversion from signed bitvector to
229  /// floatint-point operation
230  virtual SMTExprRef mkSBVtoFP(const SMTExprRef &From,
231  const SMTSortRef &To) = 0;
232 
233  /// Creates a floating-point conversion from unsigned bitvector to
234  /// floatint-point operation
235  virtual SMTExprRef mkUBVtoFP(const SMTExprRef &From,
236  const SMTSortRef &To) = 0;
237 
238  /// Creates a floating-point conversion from floatint-point to signed
239  /// bitvector operation
240  virtual SMTExprRef mkFPtoSBV(const SMTExprRef &From, unsigned ToWidth) = 0;
241 
242  /// Creates a floating-point conversion from floatint-point to unsigned
243  /// bitvector operation
244  virtual SMTExprRef mkFPtoUBV(const SMTExprRef &From, unsigned ToWidth) = 0;
245 
246  /// Creates a new symbol, given a name and a sort
247  virtual SMTExprRef mkSymbol(const char *Name, SMTSortRef Sort) = 0;
248 
249  // Returns an appropriate floating-point rounding mode.
250  virtual SMTExprRef getFloatRoundingMode() = 0;
251 
252  // If the a model is available, returns the value of a given bitvector symbol
253  virtual llvm::APSInt getBitvector(const SMTExprRef &Exp, unsigned BitWidth,
254  bool isUnsigned) = 0;
255 
256  // If the a model is available, returns the value of a given boolean symbol
257  virtual bool getBoolean(const SMTExprRef &Exp) = 0;
258 
259  /// Constructs an SMTExprRef from a boolean.
260  virtual SMTExprRef mkBoolean(const bool b) = 0;
261 
262  /// Constructs an SMTExprRef from a finite APFloat.
263  virtual SMTExprRef mkFloat(const llvm::APFloat Float) = 0;
264 
265  /// Constructs an SMTExprRef from an APSInt and its bit width
266  virtual SMTExprRef mkBitvector(const llvm::APSInt Int, unsigned BitWidth) = 0;
267 
268  /// Given an expression, extract the value of this operand in the model.
269  virtual bool getInterpretation(const SMTExprRef &Exp, llvm::APSInt &Int) = 0;
270 
271  /// Given an expression extract the value of this operand in the model.
272  virtual bool getInterpretation(const SMTExprRef &Exp,
273  llvm::APFloat &Float) = 0;
274 
275  /// Check if the constraints are satisfiable
276  virtual Optional<bool> check() const = 0;
277 
278  /// Push the current solver state
279  virtual void push() = 0;
280 
281  /// Pop the previous solver state
282  virtual void pop(unsigned NumStates = 1) = 0;
283 
284  /// Reset the solver and remove all constraints.
285  virtual void reset() = 0;
286 
287  /// Checks if the solver supports floating-points.
288  virtual bool isFPSupported() = 0;
289 
290  virtual void print(raw_ostream &OS) const = 0;
291 };
292 
293 /// Shared pointer for SMTSolvers.
294 using SMTSolverRef = std::shared_ptr<SMTSolver>;
295 
296 /// Convenience method to create and Z3Solver object
298 
299 } // namespace ento
300 } // namespace clang
301 
302 #endif
virtual SMTExprRef mkBVMul(const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a bitvector multiplication operation.
virtual void print(raw_ostream &OS) const =0
virtual SMTExprRef mkFPLe(const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a floating-point less-than-or-equal operation.
virtual SMTSortRef getBoolSort()=0
SMTSortRef getFloatSort(unsigned BitWidth)
Definition: SMTSolver.h:37
virtual bool getBoolean(const SMTExprRef &Exp)=0
virtual SMTExprRef mkSymbol(const char *Name, SMTSortRef Sort)=0
Creates a new symbol, given a name and a sort.
virtual SMTExprRef mkOr(const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a boolean or operation.
virtual SMTSortRef getFloat16Sort()=0
virtual SMTExprRef mkBVSlt(const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a bitvector signed less-than operation.
virtual SMTExprRef mkFPRem(const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a floating-point remainder operation.
virtual SMTExprRef mkFPIsZero(const SMTExprRef &Exp)=0
Creates a floating-point isZero operation.
virtual ~SMTSolver()=default
virtual Optional< bool > check() const =0
Check if the constraints are satisfiable.
Generic base class for SMT exprs.
Definition: SMTExpr.h:24
virtual SMTExprRef mkFPSub(const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a floating-point subtraction operation.
virtual SMTSortRef getSort(const SMTExprRef &AST)=0
virtual SMTExprRef mkFPMul(const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a floating-point multiplication operation.
std::shared_ptr< SMTSort > SMTSortRef
Shared pointer for SMTSorts, used by SMTSolver API.
Definition: SMTSort.h:85
virtual SMTExprRef mkBVNeg(const SMTExprRef &Exp)=0
Creates a bitvector negation operation.
virtual SMTExprRef mkBoolean(const bool b)=0
Constructs an SMTExprRef from a boolean.
virtual SMTExprRef mkFPtoUBV(const SMTExprRef &From, unsigned ToWidth)=0
Creates a floating-point conversion from floatint-point to unsigned bitvector operation.
virtual SMTExprRef mkBVSgt(const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a bitvector signed greater-than operation.
virtual SMTExprRef mkAnd(const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a boolean and operation.
virtual SMTExprRef mkBVSub(const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a bitvector subtraction operation.
virtual SMTExprRef mkBVSDiv(const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a bitvector signed division operation.
virtual SMTExprRef mkBVZeroExt(unsigned i, const SMTExprRef &Exp)=0
Creates a bitvector zero extension operation.
virtual SMTExprRef mkBVAdd(const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a bitvector addition operation.
virtual SMTExprRef mkIte(const SMTExprRef &Cond, const SMTExprRef &T, const SMTExprRef &F)=0
Creates a boolean ite operation.
virtual SMTExprRef mkBVConcat(const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a bitvector concat operation.
virtual SMTExprRef mkFPDiv(const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a floating-point division operation.
virtual SMTExprRef mkBVSle(const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a bitvector signed less-equal-than operation.
LLVM_DUMP_METHOD void dump() const
Definition: SMTSolver.h:34
virtual SMTExprRef mkFPtoSBV(const SMTExprRef &From, unsigned ToWidth)=0
Creates a floating-point conversion from floatint-point to signed bitvector operation.
virtual SMTSortRef getFloat64Sort()=0
virtual SMTSortRef getBitvectorSort(const unsigned BitWidth)=0
virtual SMTExprRef mkBVLshr(const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a bitvector logical shift right operation.
virtual SMTExprRef newExprRef(const SMTExpr &E) const =0
virtual SMTExprRef mkNot(const SMTExprRef &Exp)=0
Creates a boolean not operation.
virtual SMTExprRef mkBVSignExt(unsigned i, const SMTExprRef &Exp)=0
Creates a bitvector sign extension operation.
virtual SMTExprRef mkBVAnd(const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a bitvector and operation.
virtual SMTExprRef mkBVSRem(const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a bitvector signed modulus operation.
virtual SMTExprRef mkBVSge(const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a bitvector signed greater-equal-than operation.
virtual SMTExprRef mkBVUge(const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a bitvector unsigned greater-equal-than operation.
virtual SMTExprRef mkEqual(const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a boolean equality operation.
virtual void pop(unsigned NumStates=1)=0
Pop the previous solver state.
virtual SMTExprRef mkBVShl(const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a bitvector logical shift left operation.
virtual SMTSortRef getFloat128Sort()=0
virtual SMTExprRef mkFPAdd(const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a floating-point addition operation.
virtual SMTExprRef mkSBVtoFP(const SMTExprRef &From, const SMTSortRef &To)=0
Creates a floating-point conversion from signed bitvector to floatint-point operation.
virtual SMTExprRef mkFPGe(const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a floating-point greater-than-or-equal operation.
virtual SMTExprRef mkBVUlt(const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a bitvector unsigned less-than operation.
virtual SMTExprRef mkBVOr(const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a bitvector or operation.
virtual void reset()=0
Reset the solver and remove all constraints.
SMTSolverRef CreateZ3Solver()
Convenience method to create and Z3Solver object.
virtual SMTSortRef getFloat32Sort()=0
virtual SMTExprRef mkBVAshr(const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a bitvector arithmetic shift right operation.
Dataflow Directional Tag Classes.
virtual SMTExprRef mkFPIsNaN(const SMTExprRef &Exp)=0
Creates a floating-point isNaN operation.
virtual SMTExprRef mkBVUDiv(const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a bitvector unsigned division operation.
virtual SMTExprRef mkUBVtoFP(const SMTExprRef &From, const SMTSortRef &To)=0
Creates a floating-point conversion from unsigned bitvector to floatint-point operation.
virtual void addConstraint(const SMTExprRef &Exp) const =0
Given a constraint, adds it to the solver.
std::shared_ptr< SMTSolver > SMTSolverRef
Shared pointer for SMTSolvers.
Definition: SMTSolver.h:294
virtual SMTExprRef mkFPIsInfinite(const SMTExprRef &Exp)=0
Creates a floating-point isInfinite operation.
Generic base class for SMT Solvers.
Definition: SMTSolver.h:29
virtual SMTExprRef mkBVXor(const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a bitvector xor operation.
virtual bool getInterpretation(const SMTExprRef &Exp, llvm::APSInt &Int)=0
Given an expression, extract the value of this operand in the model.
Indicates that the tracking object is a descendant of a referenced-counted OSObject, used in the Darwin kernel.
virtual SMTExprRef mkFPEqual(const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a floating-point equality operation.
virtual SMTExprRef mkFPIsNormal(const SMTExprRef &Exp)=0
Creates a floating-point isNormal operation.
virtual SMTExprRef mkBVURem(const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a bitvector unsigned modulus operation.
virtual SMTExprRef mkBVUgt(const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a bitvector unsigned greater-than operation.
virtual SMTExprRef mkFPGt(const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a floating-point greater-than operation.
virtual SMTExprRef mkBVExtract(unsigned High, unsigned Low, const SMTExprRef &Exp)=0
Creates a bitvector extract operation.
virtual SMTExprRef mkFloat(const llvm::APFloat Float)=0
Constructs an SMTExprRef from a finite APFloat.
virtual llvm::APSInt getBitvector(const SMTExprRef &Exp, unsigned BitWidth, bool isUnsigned)=0
std::shared_ptr< SMTExpr > SMTExprRef
Shared pointer for SMTExprs, used by SMTSolver API.
Definition: SMTExpr.h:56
virtual SMTExprRef getFloatRoundingMode()=0
virtual SMTExprRef mkBitvector(const llvm::APSInt Int, unsigned BitWidth)=0
Constructs an SMTExprRef from an APSInt and its bit width.
virtual SMTExprRef mkFPtoFP(const SMTExprRef &From, const SMTSortRef &To)=0
Creates a floating-point conversion from floatint-point to floating-point operation.
virtual void push()=0
Push the current solver state.
virtual SMTExprRef mkFPLt(const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a floating-point less-than operation.
virtual SMTExprRef mkBVUle(const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a bitvector unsigned less-equal-than operation.
virtual SMTExprRef mkFPNeg(const SMTExprRef &Exp)=0
Creates a floating-point negation operation.
virtual SMTExprRef mkBVNot(const SMTExprRef &Exp)=0
Creates a bitvector not operation.
virtual bool isFPSupported()=0
Checks if the solver supports floating-points.