CVC3  2.4.1
xchaff.h
Go to the documentation of this file.
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 {
18 
19  Lit (*_decision_hook)(void *, bool *);
20  void (*_assignment_hook)(void *, Var, int);
23 
24  static Var mkVar(int id) { Var v; v.id = id; return v; }
25  static Lit mkLit(int id) { Lit l; l.id = id; return l; }
26  static Clause mkClause(int id) { Clause c; c.id = id; return c; }
27 
28 public:
29  Xchaff() { _solver = new CSolver; }
30  ~Xchaff() { delete _solver; }
31 
32  /////////////////////////////////////////////////////////////////////////////
33  // Implementation of SAT_API //
34  /////////////////////////////////////////////////////////////////////////////
35 
37  { return _solver->num_variables(); }
38  Var AddVariables(int nvars)
39  { return mkVar(_solver->add_variables(nvars)); }
40  Var GetVar(int varIndex)
41  { return mkVar(varIndex); }
43  { return v.id; }
45  { Var v; if (_solver->num_variables() != 0) v.id = 1; return v; }
47  { Var v;
48  if (var.id != _solver->num_variables()) v.id = var.id+1; return v; }
49  Lit MakeLit(Var var, int phase)
50  { return mkLit((var.id << 1)+phase); }
51  Var GetVarFromLit(Lit lit)
52  { return mkVar(lit.id >> 1); }
53  int GetPhaseFromLit(Lit lit)
54  { return lit.id & 1; }
55  int NumClauses()
56  { return _solver->num_clauses(); }
57  Clause AddClause(std::vector<Lit>& lits)
58  { return mkClause(_solver->add_clause((std::vector<long>&)lits)); }
59  Clause GetClause(int clauseIndex);
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; }
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);
73  { return _solver->variable(var.id).value(); }
74 
75  // Not implemented yet:
77  void Restart() { assert(0); }
78  void Reset() { assert(0); }
79 
80  void RegisterDLevelHook(void (*f)(void *, int), void *cookie)
81  { _solver->RegisterDLevelHook(f, cookie); }
82 
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 
90  void RegisterDecisionHook(Lit (*f)(void *, bool *), void *cookie)
91  { _decision_hook = f; _decision_hook_cookie = cookie;
93 
94  static void TranslateAssignmentHook(void *cookie, int var, int value)
95  {
96  Xchaff *b = (Xchaff*)cookie;
98  }
99 
100  void RegisterAssignmentHook(void (*f)(void *, Var, int), void *cookie)
103  void RegisterDeductionHook(void (*f)(void *), void *cookie)
104  { _solver->RegisterDeductionHook(f, cookie); }
105  bool SetBudget(int budget) // budget is time in seconds
106  { _solver->set_time_limit(float(budget)); return true; }
107  bool SetMemLimit(int mem_limit)
108  { _solver->set_mem_limit(mem_limit); return true; }
109  bool SetRandomness(int n)
110  { _solver->set_randomness(n); return true; }
111  bool SetRandSeed(int seed)
112  { _solver->set_random_seed(seed); return true; }
114  { _solver->enable_cls_deletion(true); return true; }
116  { _solver->enable_cls_deletion(false); return true; }
118  { return int(_solver->total_run_time()); }
120  { return _solver->estimate_mem_usage(); }
122  { return _solver->num_decisions(); }
124  { return -1; }
126  { return -1; }
127  float GetTotalTime()
128  { return _solver->total_run_time(); }
129  float GetSATTime()
130  { return -1; }
132  { return _solver->num_literals(); }
134  { return _solver->num_deleted_clauses(); }
136  { return _solver->num_deleted_literals(); }
138  { return _solver->num_implications(); }
140  { return _solver->max_dlevel(); }
141 };
142 
143 #endif
144 
145 
146 
147 
148 
149 
150 
int num_decisions()
CSolver * _solver
Definition: xchaff.h:17
Clause GetClause(int clauseIndex)
Definition: xchaff.cpp:20
short & value(void)
Definition: xchaff_base.h:264
int GetBudgetUsed()
Definition: xchaff.h:117
void RegisterDecisionHook(Lit(*f)(void *, bool *), void *cookie)
Definition: xchaff.h:90
int GetNumImplications()
Definition: xchaff.h:137
vector< CClause > & clauses(void)
Definition: xchaff_dbase.h:120
bool SetRandSeed(int seed)
Definition: xchaff.h:111
SatSolver::SATStatus Continue()
Definition: xchaff.cpp:57
int num_implications()
void set_mem_limit(int s)
void RegisterDecisionHook(int(*f)(void *, bool *), void *cookie)
int GetNumLiterals()
Definition: xchaff.h:131
int GetNumDeletedLiterals()
Definition: xchaff.h:135
bool & in_use(void)
Definition: xchaff_base.h:192
int num_clauses(void)
Definition: xchaff_dbase.h:214
int GetNumDeletedClauses()
Definition: xchaff.h:133
void set_time_limit(float t)
CVariable & variable(int idx)
Definition: xchaff_dbase.h:123
SatSolver::SATStatus Satisfiable(bool allowNewClauses)
Definition: xchaff.cpp:43
void * _assignment_hook_cookie
Definition: xchaff.h:22
int estimate_mem_usage()
Xchaff()
Definition: xchaff.h:29
Var GetNextVar(Var var)
Definition: xchaff.h:46
Clause GetNextClause(Clause clause)
Definition: xchaff.h:65
static Clause mkClause(int id)
Definition: xchaff.h:26
void enable_cls_deletion(bool allow)
int & num_deleted_literals()
Definition: xchaff_dbase.h:141
Lit(* _decision_hook)(void *, bool *)
Definition: xchaff.h:19
void GetClauseLits(SatSolver::Clause clause, std::vector< Lit > *lits)
Definition: xchaff.cpp:35
void(* _assignment_hook)(void *, Var, int)
Definition: xchaff.h:20
ClauseIdx add_clause(vector< long > &lits, bool addConflicts=true)
bool SetMemLimit(int mem_limit)
Definition: xchaff.h:107
void set_random_seed(int seed)
void Reset()
Definition: xchaff.h:78
int GetPhaseFromLit(Lit lit)
Definition: xchaff.h:53
void RegisterDLevelHook(void(*f)(void *, int), void *cookie)
Definition: xchaff.h:80
int max_dlevel()
int num_literals(void)
Definition: xchaff_dbase.h:217
void Restart()
Definition: xchaff.h:77
Var GetVarFromLit(Lit lit)
Definition: xchaff.h:51
float GetTotalTime()
Definition: xchaff.h:127
Var AddVariables(int nvars)
Definition: xchaff.h:38
int GetMaxDLevel()
Definition: xchaff.h:139
Definition: xchaff.h:16
bool SetBudget(int budget)
Definition: xchaff.h:105
void RegisterDLevelHook(void(*f)(void *, int), void *cookie)
void * _decision_hook_cookie
Definition: xchaff.h:21
int GetMemUsed()
Definition: xchaff.h:119
void RegisterDeductionHook(void(*f)(void *), void *cookie)
Definition: xchaff.h:103
void RegisterAssignmentHook(void(*f)(void *, Var, int), void *cookie)
Definition: xchaff.h:100
Var GetVar(int varIndex)
Definition: xchaff.h:40
int add_variables(int new_vars)
void RegisterDeductionHook(void(*f)(void *), void *cookie)
static Lit mkLit(int id)
Definition: xchaff.h:25
void RegisterAssignmentHook(void(*f)(void *, int, int), void *cookie)
int GetVarAssignment(Var var)
Definition: xchaff.h:72
bool SetRandomness(int n)
Definition: xchaff.h:109
void set_randomness(int n)
int GetNumConflicts()
Definition: xchaff.h:123
static Var mkVar(int id)
Definition: xchaff.h:24
Clause AddClause(std::vector< Lit > &lits)
Definition: xchaff.h:57
int GetNumExtConflicts()
Definition: xchaff.h:125
int GetVarIndex(Var v)
Definition: xchaff.h:42
static void TranslateAssignmentHook(void *cookie, int var, int value)
Definition: xchaff.h:94
bool EnableClauseDeletion()
Definition: xchaff.h:113
Clause GetFirstClause()
Definition: xchaff.h:60
int num_variables(void)
Definition: xchaff_dbase.h:210
Lit MakeLit(Var var, int phase)
Definition: xchaff.h:49
float total_run_time()
int NumClauses()
Definition: xchaff.h:55
CClause & clause(ClauseIdx idx)
Definition: xchaff_dbase.h:126
static int TranslateDecisionHook(void *cookie, bool *done)
Definition: xchaff.h:83
int NumVariables()
Definition: xchaff.h:36
int GetNumDecisions()
Definition: xchaff.h:121
~Xchaff()
Definition: xchaff.h:30
bool DisableClauseDeletion()
Definition: xchaff.h:115
float GetSATTime()
Definition: xchaff.h:129
Var GetFirstVar()
Definition: xchaff.h:44
int & num_deleted_clauses()
Definition: xchaff_dbase.h:140