Searched defs:proof_id (Results 1 – 4 of 4) sorted by relevance
| /dports/cad/abc/abc-a4518e6f833885c905964f1233d11e5b941ec24c/src/sat/bsat/ |
| H A D | satSolver2.c | 408 static int clause2_create_new(sat_solver2* s, lit* begin, lit* end, int learnt, int proof_id ) in clause2_create_new()
540 static void solver2_record(sat_solver2* s, veci* cls, int proof_id) in solver2_record()
785 int proof_id = 0; in solver2_analyze() local
950 int k, x, proof_id, Cid, Var = lit_var(Lit); in solver2_propagate() local
1008 int proof_id; in solver2_search() local
1366 int x, k, proof_id, CidNew; in sat_solver2_addclause() local
1840 int proof_id; in sat_solver2_solve() local
|
| /dports/math/z3/z3-z3-4.8.13/src/smt/ |
| H A D | qi_queue.cpp | 184 …f, quantifier * q, unsigned num_bindings, enode * const * bindings, unsigned proof_id, unsigned ge… in display_instance_profile()
270 unsigned proof_id = 0; in instantiate() local
|
| /dports/math/py-z3-solver/z3-z3-4.8.10/src/smt/ |
| H A D | qi_queue.cpp | 184 …f, quantifier * q, unsigned num_bindings, enode * const * bindings, unsigned proof_id, unsigned ge… in display_instance_profile()
268 unsigned proof_id = 0; in instantiate() local
|
| /dports/math/cvc4/CVC4-1.7/src/prop/ |
| H A D | cnf_stream.cpp | 679 ProofRule proof_id, in convertAndAssert()
|