Merge branch 'ffsat-prop' into ffsat

src/mcsat/ff/ff_feasible_set_db.c

@@ -180,6 +180,28 @@ uint32_t feasibility_int_set_count_approx(const feasibility_int_set_t *set, cons
   }
 }
 
+/** gets the reasons of a set */
+static
+void feasibility_int_set_get_reasons(const feasibility_int_set_t *set, ivector_t *reasons_out) {
+  // collect indices
+  size_t offset = 0;
+  for (size_t i = 0; i < set->reasons_sizes.size; ++i) {
+    uint32_t reason_size = set->reasons_sizes.data[i];
+    if (reason_size == 0) {
+      // skip empty reasons, i.e. updates that didn't to anything
+      continue;
+    }
+    assert(offset + reason_size <= set->reasons.size);
+    // currently only single reasons are used
+    assert(reason_size == 1);
+    for (uint32_t j = 0; j < reason_size; ++j) {
+      variable_t reason = set->reasons.data[offset + j];
+      ivector_push(reasons_out, reason);
+    }
+    offset += reason_size;
+  }
+}
+
 /** prints the set at the timestamp if the timestamp exists */
 static
 void feasibility_int_set_print_at(const feasibility_int_set_t *set, uint32_t timestamp, bool print_reasons, FILE *out) {
@@ -461,6 +483,15 @@ bool ff_feasible_set_db_pick_value(const ff_feasible_set_db_t* db, variable_t x,
   }
 }
 
