Additional changes to Satoko to enable various integrations.

src/sat/satoko/satoko.h

@@ -86,13 +86,15 @@ extern void satoko_reset(satoko_t *);
 extern void satoko_default_opts(satoko_opts_t *);
 extern void satoko_configure(satoko_t *, satoko_opts_t *);
 extern int  satoko_parse_dimacs(char *, satoko_t **);
+extern void satoko_setnvars(satoko_t *, int);
 extern int  satoko_add_variable(satoko_t *, char);
 extern int  satoko_add_clause(satoko_t *, int *, int);
 extern void satoko_assump_push(satoko_t *s, int);
 extern void satoko_assump_pop(satoko_t *s);
 extern int  satoko_simplify(satoko_t *);
 extern int  satoko_solve(satoko_t *);
-extern int  satoko_solve_with_assumptions(satoko_t *s, int * plits, int nlits);
+extern int  satoko_solve_assumptions(satoko_t *s, int * plits, int nlits);
+extern int  satoko_solve_assumptions_limit(satoko_t *s, int * plits, int nlits, int nconflim);
 extern void satoko_mark_cone(satoko_t *, int *, int);
 extern void satoko_unmark_cone(satoko_t *, int *, int);
 
@@ -101,14 +103,12 @@ extern void satoko_bookmark(satoko_t *);
 extern void satoko_unbookmark(satoko_t *);
 /* If problem is unsatisfiable under assumptions, this function is used to
  * obtain the final conflict clause expressed in the assumptions.
- *
- *  - It receives as inputs the solver and a pointer to a array where clause
- * will be copied. The memory is allocated by the solver, but must be freed by
- * the caller.
+ *  - It receives as inputs the solver and a pointer to an array where clause
+ * is stored. The memory for the clause is managed by the solver.
  *  - The return value is either the size of the array or -1 in case the final
  * conflict cluase was not generated.
  */
-extern int satoko_final_conflict(satoko_t *, unsigned *);
+extern int satoko_final_conflict(satoko_t *, int **);
 
 /* Procedure to dump a DIMACS file.
  * - It receives as input the solver, a file name string and two integers.

src/sat/satoko/solver.c

@@ -639,7 +639,8 @@ char solver_search(solver_t *s)
             /* No conflict */
             unsigned next_lit;
 
-            if (solver_rst(s) || solver_check_limits(s) == 0 || solver_stop(s)) {
+            if (solver_rst(s) || solver_check_limits(s) == 0 || solver_stop(s) || 
+                (s->nRuntimeLimit && (s->stats.n_conflicts & 63) == 0 && Abc_Clock() > s->nRuntimeLimit)) {
                 b_queue_clean(s->bq_lbd);
                 solver_cancel_until(s, 0);
                 return SATOKO_UNDEC;
@@ -648,7 +649,7 @@ char solver_search(solver_t *s)
                 satoko_simplify(s);
 
             /* Reduce the set of learnt clauses */
-            if (s->opts.learnt_ratio &&
+            if (s->opts.learnt_ratio && vec_uint_size(s->learnts) > 100 &&
                 s->stats.n_conflicts >= s->n_confl_bfr_reduce) {
                 s->RC1 = (s->stats.n_conflicts / s->RC2) + 1;
                 solver_reduce_cdb(s);

src/sat/satoko/solver.h

@@ -103,8 +103,11 @@ struct solver_t_ {
     /* Temporary data used for solving cones */
     vec_char_t *marks;
     
-    /* Callback to stop the solver */
-    int * pstop;
+    /* Callbacks to stop the solver */
+    abctime nRuntimeLimit;
+    int    *pstop;
+    int     RunId;           
+    int   (*pFuncStop)(int);  
 
     struct satoko_stats stats;
     struct satoko_opts opts;
@@ -251,6 +254,12 @@ static inline int solver_read_cex_varvalue(solver_t *s, int ivar)
 {
     return var_polarity(s, ivar) == LIT_TRUE;
 }
+static abctime solver_set_runtime_limit(solver_t* s, abctime Limit)
+{
+    abctime nRuntimeLimit = s->nRuntimeLimit;
+    s->nRuntimeLimit = Limit;
+    return nRuntimeLimit;
+}
 
 //===------------------------------------------------------------------------===
 // Inline clause functions

src/sat/satoko/solver_api.c

@@ -218,6 +218,13 @@ int satoko_simplify(solver_t * s)
     return SATOKO_OK;
 }
 
+void satoko_setnvars(solver_t *s, int nvars)
+{
+    int i;
+    for (i = solver_varnum(s); i < nvars; i++)
+        satoko_add_variable(s, 0);
+}
+
 int satoko_add_variable(solver_t *s, char sign)
 {
     unsigned var = vec_act_size(s->activity);
@@ -305,6 +312,10 @@ int satoko_solve(solver_t *s)
         status = solver_search(s);
         if (solver_check_limits(s) == 0 || solver_stop(s))
             break;
+        if (s->nRuntimeLimit && Abc_Clock() > s->nRuntimeLimit)
+            break;
+        if (s->pFuncStop && s->pFuncStop(s->RunId))
+            break;
     }
     if (s->opts.verbose)
         print_stats(s);
@@ -313,7 +324,7 @@ int satoko_solve(solver_t *s)
     return status;
 }
 
-int satoko_solve_with_assumptions(solver_t *s, int * plits, int nlits)
+int satoko_solve_assumptions(solver_t *s, int * plits, int nlits)
 {
     int i, status;
     for ( i = 0; i < nlits; i++ )
@@ -321,20 +332,21 @@ int satoko_solve_with_assumptions(solver_t *s, int * plits, int nlits)
     status = satoko_solve( s );
     for ( i = 0; i < nlits; i++ )
         satoko_assump_pop( s );
-    if ( status == SATOKO_UNSAT )
-        return 1;
-    if ( status == SATOKO_SAT )
-        return 0;
-    return -1;
+    return status;
 }
 
-int satoko_final_conflict(solver_t *s, unsigned *out)
+int satoko_solve_assumptions_limit(satoko_t *s, int * plits, int nlits, int nconflim)
 {
-    if (vec_uint_size(s->final_conflict) == 0)
-        return -1;
-    out = satoko_alloc(unsigned, vec_uint_size(s->final_conflict));
-    memcpy(out, vec_uint_data(s->final_conflict),
-           sizeof(unsigned) * vec_uint_size(s->final_conflict));
+    int temp = s->opts.conf_limit, status;
+    s->opts.conf_limit = nconflim;
+    status = satoko_solve_assumptions(s, plits, nlits);
+    s->opts.conf_limit = temp;
+    return status;
+}
+
+int satoko_final_conflict(solver_t *s, int **out)
+{
+    *out = (int *)vec_uint_data(s->final_conflict);
     return vec_uint_size(s->final_conflict);
 }