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");