Home
last modified time | relevance | path

Searched refs:mkIte (Results 1 – 25 of 56) sorted by relevance

123

/dports/math/cvc4/CVC4-1.7/src/theory/bv/bitblast/
H A Dbitblast_strategies_template.h480 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 Dbitblast_utils.h59 template <class T> T mkIte(T cond, T a, T b);
116 Node mkIte<Node>(Node cond, Node a, Node b) {
H A Daig_bitblaster.cpp116 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 DSMTSolver.h162 virtual SMTExprRef mkIte(const SMTExprRef &Cond, const SMTExprRef &T,
H A DSMTConv.h270 return Solver->mkIte( in fromCast()
/dports/www/chromium-legacy/chromium-88.0.4324.182/third_party/llvm/llvm/include/llvm/Support/
H A DSMTAPI.h265 virtual SMTExprRef mkIte(const SMTExprRef &Cond, const SMTExprRef &T,
/dports/devel/llvm-cheri/llvm-project-37c49ff00e3eadce5d8703fdc4497f28458c64a8/llvm/include/llvm/Support/
H A DSMTAPI.h265 virtual SMTExprRef mkIte(const SMTExprRef &Cond, const SMTExprRef &T,
/dports/devel/llvm10/llvm-10.0.1.src/include/llvm/Support/
H A DSMTAPI.h265 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 DSMTAPI.h265 virtual SMTExprRef mkIte(const SMTExprRef &Cond, const SMTExprRef &T,
/dports/graphics/llvm-mesa/llvm-13.0.1.src/include/llvm/Support/
H A DSMTAPI.h265 virtual SMTExprRef mkIte(const SMTExprRef &Cond, const SMTExprRef &T,
/dports/devel/llvm12/llvm-project-12.0.1.src/llvm/include/llvm/Support/
H A DSMTAPI.h265 virtual SMTExprRef mkIte(const SMTExprRef &Cond, const SMTExprRef &T,
/dports/devel/llvm11/llvm-11.0.1.src/include/llvm/Support/
H A DSMTAPI.h265 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 DSMTAPI.h265 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 DSMTAPI.h265 virtual SMTExprRef mkIte(const SMTExprRef &Cond, const SMTExprRef &T,
/dports/devel/llvm-devel/llvm-project-f05c95f10fc1d8171071735af8ad3a9e87633120/llvm/include/llvm/Support/
H A DSMTAPI.h265 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 DSMTAPI.h265 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 DSMTAPI.h265 virtual SMTExprRef mkIte(const SMTExprRef &Cond, const SMTExprRef &T,
/dports/devel/tinygo/tinygo-0.14.1/llvm-project/llvm/include/llvm/Support/
H A DSMTAPI.h265 virtual SMTExprRef mkIte(const SMTExprRef &Cond, const SMTExprRef &T,
/dports/devel/llvm13/llvm-project-13.0.1.src/llvm/include/llvm/Support/
H A DSMTAPI.h265 virtual SMTExprRef mkIte(const SMTExprRef &Cond, const SMTExprRef &T,
/dports/devel/llvm90/llvm-9.0.1.src/include/llvm/Support/
H A DSMTAPI.h265 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 DSMTSolver.h283 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 DC.hs657 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 DBuilder.hs1239 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 DSMTConv.h273 return Solver->mkIte( in fromCast()
/dports/devel/llvm12/llvm-project-12.0.1.src/clang/include/clang/StaticAnalyzer/Core/PathSensitive/
H A DSMTConv.h273 return Solver->mkIte( in fromCast()

123