1 /////////////////////////////////////////////////////////////////////////////// 2 // // 3 // File: xchaff.h // 4 // Author: Clark Barrett // 5 // Created: Wed Oct 16 17:31:50 2002 // 6 // Description: Enhanced C++ API for Chaff // 7 // // 8 /////////////////////////////////////////////////////////////////////////////// 9 10 #ifndef _XCHAFF_H_ 11 #define _XCHAFF_H_ 12 13 #include "sat_api.h" 14 #include "xchaff_solver.h" 15 16 class Xchaff :public SatSolver { 17 CSolver *_solver; 18 19 Lit (*_decision_hook)(void *, bool *); 20 void (*_assignment_hook)(void *, Var, int); 21 void *_decision_hook_cookie; 22 void *_assignment_hook_cookie; 23 mkVar(int id)24 static Var mkVar(int id) { Var v; v.id = id; return v; } mkLit(int id)25 static Lit mkLit(int id) { Lit l; l.id = id; return l; } mkClause(int id)26 static Clause mkClause(int id) { Clause c; c.id = id; return c; } 27 28 public: Xchaff()29 Xchaff() { _solver = new CSolver; } ~Xchaff()30 ~Xchaff() { delete _solver; } 31 32 ///////////////////////////////////////////////////////////////////////////// 33 // Implementation of SAT_API // 34 ///////////////////////////////////////////////////////////////////////////// 35 NumVariables()36 int NumVariables() 37 { return _solver->num_variables(); } AddVariables(int nvars)38 Var AddVariables(int nvars) 39 { return mkVar(_solver->add_variables(nvars)); } GetVar(int varIndex)40 Var GetVar(int varIndex) 41 { return mkVar(varIndex); } GetVarIndex(Var v)42 int GetVarIndex(Var v) 43 { return v.id; } GetFirstVar()44 Var GetFirstVar() 45 { Var v; if (_solver->num_variables() != 0) v.id = 1; return v; } GetNextVar(Var var)46 Var GetNextVar(Var var) 47 { Var v; 48 if (var.id != _solver->num_variables()) v.id = var.id+1; return v; } MakeLit(Var var,int phase)49 Lit MakeLit(Var var, int phase) 50 { return mkLit((var.id << 1)+phase); } GetVarFromLit(Lit lit)51 Var GetVarFromLit(Lit lit) 52 { return mkVar(lit.id >> 1); } GetPhaseFromLit(Lit lit)53 int GetPhaseFromLit(Lit lit) 54 { return lit.id & 1; } NumClauses()55 int NumClauses() 56 { return _solver->num_clauses(); } AddClause(std::vector<Lit> & lits)57 Clause AddClause(std::vector<Lit>& lits) 58 { return mkClause(_solver->add_clause((std::vector<long>&)lits)); } 59 Clause GetClause(int clauseIndex); GetFirstClause()60 Clause GetFirstClause() 61 { Clause c; 62 for (unsigned i=0; i< _solver->clauses().size(); ++i) 63 if ( _solver->clause(i).in_use()) { c.id = i; break; } 64 return c; } GetNextClause(Clause clause)65 Clause GetNextClause(Clause clause) 66 { Clause c; 67 for (unsigned i= clause.id + 1; i< _solver->clauses().size(); ++i) 68 if ( _solver->clause(i).in_use()) { c.id = i; break; } 69 return c; } 70 void GetClauseLits(SatSolver::Clause clause, std::vector<Lit>* lits); 71 SatSolver::SATStatus Satisfiable(bool allowNewClauses); GetVarAssignment(Var var)72 int GetVarAssignment(Var var) 73 { return _solver->variable(var.id).value(); } 74 75 // Not implemented yet: 76 SatSolver::SATStatus Continue(); Restart()77 void Restart() { assert(0); } Reset()78 void Reset() { assert(0); } 79 RegisterDLevelHook(void (* f)(void *,int),void * cookie)80 void RegisterDLevelHook(void (*f)(void *, int), void *cookie) 81 { _solver->RegisterDLevelHook(f, cookie); } 82 TranslateDecisionHook(void * cookie,bool * done)83 static int TranslateDecisionHook(void *cookie, bool *done) 84 { 85 Xchaff *b = (Xchaff*)cookie; 86 Lit lit = b->_decision_hook(b->_decision_hook_cookie, done); 87 return lit.id; 88 } 89 RegisterDecisionHook(Lit (* f)(void *,bool *),void * cookie)90 void RegisterDecisionHook(Lit (*f)(void *, bool *), void *cookie) 91 { _decision_hook = f; _decision_hook_cookie = cookie; 92 _solver->RegisterDecisionHook(TranslateDecisionHook, this); } 93 TranslateAssignmentHook(void * cookie,int var,int value)94 static void TranslateAssignmentHook(void *cookie, int var, int value) 95 { 96 Xchaff *b = (Xchaff*)cookie; 97 b->_assignment_hook(b->_assignment_hook_cookie, mkVar(var), value); 98 } 99 RegisterAssignmentHook(void (* f)(void *,Var,int),void * cookie)100 void RegisterAssignmentHook(void (*f)(void *, Var, int), void *cookie) 101 { _assignment_hook = f; _assignment_hook_cookie = cookie; 102 _solver->RegisterAssignmentHook(TranslateAssignmentHook, this); } RegisterDeductionHook(void (* f)(void *),void * cookie)103 void RegisterDeductionHook(void (*f)(void *), void *cookie) 104 { _solver->RegisterDeductionHook(f, cookie); } SetBudget(int budget)105 bool SetBudget(int budget) // budget is time in seconds 106 { _solver->set_time_limit(float(budget)); return true; } SetMemLimit(int mem_limit)107 bool SetMemLimit(int mem_limit) 108 { _solver->set_mem_limit(mem_limit); return true; } SetRandomness(int n)109 bool SetRandomness(int n) 110 { _solver->set_randomness(n); return true; } SetRandSeed(int seed)111 bool SetRandSeed(int seed) 112 { _solver->set_random_seed(seed); return true; } EnableClauseDeletion()113 bool EnableClauseDeletion() 114 { _solver->enable_cls_deletion(true); return true; } DisableClauseDeletion()115 bool DisableClauseDeletion() 116 { _solver->enable_cls_deletion(false); return true; } GetBudgetUsed()117 int GetBudgetUsed() 118 { return int(_solver->total_run_time()); } GetMemUsed()119 int GetMemUsed() 120 { return _solver->estimate_mem_usage(); } GetNumDecisions()121 int GetNumDecisions() 122 { return _solver->num_decisions(); } GetNumConflicts()123 int GetNumConflicts() 124 { return -1; } GetNumExtConflicts()125 int GetNumExtConflicts() 126 { return -1; } GetTotalTime()127 float GetTotalTime() 128 { return _solver->total_run_time(); } GetSATTime()129 float GetSATTime() 130 { return -1; } GetNumLiterals()131 int GetNumLiterals() 132 { return _solver->num_literals(); } GetNumDeletedClauses()133 int GetNumDeletedClauses() 134 { return _solver->num_deleted_clauses(); } GetNumDeletedLiterals()135 int GetNumDeletedLiterals() 136 { return _solver->num_deleted_literals(); } GetNumImplications()137 int GetNumImplications() 138 { return _solver->num_implications(); } GetMaxDLevel()139 int GetMaxDLevel() 140 { return _solver->max_dlevel(); } 141 }; 142 143 #endif 144 145 146 147 148 149 150 151