21 #define _CVC3_TRUSTED_
35 bool printStats,
bool createProof)
36 :
DPLLT(theoryAPI, decider), d_printStats(printStats),
37 d_createProof(createProof), d_proof(NULL) {
80 cout <<
"Instance unsatisfiable" <<
endl;
83 cout <<
"aborted, unable to determine the satisfiablility of the instance" <<
endl;
86 cout <<
"unknown, unable to determing the satisfiablility of the instance" <<
endl;
89 FatalAssert(
false,
"DPLTBasic::handle_result: Unknown outcome");
94 cout <<
"Number of Propositional Conflicts\t"
97 cout <<
"Number of Variables\t\t\t" << solver->
nVars() <<
endl;
98 cout <<
"Number of Literals\t\t\t"
101 cout <<
"Number of Clauses\t\t\t" << solver->
getClauses().size() <<
endl;
102 cout <<
"Number of Lemmas\t\t\t" << solver->
getLemmas().size() <<
endl;
246 "DPLLTMiniSat::getValue: should be called after a previous satisfiable result");
295 pfs.push_back(leftProof);
296 pfs.push_back(rightProof);
322 pf = thmProducer->
newPf(
"bool_resolution", e_trans, pfs);
335 cout<<
"theorem null"<<
endl;
338 cout<<
"====================" <<
endl;