Home
last modified time | relevance | path

Searched refs:add_clause (Results 1 – 25 of 465) sorted by relevance

12345678910>>...19

/dports/math/z3/z3-z3-4.8.13/src/ast/rewriter/
H A Dseq_axioms.cpp104 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 Dimplied_by_test.cpp59 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 Dstp_test.cpp37 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 Ddump_test.cpp70 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 Dbasic_test.cpp47 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 Dassump_test.cpp48 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 Dimplied_by_test.cpp59 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 Dstp_test.cpp37 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 Ddump_test.cpp70 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 Dbasic_test.cpp47 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 Dassump_test.cpp48 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 Dadd-clause-py.lp15 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 Dadd-clause-lua.lp21 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 Darith_axioms.cpp29 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 Dsat_th.cpp129 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 Darith_axioms.cpp29 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 Dsat_th.cpp134 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 Dgeas_constraints.cpp395 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 Dtest_pycryptosat.py170 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 Dtest_pycryptosat.py170 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 D503-booleanquery.t39 $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 Dsat_solver_core.h37 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 Dsorting_network.h618 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 Dsorting_network.h618 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 Dsat_solver_core.h59 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()

12345678910>>...19