Searched refs:mk_nary_clause (Results 1 – 4 of 4) sorted by relevance
| /dports/math/z3/z3-z3-4.8.13/src/sat/ |
| H A D | sat_solver.h | 302 clause * mk_nary_clause(unsigned num_lits, literal * lits, status st);
|
| H A D | sat_solver.cpp | 453 return mk_nary_clause(num_lits, lits, st); in mk_clause_core()
592 clause * solver::mk_nary_clause(unsigned num_lits, literal * lits, sat::status st) { in mk_nary_clause() function in sat::solver
|
| /dports/math/py-z3-solver/z3-z3-4.8.10/src/sat/ |
| H A D | sat_solver.h | 291 clause * mk_nary_clause(unsigned num_lits, literal * lits, status st);
|
| H A D | sat_solver.cpp | 447 return mk_nary_clause(num_lits, lits, st);
586 clause * solver::mk_nary_clause(unsigned num_lits, literal * lits, sat::status st) {
|