CVC3
xchaff.cpp
Go to the documentation of this file.
1 ///////////////////////////////////////////////////////////////////////////////
2 // //
3 // File: xchaff.cpp //
4 // Author: Clark Barrett //
5 // Created: Wed Oct 16 17:31:50 2002 //
6 // Description: Enhanced C++ API for Chaff //
7 // //
8 ///////////////////////////////////////////////////////////////////////////////
9 
10 
11 #include "xchaff.h"
12 
13 
15 {
16  return new Xchaff();
17 }
18 
19 
21 {
22  int i,j;
24  assert(clauseIndex >= 0 && clauseIndex < _solver->num_clauses());
25  if (clauseIndex >= _solver->init_num_clauses()) {
26  for (i = j = _solver->init_num_clauses()-1; j < clauseIndex;)
27  if (_solver->clause(++i).in_use()) j++;
28  c.id = j;
29  }
30  else c.id = clauseIndex;
31  return c;
32 }
33 
34 
35 void Xchaff::GetClauseLits(SatSolver::Clause clause, vector<Lit>* lits)
36 {
37  int i;
38  for (i = 0; i < _solver->clause(clause.id).num_lits(); ++i)
39  lits->push_back(mkLit(_solver->clause(clause.id).literal(i).s_var()));
40 }
41 
42 
44 {
45  int status;
46  status = _solver->solve(allowNewClauses);
47  switch (status) {
51  case MEM_OUT: return SatSolver::OUT_OF_MEMORY;
52  }
53  return SatSolver::UNKNOWN;
54 }
55 
56 
58 {
59  int status;
60  status = _solver->continueCheck();
61  switch (status) {
65  case MEM_OUT: return SatSolver::OUT_OF_MEMORY;
66  }
67  return SatSolver::UNKNOWN;
68 }