+void ff_feasible_set_db_get_reasons(const ff_feasible_set_db_t* db, variable_t x, ivector_t* reasons_out) {
+  ptr_hmap_pair_t *found = ptr_hmap_find(&db->sets, x);
+  if (found == NULL) {
+    return;
+  }
+  feasibility_int_set_t *set = found->val;
+  feasibility_int_set_get_reasons(set, reasons_out);
+}
+
 void ff_feasible_set_db_get_conflict_reasons(const ff_feasible_set_db_t* db, variable_t x, ivector_t* reasons_out, ivector_t* lemma_reasons) {
   // we only do a very trivial conflict core minimization yet
 
@@ -480,25 +511,8 @@ void ff_feasible_set_db_get_conflict_reasons(const ff_feasible_set_db_t* db, var
   if (set->last_reason_unsat) {
     assert(ivector_last(&set->reasons_sizes) == 1);
     ivector_push(reasons_out, ivector_last(&set->reasons));
-    return;
-  }
-
-  // collect indices
-  size_t offset = 0;
-  for (size_t i = 0; i < set->reasons_sizes.size; ++i) {
-    uint32_t reason_size = set->reasons_sizes.data[i];
-    if (reason_size == 0) {
-      // skip empty reasons, i.e. updates that didn't to anything
-      continue;
-    }
-    assert(offset + reason_size <= set->reasons.size);
-    ivector_t *v = (reason_size == 1) ? reasons_out : lemma_reasons;
-    for (uint32_t j = 0; j < reason_size; ++j) {
-      variable_t reason = set->reasons.data[offset + j];
-      assert(variable_db_is_boolean(db->ctx->var_db, reason));
-      ivector_push(v, reason);
-    }
-    offset += reason_size;
+  } else {
+    feasibility_int_set_get_reasons(set, reasons_out);
   }
 }
 

src/mcsat/ff/ff_feasible_set_db.h

@@ -59,6 +59,9 @@ bool ff_feasible_set_db_is_value_valid(const ff_feasible_set_db_t *db, variable_
 /** Returns true if the database has infos for x */
 bool ff_feasible_set_db_has_info(const ff_feasible_set_db_t* db, variable_t x);
 
+/** Get all reasons (mcsat variables) for the variable x. */
+void ff_feasible_set_db_get_reasons(const ff_feasible_set_db_t* db, variable_t x, ivector_t* reasons_out);
+
 /** Get the reason for a conflict on x. Feasible set of x should be empty. */
 void ff_feasible_set_db_get_conflict_reasons(const ff_feasible_set_db_t* db, variable_t x, ivector_t* reasons_out, ivector_t* lemma_reasons);
 

src/mcsat/ff/ff_libpoly.c

@@ -64,23 +64,32 @@ term_t lp_polynomial_to_yices_term_ff(ff_plugin_t *ff, const lp_polynomial_t *lp
   return result;
 }
 
-void ff_poly_constraint_create(ff_plugin_t *ff, variable_t constraint_var) {
-  // assert(poly_constraint_db_check(db));
-
+void ff_poly_constraint_add(ff_plugin_t *ff, variable_t constraint_var) {
   if (poly_constraint_db_has(ff->constraint_db, constraint_var)) {
     // Already added
     return;
   }
 
+  poly_constraint_t* cstr = ff_poly_constraint_create(ff, constraint_var);
+
+  (*ff->stats.constraint) ++;
+
+  if (ctx_trace_enabled(ff->ctx, "mcsat::new_term")) {
+    ctx_trace_printf(ff->ctx, "poly_constraint_add: ");
+    poly_constraint_print(cstr, ctx_trace_out(ff->ctx));
+    ctx_trace_printf(ff->ctx, "\n");
+  }
+
+  poly_constraint_db_add_constraint(ff->constraint_db, constraint_var, cstr);
+}
+
+poly_constraint_t* ff_poly_constraint_create(ff_plugin_t *ff, variable_t constraint_var) {
   term_t constraint_var_term;
 
   // Constraint components
   lp_polynomial_t* cstr_polynomial;
   lp_sign_condition_t sgn_condition;
 
-  // Result constraint
-  poly_constraint_t* cstr;
-
   // Context
   variable_db_t* var_db = ff->ctx->var_db;
   term_table_t* terms = ff->ctx->terms;
@@ -114,17 +123,9 @@ void ff_poly_constraint_create(ff_plugin_t *ff, variable_t constraint_var) {
   }
   default:
     assert(0);
-    return;
+    return NULL;
   }
 
-  cstr = poly_constraint_new_regular(cstr_polynomial, sgn_condition);
-  (*ff->stats.constraint) ++;
-
-  if (ctx_trace_enabled(ff->ctx, "mcsat::new_term")) {
-    ctx_trace_printf(ff->ctx, "poly_constraint_add: ");
-    poly_constraint_print(cstr, ctx_trace_out(ff->ctx));
-    ctx_trace_printf(ff->ctx, "\n");
-  }
-
-  poly_constraint_db_add_constraint(ff->constraint_db, constraint_var, cstr);
+  // Result constraint
+  return poly_constraint_new_regular(cstr_polynomial, sgn_condition);
 }

src/mcsat/ff/ff_libpoly.h

@@ -39,6 +39,9 @@ lp_polynomial_t* lp_polynomial_from_term_ff(ff_plugin_t* ff, term_t t, lp_intege
 term_t lp_polynomial_to_yices_term_ff(ff_plugin_t *ff, const lp_polynomial_t *lp_p);
 
 /** Add a new constraint */
-void ff_poly_constraint_create(ff_plugin_t *ff, variable_t constraint_var);
+void ff_poly_constraint_add(ff_plugin_t *ff, variable_t constraint_var);
+
+/** Create a new constraint */
+poly_constraint_t* ff_poly_constraint_create(ff_plugin_t *ff, variable_t constraint_var);
 
 #endif /* FF_LIBPOLY_H_ */

src/mcsat/ff/ff_plugin.c

@@ -55,6 +55,7 @@ void ff_plugin_stats_init(ff_plugin_t* ff) {
   ff->stats.constraints_attached = statistics_new_int(ff->ctx->stats, "mcsat::ff::constraints_attached");
   ff->stats.evaluations = statistics_new_int(ff->ctx->stats, "mcsat::ff::evaluations");
   ff->stats.constraint = statistics_new_int(ff->ctx->stats, "mcsat::ff::constraints");
+  ff->stats.variable_hints = statistics_new_int(ff->ctx->stats, "mcsat::ff::variable_hints");
 }
 
 static
@@ -256,7 +257,7 @@ void ff_plugin_set_lp_data(ff_plugin_t *ff, term_t t) {
 
   mpz_t order;
   mpz_init(order);
-  rational_t *order_q = ff_type_size(ff->ctx->types, tau);
+  const rational_t *order_q = ff_type_size(ff->ctx->types, tau);
   q_get_mpz(order_q, order);
 
   if (ff->lp_data) {
@@ -374,7 +375,7 @@ void ff_plugin_new_term_notify(plugin_t* plugin, term_t t, trail_token_t* prop)
     constraint_unit_info_set(&ff->unit_info, t_var, unit_status == CONSTRAINT_UNIT ? top_var : variable_null, unit_status);
 
     // Add the constraint to the database
-    ff_poly_constraint_create(ff, t_var);
+    ff_poly_constraint_add(ff, t_var);
 
     // Propagate if fully assigned
     if (unit_status == CONSTRAINT_FULLY_ASSIGNED) {
@@ -580,15 +581,20 @@ void ff_plugin_process_unit_constraint(ff_plugin_t* ff, trail_token_t* prop, var
       // you need to find a term s that evaluates to the propagated value under the current assignment, but works in general
       // and you need to find an explanaiton for this propagation
       // TODO this can be done in ff -> propagation like single polynomial propagation
-      if (!trail_has_value(ff->ctx->trail, x) && trail_is_at_base_level(ff->ctx->trail)) {
-        mcsat_value_t value;
-        lp_value_t x_value;
-        lp_value_construct_none(&x_value);
-        ff_feasible_set_db_pick_value(ff->feasible_set_db, x, &x_value);
-        mcsat_value_construct_lp_value(&value, &x_value);
-        prop->add_at_level(prop, x, &value, ff->ctx->trail->decision_level_base);
-        mcsat_value_destruct(&value);
-        lp_value_destruct(&x_value);
+      if (!trail_has_value(ff->ctx->trail, x)) {
+        if (trail_is_at_base_level(ff->ctx->trail)) {
+          mcsat_value_t value;
+          lp_value_t x_value;
+          lp_value_construct_none(&x_value);
+          ff_feasible_set_db_pick_value(ff->feasible_set_db, x, &x_value);
+          mcsat_value_construct_lp_value(&value, &x_value);
+          prop->add_at_level(prop, x, &value, ff->ctx->trail->decision_level_base);
+          mcsat_value_destruct(&value);
+          lp_value_destruct(&x_value);
+        } else {
+          (*ff->stats.variable_hints) ++;
+          ff->ctx->hint_next_decision(ff->ctx, x);
+        }
       }
     }
     polynomial_zeros_delete(zeros);

src/mcsat/ff/ff_plugin_internal.h

@@ -91,6 +91,7 @@ struct ff_plugin_s {
     statistic_int_t* constraints_attached;
     statistic_int_t* evaluations;
     statistic_int_t* constraint;
+    statistic_int_t* variable_hints;
   } stats;
 
   /** Database of polynomial constraints */

src/mcsat/nra/nra_libpoly.c

@@ -64,14 +64,31 @@ term_t lp_polynomial_to_yices_term_nra(nra_plugin_t *nra, const lp_polynomial_t
   return result;
 }
 
-void nra_poly_constraint_create(nra_plugin_t *nra, variable_t constraint_var) {
-  // assert(poly_constraint_db_check(db));
-
+void nra_poly_constraint_add(nra_plugin_t *nra, variable_t constraint_var) {
   if (poly_constraint_db_has(nra->constraint_db, constraint_var)) {
     // Already added
     return;
   }
 
+  poly_constraint_t* cstr = nra_poly_constraint_create(nra, constraint_var);
+
+  if (poly_constraint_is_root_constraint(cstr)) {
+    (*nra->stats.constraint_root) ++;
+  } else {
+    (*nra->stats.constraint_regular) ++;
+  }
+
+  if (ctx_trace_enabled(nra->ctx, "mcsat::new_term")) {
+    ctx_trace_printf(nra->ctx, "poly_constraint_add: ");
+    poly_constraint_print(cstr, ctx_trace_out(nra->ctx));
+    ctx_trace_printf(nra->ctx, "\n");
+  }
+
+  poly_constraint_db_add_constraint(nra->constraint_db, constraint_var, cstr);
+}
+
+poly_constraint_t* nra_poly_constraint_create(nra_plugin_t *nra, variable_t constraint_var) {
+  // assert(poly_constraint_db_check(db));
   term_t constraint_var_term;
 
   // Constraint components
@@ -80,9 +97,6 @@ void nra_poly_constraint_create(nra_plugin_t *nra, variable_t constraint_var) {
   uint32_t cstr_root_index;
   lp_sign_condition_t sgn_condition;
 
-  // Result constraint
-  poly_constraint_t* cstr;
-
   // Context
   variable_db_t* var_db = nra->ctx->var_db;
   term_table_t* terms = nra->ctx->terms;
@@ -194,22 +208,11 @@ void nra_poly_constraint_create(nra_plugin_t *nra, variable_t constraint_var) {
   }
   }
 
-  // Create the appropriate constraint
   if (cstr_root_variable == lp_variable_null) {
-    cstr = poly_constraint_new_regular(cstr_polynomial, sgn_condition);
-    (*nra->stats.constraint_regular) ++;
+    return poly_constraint_new_regular(cstr_polynomial, sgn_condition);
   } else {
-    cstr = poly_constraint_new_root(cstr_polynomial, sgn_condition, cstr_root_variable, cstr_root_index);
-    (*nra->stats.constraint_root) ++;
+    return poly_constraint_new_root(cstr_polynomial, sgn_condition, cstr_root_variable, cstr_root_index);
   }
-
-  if (ctx_trace_enabled(nra->ctx, "mcsat::new_term")) {
-    ctx_trace_printf(nra->ctx, "poly_constraint_add: ");
-    poly_constraint_print(cstr, ctx_trace_out(nra->ctx));
-    ctx_trace_printf(nra->ctx, "\n");
-  }
-
-  poly_constraint_db_add_constraint(nra->constraint_db, constraint_var, cstr);
 }
 
 const mcsat_value_t* nra_poly_constraint_db_approximate(nra_plugin_t* nra, variable_t constraint_var) {

src/mcsat/nra/nra_libpoly.h

@@ -42,6 +42,9 @@ term_t lp_polynomial_to_yices_term_nra(nra_plugin_t *nra, const lp_polynomial_t
 const mcsat_value_t* nra_poly_constraint_db_approximate(nra_plugin_t* nra, variable_t constraint_var);
 
 /** Add a new constraint */
-void nra_poly_constraint_create(nra_plugin_t *nra, variable_t constraint_var);
+void nra_poly_constraint_add(nra_plugin_t *nra, variable_t constraint_var);
+
+/** Create a new constraint */
+poly_constraint_t* nra_poly_constraint_create(nra_plugin_t *nra, variable_t constraint_var);
 
 #endif /* NRA_LIBPOLY_H_ */

src/mcsat/nra/nra_plugin.c

@@ -561,7 +561,7 @@ void nra_plugin_new_term_notify(plugin_t* plugin, term_t t, trail_token_t* prop)
     constraint_unit_info_set(&nra->unit_info, t_var, unit_status == CONSTRAINT_UNIT ? top_var : variable_null, unit_status);
 
     // Add the constraint to the database
-    nra_poly_constraint_create(nra, t_var);
+    nra_poly_constraint_add(nra, t_var);
 
     // Propagate if fully assigned
     if (unit_status == CONSTRAINT_FULLY_ASSIGNED) {
@@ -1351,7 +1351,7 @@ bool nra_plugin_speculate_constraint(nra_plugin_t* nra, int_mset_t* pos, int_mse
   term_t constraint_atom = unsigned_term(constraint);
   bool negated = constraint != constraint_atom;
   variable_t constraint_var = variable_db_get_variable(nra->ctx->var_db, constraint_atom);
-  nra_poly_constraint_create(nra, constraint_var);
+  nra_poly_constraint_add(nra, constraint_var);
 
   // Check if the constraint is in Boolean conflict
   if (trail_has_value(nra->ctx->trail, constraint_var)) {

src/mcsat/preprocessor.c

@@ -949,7 +949,7 @@ term_t preprocessor_apply(preprocessor_t* pre, term_t t, ivector_t* out, bool is
     case ARITH_FF_POLY:    // polynomial with finite field coefficients
     {
       polynomial_t* p = finitefield_poly_term_desc(terms, current);
-      rational_t *mod = finitefield_term_order(terms, current);
+      const rational_t *mod = finitefield_term_order(terms, current);
 
       bool children_done = true;
       bool children_same = true;

src/mcsat/solver.c

@@ -2451,6 +2451,19 @@ bool mcsat_decide(mcsat_solver_t* mcsat) {
       var = variable_null;
     }
 
+    // then try the variables a plugin requested
+    if (var == variable_null) {
+      while (!int_queue_is_empty(&mcsat->hinted_decision_vars)) {
+        var = int_queue_pop(&mcsat->hinted_decision_vars);
+        assert(var != variable_null);
+        if (!trail_has_value(mcsat->trail, var)) {
+          force_decision = true;
+          break;
+        }
+        var = variable_null;
+      }
+    }
+
     // If there is a fixed order that was passed in, try that
     if (var == variable_null) {
       const ivector_t* order = &mcsat->ctx->mcsat_var_order;