CVC3
2.4.1
Main Page
Related Pages
Modules
Namespaces
Classes
Files
File List
File Members
src
sat
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
{
17
CSolver
*
_solver
;
18
19
Lit (*
_decision_hook
)(
void
*,
bool
*);
20
void (*
_assignment_hook
)(
void
*,
Var
, int);
21
void
*
_decision_hook_cookie
;
22
void
*
_assignment_hook_cookie
;
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
36
int
NumVariables
()
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); }
42
int
GetVarIndex
(
Var
v)
43
{
return
v.
id
; }
44
Var
GetFirstVar
()
45
{
Var
v;
if
(
_solver
->
num_variables
() != 0) v.
id
= 1;
return
v; }
46
Var
GetNextVar
(
Var
var)
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);
60
Clause
GetFirstClause
()
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; }
65
Clause
GetNextClause
(
Clause
clause)
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);
72
int
GetVarAssignment
(
Var
var)
73
{
return
_solver
->
variable
(var.
id
).
value
(); }
74
75
// Not implemented yet:
76
SatSolver::SATStatus
Continue
();
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;
92
_solver
->
RegisterDecisionHook
(
TranslateDecisionHook
,
this
); }
93
94
static
void
TranslateAssignmentHook
(
void
*cookie,
int
var,
int
value)
95
{
96
Xchaff
*b = (
Xchaff
*)cookie;
97
b->
_assignment_hook
(b->
_assignment_hook_cookie
,
mkVar
(var), value);
98
}
99
100
void
RegisterAssignmentHook
(
void
(*f)(
void
*,
Var
,
int
),
void
*cookie)
101
{
_assignment_hook
= f;
_assignment_hook_cookie
= cookie;
102
_solver
->
RegisterAssignmentHook
(
TranslateAssignmentHook
,
this
); }
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
; }
113
bool
EnableClauseDeletion
()
114
{
_solver
->
enable_cls_deletion
(
true
);
return
true
; }
115
bool
DisableClauseDeletion
()
116
{
_solver
->
enable_cls_deletion
(
false
);
return
true
; }
117
int
GetBudgetUsed
()
118
{
return
int(
_solver
->
total_run_time
()); }
119
int
GetMemUsed
()
120
{
return
_solver
->
estimate_mem_usage
(); }
121
int
GetNumDecisions
()
122
{
return
_solver
->
num_decisions
(); }
123
int
GetNumConflicts
()
124
{
return
-1; }
125
int
GetNumExtConflicts
()
126
{
return
-1; }
127
float
GetTotalTime
()
128
{
return
_solver
->
total_run_time
(); }
129
float
GetSATTime
()
130
{
return
-1; }
131
int
GetNumLiterals
()
132
{
return
_solver
->
num_literals
(); }
133
int
GetNumDeletedClauses
()
134
{
return
_solver
->
num_deleted_clauses
(); }
135
int
GetNumDeletedLiterals
()
136
{
return
_solver
->
num_deleted_literals
(); }
137
int
GetNumImplications
()
138
{
return
_solver
->
num_implications
(); }
139
int
GetMaxDLevel
()
140
{
return
_solver
->
max_dlevel
(); }
141
};
142
143
#endif
144
145
146
147
148
149
150
Generated on Sat May 18 2013 12:01:29 for CVC3 by
1.8.3.1