CVC3  2.4.1
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 }
CSolver * _solver
Definition: xchaff.h:17
Clause GetClause(int clauseIndex)
Definition: xchaff.cpp:20
int & num_lits(void)
Definition: xchaff_base.h:189
SatSolver::SATStatus Continue()
Definition: xchaff.cpp:57
bool & in_use(void)
Definition: xchaff_base.h:192
CLitPoolElement & literal(int idx)
Definition: xchaff_base.h:195
SatSolver::SATStatus Satisfiable(bool allowNewClauses)
Definition: xchaff.cpp:43
int s_var(void)
Definition: xchaff_base.h:95
void GetClauseLits(SatSolver::Clause clause, std::vector< Lit > *lits)
Definition: xchaff.cpp:35
Definition: xchaff.h:16
static Lit mkLit(int id)
Definition: xchaff.h:25
int & init_num_clauses()
Definition: xchaff_dbase.h:136
static SatSolver * Create()
Definition: sat_api.cpp:15
CClause & clause(ClauseIdx idx)
Definition: xchaff_dbase.h:126
int continueCheck()
int solve(bool allowNewClauses)