Searched refs:satProof (Results 1 – 8 of 8) sorted by relevance
/dports/math/cvc4/CVC4-1.7/src/proof/ |
H A D | lfsc_proof_printer.cpp | 34 if (satProof->isInputClause(id)) in clauseName() 38 else if (satProof->isLemmaClause(id)) in clauseName() 68 out << " " << clauseName(satProof, start_id); in printResolution() 78 if (id == satProof->getEmptyClauseId()) in printResolution() 94 Assert(satProof->isAssumptionConflict(id)); in printAssumptionsResolution() 96 printResolution(satProof, id, out, paren); in printAssumptionsResolution() 111 out << clauseName(satProof, id) << " "; in printAssumptionsResolution() 132 if (*it != satProof->getEmptyClauseId()) in printResolutions() 146 printResolution(satProof, satProof->getEmptyClauseId(), out, paren); in printResolutionEmptyClause() 190 TSatProof<CVC4::Minisat::Solver>* satProof, [all …]
|
H A D | lfsc_proof_printer.h | 47 static void printAssumptionsResolution(TSatProof<Solver>* satProof, 61 static void printResolutions(TSatProof<Solver>* satProof, 73 static void printResolutionEmptyClause(TSatProof<Solver>* satProof, 134 static std::string clauseName(TSatProof<Solver>* satProof, ClauseId id); 145 static void printResolution(TSatProof<Solver>* satProof,
|
/dports/math/cvc3/cvc3-2.4.1/src/search/ |
H A D | search_rules.h | 257 virtual Theorem satProof(const Expr& queryExpr, const Proof& satProof) = 0;
|
H A D | search_theorem_producer.h | 191 Theorem satProof(const Expr& queryExpr, const Proof& satProof);
|
H A D | search_theorem_producer.cpp | 91 satProof(a, pf); in proofByContradiction() 1419 Theorem SearchEngineTheoremProducer::satProof(const Expr& queryExpr, const Proof& satProof) { in satProof() argument 1422 pf = newPf("minisat_proof", queryExpr, satProof); in satProof()
|
H A D | search_sat.cpp | 721 d_lastValid = d_rules->satProof(e2, pf); in check()
|
/dports/cad/abc/abc-a4518e6f833885c905964f1233d11e5b941ec24c/src/sat/bsat/ |
H A D | module.make | 6 src/sat/bsat/satProof.c \
|
/dports/cad/abc/abc-a4518e6f833885c905964f1233d11e5b941ec24c/ |
H A D | abclib.dsp | 1842 SOURCE=.\src\sat\bsat\satProof.c
|