summaryrefslogtreecommitdiffstats
path: root/src/sat/bsat/satSolver2.h
diff options
context:
space:
mode:
authorAlan Mishchenko <alanmi@berkeley.edu>2011-12-23 00:29:26 -0800
committerAlan Mishchenko <alanmi@berkeley.edu>2011-12-23 00:29:26 -0800
commit9d2893040ea7c69f384b0735a1407e9d91f89e35 (patch)
tree2202268143c4175f7a126d820c8036c13da37ad5 /src/sat/bsat/satSolver2.h
parent844c385e2b8610ec8bdc4a55400f8efe79eac119 (diff)
downloadabc-9d2893040ea7c69f384b0735a1407e9d91f89e35.tar.gz
abc-9d2893040ea7c69f384b0735a1407e9d91f89e35.tar.bz2
abc-9d2893040ea7c69f384b0735a1407e9d91f89e35.zip
Transforming the solver to use different clause representation.
Diffstat (limited to 'src/sat/bsat/satSolver2.h')
-rw-r--r--src/sat/bsat/satSolver2.h2
1 files changed, 2 insertions, 0 deletions
diff --git a/src/sat/bsat/satSolver2.h b/src/sat/bsat/satSolver2.h
index 0c08ac1e..21dc3b21 100644
--- a/src/sat/bsat/satSolver2.h
+++ b/src/sat/bsat/satSolver2.h
@@ -126,6 +126,8 @@ struct sat_solver2_t
// internal state
varinfo * vi; // variable information
+ int* levels; //
+ char* assigns; //
lit* trail; // sequence of assignment and implications
int* orderpos; // Index in variable order.
cla* reasons; // reason clauses