summaryrefslogtreecommitdiffstats
path: root/src/sat/bsat
diff options
context:
space:
mode:
authorAlan Mishchenko <alanmi@berkeley.edu>2017-04-11 18:23:09 -0700
committerAlan Mishchenko <alanmi@berkeley.edu>2017-04-11 18:23:09 -0700
commit000e51f323b0490e9e0d2e740f90b069d4028105 (patch)
treef45e9803946f8eeda0f8da854e2ec1578ab7ec37 /src/sat/bsat
parent175b42b48f52852b10af26a59c7e5e7b8e0ee13c (diff)
downloadabc-000e51f323b0490e9e0d2e740f90b069d4028105.tar.gz
abc-000e51f323b0490e9e0d2e740f90b069d4028105.tar.bz2
abc-000e51f323b0490e9e0d2e740f90b069d4028105.zip
Experiments with hashing.
Diffstat (limited to 'src/sat/bsat')
-rw-r--r--src/sat/bsat/satSolver.c5
-rw-r--r--src/sat/bsat/satSolver.h1
2 files changed, 6 insertions, 0 deletions
diff --git a/src/sat/bsat/satSolver.c b/src/sat/bsat/satSolver.c
index 673a6b66..a16ac96b 100644
--- a/src/sat/bsat/satSolver.c
+++ b/src/sat/bsat/satSolver.c
@@ -1246,6 +1246,11 @@ sat_solver* zsat_solver_new_seed(double seed)
return s;
}
+int sat_solver_addvar(sat_solver* s)
+{
+ sat_solver_setnvars(s, s->size+1);
+ return s->size-1;
+}
void sat_solver_setnvars(sat_solver* s,int n)
{
int var;
diff --git a/src/sat/bsat/satSolver.h b/src/sat/bsat/satSolver.h
index 6ec437f7..f62f3117 100644
--- a/src/sat/bsat/satSolver.h
+++ b/src/sat/bsat/satSolver.h
@@ -65,6 +65,7 @@ extern int sat_solver_nconflicts(sat_solver* s);
extern double sat_solver_memory(sat_solver* s);
extern int sat_solver_count_assigned(sat_solver* s);
+extern int sat_solver_addvar(sat_solver* s);
extern void sat_solver_setnvars(sat_solver* s,int n);
extern int sat_solver_get_var_value(sat_solver* s, int v);
extern void sat_solver_set_var_activity(sat_solver* s, int * pVars, int nVars);