/dports/math/cvc4/CVC4-1.7/src/theory/bv/bitblast/ |
H A D | bitblast_strategies_template.h | 480 T one_if_odd = mkIte(is_odd, mkTrue<T>(), mkFalse<T>()); in uDivModRec() 498 q1[0] = mkIte(sign, q1[0], mkTrue<T>()); in uDivModRec() 513 T qval = mkIte(a_lt_b, mkFalse<T>(), q1[i]); in uDivModRec() 514 T rval = mkIte(a_lt_b, a[i], r1_shift_add[i]); in uDivModRec() 545 r[i] = mkIte(b_is_0, a[i], r[i]); // a urem 0 is a in DefaultUdivBB() 641 res[i] = mkIte(b[s], mkFalse<T>(), prev_res[i]); in DefaultShlBB() 655 res[i] = mkIte(b_ult_a_size, prev_res[i], mkFalse<T>()); in DefaultShlBB() 698 res[i] = mkIte(b[s], mkFalse<T>(), prev_res[i]); in DefaultLshrBB() 713 res[i] = mkIte(b_ult_a_size, prev_res[i], mkFalse<T>()); in DefaultLshrBB() 759 res[i] = mkIte(b[s], sign_bit, prev_res[i]); in DefaultAshrBB() [all …]
|
H A D | bitblast_utils.h | 59 template <class T> T mkIte(T cond, T a, T b); 116 Node mkIte<Node>(Node cond, Node a, Node b) {
|
H A D | aig_bitblaster.cpp | 116 Abc_Obj_t* mkIte<Abc_Obj_t*>(Abc_Obj_t* cond, Abc_Obj_t* a, Abc_Obj_t* b) { in mkIte() function 227 result = mkIte(a, b, c); in bbFormula()
|
/dports/devel/llvm80/llvm-8.0.1.src/tools/clang/include/clang/StaticAnalyzer/Core/PathSensitive/ |
H A D | SMTSolver.h | 162 virtual SMTExprRef mkIte(const SMTExprRef &Cond, const SMTExprRef &T,
|
H A D | SMTConv.h | 270 return Solver->mkIte( in fromCast()
|
/dports/www/chromium-legacy/chromium-88.0.4324.182/third_party/llvm/llvm/include/llvm/Support/ |
H A D | SMTAPI.h | 265 virtual SMTExprRef mkIte(const SMTExprRef &Cond, const SMTExprRef &T,
|
/dports/devel/llvm-cheri/llvm-project-37c49ff00e3eadce5d8703fdc4497f28458c64a8/llvm/include/llvm/Support/ |
H A D | SMTAPI.h | 265 virtual SMTExprRef mkIte(const SMTExprRef &Cond, const SMTExprRef &T,
|
/dports/devel/llvm10/llvm-10.0.1.src/include/llvm/Support/ |
H A D | SMTAPI.h | 265 virtual SMTExprRef mkIte(const SMTExprRef &Cond, const SMTExprRef &T,
|
/dports/devel/wasi-libcxx/llvm-project-13.0.1.src/llvm/include/llvm/Support/ |
H A D | SMTAPI.h | 265 virtual SMTExprRef mkIte(const SMTExprRef &Cond, const SMTExprRef &T,
|
/dports/graphics/llvm-mesa/llvm-13.0.1.src/include/llvm/Support/ |
H A D | SMTAPI.h | 265 virtual SMTExprRef mkIte(const SMTExprRef &Cond, const SMTExprRef &T,
|
/dports/devel/llvm12/llvm-project-12.0.1.src/llvm/include/llvm/Support/ |
H A D | SMTAPI.h | 265 virtual SMTExprRef mkIte(const SMTExprRef &Cond, const SMTExprRef &T,
|
/dports/devel/llvm11/llvm-11.0.1.src/include/llvm/Support/ |
H A D | SMTAPI.h | 265 virtual SMTExprRef mkIte(const SMTExprRef &Cond, const SMTExprRef &T,
|
/dports/www/chromium-legacy/chromium-88.0.4324.182/third_party/swiftshader/third_party/llvm-10.0/llvm/include/llvm/Support/ |
H A D | SMTAPI.h | 265 virtual SMTExprRef mkIte(const SMTExprRef &Cond, const SMTExprRef &T,
|
/dports/lang/rust/rustc-1.58.1-src/src/llvm-project/llvm/include/llvm/Support/ |
H A D | SMTAPI.h | 265 virtual SMTExprRef mkIte(const SMTExprRef &Cond, const SMTExprRef &T,
|
/dports/devel/llvm-devel/llvm-project-f05c95f10fc1d8171071735af8ad3a9e87633120/llvm/include/llvm/Support/ |
H A D | SMTAPI.h | 265 virtual SMTExprRef mkIte(const SMTExprRef &Cond, const SMTExprRef &T,
|
/dports/devel/wasi-compiler-rt13/llvm-project-13.0.1.src/llvm/include/llvm/Support/ |
H A D | SMTAPI.h | 265 virtual SMTExprRef mkIte(const SMTExprRef &Cond, const SMTExprRef &T,
|
/dports/devel/wasi-compiler-rt12/llvm-project-12.0.1.src/llvm/include/llvm/Support/ |
H A D | SMTAPI.h | 265 virtual SMTExprRef mkIte(const SMTExprRef &Cond, const SMTExprRef &T,
|
/dports/devel/tinygo/tinygo-0.14.1/llvm-project/llvm/include/llvm/Support/ |
H A D | SMTAPI.h | 265 virtual SMTExprRef mkIte(const SMTExprRef &Cond, const SMTExprRef &T,
|
/dports/devel/llvm13/llvm-project-13.0.1.src/llvm/include/llvm/Support/ |
H A D | SMTAPI.h | 265 virtual SMTExprRef mkIte(const SMTExprRef &Cond, const SMTExprRef &T,
|
/dports/devel/llvm90/llvm-9.0.1.src/include/llvm/Support/ |
H A D | SMTAPI.h | 265 virtual SMTExprRef mkIte(const SMTExprRef &Cond, const SMTExprRef &T,
|
/dports/devel/llvm70/llvm-7.0.1.src/tools/clang/include/clang/StaticAnalyzer/Core/PathSensitive/ |
H A D | SMTSolver.h | 283 return mkIte(Exp, mkBitvector(llvm::APSInt("1"), ToBitWidth), in fromCast() 842 virtual SMTExprRef mkIte(const SMTExprRef &Cond, const SMTExprRef &T,
|
/dports/security/hs-cryptol/cryptol-2.11.0/_cabal_deps/sbv-8.12/Data/SBV/Compilers/ |
H A D | C.hs | 657 cvt FP_ObjEqual = let mkIte x y z = x <+> text "?" <+> y <+> text ":" <+> z function 663 …in dispatch $ same $ \_ [a, b] -> mkIte (chkNaN a) (chkNaN b) (mkIte (negZero a) (negZero b) (mkIt…
|
/dports/security/hs-cryptol/cryptol-2.11.0/_cabal_deps/what4-1.1/src/What4/Expr/ |
H A D | Builder.hs | 1239 mkIte :: 1245 mkIte sym c x y function 1252 = mkIte sym c' y x 2289 mkIte sym c x y) 2711 | otherwise = mkIte sym p x y 2738 = mkIte sym c x y 2944 | otherwise = mkIte sym p x y 3294 floatIte sym c x y = mkIte sym c x y
|
/dports/devel/llvm-devel/llvm-project-f05c95f10fc1d8171071735af8ad3a9e87633120/clang/include/clang/StaticAnalyzer/Core/PathSensitive/ |
H A D | SMTConv.h | 273 return Solver->mkIte( in fromCast()
|
/dports/devel/llvm12/llvm-project-12.0.1.src/clang/include/clang/StaticAnalyzer/Core/PathSensitive/ |
H A D | SMTConv.h | 273 return Solver->mkIte( in fromCast()
|