- Adding a compile time option to use floats for var activity (now it can be either ‘double’, ‘float’ or ‘unsigned’ (default))

- Adding vector of ‘float’
- Adding an option to configure the ratio of learnt clauses to be kept in clause database at each reduction (0 means no reduction).
- Other small changes.

1 files changed, 4 insertions, 3 deletions

diff --git a/src/sat/satoko/solver_api.c b/src/sat/satoko/solver_api.c
index e041cc62..980cc160 100644
--- a/src/sat/satoko/solver_api.c
+++ b/src/sat/satoko/solver_api.c
@@ -165,6 +165,7 @@ void satoko_default_opts(satoko_opts_t *opts)
     opts->inc_reduce = 300;
     opts->inc_special_reduce = 1000;
     opts->lbd_freeze_clause = 30;
+    opts->learnt_ratio = 0.5;
     /* VSIDS heuristic */
     opts->var_decay = (act_t) 0.95;
     opts->clause_decay = (clause_act_t) 0.995;
@@ -187,7 +188,7 @@ void satoko_configure(satoko_t *s, satoko_opts_t *user_opts)
 int satoko_simplify(solver_t * s)
 {
     unsigned i, j = 0;
-        unsigned cref;
+    unsigned cref;
 
     assert(solver_dlevel(s) == 0);
     if (solver_propagate(s) != UNDEF)
@@ -198,7 +199,7 @@ int satoko_simplify(solver_t * s)
     vec_uint_foreach(s->originals, cref, i) {
         struct clause *clause = clause_read(s, cref);
 
-            if (clause_is_satisfied(s, clause)) {
+    if (clause_is_satisfied(s, clause)) {
             clause->f_mark = 1;
             s->stats.n_original_lits -= clause->size;
             clause_unwatch(s, cref);
@@ -236,7 +237,7 @@ int satoko_add_clause(solver_t *s, unsigned *lits, unsigned size)
     unsigned max_var;
     unsigned cref;
 
-    qsort((void *) lits, size, sizeof(unsigned), mkt_uint_compare);
+    qsort((void *) lits, size, sizeof(unsigned), stk_uint_compare);
     max_var = lit2var(lits[size - 1]);
     while (max_var >= vec_act_size(s->activity))
         satoko_add_variable(s, LIT_FALSE);