CVC3
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