CVC3: xchaff.cpp Source File

00001 ///////////////////////////////////////////////////////////////////////////////
00002 //                                                                           //
00003 // File: xchaff.cpp                      //
00004 // Author: Clark Barrett                                                     //
00005 // Created: Wed Oct 16 17:31:50 2002               //
00006 // Description: Enhanced C++ API for Chaff                                   //
00007 //                                                                           //
00008 ///////////////////////////////////////////////////////////////////////////////
00009 
00010 
00011 #include "xchaff.h"
00012 
00013 
00014 SatSolver *SatSolver::Create()
00015 {
00016   return new Xchaff();
00017 }
00018 
00019 
00020 SatSolver::Clause Xchaff::GetClause(int clauseIndex)
00021 {
00022   int i,j;
00023   SatSolver::Clause c;
00024   assert(clauseIndex >= 0 && clauseIndex < _solver->num_clauses());
00025   if (clauseIndex >= _solver->init_num_clauses()) {
00026     for (i = j = _solver->init_num_clauses()-1; j < clauseIndex;)
00027       if (_solver->clause(++i).in_use()) j++;
00028     c.id = j;
00029   }
00030   else c.id = clauseIndex;
00031   return c;
00032 }
00033 
00034 
00035 void Xchaff::GetClauseLits(SatSolver::Clause clause, vector<Lit>* lits)
00036 {
00037   int i;
00038   for (i = 0; i < _solver->clause(clause.id).num_lits(); ++i)
00039     lits->push_back(mkLit(_solver->clause(clause.id).literal(i).s_var()));
00040 }
00041 
00042 
00043 SatSolver::SATStatus Xchaff::Satisfiable(bool allowNewClauses)
00044 {
00045   int status;
00046   status = _solver->solve(allowNewClauses);
00047   switch (status) {
00048     case UNSATISFIABLE: return SatSolver::UNSATISFIABLE;
00049     case SATISFIABLE: return SatSolver::SATISFIABLE;
00050     case TIME_OUT: return SatSolver::BUDGET_EXCEEDED;
00051     case MEM_OUT: return SatSolver::OUT_OF_MEMORY;
00052   }
00053   return SatSolver::UNKNOWN;
00054 }
00055 
00056 
00057 SatSolver::SATStatus Xchaff::Continue()
00058 {
00059   int status;
00060   status = _solver->continueCheck();
00061   switch (status) {
00062     case UNSATISFIABLE: return SatSolver::UNSATISFIABLE;
00063     case SATISFIABLE: return SatSolver::SATISFIABLE;
00064     case TIME_OUT: return SatSolver::BUDGET_EXCEEDED;
00065     case MEM_OUT: return SatSolver::OUT_OF_MEMORY;
00066   }
00067   return SatSolver::UNKNOWN;
00068 }