xchaff.h

Go to the documentation of this file.
00001 ///////////////////////////////////////////////////////////////////////////////
00002 //                                                                           //
00003 // File: xchaff.h                        //
00004 // Author: Clark Barrett                                                     //
00005 // Created: Wed Oct 16 17:31:50 2002               //
00006 // Description: Enhanced C++ API for Chaff                                   //
00007 //                                                                           //
00008 ///////////////////////////////////////////////////////////////////////////////
00009 
00010 #ifndef _XCHAFF_H_
00011 #define _XCHAFF_H_
00012 
00013 #include "sat_api.h"
00014 #include "xchaff_solver.h"
00015 
00016 class Xchaff :public SatSolver {
00017   CSolver *_solver;
00018 
00019   Lit  (*_decision_hook)(void *, bool *);
00020   void (*_assignment_hook)(void *, Var, int);
00021   void *_decision_hook_cookie;
00022   void *_assignment_hook_cookie;
00023 
00024   static Var mkVar(int id) { Var v; v.id = id; return v; }
00025   static Lit mkLit(int id) { Lit l; l.id = id; return l; }
00026   static Clause mkClause(int id) { Clause c; c.id = id; return c; }
00027 
00028 public:
00029   Xchaff()  { _solver = new CSolver; }
00030   ~Xchaff() { delete _solver; }
00031 
00032   /////////////////////////////////////////////////////////////////////////////
00033   // Implementation of SAT_API                                               //
00034   /////////////////////////////////////////////////////////////////////////////
00035 
00036   int   NumVariables()
00037         { return _solver->num_variables(); }
00038   Var   AddVariables(int nvars)
00039         { return mkVar(_solver->add_variables(nvars)); }
00040   Var   GetVar(int varIndex)
00041         { return mkVar(varIndex); }
00042   int   GetVarIndex(Var v)
00043         { return v.id; }
00044   Var   GetFirstVar()
00045         { Var v; if (_solver->num_variables() != 0) v.id = 1; return v; }
00046   Var   GetNextVar(Var var)
00047         { Var v;
00048     if (var.id != _solver->num_variables()) v.id = var.id+1; return v; }
00049   Lit   MakeLit(Var var, int phase)
00050         { return mkLit((var.id << 1)+phase); }
00051   Var   GetVarFromLit(Lit lit)
00052         { return mkVar(lit.id >> 1); }
00053   int   GetPhaseFromLit(Lit lit)
00054         { return lit.id & 1; }
00055   int   NumClauses()
00056         { return _solver->num_clauses(); }
00057   Clause AddClause(std::vector<Lit>& lits)
00058         { return mkClause(_solver->add_clause((std::vector<long>&)lits)); }
00059   Clause GetClause(int clauseIndex);
00060   Clause GetFirstClause()
00061         { Clause c;
00062     for (unsigned i=0; i< _solver->clauses().size(); ++i)
00063       if ( _solver->clause(i).in_use()) { c.id = i; break; }
00064     return c; }
00065   Clause GetNextClause(Clause clause)
00066         { Clause c;
00067     for (unsigned i= clause.id + 1; i< _solver->clauses().size(); ++i)
00068             if ( _solver->clause(i).in_use()) { c.id = i; break; }
00069           return c; }
00070   void  GetClauseLits(SatSolver::Clause clause, std::vector<Lit>* lits);
00071   SatSolver::SATStatus Satisfiable(bool allowNewClauses);
00072   int   GetVarAssignment(Var var)
00073         { return _solver->variable(var.id).value(); }
00074 
00075   // Not implemented yet:
00076   SatSolver::SATStatus Continue();
00077   void Restart() { assert(0); }
00078   void Reset() { assert(0); }
00079 
00080   void  RegisterDLevelHook(void (*f)(void *, int), void *cookie)
00081         { _solver->RegisterDLevelHook(f, cookie); }
00082 
00083   static int TranslateDecisionHook(void *cookie, bool *done)
00084   {
00085     Xchaff *b = (Xchaff*)cookie;
00086     Lit lit = b->_decision_hook(b->_decision_hook_cookie, done);
00087     return lit.id;
00088   }
00089 
00090   void  RegisterDecisionHook(Lit (*f)(void *, bool *), void *cookie)
00091         { _decision_hook = f; _decision_hook_cookie = cookie;
00092     _solver->RegisterDecisionHook(TranslateDecisionHook, this); }
00093 
00094   static void TranslateAssignmentHook(void *cookie, int var, int value)
00095   {
00096     Xchaff *b = (Xchaff*)cookie;
00097     b->_assignment_hook(b->_assignment_hook_cookie, mkVar(var), value);
00098   }
00099 
00100   void  RegisterAssignmentHook(void (*f)(void *, Var, int), void *cookie)
00101         { _assignment_hook = f; _assignment_hook_cookie = cookie;
00102     _solver->RegisterAssignmentHook(TranslateAssignmentHook, this); }
00103   void  RegisterDeductionHook(void (*f)(void *), void *cookie)
00104         { _solver->RegisterDeductionHook(f, cookie); }
00105   bool  SetBudget(int budget)  // budget is time in seconds
00106         { _solver->set_time_limit(float(budget)); return true; }
00107   bool  SetMemLimit(int mem_limit)
00108         { _solver->set_mem_limit(mem_limit); return true; }
00109   bool  SetRandomness(int n)
00110         { _solver->set_randomness(n); return true; }
00111   bool  SetRandSeed(int seed)
00112         { _solver->set_random_seed(seed); return true; }
00113   bool  EnableClauseDeletion()
00114         { _solver->enable_cls_deletion(true); return true; }
00115   bool  DisableClauseDeletion()
00116         { _solver->enable_cls_deletion(false); return true; }
00117   int   GetBudgetUsed()
00118         { return int(_solver->total_run_time()); }
00119   int   GetMemUsed()
00120         { return _solver->estimate_mem_usage(); }
00121   int   GetNumDecisions()
00122         { return _solver->num_decisions(); }
00123   int   GetNumConflicts()
00124         { return -1; }
00125   int   GetNumExtConflicts()
00126         { return -1; }
00127   float GetTotalTime()
00128         { return _solver->total_run_time(); }
00129   float GetSATTime()
00130         { return -1; }
00131   int   GetNumLiterals()
00132         { return _solver->num_literals(); }
00133   int   GetNumDeletedClauses()
00134         { return _solver->num_deleted_clauses(); }
00135   int   GetNumDeletedLiterals()
00136         { return _solver->num_deleted_literals(); }
00137   int   GetNumImplications()
00138         { return _solver->num_implications(); }
00139   int   GetMaxDLevel()
00140         { return _solver->max_dlevel(); }
00141 };
00142 
00143 #endif
00144 
00145 
00146 
00147 
00148 
00149 
00150 

Generated on Tue Jul 3 14:33:42 2007 for CVC3 by  doxygen 1.5.1