/dports/math/cvc4/CVC4-1.7/src/theory/bv/bitblast/ |
H A D | bitblast_utils.h | 55 template <class T> T mkAnd(T a, T b); 92 Node mkAnd<Node>(Node a, Node b) { 194 carry = mkOr( mkAnd(a[i], b[i]), in rippleCarryAdder() 195 mkAnd( mkXor(a[i], b[i]), in rippleCarryAdder() 207 res.push_back(mkAnd(b[0], a[i])); in shiftAddMultiplier() 214 T aj = mkAnd(b[k], a[j]); in shiftAddMultiplier() 227 T res = mkAnd(mkNot(a[0]), b[0]); in uLessThanBB() 236 mkAnd(mkNot(a[i]), b[i])); in uLessThanBB() 250 return mkAnd(a[0], mkNot(b[0])); in sLessThanBB() 260 mkAnd(mkIff(a[n], b[n]), in sLessThanBB() [all …]
|
H A D | bitblast_strategies_template.h | 66 T bv_eq = mkAnd(bits_eq); in DefaultEqBB() 85 carry = mkOr( mkAnd(a[i], not_b[i]), in AdderUltBB() 86 mkAnd( mkXor(a[i], not_b[i]), in AdderUltBB() 266 bits[i] = mkAnd(bits[i], current[i]); in DefaultAndBB() 355 T a_eq_b = mkAnd(bit_eqs); in DefaultCompBB() 540 T b_is_0 = mkAnd(iszero); in DefaultUdivBB() 573 T b_is_0 = mkAnd(iszero); in DefaultUremBB() 823 res.push_back(mkAnd(mkOr(mkNot(cond[0]),thenpart[i]),mkOr(cond[0],elsepart[i]))); in DefaultIteBB()
|
H A D | aig_bitblaster.cpp | 88 Abc_Obj_t* mkAnd<Abc_Obj_t*>(Abc_Obj_t* a, Abc_Obj_t* b) { in mkAnd() function 93 Abc_Obj_t* mkAnd<Abc_Obj_t*>(const std::vector<Abc_Obj_t*>& children) { in mkAnd() function 190 result = mkAnd(result, child); in bbFormula()
|
/dports/math/cvc4/CVC4-1.7/src/theory/bv/ |
H A D | bv_subtheory_bitblast.cpp | 166 setConflict(utils::mkAnd(conflictAtoms)); in check() 182 setConflict(utils::mkAnd(conflictAtoms)); in check() 199 Node conflict = utils::mkAnd(conflictAtoms); in check() 225 setConflict(utils::mkAnd(conflictAtoms)); in check() 236 Node conflict = utils::mkAnd(conflictAtoms); in check()
|
H A D | theory_bv_utils.h | 138 Node mkAnd(TNode node1, TNode node2); 141 Node mkAnd(const std::vector<NodeTemplate<ref_count>>& conjunctions) in mkAnd() function
|
H A D | bv_quick_check.cpp | 48 Node confl = utils::mkAnd(conflict); in setConflict() 351 return utils::mkAnd(minimized); in minimizeConflict()
|
H A D | bv_eager_solver.cpp | 108 Node query = utils::mkAnd(assertions); in checkSat()
|
H A D | theory_bv_utils.cpp | 324 Node mkAnd(TNode node1, TNode node2) in mkAnd() function 457 return mkAnd(children); in flattenAnd()
|
H A D | bv_inequality_graph.cpp | 363 Node explanation = utils::mkAnd(explanation_nodes); in addDisequality() 376 Node explanation = utils::mkAnd(explanation_nodes); in addDisequality()
|
/dports/math/z3/z3-z3-4.8.13/examples/java/ |
H A D | JavaExample.java | 549 sudoku_c = ctx.mkAnd(ctx.mkAnd(t), sudoku_c); in sudokuExample() 550 sudoku_c = ctx.mkAnd(ctx.mkAnd(rows_c), sudoku_c); in sudokuExample() 551 sudoku_c = ctx.mkAnd(ctx.mkAnd(cols_c), sudoku_c); in sudokuExample() 553 sudoku_c = ctx.mkAnd(ctx.mkAnd(t), sudoku_c); in sudokuExample() 566 instance_c = ctx.mkAnd( in sudokuExample() 616 Expr body_vars = ctx.mkAnd( in quantifierExample1() 621 Expr body_const = ctx.mkAnd( in quantifierExample1() 1171 BoolExpr q = ctx.mkAnd(c1, c2); in findModelExample2() 1182 q = ctx.mkAnd(q, c3); in findModelExample2() 2052 BoolExpr f1 = ctx.mkAnd(pa, pb, pc); in unsatCoreAndProofExample() [all …]
|
H A D | JavaGenericExample.java | 519 BoolExpr sudoku_c = ctx.mkAnd(sudoku_s.toArray(BoolExpr[]::new)); in sudokuExample() 568 BoolExpr body_vars = ctx.mkAnd( in quantifierExample1() 573 BoolExpr body_const = ctx.mkAnd( in quantifierExample1() 962 BoolExpr q = ctx.mkAnd(c1, c2); in findModelExample2() 972 q = ctx.mkAnd(q, c3); in findModelExample2() 1858 BoolExpr f1 = ctx.mkAnd(pa, pb, pc); in unsatCoreAndProofExample() 1859 BoolExpr f2 = ctx.mkAnd(pa, ctx.mkNot(pb), pc); in unsatCoreAndProofExample() 1895 BoolExpr f1 = ctx.mkAnd(new BoolExpr[] { pa, pb, pc }); in unsatCoreAndProofExample2() 1896 BoolExpr f2 = ctx.mkAnd(new BoolExpr[] { pa, ctx.mkNot(pb), pc }); in unsatCoreAndProofExample2() 1955 BoolExpr a = ctx.mkAnd(ctx.mkFPEq(x, y), ctx.mkFPEq(y, z)); in floatingPointExample1() [all …]
|
/dports/math/py-z3-solver/z3-z3-4.8.10/examples/java/ |
H A D | JavaExample.java | 549 sudoku_c = ctx.mkAnd(ctx.mkAnd(t), sudoku_c); in sudokuExample() 550 sudoku_c = ctx.mkAnd(ctx.mkAnd(rows_c), sudoku_c); in sudokuExample() 551 sudoku_c = ctx.mkAnd(ctx.mkAnd(cols_c), sudoku_c); in sudokuExample() 553 sudoku_c = ctx.mkAnd(ctx.mkAnd(t), sudoku_c); in sudokuExample() 566 instance_c = ctx.mkAnd( in sudokuExample() 616 Expr body_vars = ctx.mkAnd( in quantifierExample1() 621 Expr body_const = ctx.mkAnd( in quantifierExample1() 1171 BoolExpr q = ctx.mkAnd(c1, c2); in findModelExample2() 1182 q = ctx.mkAnd(q, c3); in findModelExample2() 2052 BoolExpr f1 = ctx.mkAnd(pa, pb, pc); in unsatCoreAndProofExample() [all …]
|
H A D | JavaGenericExample.java | 519 BoolExpr sudoku_c = ctx.mkAnd(sudoku_s.toArray(BoolExpr[]::new)); 568 BoolExpr body_vars = ctx.mkAnd( 573 BoolExpr body_const = ctx.mkAnd( 931 BoolExpr q = ctx.mkAnd(c1, c2); 941 q = ctx.mkAnd(q, c3); 1827 BoolExpr f1 = ctx.mkAnd(pa, pb, pc); 1828 BoolExpr f2 = ctx.mkAnd(pa, ctx.mkNot(pb), pc); 1864 BoolExpr f1 = ctx.mkAnd(new BoolExpr[] { pa, pb, pc }); 1865 BoolExpr f2 = ctx.mkAnd(new BoolExpr[] { pa, ctx.mkNot(pb), pc }); 1924 BoolExpr a = ctx.mkAnd(ctx.mkFPEq(x, y), ctx.mkFPEq(y, z)); [all …]
|
/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, 54 mkAnd :: Eq a => [LBooleanFormula a] -> BooleanFormula a 55 mkAnd = maybe mkFalse (mkAnd' . nub) . concatMapM fromAnd function 137 simplify f (And xs) = mkAnd (map (\(L l x) -> L l (simplify f x)) xs)
|
/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, 54 mkAnd :: Eq a => [LBooleanFormula a] -> BooleanFormula a 55 mkAnd = maybe mkFalse (mkAnd' . nub) . concatMapM fromAnd function 137 simplify f (And xs) = mkAnd (map (\(L l x) -> L l (simplify f x)) xs)
|
/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, 55 mkAnd :: Eq a => [LBooleanFormula a] -> BooleanFormula a 56 mkAnd = maybe mkFalse (mkAnd' . nub) . concatMapM fromAnd function 138 simplify f (And xs) = mkAnd (map (\(L l x) -> L l (simplify f x)) xs)
|
/dports/lang/ghc/ghc-8.10.7/compiler/utils/ |
H A D | BooleanFormula.hs | 12 mkFalse, mkTrue, mkAnd, mkOr, mkVar, 54 mkAnd :: Eq a => [LBooleanFormula a] -> BooleanFormula a 55 mkAnd = maybe mkFalse (mkAnd' . nub) . concatMapM fromAnd function 137 simplify f (And xs) = mkAnd (map (\(L l x) -> L l (simplify f x)) xs)
|
/dports/math/cvc4/CVC4-1.7/src/theory/ |
H A D | shared_terms_database.cpp | 215 static Node mkAnd(const std::vector<TNode>& conjunctions) { in mkAnd() function 242 Node conflict = mkAnd(assumptions); in checkForConflict() 264 return mkAnd(assumptions); in explain()
|
/dports/math/cvc4/CVC4-1.7/src/theory/strings/ |
H A D | regexp_solver.h | 73 Node mkAnd(Node c1, Node c2);
|
/dports/math/z3/z3-z3-4.8.13/src/api/java/ |
H A D | Goal.java | 229 return getContext().mkAnd(getFormulas()); in AsBoolExpr()
|
/dports/math/py-z3-solver/z3-z3-4.8.10/src/api/java/ |
H A D | Goal.java | 229 return getContext().mkAnd(getFormulas()); in AsBoolExpr()
|
/dports/math/cvc4/CVC4-1.7/src/preprocessing/passes/ |
H A D | bv_ackermann.cpp | 61 args_eq = bv::utils::mkAnd(eqs); in addLemmaForPair()
|
/dports/math/cvc4/CVC4-1.7/src/theory/datatypes/ |
H A D | theory_datatypes.cpp | 779 return mkAnd( assumptions ); in explain() 787 return mkAnd( assumptions ); in explain() 1061 d_conflictNode = mkAnd( assumptions ); in addTester() 1178 d_conflictNode = mkAnd( assumptions ); in addTester() 1236 d_conflictNode = mkAnd( assumptions ); in addConstructor() 1830 d_conflictNode = mkAnd( expl ); in checkCycles() 1882 Node eqExp = mkAnd( exp ); in checkCycles() 2203 Node TheoryDatatypes::mkAnd( std::vector< TNode >& assumptions ) { in mkAnd() function in CVC4::theory::datatypes::TheoryDatatypes 2288 Node exp = mkAnd( exp_c ); in entailmentCheck()
|
/dports/math/cvc4/CVC4-1.7/src/proof/ |
H A D | proof_utils.h | 171 inline Expr mkAnd(const std::vector<Expr>& conjunctions) { in mkAnd() function
|
/dports/math/fricas/fricas-1.3.7/src/interp/ |
H A D | category.boot | 140 mkAnd(a,b) == 232 -- ll := [[CatEval xf, mkAnd(cond1, xc)] for [xf, xc] in CADR f1.4] 233 ll := [[CatEval first x, mkAnd(cond1, get_cond(x))] for x in CADR f1.4]
|