/dports/math/z3/z3-z3-4.8.13/src/ast/rewriter/ |
H A D | seq_axioms.cpp | 104 add_clause(mk_eq(p, e)); in purify() 673 add_clause(eq1, ge0); in itos_axiom() 679 add_clause(~ge0, eq); in itos_axiom() 816 add_clause(le); in ubv2s_len_axiom() 817 add_clause(ge); in ubv2s_len_axiom() 839 add_clause(~ge); in ubv2s_len_axiom() 865 add_clause(eq); in ubv2ch_axiom() 978 add_clause(~eq, le); in le_axiom() 979 add_clause(~lt, le); in le_axiom() 1028 add_clause(ge, emp); in str_from_code_axiom() [all …]
|
/dports/math/py-cryptominisat/cryptominisat-5.8.0/tests/ |
H A D | implied_by_test.cpp | 59 s->add_clause(str_to_cl("1")); in TEST_F() 68 s->add_clause(str_to_cl("1, 2")); in TEST_F() 77 s->add_clause(str_to_cl("1, 2")); in TEST_F() 89 s->add_clause(str_to_cl("1, 2")); in TEST_F() 101 s->add_clause(str_to_cl("1, 2")); in TEST_F() 103 s->add_clause(str_to_cl("1, -2")); in TEST_F() 104 s->add_clause(str_to_cl("-1, 2")); in TEST_F() 113 s->add_clause(str_to_cl("1")); in TEST_F() 132 s->add_clause(str_to_cl("-1")); in TEST_F() 142 s->add_clause(str_to_cl("-1")); in TEST_F() [all …]
|
H A D | stp_test.cpp | 37 s.add_clause(str_to_cl("1, -2")); in add_clauses_for_simp_check() 38 s.add_clause(str_to_cl("-1, 2")); in add_clauses_for_simp_check() 41 s.add_clause(str_to_cl("3, -4")); in add_clauses_for_simp_check() 42 s.add_clause(str_to_cl("-3, 4")); in add_clauses_for_simp_check() 45 s.add_clause(str_to_cl("3, 2")); in add_clauses_for_simp_check() 46 s.add_clause(str_to_cl("4, 1")); in add_clauses_for_simp_check() 76 s.add_clause(str_to_cl("1,2")); in TEST() 77 s.add_clause(str_to_cl("1,-2")); in TEST() 90 s.add_clause(str_to_cl("1,2")); in TEST() 91 s.add_clause(str_to_cl("1,-2")); in TEST() [all …]
|
H A D | dump_test.cpp | 70 s.add_clause(str_to_cl("1")); in TEST_F() 82 s.add_clause(str_to_cl("1")); in TEST_F() 83 s.add_clause(str_to_cl("1, 2")); in TEST_F() 97 s.add_clause(str_to_cl("-4")); in TEST_F() 112 s.add_clause(str_to_cl("-4")); in TEST_F() 125 s.add_clause(str_to_cl("1, 2")); in TEST_F() 126 s.add_clause(str_to_cl("-1, -2")); in TEST_F() 139 s.add_clause(str_to_cl("-1, 2")); in TEST_F() 140 s.add_clause(str_to_cl("1, -2")); in TEST_F() 153 s.add_clause(str_to_cl("-1, -2, 3")); in TEST_F() [all …]
|
H A D | basic_test.cpp | 47 s.add_clause(str_to_cl("1")); in TEST() 57 s.add_clause(str_to_cl("1")); in TEST() 58 s.add_clause(str_to_cl("-1")); in TEST() 68 s.add_clause(str_to_cl("1")); in TEST() 69 s.add_clause(str_to_cl("-1")); in TEST() 85 s.add_clause(str_to_cl("1")); in TEST() 86 s.add_clause(str_to_cl("-1")); in TEST() 106 s.add_clause(str_to_cl("-1")); in TEST() 138 s->add_clause(str_to_cl("1")); in TEST() 166 s->add_clause(str_to_cl("1")); in TEST() [all …]
|
H A D | assump_test.cpp | 48 s->add_clause(vector<Lit>{Lit(0, false)}); in TEST_F() 57 s->add_clause(vector<Lit>{Lit(0, false)}); in TEST_F() 67 s->add_clause(vector<Lit>{Lit(0, false)}); in TEST_F() 79 s->add_clause(vector<Lit>{Lit(0, false)}); in TEST_F() 95 s->add_clause(vector<Lit>{Lit(0, false), Lit(1, false)}); in TEST_F() 107 s->add_clause(vector<Lit>{Lit(0, false), Lit(1, false)}); in TEST_F() 124 s->add_clause(vector<Lit>{Lit(0, false), Lit(1, true)}); in TEST_F() 125 s->add_clause(vector<Lit>{Lit(0, true), Lit(1, false)}); in TEST_F() 144 s->add_clause(vector<Lit>{Lit(0, false), Lit(1, true)}); //a V -b in TEST_F() 145 s->add_clause(vector<Lit>{Lit(0, true), Lit(1, false)}); //-a V b in TEST_F() [all …]
|
/dports/math/cryptominisat/cryptominisat-5.8.0/tests/ |
H A D | implied_by_test.cpp | 59 s->add_clause(str_to_cl("1")); in TEST_F() 68 s->add_clause(str_to_cl("1, 2")); in TEST_F() 77 s->add_clause(str_to_cl("1, 2")); in TEST_F() 89 s->add_clause(str_to_cl("1, 2")); in TEST_F() 101 s->add_clause(str_to_cl("1, 2")); in TEST_F() 103 s->add_clause(str_to_cl("1, -2")); in TEST_F() 104 s->add_clause(str_to_cl("-1, 2")); in TEST_F() 113 s->add_clause(str_to_cl("1")); in TEST_F() 132 s->add_clause(str_to_cl("-1")); in TEST_F() 142 s->add_clause(str_to_cl("-1")); in TEST_F() [all …]
|
H A D | stp_test.cpp | 37 s.add_clause(str_to_cl("1, -2")); in add_clauses_for_simp_check() 38 s.add_clause(str_to_cl("-1, 2")); in add_clauses_for_simp_check() 41 s.add_clause(str_to_cl("3, -4")); in add_clauses_for_simp_check() 42 s.add_clause(str_to_cl("-3, 4")); in add_clauses_for_simp_check() 45 s.add_clause(str_to_cl("3, 2")); in add_clauses_for_simp_check() 46 s.add_clause(str_to_cl("4, 1")); in add_clauses_for_simp_check() 76 s.add_clause(str_to_cl("1,2")); in TEST() 77 s.add_clause(str_to_cl("1,-2")); in TEST() 90 s.add_clause(str_to_cl("1,2")); in TEST() 91 s.add_clause(str_to_cl("1,-2")); in TEST() [all …]
|
H A D | dump_test.cpp | 70 s.add_clause(str_to_cl("1")); in TEST_F() 82 s.add_clause(str_to_cl("1")); in TEST_F() 83 s.add_clause(str_to_cl("1, 2")); in TEST_F() 97 s.add_clause(str_to_cl("-4")); in TEST_F() 112 s.add_clause(str_to_cl("-4")); in TEST_F() 125 s.add_clause(str_to_cl("1, 2")); in TEST_F() 126 s.add_clause(str_to_cl("-1, -2")); in TEST_F() 139 s.add_clause(str_to_cl("-1, 2")); in TEST_F() 140 s.add_clause(str_to_cl("1, -2")); in TEST_F() 153 s.add_clause(str_to_cl("-1, -2, 3")); in TEST_F() [all …]
|
H A D | basic_test.cpp | 47 s.add_clause(str_to_cl("1")); in TEST() 57 s.add_clause(str_to_cl("1")); in TEST() 58 s.add_clause(str_to_cl("-1")); in TEST() 68 s.add_clause(str_to_cl("1")); in TEST() 69 s.add_clause(str_to_cl("-1")); in TEST() 85 s.add_clause(str_to_cl("1")); in TEST() 86 s.add_clause(str_to_cl("-1")); in TEST() 106 s.add_clause(str_to_cl("-1")); in TEST() 138 s->add_clause(str_to_cl("1")); in TEST() 166 s->add_clause(str_to_cl("1")); in TEST() [all …]
|
H A D | assump_test.cpp | 48 s->add_clause(vector<Lit>{Lit(0, false)}); in TEST_F() 57 s->add_clause(vector<Lit>{Lit(0, false)}); in TEST_F() 67 s->add_clause(vector<Lit>{Lit(0, false)}); in TEST_F() 79 s->add_clause(vector<Lit>{Lit(0, false)}); in TEST_F() 95 s->add_clause(vector<Lit>{Lit(0, false), Lit(1, false)}); in TEST_F() 107 s->add_clause(vector<Lit>{Lit(0, false), Lit(1, false)}); in TEST_F() 124 s->add_clause(vector<Lit>{Lit(0, false), Lit(1, true)}); in TEST_F() 125 s->add_clause(vector<Lit>{Lit(0, true), Lit(1, false)}); in TEST_F() 144 s->add_clause(vector<Lit>{Lit(0, false), Lit(1, true)}); //a V -b in TEST_F() 145 s->add_clause(vector<Lit>{Lit(0, true), Lit(1, false)}); //-a V b in TEST_F() [all …]
|
/dports/math/clingo/clingo-5.5.1/app/clingo/tests/python/ |
H A D | add-clause-py.lp | 15 init.add_clause([-b, l]) 17 init.add_clause([-l, b]) 19 init.add_clause([-c, l]) 21 init.add_clause([-l, c]) 32 init.add_clause([b]) 34 init.add_clause([b]) 37 init.add_clause([]) 39 init.add_clause([a]) 41 init.add_clause([b]) 43 init.add_clause([-a]) [all …]
|
/dports/math/clingo/clingo-5.5.1/app/clingo/tests/lua/ |
H A D | add-clause-lua.lp | 21 init:add_clause({-b, l}) 23 init:add_clause({-l, b}) 25 init:add_clause({-c, l}) 27 init:add_clause({-l, c}) 39 init:add_clause({b}) 41 init:add_clause({b}) 45 init:add_clause({}) 47 init:add_clause({a}) 49 init:add_clause({b}) 51 init:add_clause({-a}) [all …]
|
/dports/math/py-z3-solver/z3-z3-4.8.10/src/sat/smt/ |
H A D | arith_axioms.cpp | 29 add_clause(eqz, eq); in mk_div_axiom() 39 add_clause(eq); in mk_to_int_axiom() 47 add_clause(llo); in mk_to_int_axiom() 48 add_clause(~lhi); in mk_to_int_axiom() 117 add_clause(eq); in mk_idiv_mod_axioms() 118 add_clause(mod_ge_0); in mk_idiv_mod_axioms() 152 add_clause(lits); in mk_idiv_mod_axioms() 167 add_clause(~dgez, pos); in mk_rem_axiom() 168 add_clause(dgez, neg); in mk_rem_axiom() 364 add_clause(~eq, le); in mk_eq_axiom() [all …]
|
H A D | sat_th.cpp | 129 ctx.s().add_clause(1, &lit, mk_status()); in add_unit() 141 bool th_euf_solver::add_clause(sat::literal a, sat::literal b) { in add_clause() function in euf::th_euf_solver 144 ctx.s().add_clause(2, lits, mk_status()); in add_clause() 151 ctx.s().add_clause(3, lits, mk_status()); in add_clause() 158 ctx.s().add_clause(4, lits, mk_status()); in add_clause() 162 bool th_euf_solver::add_clause(sat::literal_vector const& lits) { in add_clause() function in euf::th_euf_solver 166 s().add_clause(lits.size(), lits.c_ptr(), mk_status()); in add_clause() 171 add_clause(~a, b); in add_equiv() 172 add_clause(a, ~b); in add_equiv() 177 add_clause(~a, b); in add_equiv_and() [all …]
|
/dports/math/z3/z3-z3-4.8.13/src/sat/smt/ |
H A D | arith_axioms.cpp | 29 add_clause(eqz, eq); in mk_div_axiom() 39 add_clause(eq); in mk_to_int_axiom() 47 add_clause(llo); in mk_to_int_axiom() 48 add_clause(~lhi); in mk_to_int_axiom() 117 add_clause(eq); in mk_idiv_mod_axioms() 118 add_clause(mod_ge_0); in mk_idiv_mod_axioms() 152 add_clause(lits); in mk_idiv_mod_axioms() 167 add_clause(~dgez, pos); in mk_rem_axiom() 168 add_clause(dgez, neg); in mk_rem_axiom() 376 add_clause(~eq, le); in mk_diseq_axiom() [all …]
|
H A D | sat_th.cpp | 134 ctx.s().add_clause(1, &lit, mk_status()); in add_unit() 146 bool th_euf_solver::add_clause(sat::literal a, sat::literal b) { in add_clause() function in euf::th_euf_solver 149 ctx.s().add_clause(2, lits, mk_status()); in add_clause() 156 ctx.s().add_clause(3, lits, mk_status()); in add_clause() 163 ctx.s().add_clause(4, lits, mk_status()); in add_clause() 167 bool th_euf_solver::add_clause(sat::literal_vector const& lits) { in add_clause() function in euf::th_euf_solver 171 s().add_clause(lits.size(), lits.data(), mk_status()); in add_clause() 176 add_clause(~a, b); in add_equiv() 177 add_clause(a, ~b); in add_equiv() 182 add_clause(~a, b); in add_equiv_and() [all …]
|
/dports/math/minizinc/libminizinc-2.5.5/solvers/geas/ |
H A D | geas_constraints.cpp | 395 geas::add_clause(SD, BOOLVAR(2), ~BOOLVAR(0)); in p_bool_or() 438 geas::add_clause(*SD, clause); in p_bool_clause() 447 geas::add_clause(SD, BOOLVAR(1), ~elem); in p_array_bool_or() 450 geas::add_clause(*SD, clause); in p_array_bool_or() 459 geas::add_clause(SD, ~BOOLVAR(1), elem); in p_array_bool_and() 462 geas::add_clause(*SD, clause); in p_array_bool_and() 476 geas::add_clause(*SD, clause); in p_bool_clause_imp() 487 geas::add_clause(*SD, clause); in p_array_bool_or_imp() 504 geas::add_clause(SD, BOOLVAR(2), ~elem); in p_bool_clause_reif() 509 geas::add_clause(SD, BOOLVAR(2), elem); in p_bool_clause_reif() [all …]
|
/dports/math/py-cryptominisat/cryptominisat-5.8.0/python/tests/ |
H A D | test_pycryptosat.py | 170 self.solver.add_clause(out) 187 self.assertRaises(TypeError, self.solver.add_clause, 'A') 188 self.assertRaises(TypeError, self.solver.add_clause, 1) 202 self.solver.add_clause(cl) 267 self.solver.add_clause(cl) 272 self.solver.add_clause(cl) 281 self.solver.add_clause(cl) 287 self.solver.add_clause([-1, -2, 3]) 291 self.solver.add_clause([-5, 1]) 292 self.solver.add_clause([4, -3]) [all …]
|
/dports/math/cryptominisat/cryptominisat-5.8.0/python/tests/ |
H A D | test_pycryptosat.py | 170 self.solver.add_clause(out) 187 self.assertRaises(TypeError, self.solver.add_clause, 'A') 188 self.assertRaises(TypeError, self.solver.add_clause, 1) 202 self.solver.add_clause(cl) 267 self.solver.add_clause(cl) 272 self.solver.add_clause(cl) 281 self.solver.add_clause(cl) 287 self.solver.add_clause([-1, -2, 3]) 291 self.solver.add_clause([-5, 1]) 292 self.solver.add_clause([4, -3]) [all …]
|
/dports/textproc/p5-KinoSearch1/KinoSearch1-1.01/t/ |
H A D | 503-booleanquery.t | 39 $bool_query->add_clause( 47 $bool_query->add_clause( 55 $bool_query->add_clause( 64 $bool_query->add_clause( query => $c_query, occur => 'SHOULD' ); 66 $sub_query->add_clause( query => $d_query, occur => 'SHOULD', ); 67 $sub_query->add_clause( query => $e_query, occur => 'SHOULD', ); 68 $bool_query->add_clause( query => $sub_query, occur => 'SHOULD' );
|
/dports/math/z3/z3-z3-4.8.13/src/sat/ |
H A D | sat_solver_core.h | 37 virtual void add_clause(unsigned n, literal* lits, status st) = 0; 38 void add_clause(literal l1, literal l2, status st) { in add_clause() function 40 add_clause(2, lits, st); in add_clause() 42 void add_clause(literal l1, literal l2, literal l3, status st) { in add_clause() function 44 add_clause(3, lits, st); in add_clause()
|
/dports/math/py-z3-solver/z3-z3-4.8.10/src/util/ |
H A D | sorting_network.h | 618 add_clause(lits); in add_implies_or() 753 add_clause(ands); in mk_at_most_1() 780 add_clause(lits); in mk_at_most_1_small() 985 add_clause(3, lits); in add_clause() 989 add_clause(2, lits); in add_clause() 1007 add_clause(mk_not(y2), x1); in cmp_ge() 1008 add_clause(mk_not(y2), x2); in cmp_ge() 1015 add_clause(mk_not(x1), y1); in cmp_le() 1016 add_clause(mk_not(x2), y1); in cmp_le() 1417 add_clause(ls); in dsmerge() [all …]
|
/dports/math/z3/z3-z3-4.8.13/src/util/ |
H A D | sorting_network.h | 618 add_clause(lits); in add_implies_or() 753 add_clause(ands); in mk_at_most_1() 780 add_clause(lits); in mk_at_most_1_small() 985 add_clause(3, lits); in add_clause() 989 add_clause(2, lits); in add_clause() 1007 add_clause(mk_not(y2), x1); in cmp_ge() 1008 add_clause(mk_not(y2), x2); in cmp_ge() 1015 add_clause(mk_not(x1), y1); in cmp_le() 1016 add_clause(mk_not(x2), y1); in cmp_le() 1417 add_clause(ls); in dsmerge() [all …]
|
/dports/math/py-z3-solver/z3-z3-4.8.10/src/sat/ |
H A D | sat_solver_core.h | 59 virtual void add_clause(unsigned n, literal* lits, status st) = 0; 60 void add_clause(literal l1, literal l2, status st) { in add_clause() function 62 add_clause(2, lits, st); in add_clause() 64 void add_clause(literal l1, literal l2, literal l3, status st) { in add_clause() function 66 add_clause(3, lits, st); in add_clause()
|