From d60ebba114438ba59ca529a9bf6f23b34974f824 Mon Sep 17 00:00:00 2001 From: Ahmed <43099566+ahmed-irfan@users.noreply.github.com> Date: Wed, 29 Nov 2023 23:13:34 -0800 Subject: [PATCH 1/5] don't propagate top-level equality if the types of lhs and rhs are not the same --- src/mcsat/preprocessor.c | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/src/mcsat/preprocessor.c b/src/mcsat/preprocessor.c index 07171b1fe..7f3b5ec78 100644 --- a/src/mcsat/preprocessor.c +++ b/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_mixed = + term_type(pre->terms, desc->arg[0]) != term_type(pre->terms, desc->arg[1]); + // don't rewrite if equality is between mixed terms, e.g. between int and real terms + if (!is_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]; From b40200f1d99dacc5525a791ce09297e35c34a0ed Mon Sep 17 00:00:00 2001 From: Ahmed <43099566+ahmed-irfan@users.noreply.github.com> Date: Wed, 29 Nov 2023 23:23:15 -0800 Subject: [PATCH 2/5] add regression tests --- tests/regress/mcsat/lia/lira_00.smt2 | 23 ++++++++++++++++++++ tests/regress/mcsat/lia/lira_00.smt2.gold | 1 + tests/regress/mcsat/lia/lira_00.smt2.options | 1 + tests/regress/mcsat/nia/nira_00.smt2 | 23 ++++++++++++++++++++ tests/regress/mcsat/nia/nira_00.smt2.gold | 1 + 5 files changed, 49 insertions(+) create mode 100644 tests/regress/mcsat/lia/lira_00.smt2 create mode 100644 tests/regress/mcsat/lia/lira_00.smt2.gold create mode 100644 tests/regress/mcsat/lia/lira_00.smt2.options create mode 100644 tests/regress/mcsat/nia/nira_00.smt2 create mode 100644 tests/regress/mcsat/nia/nira_00.smt2.gold diff --git a/tests/regress/mcsat/lia/lira_00.smt2 b/tests/regress/mcsat/lia/lira_00.smt2 new file mode 100644 index 000000000..5cd3d5553 --- /dev/null +++ b/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) diff --git a/tests/regress/mcsat/lia/lira_00.smt2.gold b/tests/regress/mcsat/lia/lira_00.smt2.gold new file mode 100644 index 000000000..3f65111b0 --- /dev/null +++ b/tests/regress/mcsat/lia/lira_00.smt2.gold @@ -0,0 +1 @@ +unsat diff --git a/tests/regress/mcsat/lia/lira_00.smt2.options b/tests/regress/mcsat/lia/lira_00.smt2.options new file mode 100644 index 000000000..bcf7e6dae --- /dev/null +++ b/tests/regress/mcsat/lia/lira_00.smt2.options @@ -0,0 +1 @@ +--mcsat diff --git a/tests/regress/mcsat/nia/nira_00.smt2 b/tests/regress/mcsat/nia/nira_00.smt2 new file mode 100644 index 000000000..a6cc46bed --- /dev/null +++ b/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))) + +(check-sat) +(exit) diff --git a/tests/regress/mcsat/nia/nira_00.smt2.gold b/tests/regress/mcsat/nia/nira_00.smt2.gold new file mode 100644 index 000000000..3f65111b0 --- /dev/null +++ b/tests/regress/mcsat/nia/nira_00.smt2.gold @@ -0,0 +1 @@ +unsat From 71888bfbe38eca706b057281ecab84b14f025d0a Mon Sep 17 00:00:00 2001 From: Ahmed <43099566+ahmed-irfan@users.noreply.github.com> Date: Wed, 29 Nov 2023 23:24:41 -0800 Subject: [PATCH 3/5] api test --- tests/api/test_nira.c | 64 +++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 64 insertions(+) create mode 100644 tests/api/test_nira.c diff --git a/tests/api/test_nira.c b/tests/api/test_nira.c new file mode 100644 index 000000000..0374b2109 --- /dev/null +++ b/tests/api/test_nira.c @@ -0,0 +1,64 @@ +#ifdef NDEBUG +#undef NDEBUG +#endif + +#include + +#include "assert.h" + +#include + +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; +} From 7fa9e25e1c92d7ed559db832a6c5fbce30922063 Mon Sep 17 00:00:00 2001 From: Ahmed <43099566+ahmed-irfan@users.noreply.github.com> Date: Thu, 30 Nov 2023 13:06:18 -0800 Subject: [PATCH 4/5] fix corner case of ARITH_EQ_TERM in detecting is_mixed --- src/mcsat/preprocessor.c | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/mcsat/preprocessor.c b/src/mcsat/preprocessor.c index 7f3b5ec78..58807edd1 100644 --- a/src/mcsat/preprocessor.c +++ b/src/mcsat/preprocessor.c @@ -511,10 +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) { - bool is_mixed = - term_type(pre->terms, desc->arg[0]) != term_type(pre->terms, desc->arg[1]); - // don't rewrite if equality is between mixed terms, e.g. between int and real terms - if (!is_mixed && 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]; From 424c00633b76dfbb599cb098b6ecee755a39bd2e Mon Sep 17 00:00:00 2001 From: Ahmed <43099566+ahmed-irfan@users.noreply.github.com> Date: Thu, 30 Nov 2023 13:07:49 -0800 Subject: [PATCH 5/5] update test --- tests/regress/mcsat/nia/nira_00.smt2 | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/regress/mcsat/nia/nira_00.smt2 b/tests/regress/mcsat/nia/nira_00.smt2 index a6cc46bed..23b0936d6 100644 --- a/tests/regress/mcsat/nia/nira_00.smt2 +++ b/tests/regress/mcsat/nia/nira_00.smt2 @@ -17,7 +17,7 @@ (assert (< (+ (- 7) pure_y) 0)) (assert (= pure_xy 7)) -(assert (= pure_xy (* x y))) +(assert (= (+ pure_xy (* x (- y))) 0)) (check-sat) (exit)