CVC3
2.4.1
Main Page
Related Pages
Modules
Namespaces
Classes
Files
File List
File Members
src
sat
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
14
SatSolver
*
SatSolver::Create
()
15
{
16
return
new
Xchaff
();
17
}
18
19
20
SatSolver::Clause
Xchaff::GetClause
(
int
clauseIndex)
21
{
22
int
i,j;
23
SatSolver::Clause
c;
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
43
SatSolver::SATStatus
Xchaff::Satisfiable
(
bool
allowNewClauses)
44
{
45
int
status;
46
status =
_solver
->
solve
(allowNewClauses);
47
switch
(status) {
48
case
UNSATISFIABLE
:
return
SatSolver::UNSATISFIABLE
;
49
case
SATISFIABLE
:
return
SatSolver::SATISFIABLE
;
50
case
TIME_OUT
:
return
SatSolver::BUDGET_EXCEEDED
;
51
case
MEM_OUT
:
return
SatSolver::OUT_OF_MEMORY
;
52
}
53
return
SatSolver::UNKNOWN
;
54
}
55
56
57
SatSolver::SATStatus
Xchaff::Continue
()
58
{
59
int
status;
60
status =
_solver
->
continueCheck
();
61
switch
(status) {
62
case
UNSATISFIABLE
:
return
SatSolver::UNSATISFIABLE
;
63
case
SATISFIABLE
:
return
SatSolver::SATISFIABLE
;
64
case
TIME_OUT
:
return
SatSolver::BUDGET_EXCEEDED
;
65
case
MEM_OUT
:
return
SatSolver::OUT_OF_MEMORY
;
66
}
67
return
SatSolver::UNKNOWN
;
68
}
Generated on Fri Aug 9 2013 10:34:46 for CVC3 by
1.8.4