00001
00002
00003
00004
00005
00006
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
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
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)
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