Home
last modified time | relevance | path

Searched refs:mkAnd (Results 1 – 25 of 114) sorted by relevance

12345

/dports/math/cvc4/CVC4-1.7/src/theory/bv/bitblast/
H A Dbitblast_utils.h55 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 Dbitblast_strategies_template.h66 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 Daig_bitblaster.cpp88 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 Dbv_subtheory_bitblast.cpp166 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 Dtheory_bv_utils.h138 Node mkAnd(TNode node1, TNode node2);
141 Node mkAnd(const std::vector<NodeTemplate<ref_count>>& conjunctions) in mkAnd() function
H A Dbv_quick_check.cpp48 Node confl = utils::mkAnd(conflict); in setConflict()
351 return utils::mkAnd(minimized); in minimizeConflict()
H A Dbv_eager_solver.cpp108 Node query = utils::mkAnd(assertions); in checkSat()
H A Dtheory_bv_utils.cpp324 Node mkAnd(TNode node1, TNode node2) in mkAnd() function
457 return mkAnd(children); in flattenAnd()
H A Dbv_inequality_graph.cpp363 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 DJavaExample.java549 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 DJavaGenericExample.java519 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 DJavaExample.java549 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 DJavaGenericExample.java519 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 DBooleanFormula.hs12 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 DBooleanFormula.hs12 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 DBooleanFormula.hs12 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 DBooleanFormula.hs12 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 Dshared_terms_database.cpp215 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 Dregexp_solver.h73 Node mkAnd(Node c1, Node c2);
/dports/math/z3/z3-z3-4.8.13/src/api/java/
H A DGoal.java229 return getContext().mkAnd(getFormulas()); in AsBoolExpr()
/dports/math/py-z3-solver/z3-z3-4.8.10/src/api/java/
H A DGoal.java229 return getContext().mkAnd(getFormulas()); in AsBoolExpr()
/dports/math/cvc4/CVC4-1.7/src/preprocessing/passes/
H A Dbv_ackermann.cpp61 args_eq = bv::utils::mkAnd(eqs); in addLemmaForPair()
/dports/math/cvc4/CVC4-1.7/src/theory/datatypes/
H A Dtheory_datatypes.cpp779 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 Dproof_utils.h171 inline Expr mkAnd(const std::vector<Expr>& conjunctions) { in mkAnd() function
/dports/math/fricas/fricas-1.3.7/src/interp/
H A Dcategory.boot140 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]

12345