Merge 46bf35a into 49f89bf

src/mcsat/nra/feasible_set_db.c

@@ -674,3 +674,15 @@ variable_t feasible_set_db_get_fixed(feasible_set_db_t* db) {
   }
   return variable_null;
 }
+
+void feasible_set_db_approximate_value(feasible_set_db_t* db, variable_t constraint_var, lp_interval_t* result) {
+  lp_feasibility_set_t* feasible = feasible_set_db_get(db, constraint_var);
+  if (feasible != NULL) {
+    lp_feasibility_set_to_interval(feasible, result);
+  } else {
+    lp_interval_t full;
+    lp_interval_construct_full(&full);
+    lp_interval_swap(&full, result);
+    lp_interval_destruct(&full);
+  }
+}

src/mcsat/nra/feasible_set_db.h

@@ -69,3 +69,6 @@ variable_t feasible_set_db_get_cheap_unassigned(feasible_set_db_t* db, lp_value_
 
 /** Marks all the top level reasons */
 void feasible_set_db_gc_mark(feasible_set_db_t* db, gc_info_t* gc_vars);
+
+/** Get an interval approximation of the value */
+void feasible_set_db_approximate_value(feasible_set_db_t* db, variable_t constraint_var, lp_interval_t* result);

src/mcsat/nra/nra_plugin.c

@@ -118,13 +118,12 @@ void nra_plugin_construct(plugin_t* plugin, plugin_context_t* ctx) {
   nra->lp_data.lp_var_order_size = 0;
   nra->lp_data.lp_ctx = lp_polynomial_context_new(lp_Z, nra->lp_data.lp_var_db, nra->lp_data.lp_var_order);
   nra->lp_data.lp_assignment = lp_assignment_new(nra->lp_data.lp_var_db);
+  nra->lp_data.lp_interval_assignment = lp_interval_assignment_new(nra->lp_data.lp_var_db);
 
   // Tracing in libpoly
   if (false) {
-    lp_trace_enable("coefficient");
-    lp_trace_enable("coefficient::roots");
-    lp_trace_enable("polynomial");
-    lp_trace_enable("polynomial::check_input");
+    lp_trace_enable("coefficient::interval");
+    lp_trace_enable("polynomial::bounds");
   }
 
   // Trace pscs
@@ -206,6 +205,7 @@ void nra_plugin_destruct(plugin_t* plugin) {
   lp_variable_order_detach(nra->lp_data.lp_var_order);
   lp_variable_db_detach(nra->lp_data.lp_var_db);
   lp_assignment_delete(nra->lp_data.lp_assignment);
+  lp_interval_assignment_delete(nra->lp_data.lp_interval_assignment);
 
   delete_rba_buffer(&nra->buffer);
 }
@@ -676,6 +676,72 @@ void nra_plugin_new_term_notify(plugin_t* plugin, term_t t, trail_token_t* prop)
   int_mset_destruct(&t_variables);
 }
 
+static
+void nra_plugin_infer_bounds_from_constraint(nra_plugin_t* nra, trail_token_t* prop, variable_t constraint_var) {
+
+  uint32_t i;
+
+  // Just at base level for now
+  if (!trail_is_at_base_level(nra->ctx->trail)) {
+    return;
+  }
+
+  if (ctx_trace_enabled(nra->ctx, "mcsat::nra::learn")) {
+    ctx_trace_printf(nra->ctx, "nra infer bounds: constraint :\n");
+    ctx_trace_term(nra->ctx, variable_db_get_term(nra->ctx->var_db, constraint_var));
+  }
+
+  // Get the constraint
+  const poly_constraint_t* constraint = poly_constraint_db_get(nra->constraint_db, constraint_var);
+
+  // We don't handle root constraints
+  if (poly_constraint_is_root_constraint(constraint)) {
+    return;
+  }
+
+  // Value of the constraint in the trail
+  bool trail_value = trail_get_boolean_value(nra->ctx->trail, constraint_var);
+
+  // Potentially inferred variables
+  ivector_t lp_variables;
+  init_ivector(&lp_variables, 0);
+
+  // Compute the bounds
+  lp_interval_assignment_t* m = nra->lp_data.lp_interval_assignment;
+  lp_interval_assignment_reset(m);
+  bool conflict = poly_constraint_infer_bounds(constraint, !trail_value, m, &lp_variables);
+  if (conflict) {
+    if (ctx_trace_enabled(nra->ctx, "mcsat::nra::learn")) {
+      ctx_trace_printf(nra->ctx, "nra infer bounds: conflict\n");
+    }
+    nra_plugin_report_conflict(nra, prop, constraint_var);
+  } else {
+    if (ctx_trace_enabled(nra->ctx, "mcsat::nra::learn")) {
+      ctx_trace_printf(nra->ctx, "nra infer bounds: learned :\n");
+      lp_interval_assignment_print(m, ctx_trace_out(nra->ctx));
+      ctx_trace_printf(nra->ctx, "\n");
+    }
+
+    // Set the bounds
+    for (i = 0; i < lp_variables.size; ++ i) {
+      lp_variable_t x_lp = lp_variables.data[i];
+      const lp_interval_t* x_interval = lp_interval_assignment_get_interval(m, x_lp);
+      assert(x_interval != NULL);
+      if (!lp_interval_is_full(x_interval)) {
+        variable_t x = nra_plugin_get_variable_from_lp_variable(nra, x_lp);
+        lp_feasibility_set_t* x_feasible = lp_feasibility_set_new_from_interval(x_interval);
+        bool consistent = feasible_set_db_update(nra->feasible_set_db, x, x_feasible, &constraint_var, 1);
+        if (!consistent) {
+          nra_plugin_report_conflict(nra, prop, constraint_var);
+        }
+      }
+    }
+
+    delete_ivector(&lp_variables);
+  }
+}
+
+
 static
 void nra_plugin_process_unit_constraint(nra_plugin_t* nra, trail_token_t* prop, variable_t constraint_var) {
 
@@ -948,9 +1014,21 @@ void nra_plugin_propagate(plugin_t* plugin, trail_token_t* prop) {
       // Real variables, detect if the constraint is unit
       nra_plugin_process_variable_assignment(nra, prop, var);
     }
-    if (nra_plugin_get_unit_info(nra, var) == CONSTRAINT_UNIT) {
-      // Process any unit constraints
-      nra_plugin_process_unit_constraint(nra, prop, var);
+    if (nra_plugin_has_unit_info(nra, var)) {
+      constraint_unit_info_t info = nra_plugin_get_unit_info(nra, var);
+      switch (info) {
+      case CONSTRAINT_UNIT:
+        // Process any unit constraints
+        nra_plugin_process_unit_constraint(nra, prop, var);
+        break;
+      case CONSTRAINT_UNKNOWN:
+        // Try to infer any bounds
+        nra_plugin_infer_bounds_from_constraint(nra, prop, var);
+        break;
+      case CONSTRAINT_FULLY_ASSIGNED:
+        // Do nothing
+        break;
+      }
     }
   }
 
@@ -1785,6 +1863,70 @@ void nra_plugin_set_exception_handler(plugin_t* plugin, jmp_buf* handler) {
   nra->exception = handler;
 }
 
+
+static
+void nra_plugin_learn(plugin_t* plugin, trail_token_t* prop) {
+  uint32_t i;
+  variable_t constraint_var;
+
+  nra_plugin_t* nra = (nra_plugin_t*) plugin;
+  const mcsat_trail_t* trail = nra->ctx->trail;
+
+
+  if (ctx_trace_enabled(nra->ctx, "mcsat::nra::learn")) {
+    ctx_trace_printf(nra->ctx, "nra_plugin_learn(): trail = ");
+    trail_print(trail, ctx_trace_out(nra->ctx));
+  }
+
+  // Get constraints at
+  // - constraint_db->constraints
+  const ivector_t* all_constraint_vars = poly_constraint_db_get_constraints(nra->constraint_db);
+  for (i = 0; i < all_constraint_vars->size; ++ i)  {
+    constraint_var = all_constraint_vars->data[i];
+
+    // Check if it has a value already
+    bool has_value = trail_has_value(trail, constraint_var);
+    if (has_value) {
+      if (trail_get_source_id(trail, constraint_var) == nra->ctx->plugin_id) {
+        // No need to re-evaluate already propagated stuff
+        continue;
+      }
+    }
+
+    if (ctx_trace_enabled(nra->ctx, "mcsat::nra::learn")) {
+      ctx_trace_printf(nra->ctx, "nra_plugin_learn(): ");
+      ctx_trace_term(nra->ctx, variable_db_get_term(nra->ctx->var_db, constraint_var));
+    }
+
+    // Approximate the value
+    const mcsat_value_t* constraint_value = poly_constraint_db_approximate(nra->constraint_db, constraint_var, nra);
+    if (ctx_trace_enabled(nra->ctx, "mcsat::nra::learn")) {
+      ctx_trace_printf(nra->ctx, "nra_plugin_learn(): value = ");
+      FILE* out = ctx_trace_out(nra->ctx);
+      if (constraint_value != NULL) {
+        mcsat_value_print(constraint_value, out);
+      } else {
+        fprintf(out, "no value");
+      }
+      fprintf(out, "\n");
+    }
+    if (constraint_value != NULL) {
+      if (has_value) {
+        // Need to check
+        bool existing_value = trail_get_boolean_value(trail, constraint_var);
+        if (existing_value != constraint_value->b) {
+          // Propagates different value, mark conflict
+          nra_plugin_report_conflict(nra, prop, variable_null);
+          break;
+        }
+      } else {
+        prop->add(prop, constraint_var, constraint_value);
+      }
+    }
+  }
+
+}
+
 plugin_t* nra_plugin_allocator(void) {
   nra_plugin_t* plugin = safe_malloc(sizeof(nra_plugin_t));
   plugin_construct((plugin_t*) plugin);
@@ -1795,6 +1937,7 @@ plugin_t* nra_plugin_allocator(void) {
   plugin->plugin_interface.event_notify        = nra_plugin_event_notify;
   plugin->plugin_interface.propagate           = nra_plugin_propagate;
   plugin->plugin_interface.decide              = nra_plugin_decide;
+  plugin->plugin_interface.learn               = nra_plugin_learn;
   plugin->plugin_interface.get_conflict        = nra_plugin_get_conflict;
   plugin->plugin_interface.explain_propagation = nra_plugin_explain_propagation;
   plugin->plugin_interface.explain_evaluation  = nra_plugin_explain_evaluation;

src/mcsat/nra/nra_plugin_explain.c

@@ -1017,6 +1017,26 @@ void nra_plugin_explain_conflict(nra_plugin_t* nra, const int_mset_t* pos, const
     int_mset_destruct(&variables);
   }
 
+  // Check if there is a simple Fourier-Motzkin explanation
+  if (false && core->size == 2 && lemma_reasons->size == 0) {
+    variable_t c0_var = core->data[0];
+    variable_t c1_var = core->data[1];
+    bool c0_negated = !constraint_get_value(nra->ctx->trail, pos, neg, c0_var);
+    bool c1_negated = !constraint_get_value(nra->ctx->trail, pos, neg, c1_var);
+    const poly_constraint_t* c0 = poly_constraint_db_get(nra->constraint_db, c0_var);
+    const poly_constraint_t* c1 = poly_constraint_db_get(nra->constraint_db, c1_var);
+    bool resolved = poly_constraint_resolve_fm(c0, c0_negated, c1, c1_negated, nra, conflict);
+    if (resolved) {
+      term_t c0_term = variable_db_get_term(nra->ctx->var_db, c0_var);
+      if (c0_negated) c0_term = opposite_term(c0_term);
+      term_t c1_term = variable_db_get_term(nra->ctx->var_db, c1_var);
+      if (c1_negated) c1_term = opposite_term(c1_term);
+      ivector_push(conflict, c0_term);
+      ivector_push(conflict, c1_term);
+      return;
+    }
+  }
+
   // Create the map from variables to
   lp_projection_map_t projection_map;
   lp_projection_map_construct(&projection_map, nra);
@@ -1027,8 +1047,20 @@ void nra_plugin_explain_conflict(nra_plugin_t* nra, const int_mset_t* pos, const
     variable_t constraint_var = core->data[core_i];
     assert(constraint_has_value(nra->ctx->trail, pos, neg, constraint_var));
     const poly_constraint_t* constraint = poly_constraint_db_get(nra->constraint_db, constraint_var);
-    const lp_polynomial_t* p = poly_constraint_get_polynomial(constraint);
-    lp_projection_map_add(&projection_map, p);
+    // If the polynomial isn't unit, it is a global inference, so we explain with a different polynomial
+    if (!poly_constraint_is_unit(constraint, nra->lp_data.lp_assignment)) {
+      const lp_polynomial_t* p = poly_constraint_get_polynomial(constraint);
+      lp_sign_condition_t sgn_condition = poly_constraint_get_sign_condition(constraint);
+      bool negated = !trail_get_boolean_value(nra->ctx->trail, constraint_var);
+      lp_variable_t x = poly_constraint_get_top_variable(constraint);
+      lp_polynomial_t* p_inference_reason = lp_polynomial_constraint_explain_infer_bounds(p, sgn_condition, negated, x);
+      lp_projection_map_add(&projection_map, p_inference_reason);
+      lp_polynomial_delete(p_inference_reason);
+    } else {
+      const lp_polynomial_t* p = poly_constraint_get_polynomial(constraint);
+      lp_projection_map_add(&projection_map, p);
+    }
+
   }
 
   // Add all the top-level reasons for the conflict variable

src/mcsat/nra/nra_plugin_internal.c

@@ -154,6 +154,11 @@ void nra_plugin_set_unit_info(nra_plugin_t* nra, variable_t constraint, variable
   }
 }
 
+bool nra_plugin_has_unit_info(const nra_plugin_t* nra, variable_t constraint) {
+  int_hmap_pair_t* find = int_hmap_find(&((nra_plugin_t*)nra)->constraint_unit_info, constraint);
+  return find != NULL;
+}
+
 constraint_unit_info_t nra_plugin_get_unit_info(nra_plugin_t* nra, variable_t constraint) {
   int_hmap_pair_t* find = int_hmap_find(&nra->constraint_unit_info, constraint);
   if (find == NULL)  {

src/mcsat/nra/nra_plugin_internal.h

@@ -102,6 +102,8 @@ struct nra_plugin_s {
     lp_polynomial_context_t* lp_ctx;
     /** Libpoly model */
     lp_assignment_t* lp_assignment;
+    /** Interval assignment for bound inference */
+    lp_interval_assignment_t* lp_interval_assignment;
 
     /** Map from libpoly variables to mcsat variables */
     int_hmap_t lp_to_mcsat_var_map;
@@ -160,6 +162,9 @@ variable_t nra_plugin_get_variable_from_lp_variable(nra_plugin_t* nra, lp_variab
 /** Set the unit info for the given constraint */
 void nra_plugin_set_unit_info(nra_plugin_t* nra, variable_t constraint, variable_t unit_var, constraint_unit_info_t value);
 
+/** Are we tracking this constraint */
+bool nra_plugin_has_unit_info(const nra_plugin_t* nra, variable_t constraint);
+
 /** Get the unit info for the given constraint */
 constraint_unit_info_t nra_plugin_get_unit_info(nra_plugin_t* nra, variable_t constraint);