41 for (; change > 0; change--) {
44 for (; change < 0; change++) {
79 if (result == DPLLT::MAYBE_CONSISTENT) {
88 else if (result == DPLLT::INCONSISTENT) {
102 TRACE(
"DPLL Assign", var.
id,
" := ", value);
111 if (result == DPLLT::INCONSISTENT) {
137 void DPLLTBasic::createManager()
151 vector<SatSolver::Lit> clause;
152 if (cnf.
numVars() > unsigned(d_mng->NumVariables())) {
153 d_mng->AddVariables(cnf.
numVars() - d_mng->NumVariables());
156 for (i = cnf.
end()-1, iend = cnf.
begin()-1; i != iend; --i) {
158 if ((*i).isSatisfied())
continue;
159 for (j = (*i).begin(), jend = (*i).end(); j != jend; ++j) {
160 if (!(*j).isFalse()) clause.push_back(cvc2SAT(*j));
162 if (clause.size() != 0) {
163 d_mng->AddClause(clause);
172 const char * result =
"UNKNOWN";
196 if (d_printStats) cout <<
"Instance unsatisfiable" <<
endl;
199 result =
"ABORT : TIME OUT";
200 cout <<
"Time out, unable to determine the satisfiablility of the instance";
204 result =
"ABORT : MEM OUT";
205 cout <<
"Memory out, unable to determing the satisfiablility of the instance";
209 throw Exception(
"DPLTBasic::handle_result: Unknown outcome");
211 if (d_printStats) d_mng->PrintStatistics();
215 void DPLLTBasic::verify_solution()
221 cl = d_mng->GetNextClause(cl)) {
222 vector<SatSolver::Lit> lits;
223 d_mng->GetClauseLits(cl, &lits);
224 for (; lits.size() != 0;) {
227 int sign = d_mng->GetPhaseFromLit(lit);
228 int var_value = d_mng->GetVarAssignment(var);
229 if( (var_value == 1 && sign == 0) ||
230 (var_value == 0 && sign == 1) ||
231 (var_value == -1) )
break;
234 DebugAssert(lits.size() != 0,
"DPLLTBasic::verify_solution failed");
241 :
DPLLT(theoryAPI, decider), d_cm(cm), d_ready(true),
242 d_printStats(printStats),
243 d_pushLevel(cm->getCurrentContext(), 0),
244 d_readyPrev(cm->getCurrentContext(), true),
245 d_prevStackSize(cm->getCurrentContext(), 0),
246 d_prevAStackSize(cm->getCurrentContext(), 0)
279 "Expected no new variables");
280 vector<SatSolver::Lit> lits;
282 if (!(*i).isFalse()) lits.push_back(
cvc2SAT(*i));
293 vector<SatSolver::Lit> clause;
298 for (i = cnf.
end()-1, iend = cnf.
begin()-1; i != iend; --i) {
300 if ((*i).isSatisfied())
continue;
301 for (j = (*i).begin(), jend = (*i).end(); j != jend; ++j) {
302 if (!(*j).isFalse()) clause.push_back(
cvc2SAT(*j));
304 if (clause.size() != 0) {
369 std::vector<SAT::Lit> nothing;
374 std::vector<std::vector<SAT::Lit> > nothing;
384 for (i = cnf.
end()-1, iend = cnf.
begin()-1; i != iend; --i) {
392 (*d_assertions) += cnf;
413 else if (value == 0) {
478 (
"continueCheck should be called after a previous satisfiable result");
482 (
"a check cannot be continued if new assertions have been made");
Basic classes for reasoning about formulas in CNF.
virtual int GetVarAssignment(Var var)=0
void handle_result(SatSolver::SATStatus outcome)
const_iterator begin() const
unsigned getMaxVar() const
This theory handles the built-in logical connectives plus equality. It also handles the registration ...
virtual int NumVariables()=0
std::vector< CD_CNF_Formula * > d_assertionsStack
CVC3::CDO< bool > d_readyPrev
CVC3::CDO< unsigned > d_prevStackSize
static void SATDeductionHook(void *cookie)
static SatSolver::Lit SATDecisionHook(void *cookie, bool *done)
CVC3::CDO< unsigned > d_pushLevel
virtual Var AddVariables(int nvars)=0
static void SATDLevelHook(void *cookie, int change)
CVC3::QueryResult checkSat(const CNF_Formula &cnf)
Check the satisfiability of a set of clauses in the current context.
void generate_CDB(CNF_Formula_Impl &cnf)
virtual SATStatus Satisfiable(bool allowNewClauses=false)=0
#define DebugAssert(cond, str)
virtual SATStatus Continue()=0
void addNewClauses(CNF_Formula_Impl &cnf)
virtual bool outOfResources()=0
Check if the work budget has been exceeded.
CVC3::ExprStream & endl(CVC3::ExprStream &os)
Print the end-of-line.
Context * getCurrentContext()
virtual std::vector< SAT::Lit > getCurAssignments()
CVC3::CDO< unsigned > d_prevAStackSize
SatSolver::Lit cvc2SAT(Lit l)
CVC3::ContextManager * d_cm
virtual Clause AddClause(std::vector< Lit > &lits)=0
void addNewClause(const Clause &c)
static void SATAssignmentHook(void *cookie, SatSolver::Var var, int value)
A class representing a CNF clause (a smart pointer)
std::vector< CNF_Formula_Impl * > d_cnfStack
Basic implementation of dpllt module.
virtual Var GetVar(int varIndex)=0
virtual bool getNewClauses(CNF_Formula &cnf)=0
Get new clauses from the theory.
void pop()
Restore checkpoint.
virtual void getExplanation(Lit l, CNF_Formula &c)=0
Get an explanation for a literal that was implied.
std::vector< SatSolver * > d_mngStack
const_iterator end() const
std::vector< Lit >::const_iterator const_iterator
virtual std::vector< std::vector< SAT::Lit > > getCurClauses()
CVC3::Proof getSatProof(CNF_Manager *, CVC3::TheoryCore *)
Get the proof from SAT engine.
virtual Lit getImplication()=0
Get a literal that is implied by the current assignment.
virtual void push()=0
Set a checkpoint for backtracking.
static SatSolver * Create()
CVC3::QueryResult continueCheck(const CNF_Formula &cnf)
Continue checking the last check with additional constraints.
Manager for multiple contexts. Also holds current context.
virtual void pop()=0
Restore most recent checkpoint.
void addAssertion(const CNF_Formula &cnf)
Add new clauses to the SAT solver.
virtual Lit makeDecision()=0
Make a decision.
virtual void assertLit(Lit l)=0
Notify theory when a literal is set to true.
virtual ConsistentResult checkConsistent(CNF_Formula &cnf, bool fullEffort)=0
Check consistency of the current assignment.
CD_CNF_Formula * d_assertions
virtual int GetVarIndex(Var v)=0
void push()
Set a checkpoint for backtracking.