| /dports/math/cvc4/CVC4-1.7/src/theory/bv/bitblast/ |
| H A D | bitblast_utils.h | 51 template <class T> T mkFalse();
68 Node mkFalse<Node>() {
142 if(bits[i] != mkFalse<T>()) { in isZero()
155 bits[i] = mkFalse<T>(); in rshift()
165 bits[i] = mkFalse<T>(); in lshift()
173 bits.push_back(mkFalse<T>()); in makeZero()
211 T carry_in = mkFalse<T>(); in shiftAddMultiplier()
|
| H A D | bitblast_strategies_template.h | 211 bits.push_back(mkFalse<T>()); in DefaultConstBB()
415 rippleCarryAdder(res, current, newres, mkFalse<T>()); in DefaultPlusBB()
480 T one_if_odd = mkIte(is_odd, mkTrue<T>(), mkFalse<T>()); in uDivModRec()
513 T qval = mkIte(a_lt_b, mkFalse<T>(), q1[i]); in uDivModRec()
538 iszero.push_back(mkIff(b[i], mkFalse<T>())); in DefaultUdivBB()
571 iszero.push_back(mkIff(b[i], mkFalse<T>())); in DefaultUremBB()
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()
|
| H A D | aig_bitblaster.cpp | 59 Abc_Obj_t* mkFalse<Abc_Obj_t*>() { in mkFalse() function
238 result = node.getConst<bool>() ? mkTrue<Abc_Obj_t*>() : mkFalse<Abc_Obj_t*>(); in bbFormula()
|
| H A D | lazy_bitblaster.cpp | 452 if (a_eq_b == utils::mkFalse()) return theory::EQUALITY_FALSE; in getEqualityStatus()
|
| /dports/devel/hs-hlint/hlint-3.3.4/_cabal_deps/ghc-lib-parser-9.0.1.20210324/compiler/GHC/Data/ |
| H A D | BooleanFormula.hs | 12 mkFalse, mkTrue, mkAnd, mkOr, mkVar,
44 mkFalse, mkTrue :: BooleanFormula a function
45 mkFalse = Or [] function
50 mkBool False = mkFalse
55 mkAnd = maybe mkFalse (mkAnd' . nub) . concatMapM fromAnd
|
| /dports/devel/hs-haskell-language-server/haskell-language-server-1.4.0/_cabal_deps/ghc-lib-parser-8.10.7.20210828/compiler/utils/ |
| H A D | BooleanFormula.hs | 12 mkFalse, mkTrue, mkAnd, mkOr, mkVar,
44 mkFalse, mkTrue :: BooleanFormula a function
45 mkFalse = Or [] function
50 mkBool False = mkFalse
55 mkAnd = maybe mkFalse (mkAnd' . nub) . concatMapM fromAnd
|
| /dports/devel/hs-ormolu/ormolu-0.4.0.0/_cabal_deps/ghc-lib-parser-9.2.1.20211101/compiler/GHC/Data/ |
| H A D | BooleanFormula.hs | 12 mkFalse, mkTrue, mkAnd, mkOr, mkVar,
45 mkFalse, mkTrue :: BooleanFormula a function
46 mkFalse = Or [] function
51 mkBool False = mkFalse
56 mkAnd = maybe mkFalse (mkAnd' . nub) . concatMapM fromAnd
|
| /dports/lang/ghc/ghc-8.10.7/compiler/utils/ |
| H A D | BooleanFormula.hs | 12 mkFalse, mkTrue, mkAnd, mkOr, mkVar,
44 mkFalse, mkTrue :: BooleanFormula a function
45 mkFalse = Or [] function
50 mkBool False = mkFalse
55 mkAnd = maybe mkFalse (mkAnd' . nub) . concatMapM fromAnd
|
| /dports/math/cvc4/CVC4-1.7/src/theory/bv/ |
| H A D | theory_bv_rewrite_rules_constant_evaluation.h | 294 return utils::mkFalse(); in apply()
330 return utils::mkFalse(); in apply()
388 return utils::mkFalse(); in apply()
406 return utils::mkFalse(); in apply()
475 return utils::mkFalse(); in apply()
|
| H A D | theory_bv_utils.cpp | 222 Node mkFalse() in mkFalse() function
415 if (w == 1) return mkFalse(); in mkUmulo()
|
| H A D | theory_bv_utils.h | 91 Node mkFalse();
|
| H A D | theory_bv_rewrite_rules_simplification.h | 928 return utils::mkFalse(); in apply()
992 return utils::mkFalse(); in apply()
1053 return utils::mkFalse(); in apply()
1687 return utils::mkFalse(); in apply()
1730 return utils::mkFalse(); in apply()
|
| H A D | theory_bv_rewrite_rules_normalization.h | 643 return utils::mkFalse(); in apply()
660 return utils::mkFalse(); in apply()
767 return utils::mkFalse(); in apply()
784 return utils::mkFalse(); in apply()
|
| H A D | theory_bv_rewrite_rules_core.h | 272 return utils::mkFalse(); in apply()
|
| /dports/math/cvc4/CVC4-1.7/src/proof/ |
| H A D | proof_utils.h | 118 inline Expr mkFalse() { in mkFalse() function
|
| H A D | theory_proof.cpp | 390 Assert(n1.toExpr() == utils::mkFalse() || in printLemmaRewrites()
497 (atom == utils::mkFalse() && lit.isNegated())); in finalizeBvConflicts()
668 …(missingAssertion->getKind() == kind::NOT && (*missingAssertion)[0].toExpr() == utils::mkFalse()) { in printTheoryLemmas()
790 …(missingAssertion->getKind() == kind::NOT && (*missingAssertion)[0].toExpr() == utils::mkFalse()) { in printTheoryLemmas()
|
| H A D | resolution_bitvector_proof.cpp | 439 if (lemma[i].getKind() == kind::NOT && lemma[i][0] == utils::mkFalse()) in printTheoryLemmaProof()
|
| /dports/math/cvc4/CVC4-1.7/src/preprocessing/passes/ |
| H A D | bv_to_bool.cpp | 164 Node result = node == d_one ? bv::utils::mkTrue() : bv::utils::mkFalse(); in convertBvTerm()
|
| /dports/math/cvc4/CVC4-1.7/test/unit/api/ |
| H A D | solver_black.h | 376 TS_ASSERT_THROWS_NOTHING(d_solver->mkFalse()); in testMkFalse()
377 TS_ASSERT_THROWS_NOTHING(d_solver->mkFalse()); in testMkFalse()
|
| /dports/math/z3/z3-z3-4.8.13/examples/java/ |
| H A D | JavaExample.java | 827 g2.add(ctx.mkFalse()); in basicTests()
1014 earr[1][0] = ctx.mkFalse(); in castingTest()
1015 earr[1][1] = ctx.mkFalse(); in castingTest()
1526 BoolExpr f = ctx.mkFalse(); in iteExample()
|
| /dports/math/py-z3-solver/z3-z3-4.8.10/examples/java/ |
| H A D | JavaExample.java | 827 g2.add(ctx.mkFalse()); in basicTests()
1014 earr[1][0] = ctx.mkFalse(); in castingTest()
1015 earr[1][1] = ctx.mkFalse(); in castingTest()
1526 BoolExpr f = ctx.mkFalse(); in iteExample()
|
| /dports/math/R/R-4.1.2/src/include/ |
| H A D | Defn.h | 991 # define mkFalse Rf_mkFalse macro
1226 SEXP mkFalse(void);
|
| /dports/math/libRmath/R-4.1.1/src/include/ |
| H A D | Defn.h | 991 # define mkFalse Rf_mkFalse macro
1226 SEXP mkFalse(void);
|
| /dports/math/R/R-4.1.2/src/main/ |
| H A D | objects.c | 1018 return mkFalse(); in inherits3()
1312 SEXP value = allowPrimitiveMethods ? mkTrue() : mkFalse(); in R_set_prim_method()
|
| /dports/math/libRmath/R-4.1.1/src/main/ |
| H A D | objects.c | 1018 return mkFalse(); in inherits3()
1312 SEXP value = allowPrimitiveMethods ? mkTrue() : mkFalse(); in R_set_prim_method()
|