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