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;
Data structure of expressions in CVC3.
TheoremManager * getTM() const
This theory handles the built-in logical connectives plus equality. It also handles the registration ...
std::vector< std::vector< SAT::Lit > > curClauses()
CVC3::QueryResult search()
void addFormula(const SAT::CNF_Formula &cnf, bool isTheoryClause)
Implementation of dpllt module based on minisat.
bool isConsistent() const
#define DebugAssert(cond, str)
const std::vector< Clause * > & getLemmas() const
virtual std::vector< std::vector< SAT::Lit > > getCurClauses()
CVC3::ExprStream & endl(CVC3::ExprStream &os)
Print the end-of-line.
const SolverStats & getStats() const
Statistics.
Sat solver proof representation.
CVC3::Proof getNodeProof()
void printSatProof(SAT::SatProofNode *node)
virtual void addAssertion(const CNF_Formula &cnf)
Add new clauses to the SAT solver.
#define FatalAssert(cond, msg)
If something goes horribly wrong, print a message and abort immediately with exit(1).
CVC3::Proof getSatProof(CNF_Manager *, CVC3::TheoryCore *)
Get the proof from SAT engine.
virtual std::vector< SAT::Lit > getCurAssignments()
Var cvcToMiniSat(const SAT::Var &var)
virtual CVC3::QueryResult checkSat(const CNF_Formula &cnf)
Check the satisfiability of a set of clauses in the current context.
virtual void push()
Set a checkpoint for backtracking.
std::vector< SAT::Lit > curAssigns()
virtual void pop()
Restore checkpoint.
SatProofNode * getLeftParent()
CVC3::QueryResult search()
search
virtual Var::Val getValue(Var v)
Get value of variable: unassigned, false, or true.
CVC3::Expr concreteLit(Lit l, bool checkTranslated=true)
Convert a CNF literal to an Expr literal.
SatProofNode * getRightParent()
virtual void push()=0
Set a checkpoint for backtracking.
virtual CVC3::QueryResult continueCheck(const CNF_Formula &cnf)
Continue checking the last check with additional constraints.
void setNodeProof(CVC3::Proof pf)
Proof newPf(const std::string &name)
static Solver * createFrom(const Solver *solver)
CVC3::Proof generateSatProof(SAT::SatProofNode *node, CNF_Manager *cnfManager, TheoremProducer *thmProducer)
virtual void pop()=0
Restore most recent checkpoint.
virtual void assertLit(Lit l)=0
Notify theory when a literal is set to true.
MiniSat::Solver * getActiveSolver()
Adaptation of MiniSat to DPLL(T)
std::stack< MiniSat::Solver * > d_solvers
const std::vector< Clause * > & getClauses() const
lbool getValue(Var x) const
clauses / assignment