MCSAT: Preprocessor: fix equality simplification for mixed real-integ…

…er terms (#481)

It is wrong to remove integer variable by substituting a real variable.
This was happening in the mcsat preprocessor during equality propagation of the top-level equality x_int_var = y_real_var.
This PR fixes this issue by not doing propagation of such equalities.

This PR:

Fixes mcsat preprocessor
Adds regression tests
Adds api test

* don't propagate top-level equality if the types of lhs and rhs are not the same

* add regression tests

* api test

* fix corner case of ARITH_EQ_TERM in detecting is_mixed

* update test

src/mcsat/preprocessor.c

@@ -511,7 +511,10 @@ term_t preprocessor_apply(preprocessor_t* pre, term_t t, ivector_t* out, bool is
 
       term_t eq_solve_var = NULL_TERM;
       if (is_assertion && is_equality && !is_boolean) {
-        if (current == t) {
+	bool is_lhs_rhs_mixed = desc->arity > 1 &&
+	  term_type_kind(pre->terms, desc->arg[0]) != term_type_kind(pre->terms, desc->arg[1]);
+	// don't rewrite if equality is between mixed terms, e.g. between int and real terms
+	if (!is_lhs_rhs_mixed && current == t) {
           eq_solve_var = preprocessor_get_eq_solved_var(pre, t);
           if (eq_solve_var == NULL_TERM) {
             term_t lhs = desc->arg[0];

tests/api/test_nira.c

@@ -0,0 +1,64 @@
+#ifdef NDEBUG
+#undef NDEBUG
+#endif
+
+#include <stdlib.h>
+
+#include "assert.h"
+
+#include <yices.h>
+
+int main(void)
+{
+  if (! yices_has_mcsat()) {
+    return 1; // skipped
+  }
+  yices_init();
+
+  ctx_config_t* config = yices_new_config();
+  yices_set_config(config, "solver-type", "mcsat");
+  context_t* ctx = yices_new_context(config);
+
+  term_t x = yices_new_uninterpreted_term(yices_int_type());
+  yices_set_term_name(x, "x");
+
+  term_t y = yices_new_uninterpreted_term(yices_int_type());
+  yices_set_term_name(y, "y");
+
+  term_t p_x = yices_new_uninterpreted_term(yices_real_type());
+  yices_set_term_name(p_x, "p_x");
+
+  term_t p_y = yices_new_uninterpreted_term(yices_real_type());
+  yices_set_term_name(p_y, "p_y");
+
+  term_t p_xy = yices_new_uninterpreted_term(yices_real_type());
+  yices_set_term_name(p_xy, "p_xy");
+
+  assert(!yices_error_code());
+
+  term_t xy = yices_mul(x, y);
+
+  // assertion
+
+  yices_assert_formula(ctx, yices_arith_eq_atom(x, p_x));
+  yices_assert_formula(ctx, yices_arith_gt_atom(p_x, yices_int32(1)));
+  yices_assert_formula(ctx, yices_arith_lt_atom(p_x, yices_int32(7)));
+
+  yices_assert_formula(ctx, yices_arith_eq_atom(y, p_y));
+  yices_assert_formula(ctx, yices_arith_gt_atom(p_y, yices_int32(1)));
+  yices_assert_formula(ctx, yices_arith_lt_atom(p_y, yices_int32(7)));
+
+  yices_assert_formula(ctx, yices_arith_eq_atom(xy, p_xy));
+  yices_assert_formula(ctx, yices_arith_eq_atom(p_xy, yices_int32(7)));
+
+  smt_status_t status;
+  status = yices_check_context(ctx, NULL);
+  assert(!yices_error_code());
+
+  assert(status == STATUS_UNSAT);
+
+  yices_free_context(ctx);
+  yices_exit();
+
+  return 0;
+}

tests/regress/mcsat/lia/lira_00.smt2

@@ -0,0 +1,23 @@
+(set-logic QF_LIRA)
+(set-info :smt-lib-version 2.0)
+
+(declare-fun x () Int)
+(declare-fun y () Int)
+
+(declare-fun pure_x () Real)
+(declare-fun pure_y () Real)
+(declare-fun pure_xy () Real)
+
+(assert (= pure_x x))
+(assert (< (+ 1 (* (- 1) pure_x)) 0))
+(assert (< (+ (- 7) pure_x) 0))
+
+(assert (= pure_y y))
+(assert (< (+ 1 (* (- 1) pure_y)) 0))
+(assert (< (+ (- 7) pure_y) 0))
+
+(assert (= pure_xy 3))
+(assert (= pure_xy (+ x y)))
+
+(check-sat)
+(exit)

tests/regress/mcsat/lia/lira_00.smt2.gold

@@ -0,0 +1 @@
+unsat

tests/regress/mcsat/lia/lira_00.smt2.options

@@ -0,0 +1 @@
+--mcsat

tests/regress/mcsat/nia/nira_00.smt2

@@ -0,0 +1,23 @@
+(set-logic QF_NIRA)
+(set-info :smt-lib-version 2.0)
+
+(declare-fun x () Int)
+(declare-fun y () Int)
+
+(declare-fun pure_x () Real)
+(declare-fun pure_y () Real)
+(declare-fun pure_xy () Real)
+
+(assert (= pure_x x))
+(assert (< (+ 1 (* (- 1) pure_x)) 0))
+(assert (< (+ (- 7) pure_x) 0))
+
+(assert (= pure_y y))
+(assert (< (+ 1 (* (- 1) pure_y)) 0))
+(assert (< (+ (- 7) pure_y) 0))
+
+(assert (= pure_xy 7))
+(assert (= (+ pure_xy (* x (- y))) 0))
+
+(check-sat)
+(exit)

tests/regress/mcsat/nia/nira_00.smt2.gold

@@ -0,0 +1 @@
+unsat