From dbb56e8ed04be1fbbdd5448c738c2bfcdc5a19ea Mon Sep 17 00:00:00 2001 From: Dejan Jovanovic Date: Wed, 13 May 2020 20:31:22 -0400 Subject: [PATCH 01/16] progress and first test --- src/mcsat/nra/feasible_set_db.c | 12 ++++ src/mcsat/nra/feasible_set_db.h | 3 + src/mcsat/nra/nra_plugin.c | 64 +++++++++++++++-- src/mcsat/nra/poly_constraint.c | 72 ++++++++++++++++++- src/mcsat/nra/poly_constraint.h | 8 ++- src/mcsat/plugin.h | 8 +++ src/mcsat/solver.c | 29 ++++++-- .../mcsat/nra/sin-problem-7-chunk-0215.smt2 | 27 +++++++ .../nra/sin-problem-7-chunk-0215.smt2.gold | 1 + 9 files changed, 211 insertions(+), 13 deletions(-) create mode 100644 tests/regress/mcsat/nra/sin-problem-7-chunk-0215.smt2 create mode 100644 tests/regress/mcsat/nra/sin-problem-7-chunk-0215.smt2.gold diff --git a/src/mcsat/nra/feasible_set_db.c b/src/mcsat/nra/feasible_set_db.c index 184655122..509fc7946 100644 --- a/src/mcsat/nra/feasible_set_db.c +++ b/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); + } +} diff --git a/src/mcsat/nra/feasible_set_db.h b/src/mcsat/nra/feasible_set_db.h index 37d82e794..432f67843 100644 --- a/src/mcsat/nra/feasible_set_db.h +++ b/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); diff --git a/src/mcsat/nra/nra_plugin.c b/src/mcsat/nra/nra_plugin.c index a2bfb0e1d..cc0378a11 100644 --- a/src/mcsat/nra/nra_plugin.c +++ b/src/mcsat/nra/nra_plugin.c @@ -121,10 +121,7 @@ void nra_plugin_construct(plugin_t* plugin, plugin_context_t* ctx) { // 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"); } // Trace pscs @@ -1785,6 +1782,64 @@ 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; + + // 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 +1850,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; diff --git a/src/mcsat/nra/poly_constraint.c b/src/mcsat/nra/poly_constraint.c index 42c52b548..1089eed96 100644 --- a/src/mcsat/nra/poly_constraint.c +++ b/src/mcsat/nra/poly_constraint.c @@ -24,6 +24,8 @@ #include #include #include +#include +#include /** * A constraint of the form sgn(p(x)) = sgn_conition. @@ -69,6 +71,9 @@ struct poly_constraint_db_struct { /** Map from variables to constraint references */ int_hmap_t var_to_constraint_map; + + /** List of all constraint variables */ + ivector_t all_constraint_variables; }; static @@ -117,10 +122,11 @@ void poly_constraint_db_gc_sweep(poly_constraint_db_t* db, const gc_info_t* gc_v init_int_hmap(&new_var_to_constraint_map, 0); // Move the constraints - int_hmap_pair_t* it = int_hmap_first_record(&db->var_to_constraint_map); - for (; it != NULL; it = int_hmap_next_record(&db->var_to_constraint_map, it)) { + uint32_t i, to_keep = 0; + for (i = 0; i < db->all_constraint_variables.size; ++ i) { + variable_t old_constraint_var = db->all_constraint_variables.data[i]; + int_hmap_pair_t* it = int_hmap_find(&db->var_to_constraint_map, old_constraint_var); // Do we keep it - variable_t old_constraint_var = it->key; variable_t new_constraint_var = gc_info_get_reloc(gc_vars, old_constraint_var); poly_constraint_t* constraint = db->constraints.data[it->val]; if (new_constraint_var != gc_vars->null_value) { @@ -128,6 +134,7 @@ void poly_constraint_db_gc_sweep(poly_constraint_db_t* db, const gc_info_t* gc_v uint32_t new_index = new_constraints.size; pvector_push(&new_constraints, constraint); int_hmap_add(&new_var_to_constraint_map, new_constraint_var, new_index); + db->all_constraint_variables.data[to_keep ++] = new_constraint_var; } else { if (ctx_trace_enabled(db->nra->ctx, "nra::gc")) { ctx_trace_printf(db->nra->ctx, "Removing constraint :"); @@ -144,6 +151,7 @@ void poly_constraint_db_gc_sweep(poly_constraint_db_t* db, const gc_info_t* gc_v delete_int_hmap(&db->var_to_constraint_map); db->constraints = new_constraints; db->var_to_constraint_map = new_var_to_constraint_map; + ivector_shrink(&db->all_constraint_variables, to_keep); } @@ -287,6 +295,7 @@ void poly_constraint_db_construct(poly_constraint_db_t* db, nra_plugin_t* nra) { init_pvector(&db->constraints, 0); init_int_hmap(&db->var_to_constraint_map, 0); + init_ivector(&db->all_constraint_variables, 0); } poly_constraint_db_t* poly_constraint_db_new(nra_plugin_t* nra) { @@ -307,6 +316,7 @@ void poly_constraint_db_destruct(poly_constraint_db_t* db) { delete_pvector(&db->constraints); delete_int_hmap(&db->var_to_constraint_map); + delete_ivector(&db->all_constraint_variables); } void poly_constraint_db_delete(poly_constraint_db_t* db) { @@ -314,6 +324,11 @@ void poly_constraint_db_delete(poly_constraint_db_t* db) { safe_free(db); } +const ivector_t* poly_constraint_db_get_constraints(const poly_constraint_db_t* db) { + return &db->all_constraint_variables; +} + + bool poly_constraint_db_check(const poly_constraint_db_t* db) { uint32_t i; for (i = 0; i < db->constraints.size; ++ i) { @@ -494,6 +509,7 @@ void poly_constraint_db_add(poly_constraint_db_t* db, variable_t constraint_var) // Add the constraint pvector_push(&db->constraints, cstr); int_hmap_add(&db->var_to_constraint_map, constraint_var, index); + ivector_push(&db->all_constraint_variables, constraint_var); // assert(poly_constraint_db_check(db)); } @@ -525,3 +541,53 @@ bool poly_constraint_evaluate(const poly_constraint_t* cstr, nra_plugin_t* nra, return true; } + +const mcsat_value_t* poly_constraint_db_approximate(poly_constraint_db_t* db, variable_t constraint_var, nra_plugin_t* nra) { + const mcsat_value_t* result = NULL; + + // Get the constraints + const poly_constraint_t* cstr = poly_constraint_db_get(db, constraint_var); + if (poly_constraint_is_root_constraint(cstr)) { + // TODO: check if possible + return NULL; + } + + // Construct the interval assignmetn + lp_interval_assignment_t m; + lp_interval_assignment_construct(&m, nra->lp_data.lp_var_db); + + // Setup the assignment x -> I(x) + lp_variable_list_t vars; + lp_variable_list_construct(&vars); + lp_polynomial_get_variables(cstr->polynomial, &vars); + uint32_t var_i; + for (var_i = 0; var_i < vars.list_size; ++ var_i) { + lp_variable_t x_lp = vars.list[var_i]; + variable_t x = nra_plugin_get_variable_from_lp_variable(nra, x_lp); + lp_interval_t x_interval; + lp_interval_construct_full(&x_interval); + feasible_set_db_approximate_value(nra->feasible_set_db, x, &x_interval); + lp_interval_assignment_set_interval(&m, x_lp, &x_interval); + lp_interval_destruct(&x_interval); + } + + // Evaluate the polynomial + lp_interval_t value; + lp_interval_construct_full(&value); + lp_polynomial_interval_value(cstr->polynomial, &m, &value); + + lp_sign_condition_t pos = cstr->sgn_condition; + lp_sign_condition_t neg = lp_sign_condition_negate(cstr->sgn_condition); + + if (lp_sign_condition_consistent_interval(pos, &value)) { + result = &mcsat_value_true; + } else if (lp_sign_condition_consistent_interval(neg, &value)) { + result = &mcsat_value_false; + } + + // Remove temps + lp_variable_list_destruct(&vars); + lp_interval_assignment_destruct(&m); + + return result; +} diff --git a/src/mcsat/nra/poly_constraint.h b/src/mcsat/nra/poly_constraint.h index e80c20c24..6b6b638c4 100644 --- a/src/mcsat/nra/poly_constraint.h +++ b/src/mcsat/nra/poly_constraint.h @@ -1,4 +1,4 @@ -/* + /* * This file is part of the Yices SMT Solver. * Copyright (C) 2017 SRI International. * @@ -95,9 +95,15 @@ void poly_constraint_db_destruct(poly_constraint_db_t* db); /** Delete the database */ void poly_constraint_db_delete(poly_constraint_db_t* db); +/** Get all constraints (as variables) */ +const ivector_t* poly_constraint_db_get_constraints(const poly_constraint_db_t* db); + /** Get the constraint of the variable (must exist) */ const poly_constraint_t* poly_constraint_db_get(poly_constraint_db_t* db, variable_t constraint_var); +/** Compute an approximation of the constraint value with interval computation */ +const mcsat_value_t* poly_constraint_db_approximate(poly_constraint_db_t* db, variable_t constraint_var, nra_plugin_t* nra); + /** Add a new constraint */ void poly_constraint_db_add(poly_constraint_db_t* db, variable_t constraint_var); diff --git a/src/mcsat/plugin.h b/src/mcsat/plugin.h index 5aa3e1dcd..bf6301ed5 100644 --- a/src/mcsat/plugin.h +++ b/src/mcsat/plugin.h @@ -214,6 +214,13 @@ struct plugin_s { */ void (*decide) (plugin_t* plugin, variable_t x, trail_token_t* decide, bool must); + /** + * Optional: learn using the given trail token. This is called at base level after + * propagation is done and there is no conflict. This is a chance to perform some + * more expensive reasoning and propagate consequences. + */ + void (*learn) (plugin_t* plugin, trail_token_t* prop); + /** * Explain the conflict that you reported. The plugin should return a conflict * such that @@ -291,6 +298,7 @@ void plugin_construct(plugin_t* plugin) { plugin->new_lemma_notify = NULL; plugin->propagate = NULL; plugin->decide = NULL; + plugin->learn = NULL; plugin->get_conflict = NULL; plugin->explain_propagation = NULL; plugin->explain_evaluation = NULL; diff --git a/src/mcsat/solver.c b/src/mcsat/solver.c index 2c9dc9121..fbf1bafd0 100644 --- a/src/mcsat/solver.c +++ b/src/mcsat/solver.c @@ -1282,7 +1282,7 @@ void mcsat_process_requests(mcsat_solver_t* mcsat) { * is encountered. */ static -bool mcsat_propagate(mcsat_solver_t* mcsat) { +bool mcsat_propagate(mcsat_solver_t* mcsat, bool run_learning) { uint32_t plugin_i; plugin_t* plugin; @@ -1295,7 +1295,7 @@ bool mcsat_propagate(mcsat_solver_t* mcsat) { // Propagate with all the plugins in turn for (plugin_i = 0; trail_is_consistent(mcsat->trail) && plugin_i < mcsat->plugins_count; ++ plugin_i) { if (trace_enabled(mcsat->ctx->trace, "mcsat::propagate")) { - mcsat_trace_printf(mcsat->ctx->trace, "mcsat_propagate(): with %s\n", mcsat->plugins[plugin_i].plugin_name); + mcsat_trace_printf(mcsat->ctx->trace, "mcsat_propagate(): propagting with %s\n", mcsat->plugins[plugin_i].plugin_name); } // Make the token trail_token_construct(&prop_token, mcsat->plugins[plugin_i].plugin_ctx, variable_null); @@ -1308,6 +1308,25 @@ bool mcsat_propagate(mcsat_solver_t* mcsat) { someone_propagated = true; } } + // If at base level, plugins can do some more expensive learning/propagation + if (run_learning && !someone_propagated && trail_is_at_base_level(mcsat->trail)) { + // Propagate with all the plugins in turn + for (plugin_i = 0; trail_is_consistent(mcsat->trail) && plugin_i < mcsat->plugins_count; ++ plugin_i) { + if (trace_enabled(mcsat->ctx->trace, "mcsat::propagate")) { + mcsat_trace_printf(mcsat->ctx->trace, "mcsat_propagate(): learning with %s\n", mcsat->plugins[plugin_i].plugin_name); + } + // Make the token + trail_token_construct(&prop_token, mcsat->plugins[plugin_i].plugin_ctx, variable_null); + // Propagate + plugin = mcsat->plugins[plugin_i].plugin; + if (plugin->learn) { + plugin->learn(plugin, (trail_token_t*) &prop_token); + } + if (prop_token.used > 0) { + someone_propagated = true; + } + } + } } while (someone_propagated && trail_is_consistent(mcsat->trail)); return someone_propagated; @@ -1368,7 +1387,7 @@ void mcsat_assert_formula(mcsat_solver_t* mcsat, term_t f) { } // Do propagation - mcsat_propagate(mcsat); + mcsat_propagate(mcsat, false); } /** @@ -1528,7 +1547,7 @@ void mcsat_add_lemma(mcsat_solver_t* mcsat, ivector_t* lemma, term_t decision_bo } // Propagate any - mcsat_propagate(mcsat); + mcsat_propagate(mcsat, false); bool propagated = old_trail_size < mcsat->trail->elements.size; // Decide a literal if necessary. At this point, if it was UIP they are all @@ -2049,7 +2068,7 @@ void mcsat_solve(mcsat_solver_t* mcsat, const param_t *params) { mcsat_process_requests(mcsat); // Do propagation - mcsat_propagate(mcsat); + mcsat_propagate(mcsat, true); // If inconsistent, analyze the conflict if (!trail_is_consistent(mcsat->trail)) { diff --git a/tests/regress/mcsat/nra/sin-problem-7-chunk-0215.smt2 b/tests/regress/mcsat/nra/sin-problem-7-chunk-0215.smt2 new file mode 100644 index 000000000..cc7de8f46 --- /dev/null +++ b/tests/regress/mcsat/nra/sin-problem-7-chunk-0215.smt2 @@ -0,0 +1,27 @@ +(set-info :smt-lib-version 2.6) +(set-logic QF_NRA) +(set-info :source | +These benchmarks used in the paper: + + Dejan Jovanovic and Leonardo de Moura. Solving Non-Linear Arithmetic. + In IJCAR 2012, published as LNCS volume 7364, pp. 339--354. + +The meti-tarski benchmarks are proof obligations extracted from the +Meti-Tarski project, see: + + B. Akbarpour and L. C. Paulson. MetiTarski: An automatic theorem prover + for real-valued special functions. Journal of Automated Reasoning, + 44(3):175-205, 2010. + +Submitted by Dejan Jovanovic for SMT-LIB. + + +|) +(set-info :category "industrial") +(set-info :status unsat) +(declare-fun skoX () Real) +(declare-fun skoY () Real) +(declare-fun pi () Real) +(assert (let ((?v_0 (* skoX (/ (- 1) 6))) (?v_1 (* skoX (/ 1 120))) (?v_2 (* skoX (/ (- 1) 5040)))) (and (<= skoY 0) (and (not (<= (* skoY (+ (* skoX (* skoX (+ (/ 1 6) (* skoX (* skoX (+ (/ (- 1) 120) (* skoX (* skoX (+ (/ 1 5040) (* skoX (* skoX (+ (/ (- 1) 362880) (* skoX (* skoX (/ 1 39916800))))))))))))))) (* skoY (* skoY (/ (- 1) 6))))) 0)) (and (not (<= (* skoY (* skoY (+ ?v_0 (* skoY (* skoY (+ ?v_1 (* skoY (* skoY (+ ?v_2 (* skoY (* skoY (* skoX (/ 1 362880))))))))))))) (* skoX (* skoX (* skoX (+ (/ (- 1) 6) (* skoX (* skoX (+ (/ 1 120) (* skoX (* skoX (+ (/ (- 1) 5040) (* skoX (* skoX (+ (/ 1 362880) (* skoX (* skoX (/ (- 1) 39916800)))))))))))))))))) (and (not (<= (* skoY (+ (* skoX (* skoX (+ (/ 1 6) (* skoX (* skoX (+ (/ (- 1) 120) (* skoX (* skoX (/ 1 5040))))))))) (* skoY (* skoY (+ (/ (- 1) 6) (* skoY (* skoY (+ (/ 1 120) (* skoY (* skoY (+ (/ (- 1) 5040) (* skoY (* skoY (/ 1 362880)))))))))))))) 0)) (and (not (<= (* skoY (* skoY (+ ?v_0 (* skoY (* skoY ?v_1))))) (* skoX (* skoX (* skoX (+ (/ (- 1) 6) (* skoX (* skoX (+ (/ 1 120) (* skoX ?v_2)))))))))) (and (not (<= (* skoY (+ (* skoX (* skoX (/ 1 6))) (* skoY (* skoY (+ (/ (- 1) 6) (* skoY (* skoY (/ 1 120)))))))) 0)) (and (not (<= skoX 0)) (and (not (<= pi (/ 15707963 5000000))) (and (not (<= (/ 31415927 10000000) pi)) (and (<= skoY (* pi (/ 1 2))) (and (<= 0 skoX) (not (<= skoY skoX))))))))))))))) +(check-sat) +(exit) diff --git a/tests/regress/mcsat/nra/sin-problem-7-chunk-0215.smt2.gold b/tests/regress/mcsat/nra/sin-problem-7-chunk-0215.smt2.gold new file mode 100644 index 000000000..3f65111b0 --- /dev/null +++ b/tests/regress/mcsat/nra/sin-problem-7-chunk-0215.smt2.gold @@ -0,0 +1 @@ +unsat From 70bbab3fdd067566755263bc14417e2cc3b2a6d5 Mon Sep 17 00:00:00 2001 From: Dejan Jovanovic Date: Wed, 13 May 2020 20:37:39 -0400 Subject: [PATCH 02/16] more tests --- tests/regress/mcsat/nra/mbo_E22E23.smt2 | 47 ++++++++++++++++++++ tests/regress/mcsat/nra/mbo_E22E23.smt2.gold | 1 + 2 files changed, 48 insertions(+) create mode 100644 tests/regress/mcsat/nra/mbo_E22E23.smt2 create mode 100644 tests/regress/mcsat/nra/mbo_E22E23.smt2.gold diff --git a/tests/regress/mcsat/nra/mbo_E22E23.smt2 b/tests/regress/mcsat/nra/mbo_E22E23.smt2 new file mode 100644 index 000000000..ac48a5689 --- /dev/null +++ b/tests/regress/mcsat/nra/mbo_E22E23.smt2 @@ -0,0 +1,47 @@ +(set-info :smt-lib-version 2.6) +(set-logic QF_NRA) +(set-info :author |Thomas Sturm, CNRS France, http://science.thomas-sturm.de|) +(set-info :source | +Transmitted by: Thomas Sturm +Generated on: 20161105 +Received on: 20161105 +Generator: RedLog, http://www.redlog.eu/ +Application: qualitative analysis of systems of ODE in physics, chemistry, and the life sciences +Publication: Algebraic Biology 2008, doi:10.1007/978-3-540-85101-1_15 +Additional information: +All problems have the following form: a certain polynomial has a zero where all variables are positive. Interval solutions for satisfiable problems is a valuable information. +|) +(set-info :series |MBO - Methylene Blue Oscillator System|) +(set-info :instance |E22E23|) +(set-info :category "industrial") +(set-info :status unsat) +(declare-const j2 Real) +(declare-const h6 Real) +(declare-const h5 Real) +(declare-const h4 Real) +(declare-const h3 Real) +(declare-const h1 Real) +(assert (and (> h1 0) (> h3 0) (> h4 0) (> h5 0) (> h6 0) (> j2 0) (= (+ (* (* +h1 h1) h3 j2) (* (* h1 h1) h5 j2) (* (* h1 h1) h5) (* (* h1 h1) h6 j2) (* (* h1 +h1) h6) (* h1 (* h3 h3) (* j2 j2)) (* h1 (* h3 h3) j2) (* 2 h1 h3 h4 j2) (* h1 +h3 h4) (* 2 h1 h3 h5 (* j2 j2)) (* 4 h1 h3 h5 j2) (* 2 h1 h3 h5) (* 2 h1 h3 h6 +(* j2 j2)) (* 5 h1 h3 h6 j2) (* 2 h1 h3 h6) (* 2 h1 h4 h5 j2) (* 2 h1 h4 h5) (* +2 h1 h4 h6 j2) (* h1 h4 h6) (* h1 (* h5 h5) (* j2 j2)) (* 2 h1 (* h5 h5) j2) (* +h1 (* h5 h5)) (* 2 h1 h5 h6 (* j2 j2)) (* 4 h1 h5 h6 j2) (* 2 h1 h5 h6) (* h1 +(* h6 h6) (* j2 j2)) (* 2 h1 (* h6 h6) j2) (* h1 (* h6 h6)) (* (* h3 h3) h4 (* +j2 j2)) (* 2 (* h3 h3) h4 j2) (* (* h3 h3) h4) (* (* h3 h3) h5 (* j2 j2 j2)) (* +3 (* h3 h3) h5 (* j2 j2)) (* 3 (* h3 h3) h5 j2) (* (* h3 h3) h5) (* 2 (* h3 h3) +h6 (* j2 j2)) (* 3 (* h3 h3) h6 j2) (* (* h3 h3) h6) (* h3 (* h4 h4) j2) (* h3 +(* h4 h4)) (* 2 h3 h4 h5 (* j2 j2)) (* 4 h3 h4 h5 j2) (* 2 h3 h4 h5) (* 2 h3 h4 +h6 (* j2 j2)) (* 5 h3 h4 h6 j2) (* 2 h3 h4 h6) (* h3 (* h5 h5) (* j2 j2 j2)) (* +3 h3 (* h5 h5) (* j2 j2)) (* 3 h3 (* h5 h5) j2) (* h3 (* h5 h5)) (* 2 h3 h5 h6 +(* j2 j2 j2)) (* 6 h3 h5 h6 (* j2 j2)) (* 6 h3 h5 h6 j2) (* 2 h3 h5 h6) (* 2 h3 +(* h6 h6) (* j2 j2)) (* 3 h3 (* h6 h6) j2) (* h3 (* h6 h6)) (* (* h4 h4) h5 j2) +(* (* h4 h4) h5) (* (* h4 h4) h6 j2) (* h4 (* h5 h5) (* j2 j2)) (* 2 h4 (* h5 h5 +) j2) (* h4 (* h5 h5)) (* 2 h4 h5 h6 (* j2 j2)) (* 4 h4 h5 h6 j2) (* 2 h4 h5 h6) + (* h4 (* h6 h6) (* j2 j2)) (* h4 (* h6 h6) j2) (* (* h5 h5) h6 (* j2 j2 j2)) +(* 3 (* h5 h5) h6 (* j2 j2)) (* 3 (* h5 h5) h6 j2) (* (* h5 h5) h6) (* h5 (* h6 +h6) (* j2 j2 j2)) (* 3 h5 (* h6 h6) (* j2 j2)) (* 3 h5 (* h6 h6) j2) (* h5 (* h6 + h6))) 0))) +(check-sat) +(exit) diff --git a/tests/regress/mcsat/nra/mbo_E22E23.smt2.gold b/tests/regress/mcsat/nra/mbo_E22E23.smt2.gold new file mode 100644 index 000000000..3f65111b0 --- /dev/null +++ b/tests/regress/mcsat/nra/mbo_E22E23.smt2.gold @@ -0,0 +1 @@ +unsat From afe3529621097aa138ab9c02ddc51c8134a708f5 Mon Sep 17 00:00:00 2001 From: Dejan Jovanovic Date: Wed, 13 May 2020 20:38:44 -0400 Subject: [PATCH 03/16] more tests --- ...ics_reach.01.seq_lazy_lemmas_global_2.smt2 | 1304 +++++++++++++++++ ...each.01.seq_lazy_lemmas_global_2.smt2.gold | 1 + 2 files changed, 1305 insertions(+) create mode 100644 tests/regress/mcsat/nra/simple_ballistics_reach.01.seq_lazy_lemmas_global_2.smt2 create mode 100644 tests/regress/mcsat/nra/simple_ballistics_reach.01.seq_lazy_lemmas_global_2.smt2.gold diff --git a/tests/regress/mcsat/nra/simple_ballistics_reach.01.seq_lazy_lemmas_global_2.smt2 b/tests/regress/mcsat/nra/simple_ballistics_reach.01.seq_lazy_lemmas_global_2.smt2 new file mode 100644 index 000000000..6d622f1e6 --- /dev/null +++ b/tests/regress/mcsat/nra/simple_ballistics_reach.01.seq_lazy_lemmas_global_2.smt2 @@ -0,0 +1,1304 @@ +(set-info :smt-lib-version 2.6) +(set-logic QF_NRA) +(set-info :source |Benchmarks generated from hycomp (https://es-static.fbk.eu/tools/hycomp/). BMC instances of non-linear hybrid automata taken from: Alessandro Cimatti, Sergio Mover, Stefano Tonetta, A quantifier-free SMT encoding of non-linear hybrid automata, FMCAD 2012 and Alessandro Cimatti, Sergio Mover, Stefano Tonetta, Quantier-free encoding of invariants for Hybrid Systems, Formal Methods in System Design. This instance solves a BMC problem of depth 2 and uses the quantifier free encoding with lemmas encoding. Contacts: Sergio Mover (mover@fbk.eu), Stefano Tonetta (tonettas@fbk.eu), Alessandro Cimatti (cimatti@fbk.eu).|) +(set-info :category "industrial") +(set-info :status unsat) +;; MathSAT API call trace +;; generated on Mon Mar 19 10:38:46 2012 +(declare-fun m.event_is_timed__AT0 () Bool) +(declare-fun m.time__AT2 () Real) +(declare-fun m.y__AT2 () Real) +(declare-fun m.x__AT1 () Real) +(declare-fun m.delta__AT2 () Real) +(declare-fun m.x__AT2 () Real) +(declare-fun m.EVENT.0__AT2 () Bool) +(declare-fun m.EVENT.1__AT2 () Bool) +(declare-fun m.delta__AT0 () Real) +(declare-fun m.time__AT1 () Real) +(declare-fun m.speed_y__AT0 () Real) +(declare-fun m.EVENT.0__AT0 () Bool) +(declare-fun m.delta__AT1 () Real) +(declare-fun m.EVENT.1__AT0 () Bool) +(declare-fun m.y__AT1 () Real) +(declare-fun m.speed_x__AT2 () Real) +(declare-fun m.speed_y__AT2 () Real) +(declare-fun m.event_is_timed__AT1 () Bool) +(declare-fun m.y__AT0 () Real) +(declare-fun m.speed_x__AT1 () Real) +(declare-fun m.speed_y__AT1 () Real) +(declare-fun m.time__AT0 () Real) +(declare-fun m.x__AT0 () Real) +(declare-fun m.EVENT.0__AT1 () Bool) +(declare-fun m.event_is_timed__AT2 () Bool) +(declare-fun m.EVENT.1__AT1 () Bool) +(declare-fun m.speed_x__AT0 () Real) +(assert (let ((.def_1428 (* m.speed_y__AT2 m.delta__AT2))) +(let ((.def_1429 (* 10.0 .def_1428))) +(let ((.def_1101 (* m.delta__AT2 m.delta__AT2))) +(let ((.def_1427 (* (- 49.0) .def_1101))) +(let ((.def_1430 (+ .def_1427 .def_1429))) +(let ((.def_1431 (* 10.0 m.y__AT2))) +(let ((.def_1433 (+ .def_1431 .def_1430))) +(let ((.def_1458 (<= .def_1433 0.0 ))) +(let ((.def_1466 (not .def_1458))) +(let ((.def_1456 (<= m.y__AT2 0.0 ))) +(let ((.def_1467 (or .def_1456 .def_1466))) +(let ((.def_1062 (<= 0.0 m.y__AT2))) +(let ((.def_1464 (not .def_1062))) +(let ((.def_1454 (<= 0.0 .def_1433))) +(let ((.def_1465 (or .def_1454 .def_1464))) +(let ((.def_1468 (and .def_1465 .def_1467))) +(let ((.def_1269 (<= m.speed_y__AT2 0.0 ))) +(let ((.def_1270 (not .def_1269))) +(let ((.def_1263 (* (- 49.0) m.delta__AT2))) +(let ((.def_1264 (* 5.0 m.speed_y__AT2))) +(let ((.def_1266 (+ .def_1264 .def_1263))) +(let ((.def_1267 (<= .def_1266 0.0 ))) +(let ((.def_1268 (not .def_1267))) +(let ((.def_1271 (or .def_1268 .def_1270))) +(let ((.def_1272 (not .def_1271))) +(let ((.def_1469 (or .def_1272 .def_1468))) +(let ((.def_1460 (not .def_1454))) +(let ((.def_1461 (or .def_1062 .def_1460))) +(let ((.def_1457 (not .def_1456))) +(let ((.def_1459 (or .def_1457 .def_1458))) +(let ((.def_1462 (and .def_1459 .def_1461))) +(let ((.def_1279 (<= 0.0 .def_1266))) +(let ((.def_1280 (not .def_1279))) +(let ((.def_1277 (<= 0.0 m.speed_y__AT2))) +(let ((.def_1278 (not .def_1277))) +(let ((.def_1281 (or .def_1278 .def_1280))) +(let ((.def_1282 (not .def_1281))) +(let ((.def_1463 (or .def_1282 .def_1462))) +(let ((.def_1470 (and .def_1463 .def_1469))) +(let ((.def_1455 (and .def_1062 .def_1454))) +(let ((.def_1471 (and .def_1455 .def_1470))) +(let ((.def_1291 (and .def_1267 .def_1269))) +(let ((.def_1288 (or .def_1277 .def_1280))) +(let ((.def_1287 (or .def_1267 .def_1270))) +(let ((.def_1289 (and .def_1287 .def_1288))) +(let ((.def_1292 (and .def_1289 .def_1291))) +(let ((.def_1286 (and .def_1277 .def_1279))) +(let ((.def_1290 (and .def_1286 .def_1289))) +(let ((.def_1293 (or .def_1290 .def_1292))) +(let ((.def_1472 (and .def_1293 .def_1471))) +(let ((.def_1434 (<= .def_1433 1000.0 ))) +(let ((.def_1446 (not .def_1434))) +(let ((.def_1061 (<= m.y__AT2 100.0 ))) +(let ((.def_1447 (or .def_1061 .def_1446))) +(let ((.def_1440 (<= 100.0 m.y__AT2))) +(let ((.def_1444 (not .def_1440))) +(let ((.def_1438 (<= 1000.0 .def_1433))) +(let ((.def_1445 (or .def_1438 .def_1444))) +(let ((.def_1448 (and .def_1445 .def_1447))) +(let ((.def_1449 (or .def_1272 .def_1448))) +(let ((.def_1439 (not .def_1438))) +(let ((.def_1441 (or .def_1439 .def_1440))) +(let ((.def_1436 (not .def_1061))) +(let ((.def_1437 (or .def_1434 .def_1436))) +(let ((.def_1442 (and .def_1437 .def_1441))) +(let ((.def_1443 (or .def_1282 .def_1442))) +(let ((.def_1450 (and .def_1443 .def_1449))) +(let ((.def_1435 (and .def_1061 .def_1434))) +(let ((.def_1451 (and .def_1435 .def_1450))) +(let ((.def_1452 (and .def_1293 .def_1451))) +(let ((.def_1105 (* (- (/ 49 10)) m.speed_y__AT2))) +(let ((.def_1151 (* 3.0 .def_1105))) +(let ((.def_1324 (* (- 1.0) .def_1151))) +(let ((.def_1352 (* 2.0 .def_1324))) +(let ((.def_1396 (* (- 1.0) .def_1352))) +(let ((.def_1397 (* m.delta__AT2 .def_1396))) +(let ((.def_1398 (* (- 50.0) .def_1397))) +(let ((.def_1121 (* m.speed_x__AT2 m.speed_x__AT2))) +(let ((.def_1221 (* (- 50.0) .def_1121))) +(let ((.def_1403 (+ .def_1221 .def_1398))) +(let ((.def_1109 (* m.speed_y__AT2 m.speed_y__AT2))) +(let ((.def_1219 (* (- 50.0) .def_1109))) +(let ((.def_1404 (+ .def_1219 .def_1403))) +(let ((.def_1223 (* (- 7203.0) .def_1101))) +(let ((.def_1405 (+ .def_1223 .def_1404))) +(let ((.def_1225 (* 490.0 m.y__AT2))) +(let ((.def_1406 (+ .def_1225 .def_1405))) +(let ((.def_1409 (<= 0.0 .def_1406))) +(let ((.def_1416 (not .def_1409))) +(let ((.def_1234 (* (- 5.0) .def_1121))) +(let ((.def_1233 (* (- 5.0) .def_1109))) +(let ((.def_1235 (+ .def_1233 .def_1234))) +(let ((.def_1236 (* 49.0 m.y__AT2))) +(let ((.def_1238 (+ .def_1236 .def_1235))) +(let ((.def_1249 (<= 0.0 .def_1238))) +(let ((.def_1417 (or .def_1249 .def_1416))) +(let ((.def_1407 (<= .def_1406 0.0 ))) +(let ((.def_1239 (<= .def_1238 0.0 ))) +(let ((.def_1240 (not .def_1239))) +(let ((.def_1415 (or .def_1240 .def_1407))) +(let ((.def_1418 (and .def_1415 .def_1417))) +(let ((.def_1419 (or .def_1282 .def_1418))) +(let ((.def_1411 (not .def_1407))) +(let ((.def_1412 (or .def_1239 .def_1411))) +(let ((.def_1250 (not .def_1249))) +(let ((.def_1410 (or .def_1250 .def_1409))) +(let ((.def_1413 (and .def_1410 .def_1412))) +(let ((.def_1414 (or .def_1272 .def_1413))) +(let ((.def_1420 (and .def_1414 .def_1419))) +(let ((.def_1408 (and .def_1239 .def_1407))) +(let ((.def_1421 (and .def_1408 .def_1420))) +(let ((.def_1422 (and .def_1293 .def_1421))) +(let ((.def_1353 (* m.delta__AT2 .def_1352))) +(let ((.def_1354 (* 50.0 .def_1353))) +(let ((.def_1359 (+ .def_1221 .def_1354))) +(let ((.def_1360 (+ .def_1219 .def_1359))) +(let ((.def_1361 (+ .def_1223 .def_1360))) +(let ((.def_1362 (+ .def_1225 .def_1361))) +(let ((.def_1373 (<= .def_1362 0.0 ))) +(let ((.def_1374 (not .def_1373))) +(let ((.def_1390 (or .def_1239 .def_1374))) +(let ((.def_1363 (<= 0.0 .def_1362))) +(let ((.def_1389 (or .def_1250 .def_1363))) +(let ((.def_1391 (and .def_1389 .def_1390))) +(let ((.def_1392 (or .def_1272 .def_1391))) +(let ((.def_1364 (not .def_1363))) +(let ((.def_1386 (or .def_1249 .def_1364))) +(let ((.def_1385 (or .def_1240 .def_1373))) +(let ((.def_1387 (and .def_1385 .def_1386))) +(let ((.def_1388 (or .def_1282 .def_1387))) +(let ((.def_1393 (and .def_1388 .def_1392))) +(let ((.def_1384 (and .def_1249 .def_1363))) +(let ((.def_1394 (and .def_1384 .def_1393))) +(let ((.def_1395 (and .def_1293 .def_1394))) +(let ((.def_1423 (or .def_1395 .def_1422))) +(let ((.def_1162 (* 2.0 .def_1121))) +(let ((.def_1336 (* (- 1.0) .def_1162))) +(let ((.def_1337 (* m.delta__AT2 .def_1336))) +(let ((.def_1338 (* 25.0 .def_1337))) +(let ((.def_1113 (* (- (/ 49 10)) m.y__AT2))) +(let ((.def_1158 (* 2.0 .def_1113))) +(let ((.def_1332 (* (- 1.0) .def_1158))) +(let ((.def_1333 (* m.delta__AT2 .def_1332))) +(let ((.def_1334 (* 50.0 .def_1333))) +(let ((.def_1343 (+ .def_1334 .def_1338))) +(let ((.def_1154 (* 2.0 .def_1109))) +(let ((.def_1328 (* (- 1.0) .def_1154))) +(let ((.def_1329 (* m.delta__AT2 .def_1328))) +(let ((.def_1330 (* 25.0 .def_1329))) +(let ((.def_1344 (+ .def_1330 .def_1343))) +(let ((.def_1325 (* .def_1101 .def_1324))) +(let ((.def_1326 (* 50.0 .def_1325))) +(let ((.def_1345 (+ .def_1326 .def_1344))) +(let ((.def_1125 (* m.x__AT2 m.speed_x__AT2))) +(let ((.def_1170 (* (- 50.0) .def_1125))) +(let ((.def_1346 (+ .def_1170 .def_1345))) +(let ((.def_1117 (* m.y__AT2 m.speed_y__AT2))) +(let ((.def_1168 (* (- 50.0) .def_1117))) +(let ((.def_1347 (+ .def_1168 .def_1346))) +(let ((.def_1102 (* m.delta__AT2 .def_1101))) +(let ((.def_1166 (* (- 2401.0) .def_1102))) +(let ((.def_1348 (+ .def_1166 .def_1347))) +(let ((.def_1172 (* 1000.0 m.speed_x__AT2))) +(let ((.def_1349 (+ .def_1172 .def_1348))) +(let ((.def_1367 (<= .def_1349 0.0 ))) +(let ((.def_1378 (not .def_1367))) +(let ((.def_1184 (* (- 1.0) .def_1125))) +(let ((.def_1183 (* (- 1.0) .def_1117))) +(let ((.def_1185 (+ .def_1183 .def_1184))) +(let ((.def_1186 (* 20.0 m.speed_x__AT2))) +(let ((.def_1188 (+ .def_1186 .def_1185))) +(let ((.def_1189 (<= .def_1188 0.0 ))) +(let ((.def_1379 (or .def_1189 .def_1378))) +(let ((.def_1350 (<= 0.0 .def_1349))) +(let ((.def_1203 (<= 0.0 .def_1188))) +(let ((.def_1204 (not .def_1203))) +(let ((.def_1377 (or .def_1204 .def_1350))) +(let ((.def_1380 (and .def_1377 .def_1379))) +(let ((.def_1375 (or .def_1240 .def_1374))) +(let ((.def_1376 (not .def_1375))) +(let ((.def_1381 (or .def_1376 .def_1380))) +(let ((.def_1369 (not .def_1350))) +(let ((.def_1370 (or .def_1203 .def_1369))) +(let ((.def_1190 (not .def_1189))) +(let ((.def_1368 (or .def_1190 .def_1367))) +(let ((.def_1371 (and .def_1368 .def_1370))) +(let ((.def_1365 (or .def_1250 .def_1364))) +(let ((.def_1366 (not .def_1365))) +(let ((.def_1372 (or .def_1366 .def_1371))) +(let ((.def_1382 (and .def_1372 .def_1381))) +(let ((.def_1351 (and .def_1203 .def_1350))) +(let ((.def_1383 (and .def_1351 .def_1382))) +(let ((.def_1424 (and .def_1383 .def_1423))) +(let ((.def_1216 (* 2.0 .def_1151))) +(let ((.def_1295 (* (- 1.0) .def_1216))) +(let ((.def_1296 (* m.delta__AT2 .def_1295))) +(let ((.def_1297 (* 50.0 .def_1296))) +(let ((.def_1302 (+ .def_1221 .def_1297))) +(let ((.def_1303 (+ .def_1219 .def_1302))) +(let ((.def_1304 (+ .def_1223 .def_1303))) +(let ((.def_1305 (+ .def_1225 .def_1304))) +(let ((.def_1308 (<= .def_1305 0.0 ))) +(let ((.def_1315 (not .def_1308))) +(let ((.def_1316 (or .def_1239 .def_1315))) +(let ((.def_1306 (<= 0.0 .def_1305))) +(let ((.def_1314 (or .def_1250 .def_1306))) +(let ((.def_1317 (and .def_1314 .def_1316))) +(let ((.def_1318 (or .def_1272 .def_1317))) +(let ((.def_1310 (not .def_1306))) +(let ((.def_1311 (or .def_1249 .def_1310))) +(let ((.def_1309 (or .def_1240 .def_1308))) +(let ((.def_1312 (and .def_1309 .def_1311))) +(let ((.def_1313 (or .def_1282 .def_1312))) +(let ((.def_1319 (and .def_1313 .def_1318))) +(let ((.def_1307 (and .def_1249 .def_1306))) +(let ((.def_1320 (and .def_1307 .def_1319))) +(let ((.def_1321 (and .def_1293 .def_1320))) +(let ((.def_1217 (* m.delta__AT2 .def_1216))) +(let ((.def_1218 (* (- 50.0) .def_1217))) +(let ((.def_1227 (+ .def_1221 .def_1218))) +(let ((.def_1228 (+ .def_1219 .def_1227))) +(let ((.def_1229 (+ .def_1223 .def_1228))) +(let ((.def_1230 (+ .def_1225 .def_1229))) +(let ((.def_1247 (<= 0.0 .def_1230))) +(let ((.def_1248 (not .def_1247))) +(let ((.def_1275 (or .def_1248 .def_1249))) +(let ((.def_1231 (<= .def_1230 0.0 ))) +(let ((.def_1274 (or .def_1231 .def_1240))) +(let ((.def_1276 (and .def_1274 .def_1275))) +(let ((.def_1283 (or .def_1276 .def_1282))) +(let ((.def_1232 (not .def_1231))) +(let ((.def_1261 (or .def_1232 .def_1239))) +(let ((.def_1260 (or .def_1247 .def_1250))) +(let ((.def_1262 (and .def_1260 .def_1261))) +(let ((.def_1273 (or .def_1262 .def_1272))) +(let ((.def_1284 (and .def_1273 .def_1283))) +(let ((.def_1259 (and .def_1231 .def_1239))) +(let ((.def_1285 (and .def_1259 .def_1284))) +(let ((.def_1294 (and .def_1285 .def_1293))) +(let ((.def_1322 (or .def_1294 .def_1321))) +(let ((.def_1163 (* m.delta__AT2 .def_1162))) +(let ((.def_1164 (* (- 25.0) .def_1163))) +(let ((.def_1159 (* m.delta__AT2 .def_1158))) +(let ((.def_1160 (* (- 50.0) .def_1159))) +(let ((.def_1174 (+ .def_1160 .def_1164))) +(let ((.def_1155 (* m.delta__AT2 .def_1154))) +(let ((.def_1156 (* (- 25.0) .def_1155))) +(let ((.def_1175 (+ .def_1156 .def_1174))) +(let ((.def_1152 (* .def_1101 .def_1151))) +(let ((.def_1153 (* (- 50.0) .def_1152))) +(let ((.def_1176 (+ .def_1153 .def_1175))) +(let ((.def_1177 (+ .def_1170 .def_1176))) +(let ((.def_1178 (+ .def_1168 .def_1177))) +(let ((.def_1179 (+ .def_1166 .def_1178))) +(let ((.def_1180 (+ .def_1172 .def_1179))) +(let ((.def_1201 (<= 0.0 .def_1180))) +(let ((.def_1202 (not .def_1201))) +(let ((.def_1254 (or .def_1202 .def_1203))) +(let ((.def_1181 (<= .def_1180 0.0 ))) +(let ((.def_1253 (or .def_1181 .def_1190))) +(let ((.def_1255 (and .def_1253 .def_1254))) +(let ((.def_1251 (or .def_1248 .def_1250))) +(let ((.def_1252 (not .def_1251))) +(let ((.def_1256 (or .def_1252 .def_1255))) +(let ((.def_1182 (not .def_1181))) +(let ((.def_1244 (or .def_1182 .def_1189))) +(let ((.def_1243 (or .def_1201 .def_1204))) +(let ((.def_1245 (and .def_1243 .def_1244))) +(let ((.def_1241 (or .def_1232 .def_1240))) +(let ((.def_1242 (not .def_1241))) +(let ((.def_1246 (or .def_1242 .def_1245))) +(let ((.def_1257 (and .def_1246 .def_1256))) +(let ((.def_1215 (and .def_1181 .def_1189))) +(let ((.def_1258 (and .def_1215 .def_1257))) +(let ((.def_1323 (and .def_1258 .def_1322))) +(let ((.def_1425 (or .def_1323 .def_1424))) +(let ((.def_1129 (* (- 20.0) m.speed_x__AT2))) +(let ((.def_1130 (* m.delta__AT2 .def_1129))) +(let ((.def_1131 (* (- 200.0) .def_1130))) +(let ((.def_1126 (* m.delta__AT2 .def_1125))) +(let ((.def_1127 (* (- 200.0) .def_1126))) +(let ((.def_1139 (+ .def_1127 .def_1131))) +(let ((.def_1122 (* .def_1101 .def_1121))) +(let ((.def_1123 (* (- 100.0) .def_1122))) +(let ((.def_1140 (+ .def_1123 .def_1139))) +(let ((.def_1118 (* m.delta__AT2 .def_1117))) +(let ((.def_1119 (* (- 200.0) .def_1118))) +(let ((.def_1141 (+ .def_1119 .def_1140))) +(let ((.def_1114 (* .def_1101 .def_1113))) +(let ((.def_1115 (* (- 200.0) .def_1114))) +(let ((.def_1142 (+ .def_1115 .def_1141))) +(let ((.def_1110 (* .def_1101 .def_1109))) +(let ((.def_1111 (* (- 100.0) .def_1110))) +(let ((.def_1143 (+ .def_1111 .def_1142))) +(let ((.def_1106 (* .def_1102 .def_1105))) +(let ((.def_1107 (* (- 200.0) .def_1106))) +(let ((.def_1144 (+ .def_1107 .def_1143))) +(let ((.def_1103 (* m.delta__AT2 .def_1102))) +(let ((.def_1104 (* (- 2401.0) .def_1103))) +(let ((.def_1145 (+ .def_1104 .def_1144))) +(let ((.def_1094 (* m.x__AT2 m.x__AT2))) +(let ((.def_1135 (* (- 100.0) .def_1094))) +(let ((.def_1146 (+ .def_1135 .def_1145))) +(let ((.def_1056 (* m.y__AT2 m.y__AT2))) +(let ((.def_1133 (* (- 100.0) .def_1056))) +(let ((.def_1147 (+ .def_1133 .def_1146))) +(let ((.def_1137 (* 4000.0 m.x__AT2))) +(let ((.def_1148 (+ .def_1137 .def_1147))) +(let ((.def_1195 (<= 0.0 .def_1148))) +(let ((.def_1209 (not .def_1195))) +(let ((.def_1095 (* (- 1.0) .def_1094))) +(let ((.def_1093 (* (- 1.0) .def_1056))) +(let ((.def_1096 (+ .def_1093 .def_1095))) +(let ((.def_1097 (* 40.0 m.x__AT2))) +(let ((.def_1099 (+ .def_1097 .def_1096))) +(let ((.def_1193 (<= 0.0 .def_1099))) +(let ((.def_1210 (or .def_1193 .def_1209))) +(let ((.def_1100 (<= .def_1099 0.0 ))) +(let ((.def_1207 (not .def_1100))) +(let ((.def_1149 (<= .def_1148 0.0 ))) +(let ((.def_1208 (or .def_1149 .def_1207))) +(let ((.def_1211 (and .def_1208 .def_1210))) +(let ((.def_1205 (or .def_1202 .def_1204))) +(let ((.def_1206 (not .def_1205))) +(let ((.def_1212 (or .def_1206 .def_1211))) +(let ((.def_1197 (not .def_1149))) +(let ((.def_1198 (or .def_1100 .def_1197))) +(let ((.def_1194 (not .def_1193))) +(let ((.def_1196 (or .def_1194 .def_1195))) +(let ((.def_1199 (and .def_1196 .def_1198))) +(let ((.def_1191 (or .def_1182 .def_1190))) +(let ((.def_1192 (not .def_1191))) +(let ((.def_1200 (or .def_1192 .def_1199))) +(let ((.def_1213 (and .def_1200 .def_1212))) +(let ((.def_1150 (and .def_1100 .def_1149))) +(let ((.def_1214 (and .def_1150 .def_1213))) +(let ((.def_1426 (and .def_1214 .def_1425))) +(let ((.def_1453 (and .def_1426 .def_1452))) +(let ((.def_1473 (and .def_1453 .def_1472))) +(let ((.def_1071 (* m.speed_x__AT2 m.delta__AT2))) +(let ((.def_1072 (+ m.x__AT2 .def_1071))) +(let ((.def_1078 (<= .def_1072 0.0 ))) +(let ((.def_1087 (not .def_1078))) +(let ((.def_1076 (<= m.x__AT2 0.0 ))) +(let ((.def_1088 (or .def_1076 .def_1087))) +(let ((.def_1059 (<= 0.0 m.x__AT2))) +(let ((.def_1085 (not .def_1059))) +(let ((.def_1073 (<= 0.0 .def_1072))) +(let ((.def_1086 (or .def_1073 .def_1085))) +(let ((.def_1089 (and .def_1086 .def_1088))) +(let ((.def_1084 (<= m.speed_x__AT2 0.0 ))) +(let ((.def_1090 (or .def_1084 .def_1089))) +(let ((.def_1080 (not .def_1073))) +(let ((.def_1081 (or .def_1059 .def_1080))) +(let ((.def_1077 (not .def_1076))) +(let ((.def_1079 (or .def_1077 .def_1078))) +(let ((.def_1082 (and .def_1079 .def_1081))) +(let ((.def_1075 (<= 0.0 m.speed_x__AT2))) +(let ((.def_1083 (or .def_1075 .def_1082))) +(let ((.def_1091 (and .def_1083 .def_1090))) +(let ((.def_1074 (and .def_1059 .def_1073))) +(let ((.def_1092 (and .def_1074 .def_1091))) +(let ((.def_1474 (and .def_1092 .def_1473))) +(let ((.def_1067 (<= m.x__AT1 20.0 ))) +(let ((.def_1063 (and .def_1061 .def_1062))) +(let ((.def_1054 (+ m.x__AT2 (- 20.0) ))) +(let ((.def_1055 (* .def_1054 .def_1054))) +(let ((.def_1057 (+ .def_1055 .def_1056))) +(let ((.def_1058 (<= 400.0 .def_1057))) +(let ((.def_1060 (and .def_1058 .def_1059))) +(let ((.def_1064 (and .def_1060 .def_1063))) +(let ((.def_1052 (not m.EVENT.0__AT2))) +(let ((.def_1050 (not m.EVENT.1__AT2))) +(let ((.def_1053 (or .def_1050 .def_1052))) +(let ((.def_1065 (and .def_1053 .def_1064))) +(let ((.def_1044 (<= 0.0 m.delta__AT1))) +(let ((.def_551 (not m.EVENT.0__AT1))) +(let ((.def_549 (not m.EVENT.1__AT1))) +(let ((.def_975 (and .def_549 .def_551))) +(let ((.def_977 (not .def_975))) +(let ((.def_1045 (or .def_977 .def_1044))) +(let ((.def_1046 (or m.EVENT.1__AT1 .def_1045))) +(let ((.def_1032 (* (- 10.0) m.y__AT2))) +(let ((.def_927 (* m.speed_y__AT1 m.delta__AT1))) +(let ((.def_928 (* 10.0 .def_927))) +(let ((.def_1036 (+ .def_928 .def_1032))) +(let ((.def_600 (* m.delta__AT1 m.delta__AT1))) +(let ((.def_926 (* (- 49.0) .def_600))) +(let ((.def_1037 (+ .def_926 .def_1036))) +(let ((.def_930 (* 10.0 m.y__AT1))) +(let ((.def_1038 (+ .def_930 .def_1037))) +(let ((.def_1039 (= .def_1038 0.0 ))) +(let ((.def_1027 (* (- 5.0) m.speed_y__AT2))) +(let ((.def_762 (* (- 49.0) m.delta__AT1))) +(let ((.def_1028 (+ .def_762 .def_1027))) +(let ((.def_763 (* 5.0 m.speed_y__AT1))) +(let ((.def_1029 (+ .def_763 .def_1028))) +(let ((.def_1030 (= .def_1029 0.0 ))) +(let ((.def_570 (* m.speed_x__AT1 m.delta__AT1))) +(let ((.def_1022 (* (- 1.0) .def_570))) +(let ((.def_521 (* (- 1.0) m.x__AT1))) +(let ((.def_1023 (+ .def_521 .def_1022))) +(let ((.def_1024 (+ m.x__AT2 .def_1023))) +(let ((.def_1025 (= .def_1024 0.0 ))) +(let ((.def_1000 (= m.speed_x__AT1 m.speed_x__AT2))) +(let ((.def_1026 (and .def_1000 .def_1025))) +(let ((.def_1031 (and .def_1026 .def_1030))) +(let ((.def_1040 (and .def_1031 .def_1039))) +(let ((.def_1041 (or .def_977 .def_1040))) +(let ((.def_1013 (= m.delta__AT1 0.0 ))) +(let ((.def_1014 (and .def_975 .def_1013))) +(let ((.def_1015 (not .def_1014))) +(let ((.def_997 (= m.y__AT1 m.y__AT2))) +(let ((.def_994 (= m.x__AT2 m.x__AT1))) +(let ((.def_1008 (and .def_994 .def_997))) +(let ((.def_1009 (and .def_1000 .def_1008))) +(let ((.def_1003 (= m.speed_y__AT1 m.speed_y__AT2))) +(let ((.def_1010 (and .def_1003 .def_1009))) +(let ((.def_1016 (or .def_1010 .def_1015))) +(let ((.def_1017 (or m.EVENT.1__AT1 .def_1016))) +(let ((.def_1011 (or .def_975 .def_1010))) +(let ((.def_1012 (or m.EVENT.1__AT1 .def_1011))) +(let ((.def_1018 (and .def_1012 .def_1017))) +(let ((.def_1042 (and .def_1018 .def_1041))) +(let ((.def_982 (= m.time__AT1 m.time__AT2))) +(let ((.def_995 (and .def_982 .def_994))) +(let ((.def_998 (and .def_995 .def_997))) +(let ((.def_1001 (and .def_998 .def_1000))) +(let ((.def_1004 (and .def_1001 .def_1003))) +(let ((.def_1005 (or .def_549 .def_1004))) +(let ((.def_985 (* (- 1.0) m.time__AT2))) +(let ((.def_988 (+ m.delta__AT1 .def_985))) +(let ((.def_989 (+ m.time__AT1 .def_988))) +(let ((.def_990 (= .def_989 0.0 ))) +(let ((.def_991 (or .def_977 .def_990))) +(let ((.def_992 (or m.EVENT.1__AT1 .def_991))) +(let ((.def_983 (or .def_975 .def_982))) +(let ((.def_984 (or m.EVENT.1__AT1 .def_983))) +(let ((.def_993 (and .def_984 .def_992))) +(let ((.def_1006 (and .def_993 .def_1005))) +(let ((.def_979 (= .def_977 m.event_is_timed__AT2))) +(let ((.def_976 (= m.event_is_timed__AT1 .def_975))) +(let ((.def_980 (and .def_976 .def_979))) +(let ((.def_1007 (and .def_980 .def_1006))) +(let ((.def_1043 (and .def_1007 .def_1042))) +(let ((.def_1047 (and .def_1043 .def_1046))) +(let ((.def_1048 (and .def_549 .def_1047))) +(let ((.def_1066 (and .def_1048 .def_1065))) +(let ((.def_1068 (and .def_1066 .def_1067))) +(let ((.def_929 (+ .def_926 .def_928))) +(let ((.def_932 (+ .def_930 .def_929))) +(let ((.def_957 (<= .def_932 0.0 ))) +(let ((.def_965 (not .def_957))) +(let ((.def_955 (<= m.y__AT1 0.0 ))) +(let ((.def_966 (or .def_955 .def_965))) +(let ((.def_561 (<= 0.0 m.y__AT1))) +(let ((.def_963 (not .def_561))) +(let ((.def_953 (<= 0.0 .def_932))) +(let ((.def_964 (or .def_953 .def_963))) +(let ((.def_967 (and .def_964 .def_966))) +(let ((.def_768 (<= m.speed_y__AT1 0.0 ))) +(let ((.def_769 (not .def_768))) +(let ((.def_765 (+ .def_763 .def_762))) +(let ((.def_766 (<= .def_765 0.0 ))) +(let ((.def_767 (not .def_766))) +(let ((.def_770 (or .def_767 .def_769))) +(let ((.def_771 (not .def_770))) +(let ((.def_968 (or .def_771 .def_967))) +(let ((.def_959 (not .def_953))) +(let ((.def_960 (or .def_561 .def_959))) +(let ((.def_956 (not .def_955))) +(let ((.def_958 (or .def_956 .def_957))) +(let ((.def_961 (and .def_958 .def_960))) +(let ((.def_778 (<= 0.0 .def_765))) +(let ((.def_779 (not .def_778))) +(let ((.def_776 (<= 0.0 m.speed_y__AT1))) +(let ((.def_777 (not .def_776))) +(let ((.def_780 (or .def_777 .def_779))) +(let ((.def_781 (not .def_780))) +(let ((.def_962 (or .def_781 .def_961))) +(let ((.def_969 (and .def_962 .def_968))) +(let ((.def_954 (and .def_561 .def_953))) +(let ((.def_970 (and .def_954 .def_969))) +(let ((.def_790 (and .def_766 .def_768))) +(let ((.def_787 (or .def_776 .def_779))) +(let ((.def_786 (or .def_766 .def_769))) +(let ((.def_788 (and .def_786 .def_787))) +(let ((.def_791 (and .def_788 .def_790))) +(let ((.def_785 (and .def_776 .def_778))) +(let ((.def_789 (and .def_785 .def_788))) +(let ((.def_792 (or .def_789 .def_791))) +(let ((.def_971 (and .def_792 .def_970))) +(let ((.def_933 (<= .def_932 1000.0 ))) +(let ((.def_945 (not .def_933))) +(let ((.def_560 (<= m.y__AT1 100.0 ))) +(let ((.def_946 (or .def_560 .def_945))) +(let ((.def_939 (<= 100.0 m.y__AT1))) +(let ((.def_943 (not .def_939))) +(let ((.def_937 (<= 1000.0 .def_932))) +(let ((.def_944 (or .def_937 .def_943))) +(let ((.def_947 (and .def_944 .def_946))) +(let ((.def_948 (or .def_771 .def_947))) +(let ((.def_938 (not .def_937))) +(let ((.def_940 (or .def_938 .def_939))) +(let ((.def_935 (not .def_560))) +(let ((.def_936 (or .def_933 .def_935))) +(let ((.def_941 (and .def_936 .def_940))) +(let ((.def_942 (or .def_781 .def_941))) +(let ((.def_949 (and .def_942 .def_948))) +(let ((.def_934 (and .def_560 .def_933))) +(let ((.def_950 (and .def_934 .def_949))) +(let ((.def_951 (and .def_792 .def_950))) +(let ((.def_604 (* (- (/ 49 10)) m.speed_y__AT1))) +(let ((.def_650 (* 3.0 .def_604))) +(let ((.def_823 (* (- 1.0) .def_650))) +(let ((.def_851 (* 2.0 .def_823))) +(let ((.def_895 (* (- 1.0) .def_851))) +(let ((.def_896 (* m.delta__AT1 .def_895))) +(let ((.def_897 (* (- 50.0) .def_896))) +(let ((.def_620 (* m.speed_x__AT1 m.speed_x__AT1))) +(let ((.def_720 (* (- 50.0) .def_620))) +(let ((.def_902 (+ .def_720 .def_897))) +(let ((.def_608 (* m.speed_y__AT1 m.speed_y__AT1))) +(let ((.def_718 (* (- 50.0) .def_608))) +(let ((.def_903 (+ .def_718 .def_902))) +(let ((.def_722 (* (- 7203.0) .def_600))) +(let ((.def_904 (+ .def_722 .def_903))) +(let ((.def_724 (* 490.0 m.y__AT1))) +(let ((.def_905 (+ .def_724 .def_904))) +(let ((.def_908 (<= 0.0 .def_905))) +(let ((.def_915 (not .def_908))) +(let ((.def_733 (* (- 5.0) .def_620))) +(let ((.def_732 (* (- 5.0) .def_608))) +(let ((.def_734 (+ .def_732 .def_733))) +(let ((.def_735 (* 49.0 m.y__AT1))) +(let ((.def_737 (+ .def_735 .def_734))) +(let ((.def_748 (<= 0.0 .def_737))) +(let ((.def_916 (or .def_748 .def_915))) +(let ((.def_906 (<= .def_905 0.0 ))) +(let ((.def_738 (<= .def_737 0.0 ))) +(let ((.def_739 (not .def_738))) +(let ((.def_914 (or .def_739 .def_906))) +(let ((.def_917 (and .def_914 .def_916))) +(let ((.def_918 (or .def_781 .def_917))) +(let ((.def_910 (not .def_906))) +(let ((.def_911 (or .def_738 .def_910))) +(let ((.def_749 (not .def_748))) +(let ((.def_909 (or .def_749 .def_908))) +(let ((.def_912 (and .def_909 .def_911))) +(let ((.def_913 (or .def_771 .def_912))) +(let ((.def_919 (and .def_913 .def_918))) +(let ((.def_907 (and .def_738 .def_906))) +(let ((.def_920 (and .def_907 .def_919))) +(let ((.def_921 (and .def_792 .def_920))) +(let ((.def_852 (* m.delta__AT1 .def_851))) +(let ((.def_853 (* 50.0 .def_852))) +(let ((.def_858 (+ .def_720 .def_853))) +(let ((.def_859 (+ .def_718 .def_858))) +(let ((.def_860 (+ .def_722 .def_859))) +(let ((.def_861 (+ .def_724 .def_860))) +(let ((.def_872 (<= .def_861 0.0 ))) +(let ((.def_873 (not .def_872))) +(let ((.def_889 (or .def_738 .def_873))) +(let ((.def_862 (<= 0.0 .def_861))) +(let ((.def_888 (or .def_749 .def_862))) +(let ((.def_890 (and .def_888 .def_889))) +(let ((.def_891 (or .def_771 .def_890))) +(let ((.def_863 (not .def_862))) +(let ((.def_885 (or .def_748 .def_863))) +(let ((.def_884 (or .def_739 .def_872))) +(let ((.def_886 (and .def_884 .def_885))) +(let ((.def_887 (or .def_781 .def_886))) +(let ((.def_892 (and .def_887 .def_891))) +(let ((.def_883 (and .def_748 .def_862))) +(let ((.def_893 (and .def_883 .def_892))) +(let ((.def_894 (and .def_792 .def_893))) +(let ((.def_922 (or .def_894 .def_921))) +(let ((.def_661 (* 2.0 .def_620))) +(let ((.def_835 (* (- 1.0) .def_661))) +(let ((.def_836 (* m.delta__AT1 .def_835))) +(let ((.def_837 (* 25.0 .def_836))) +(let ((.def_612 (* (- (/ 49 10)) m.y__AT1))) +(let ((.def_657 (* 2.0 .def_612))) +(let ((.def_831 (* (- 1.0) .def_657))) +(let ((.def_832 (* m.delta__AT1 .def_831))) +(let ((.def_833 (* 50.0 .def_832))) +(let ((.def_842 (+ .def_833 .def_837))) +(let ((.def_653 (* 2.0 .def_608))) +(let ((.def_827 (* (- 1.0) .def_653))) +(let ((.def_828 (* m.delta__AT1 .def_827))) +(let ((.def_829 (* 25.0 .def_828))) +(let ((.def_843 (+ .def_829 .def_842))) +(let ((.def_824 (* .def_600 .def_823))) +(let ((.def_825 (* 50.0 .def_824))) +(let ((.def_844 (+ .def_825 .def_843))) +(let ((.def_624 (* m.x__AT1 m.speed_x__AT1))) +(let ((.def_669 (* (- 50.0) .def_624))) +(let ((.def_845 (+ .def_669 .def_844))) +(let ((.def_616 (* m.y__AT1 m.speed_y__AT1))) +(let ((.def_667 (* (- 50.0) .def_616))) +(let ((.def_846 (+ .def_667 .def_845))) +(let ((.def_601 (* m.delta__AT1 .def_600))) +(let ((.def_665 (* (- 2401.0) .def_601))) +(let ((.def_847 (+ .def_665 .def_846))) +(let ((.def_671 (* 1000.0 m.speed_x__AT1))) +(let ((.def_848 (+ .def_671 .def_847))) +(let ((.def_866 (<= .def_848 0.0 ))) +(let ((.def_877 (not .def_866))) +(let ((.def_683 (* (- 1.0) .def_624))) +(let ((.def_682 (* (- 1.0) .def_616))) +(let ((.def_684 (+ .def_682 .def_683))) +(let ((.def_685 (* 20.0 m.speed_x__AT1))) +(let ((.def_687 (+ .def_685 .def_684))) +(let ((.def_688 (<= .def_687 0.0 ))) +(let ((.def_878 (or .def_688 .def_877))) +(let ((.def_849 (<= 0.0 .def_848))) +(let ((.def_702 (<= 0.0 .def_687))) +(let ((.def_703 (not .def_702))) +(let ((.def_876 (or .def_703 .def_849))) +(let ((.def_879 (and .def_876 .def_878))) +(let ((.def_874 (or .def_739 .def_873))) +(let ((.def_875 (not .def_874))) +(let ((.def_880 (or .def_875 .def_879))) +(let ((.def_868 (not .def_849))) +(let ((.def_869 (or .def_702 .def_868))) +(let ((.def_689 (not .def_688))) +(let ((.def_867 (or .def_689 .def_866))) +(let ((.def_870 (and .def_867 .def_869))) +(let ((.def_864 (or .def_749 .def_863))) +(let ((.def_865 (not .def_864))) +(let ((.def_871 (or .def_865 .def_870))) +(let ((.def_881 (and .def_871 .def_880))) +(let ((.def_850 (and .def_702 .def_849))) +(let ((.def_882 (and .def_850 .def_881))) +(let ((.def_923 (and .def_882 .def_922))) +(let ((.def_715 (* 2.0 .def_650))) +(let ((.def_794 (* (- 1.0) .def_715))) +(let ((.def_795 (* m.delta__AT1 .def_794))) +(let ((.def_796 (* 50.0 .def_795))) +(let ((.def_801 (+ .def_720 .def_796))) +(let ((.def_802 (+ .def_718 .def_801))) +(let ((.def_803 (+ .def_722 .def_802))) +(let ((.def_804 (+ .def_724 .def_803))) +(let ((.def_807 (<= .def_804 0.0 ))) +(let ((.def_814 (not .def_807))) +(let ((.def_815 (or .def_738 .def_814))) +(let ((.def_805 (<= 0.0 .def_804))) +(let ((.def_813 (or .def_749 .def_805))) +(let ((.def_816 (and .def_813 .def_815))) +(let ((.def_817 (or .def_771 .def_816))) +(let ((.def_809 (not .def_805))) +(let ((.def_810 (or .def_748 .def_809))) +(let ((.def_808 (or .def_739 .def_807))) +(let ((.def_811 (and .def_808 .def_810))) +(let ((.def_812 (or .def_781 .def_811))) +(let ((.def_818 (and .def_812 .def_817))) +(let ((.def_806 (and .def_748 .def_805))) +(let ((.def_819 (and .def_806 .def_818))) +(let ((.def_820 (and .def_792 .def_819))) +(let ((.def_716 (* m.delta__AT1 .def_715))) +(let ((.def_717 (* (- 50.0) .def_716))) +(let ((.def_726 (+ .def_720 .def_717))) +(let ((.def_727 (+ .def_718 .def_726))) +(let ((.def_728 (+ .def_722 .def_727))) +(let ((.def_729 (+ .def_724 .def_728))) +(let ((.def_746 (<= 0.0 .def_729))) +(let ((.def_747 (not .def_746))) +(let ((.def_774 (or .def_747 .def_748))) +(let ((.def_730 (<= .def_729 0.0 ))) +(let ((.def_773 (or .def_730 .def_739))) +(let ((.def_775 (and .def_773 .def_774))) +(let ((.def_782 (or .def_775 .def_781))) +(let ((.def_731 (not .def_730))) +(let ((.def_760 (or .def_731 .def_738))) +(let ((.def_759 (or .def_746 .def_749))) +(let ((.def_761 (and .def_759 .def_760))) +(let ((.def_772 (or .def_761 .def_771))) +(let ((.def_783 (and .def_772 .def_782))) +(let ((.def_758 (and .def_730 .def_738))) +(let ((.def_784 (and .def_758 .def_783))) +(let ((.def_793 (and .def_784 .def_792))) +(let ((.def_821 (or .def_793 .def_820))) +(let ((.def_662 (* m.delta__AT1 .def_661))) +(let ((.def_663 (* (- 25.0) .def_662))) +(let ((.def_658 (* m.delta__AT1 .def_657))) +(let ((.def_659 (* (- 50.0) .def_658))) +(let ((.def_673 (+ .def_659 .def_663))) +(let ((.def_654 (* m.delta__AT1 .def_653))) +(let ((.def_655 (* (- 25.0) .def_654))) +(let ((.def_674 (+ .def_655 .def_673))) +(let ((.def_651 (* .def_600 .def_650))) +(let ((.def_652 (* (- 50.0) .def_651))) +(let ((.def_675 (+ .def_652 .def_674))) +(let ((.def_676 (+ .def_669 .def_675))) +(let ((.def_677 (+ .def_667 .def_676))) +(let ((.def_678 (+ .def_665 .def_677))) +(let ((.def_679 (+ .def_671 .def_678))) +(let ((.def_700 (<= 0.0 .def_679))) +(let ((.def_701 (not .def_700))) +(let ((.def_753 (or .def_701 .def_702))) +(let ((.def_680 (<= .def_679 0.0 ))) +(let ((.def_752 (or .def_680 .def_689))) +(let ((.def_754 (and .def_752 .def_753))) +(let ((.def_750 (or .def_747 .def_749))) +(let ((.def_751 (not .def_750))) +(let ((.def_755 (or .def_751 .def_754))) +(let ((.def_681 (not .def_680))) +(let ((.def_743 (or .def_681 .def_688))) +(let ((.def_742 (or .def_700 .def_703))) +(let ((.def_744 (and .def_742 .def_743))) +(let ((.def_740 (or .def_731 .def_739))) +(let ((.def_741 (not .def_740))) +(let ((.def_745 (or .def_741 .def_744))) +(let ((.def_756 (and .def_745 .def_755))) +(let ((.def_714 (and .def_680 .def_688))) +(let ((.def_757 (and .def_714 .def_756))) +(let ((.def_822 (and .def_757 .def_821))) +(let ((.def_924 (or .def_822 .def_923))) +(let ((.def_628 (* (- 20.0) m.speed_x__AT1))) +(let ((.def_629 (* m.delta__AT1 .def_628))) +(let ((.def_630 (* (- 200.0) .def_629))) +(let ((.def_625 (* m.delta__AT1 .def_624))) +(let ((.def_626 (* (- 200.0) .def_625))) +(let ((.def_638 (+ .def_626 .def_630))) +(let ((.def_621 (* .def_600 .def_620))) +(let ((.def_622 (* (- 100.0) .def_621))) +(let ((.def_639 (+ .def_622 .def_638))) +(let ((.def_617 (* m.delta__AT1 .def_616))) +(let ((.def_618 (* (- 200.0) .def_617))) +(let ((.def_640 (+ .def_618 .def_639))) +(let ((.def_613 (* .def_600 .def_612))) +(let ((.def_614 (* (- 200.0) .def_613))) +(let ((.def_641 (+ .def_614 .def_640))) +(let ((.def_609 (* .def_600 .def_608))) +(let ((.def_610 (* (- 100.0) .def_609))) +(let ((.def_642 (+ .def_610 .def_641))) +(let ((.def_605 (* .def_601 .def_604))) +(let ((.def_606 (* (- 200.0) .def_605))) +(let ((.def_643 (+ .def_606 .def_642))) +(let ((.def_602 (* m.delta__AT1 .def_601))) +(let ((.def_603 (* (- 2401.0) .def_602))) +(let ((.def_644 (+ .def_603 .def_643))) +(let ((.def_593 (* m.x__AT1 m.x__AT1))) +(let ((.def_634 (* (- 100.0) .def_593))) +(let ((.def_645 (+ .def_634 .def_644))) +(let ((.def_555 (* m.y__AT1 m.y__AT1))) +(let ((.def_632 (* (- 100.0) .def_555))) +(let ((.def_646 (+ .def_632 .def_645))) +(let ((.def_636 (* 4000.0 m.x__AT1))) +(let ((.def_647 (+ .def_636 .def_646))) +(let ((.def_694 (<= 0.0 .def_647))) +(let ((.def_708 (not .def_694))) +(let ((.def_594 (* (- 1.0) .def_593))) +(let ((.def_592 (* (- 1.0) .def_555))) +(let ((.def_595 (+ .def_592 .def_594))) +(let ((.def_596 (* 40.0 m.x__AT1))) +(let ((.def_598 (+ .def_596 .def_595))) +(let ((.def_692 (<= 0.0 .def_598))) +(let ((.def_709 (or .def_692 .def_708))) +(let ((.def_599 (<= .def_598 0.0 ))) +(let ((.def_706 (not .def_599))) +(let ((.def_648 (<= .def_647 0.0 ))) +(let ((.def_707 (or .def_648 .def_706))) +(let ((.def_710 (and .def_707 .def_709))) +(let ((.def_704 (or .def_701 .def_703))) +(let ((.def_705 (not .def_704))) +(let ((.def_711 (or .def_705 .def_710))) +(let ((.def_696 (not .def_648))) +(let ((.def_697 (or .def_599 .def_696))) +(let ((.def_693 (not .def_692))) +(let ((.def_695 (or .def_693 .def_694))) +(let ((.def_698 (and .def_695 .def_697))) +(let ((.def_690 (or .def_681 .def_689))) +(let ((.def_691 (not .def_690))) +(let ((.def_699 (or .def_691 .def_698))) +(let ((.def_712 (and .def_699 .def_711))) +(let ((.def_649 (and .def_599 .def_648))) +(let ((.def_713 (and .def_649 .def_712))) +(let ((.def_925 (and .def_713 .def_924))) +(let ((.def_952 (and .def_925 .def_951))) +(let ((.def_972 (and .def_952 .def_971))) +(let ((.def_571 (+ m.x__AT1 .def_570))) +(let ((.def_577 (<= .def_571 0.0 ))) +(let ((.def_586 (not .def_577))) +(let ((.def_575 (<= m.x__AT1 0.0 ))) +(let ((.def_587 (or .def_575 .def_586))) +(let ((.def_558 (<= 0.0 m.x__AT1))) +(let ((.def_584 (not .def_558))) +(let ((.def_572 (<= 0.0 .def_571))) +(let ((.def_585 (or .def_572 .def_584))) +(let ((.def_588 (and .def_585 .def_587))) +(let ((.def_583 (<= m.speed_x__AT1 0.0 ))) +(let ((.def_589 (or .def_583 .def_588))) +(let ((.def_579 (not .def_572))) +(let ((.def_580 (or .def_558 .def_579))) +(let ((.def_576 (not .def_575))) +(let ((.def_578 (or .def_576 .def_577))) +(let ((.def_581 (and .def_578 .def_580))) +(let ((.def_574 (<= 0.0 m.speed_x__AT1))) +(let ((.def_582 (or .def_574 .def_581))) +(let ((.def_590 (and .def_582 .def_589))) +(let ((.def_573 (and .def_558 .def_572))) +(let ((.def_591 (and .def_573 .def_590))) +(let ((.def_973 (and .def_591 .def_972))) +(let ((.def_566 (<= m.x__AT0 20.0 ))) +(let ((.def_562 (and .def_560 .def_561))) +(let ((.def_553 (+ (- 20.0) m.x__AT1))) +(let ((.def_554 (* .def_553 .def_553))) +(let ((.def_556 (+ .def_554 .def_555))) +(let ((.def_557 (<= 400.0 .def_556))) +(let ((.def_559 (and .def_557 .def_558))) +(let ((.def_563 (and .def_559 .def_562))) +(let ((.def_552 (or .def_549 .def_551))) +(let ((.def_564 (and .def_552 .def_563))) +(let ((.def_543 (<= 0.0 m.delta__AT0))) +(let ((.def_27 (not m.EVENT.0__AT0))) +(let ((.def_25 (not m.EVENT.1__AT0))) +(let ((.def_476 (and .def_25 .def_27))) +(let ((.def_478 (not .def_476))) +(let ((.def_544 (or .def_478 .def_543))) +(let ((.def_545 (or m.EVENT.1__AT0 .def_544))) +(let ((.def_532 (* (- 10.0) m.y__AT1))) +(let ((.def_428 (* m.speed_y__AT0 m.delta__AT0))) +(let ((.def_429 (* 10.0 .def_428))) +(let ((.def_535 (+ .def_429 .def_532))) +(let ((.def_79 (* m.delta__AT0 m.delta__AT0))) +(let ((.def_427 (* (- 49.0) .def_79))) +(let ((.def_536 (+ .def_427 .def_535))) +(let ((.def_431 (* 10.0 m.y__AT0))) +(let ((.def_537 (+ .def_431 .def_536))) +(let ((.def_538 (= .def_537 0.0 ))) +(let ((.def_526 (* (- 5.0) m.speed_y__AT1))) +(let ((.def_264 (* (- 49.0) m.delta__AT0))) +(let ((.def_527 (+ .def_264 .def_526))) +(let ((.def_265 (* 5.0 m.speed_y__AT0))) +(let ((.def_528 (+ .def_265 .def_527))) +(let ((.def_529 (= .def_528 0.0 ))) +(let ((.def_47 (* m.speed_x__AT0 m.delta__AT0))) +(let ((.def_522 (+ .def_47 .def_521))) +(let ((.def_523 (+ m.x__AT0 .def_522))) +(let ((.def_524 (= .def_523 0.0 ))) +(let ((.def_502 (= m.speed_x__AT0 m.speed_x__AT1))) +(let ((.def_525 (and .def_502 .def_524))) +(let ((.def_530 (and .def_525 .def_529))) +(let ((.def_539 (and .def_530 .def_538))) +(let ((.def_540 (or .def_478 .def_539))) +(let ((.def_515 (= m.delta__AT0 0.0 ))) +(let ((.def_516 (and .def_476 .def_515))) +(let ((.def_517 (not .def_516))) +(let ((.def_499 (= m.y__AT0 m.y__AT1))) +(let ((.def_496 (= m.x__AT0 m.x__AT1))) +(let ((.def_510 (and .def_496 .def_499))) +(let ((.def_511 (and .def_502 .def_510))) +(let ((.def_505 (= m.speed_y__AT0 m.speed_y__AT1))) +(let ((.def_512 (and .def_505 .def_511))) +(let ((.def_518 (or .def_512 .def_517))) +(let ((.def_519 (or m.EVENT.1__AT0 .def_518))) +(let ((.def_513 (or .def_476 .def_512))) +(let ((.def_514 (or m.EVENT.1__AT0 .def_513))) +(let ((.def_520 (and .def_514 .def_519))) +(let ((.def_541 (and .def_520 .def_540))) +(let ((.def_483 (= m.time__AT0 m.time__AT1))) +(let ((.def_497 (and .def_483 .def_496))) +(let ((.def_500 (and .def_497 .def_499))) +(let ((.def_503 (and .def_500 .def_502))) +(let ((.def_506 (and .def_503 .def_505))) +(let ((.def_507 (or .def_25 .def_506))) +(let ((.def_486 (* (- 1.0) m.time__AT1))) +(let ((.def_489 (+ m.delta__AT0 .def_486))) +(let ((.def_490 (+ m.time__AT0 .def_489))) +(let ((.def_491 (= .def_490 0.0 ))) +(let ((.def_492 (or .def_478 .def_491))) +(let ((.def_493 (or m.EVENT.1__AT0 .def_492))) +(let ((.def_484 (or .def_476 .def_483))) +(let ((.def_485 (or m.EVENT.1__AT0 .def_484))) +(let ((.def_494 (and .def_485 .def_493))) +(let ((.def_508 (and .def_494 .def_507))) +(let ((.def_480 (= .def_478 m.event_is_timed__AT1))) +(let ((.def_477 (= m.event_is_timed__AT0 .def_476))) +(let ((.def_481 (and .def_477 .def_480))) +(let ((.def_509 (and .def_481 .def_508))) +(let ((.def_542 (and .def_509 .def_541))) +(let ((.def_546 (and .def_542 .def_545))) +(let ((.def_547 (and .def_25 .def_546))) +(let ((.def_565 (and .def_547 .def_564))) +(let ((.def_567 (and .def_565 .def_566))) +(let ((.def_430 (+ .def_427 .def_429))) +(let ((.def_433 (+ .def_431 .def_430))) +(let ((.def_458 (<= .def_433 0.0 ))) +(let ((.def_466 (not .def_458))) +(let ((.def_456 (<= m.y__AT0 0.0 ))) +(let ((.def_467 (or .def_456 .def_466))) +(let ((.def_40 (<= 0.0 m.y__AT0))) +(let ((.def_464 (not .def_40))) +(let ((.def_454 (<= 0.0 .def_433))) +(let ((.def_465 (or .def_454 .def_464))) +(let ((.def_468 (and .def_465 .def_467))) +(let ((.def_270 (<= m.speed_y__AT0 0.0 ))) +(let ((.def_271 (not .def_270))) +(let ((.def_267 (+ .def_265 .def_264))) +(let ((.def_268 (<= .def_267 0.0 ))) +(let ((.def_269 (not .def_268))) +(let ((.def_272 (or .def_269 .def_271))) +(let ((.def_273 (not .def_272))) +(let ((.def_469 (or .def_273 .def_468))) +(let ((.def_460 (not .def_454))) +(let ((.def_461 (or .def_40 .def_460))) +(let ((.def_457 (not .def_456))) +(let ((.def_459 (or .def_457 .def_458))) +(let ((.def_462 (and .def_459 .def_461))) +(let ((.def_279 (<= 0.0 .def_267))) +(let ((.def_280 (not .def_279))) +(let ((.def_22 (<= 0.0 m.speed_y__AT0))) +(let ((.def_278 (not .def_22))) +(let ((.def_281 (or .def_278 .def_280))) +(let ((.def_282 (not .def_281))) +(let ((.def_463 (or .def_282 .def_462))) +(let ((.def_470 (and .def_463 .def_469))) +(let ((.def_455 (and .def_40 .def_454))) +(let ((.def_471 (and .def_455 .def_470))) +(let ((.def_291 (and .def_268 .def_270))) +(let ((.def_288 (or .def_22 .def_280))) +(let ((.def_287 (or .def_268 .def_271))) +(let ((.def_289 (and .def_287 .def_288))) +(let ((.def_292 (and .def_289 .def_291))) +(let ((.def_286 (and .def_22 .def_279))) +(let ((.def_290 (and .def_286 .def_289))) +(let ((.def_293 (or .def_290 .def_292))) +(let ((.def_472 (and .def_293 .def_471))) +(let ((.def_434 (<= .def_433 1000.0 ))) +(let ((.def_446 (not .def_434))) +(let ((.def_39 (<= m.y__AT0 100.0 ))) +(let ((.def_447 (or .def_39 .def_446))) +(let ((.def_440 (<= 100.0 m.y__AT0))) +(let ((.def_444 (not .def_440))) +(let ((.def_438 (<= 1000.0 .def_433))) +(let ((.def_445 (or .def_438 .def_444))) +(let ((.def_448 (and .def_445 .def_447))) +(let ((.def_449 (or .def_273 .def_448))) +(let ((.def_439 (not .def_438))) +(let ((.def_441 (or .def_439 .def_440))) +(let ((.def_436 (not .def_39))) +(let ((.def_437 (or .def_434 .def_436))) +(let ((.def_442 (and .def_437 .def_441))) +(let ((.def_443 (or .def_282 .def_442))) +(let ((.def_450 (and .def_443 .def_449))) +(let ((.def_435 (and .def_39 .def_434))) +(let ((.def_451 (and .def_435 .def_450))) +(let ((.def_452 (and .def_293 .def_451))) +(let ((.def_89 (* (- (/ 49 10)) m.speed_y__AT0))) +(let ((.def_140 (* 3.0 .def_89))) +(let ((.def_324 (* (- 1.0) .def_140))) +(let ((.def_352 (* 2.0 .def_324))) +(let ((.def_396 (* (- 1.0) .def_352))) +(let ((.def_397 (* m.delta__AT0 .def_396))) +(let ((.def_398 (* (- 50.0) .def_397))) +(let ((.def_108 (* m.speed_x__AT0 m.speed_x__AT0))) +(let ((.def_216 (* (- 50.0) .def_108))) +(let ((.def_403 (+ .def_216 .def_398))) +(let ((.def_95 (* m.speed_y__AT0 m.speed_y__AT0))) +(let ((.def_214 (* (- 50.0) .def_95))) +(let ((.def_404 (+ .def_214 .def_403))) +(let ((.def_220 (* (- 7203.0) .def_79))) +(let ((.def_405 (+ .def_220 .def_404))) +(let ((.def_223 (* 490.0 m.y__AT0))) +(let ((.def_406 (+ .def_223 .def_405))) +(let ((.def_409 (<= 0.0 .def_406))) +(let ((.def_416 (not .def_409))) +(let ((.def_234 (* (- 5.0) .def_108))) +(let ((.def_233 (* (- 5.0) .def_95))) +(let ((.def_235 (+ .def_233 .def_234))) +(let ((.def_236 (* 49.0 m.y__AT0))) +(let ((.def_238 (+ .def_236 .def_235))) +(let ((.def_249 (<= 0.0 .def_238))) +(let ((.def_417 (or .def_249 .def_416))) +(let ((.def_407 (<= .def_406 0.0 ))) +(let ((.def_239 (<= .def_238 0.0 ))) +(let ((.def_240 (not .def_239))) +(let ((.def_415 (or .def_240 .def_407))) +(let ((.def_418 (and .def_415 .def_417))) +(let ((.def_419 (or .def_282 .def_418))) +(let ((.def_411 (not .def_407))) +(let ((.def_412 (or .def_239 .def_411))) +(let ((.def_250 (not .def_249))) +(let ((.def_410 (or .def_250 .def_409))) +(let ((.def_413 (and .def_410 .def_412))) +(let ((.def_414 (or .def_273 .def_413))) +(let ((.def_420 (and .def_414 .def_419))) +(let ((.def_408 (and .def_239 .def_407))) +(let ((.def_421 (and .def_408 .def_420))) +(let ((.def_422 (and .def_293 .def_421))) +(let ((.def_353 (* m.delta__AT0 .def_352))) +(let ((.def_354 (* 50.0 .def_353))) +(let ((.def_359 (+ .def_216 .def_354))) +(let ((.def_360 (+ .def_214 .def_359))) +(let ((.def_361 (+ .def_220 .def_360))) +(let ((.def_362 (+ .def_223 .def_361))) +(let ((.def_373 (<= .def_362 0.0 ))) +(let ((.def_374 (not .def_373))) +(let ((.def_390 (or .def_239 .def_374))) +(let ((.def_363 (<= 0.0 .def_362))) +(let ((.def_389 (or .def_250 .def_363))) +(let ((.def_391 (and .def_389 .def_390))) +(let ((.def_392 (or .def_273 .def_391))) +(let ((.def_364 (not .def_363))) +(let ((.def_386 (or .def_249 .def_364))) +(let ((.def_385 (or .def_240 .def_373))) +(let ((.def_387 (and .def_385 .def_386))) +(let ((.def_388 (or .def_282 .def_387))) +(let ((.def_393 (and .def_388 .def_392))) +(let ((.def_384 (and .def_249 .def_363))) +(let ((.def_394 (and .def_384 .def_393))) +(let ((.def_395 (and .def_293 .def_394))) +(let ((.def_423 (or .def_395 .def_422))) +(let ((.def_156 (* 2.0 .def_108))) +(let ((.def_336 (* (- 1.0) .def_156))) +(let ((.def_337 (* m.delta__AT0 .def_336))) +(let ((.def_338 (* 25.0 .def_337))) +(let ((.def_100 (* (- (/ 49 10)) m.y__AT0))) +(let ((.def_152 (* 2.0 .def_100))) +(let ((.def_332 (* (- 1.0) .def_152))) +(let ((.def_333 (* m.delta__AT0 .def_332))) +(let ((.def_334 (* 50.0 .def_333))) +(let ((.def_343 (+ .def_334 .def_338))) +(let ((.def_146 (* 2.0 .def_95))) +(let ((.def_328 (* (- 1.0) .def_146))) +(let ((.def_329 (* m.delta__AT0 .def_328))) +(let ((.def_330 (* 25.0 .def_329))) +(let ((.def_344 (+ .def_330 .def_343))) +(let ((.def_325 (* .def_79 .def_324))) +(let ((.def_326 (* 50.0 .def_325))) +(let ((.def_345 (+ .def_326 .def_344))) +(let ((.def_112 (* m.x__AT0 m.speed_x__AT0))) +(let ((.def_164 (* (- 50.0) .def_112))) +(let ((.def_346 (+ .def_164 .def_345))) +(let ((.def_104 (* m.y__AT0 m.speed_y__AT0))) +(let ((.def_162 (* (- 50.0) .def_104))) +(let ((.def_347 (+ .def_162 .def_346))) +(let ((.def_80 (* m.delta__AT0 .def_79))) +(let ((.def_160 (* (- 2401.0) .def_80))) +(let ((.def_348 (+ .def_160 .def_347))) +(let ((.def_167 (* 1000.0 m.speed_x__AT0))) +(let ((.def_349 (+ .def_167 .def_348))) +(let ((.def_367 (<= .def_349 0.0 ))) +(let ((.def_378 (not .def_367))) +(let ((.def_179 (* (- 1.0) .def_112))) +(let ((.def_178 (* (- 1.0) .def_104))) +(let ((.def_180 (+ .def_178 .def_179))) +(let ((.def_181 (* 20.0 m.speed_x__AT0))) +(let ((.def_183 (+ .def_181 .def_180))) +(let ((.def_184 (<= .def_183 0.0 ))) +(let ((.def_379 (or .def_184 .def_378))) +(let ((.def_350 (<= 0.0 .def_349))) +(let ((.def_198 (<= 0.0 .def_183))) +(let ((.def_199 (not .def_198))) +(let ((.def_377 (or .def_199 .def_350))) +(let ((.def_380 (and .def_377 .def_379))) +(let ((.def_375 (or .def_240 .def_374))) +(let ((.def_376 (not .def_375))) +(let ((.def_381 (or .def_376 .def_380))) +(let ((.def_369 (not .def_350))) +(let ((.def_370 (or .def_198 .def_369))) +(let ((.def_185 (not .def_184))) +(let ((.def_368 (or .def_185 .def_367))) +(let ((.def_371 (and .def_368 .def_370))) +(let ((.def_365 (or .def_250 .def_364))) +(let ((.def_366 (not .def_365))) +(let ((.def_372 (or .def_366 .def_371))) +(let ((.def_382 (and .def_372 .def_381))) +(let ((.def_351 (and .def_198 .def_350))) +(let ((.def_383 (and .def_351 .def_382))) +(let ((.def_424 (and .def_383 .def_423))) +(let ((.def_211 (* 2.0 .def_140))) +(let ((.def_295 (* (- 1.0) .def_211))) +(let ((.def_296 (* m.delta__AT0 .def_295))) +(let ((.def_297 (* 50.0 .def_296))) +(let ((.def_302 (+ .def_216 .def_297))) +(let ((.def_303 (+ .def_214 .def_302))) +(let ((.def_304 (+ .def_220 .def_303))) +(let ((.def_305 (+ .def_223 .def_304))) +(let ((.def_308 (<= .def_305 0.0 ))) +(let ((.def_315 (not .def_308))) +(let ((.def_316 (or .def_239 .def_315))) +(let ((.def_306 (<= 0.0 .def_305))) +(let ((.def_314 (or .def_250 .def_306))) +(let ((.def_317 (and .def_314 .def_316))) +(let ((.def_318 (or .def_273 .def_317))) +(let ((.def_310 (not .def_306))) +(let ((.def_311 (or .def_249 .def_310))) +(let ((.def_309 (or .def_240 .def_308))) +(let ((.def_312 (and .def_309 .def_311))) +(let ((.def_313 (or .def_282 .def_312))) +(let ((.def_319 (and .def_313 .def_318))) +(let ((.def_307 (and .def_249 .def_306))) +(let ((.def_320 (and .def_307 .def_319))) +(let ((.def_321 (and .def_293 .def_320))) +(let ((.def_212 (* m.delta__AT0 .def_211))) +(let ((.def_213 (* (- 50.0) .def_212))) +(let ((.def_225 (+ .def_216 .def_213))) +(let ((.def_226 (+ .def_214 .def_225))) +(let ((.def_227 (+ .def_220 .def_226))) +(let ((.def_228 (+ .def_223 .def_227))) +(let ((.def_247 (<= 0.0 .def_228))) +(let ((.def_248 (not .def_247))) +(let ((.def_276 (or .def_248 .def_249))) +(let ((.def_229 (<= .def_228 0.0 ))) +(let ((.def_275 (or .def_229 .def_240))) +(let ((.def_277 (and .def_275 .def_276))) +(let ((.def_283 (or .def_277 .def_282))) +(let ((.def_230 (not .def_229))) +(let ((.def_261 (or .def_230 .def_239))) +(let ((.def_260 (or .def_247 .def_250))) +(let ((.def_262 (and .def_260 .def_261))) +(let ((.def_274 (or .def_262 .def_273))) +(let ((.def_284 (and .def_274 .def_283))) +(let ((.def_259 (and .def_229 .def_239))) +(let ((.def_285 (and .def_259 .def_284))) +(let ((.def_294 (and .def_285 .def_293))) +(let ((.def_322 (or .def_294 .def_321))) +(let ((.def_157 (* m.delta__AT0 .def_156))) +(let ((.def_158 (* (- 25.0) .def_157))) +(let ((.def_153 (* m.delta__AT0 .def_152))) +(let ((.def_154 (* (- 50.0) .def_153))) +(let ((.def_169 (+ .def_154 .def_158))) +(let ((.def_147 (* m.delta__AT0 .def_146))) +(let ((.def_150 (* (- 25.0) .def_147))) +(let ((.def_170 (+ .def_150 .def_169))) +(let ((.def_141 (* .def_79 .def_140))) +(let ((.def_144 (* (- 50.0) .def_141))) +(let ((.def_171 (+ .def_144 .def_170))) +(let ((.def_172 (+ .def_164 .def_171))) +(let ((.def_173 (+ .def_162 .def_172))) +(let ((.def_174 (+ .def_160 .def_173))) +(let ((.def_175 (+ .def_167 .def_174))) +(let ((.def_196 (<= 0.0 .def_175))) +(let ((.def_197 (not .def_196))) +(let ((.def_254 (or .def_197 .def_198))) +(let ((.def_176 (<= .def_175 0.0 ))) +(let ((.def_253 (or .def_176 .def_185))) +(let ((.def_255 (and .def_253 .def_254))) +(let ((.def_251 (or .def_248 .def_250))) +(let ((.def_252 (not .def_251))) +(let ((.def_256 (or .def_252 .def_255))) +(let ((.def_177 (not .def_176))) +(let ((.def_244 (or .def_177 .def_184))) +(let ((.def_243 (or .def_196 .def_199))) +(let ((.def_245 (and .def_243 .def_244))) +(let ((.def_241 (or .def_230 .def_240))) +(let ((.def_242 (not .def_241))) +(let ((.def_246 (or .def_242 .def_245))) +(let ((.def_257 (and .def_246 .def_256))) +(let ((.def_210 (and .def_176 .def_184))) +(let ((.def_258 (and .def_210 .def_257))) +(let ((.def_323 (and .def_258 .def_322))) +(let ((.def_425 (or .def_323 .def_424))) +(let ((.def_116 (* (- 20.0) m.speed_x__AT0))) +(let ((.def_117 (* m.delta__AT0 .def_116))) +(let ((.def_118 (* (- 200.0) .def_117))) +(let ((.def_113 (* m.delta__AT0 .def_112))) +(let ((.def_114 (* (- 200.0) .def_113))) +(let ((.def_127 (+ .def_114 .def_118))) +(let ((.def_109 (* .def_79 .def_108))) +(let ((.def_110 (* (- 100.0) .def_109))) +(let ((.def_128 (+ .def_110 .def_127))) +(let ((.def_105 (* m.delta__AT0 .def_104))) +(let ((.def_106 (* (- 200.0) .def_105))) +(let ((.def_129 (+ .def_106 .def_128))) +(let ((.def_101 (* .def_79 .def_100))) +(let ((.def_102 (* (- 200.0) .def_101))) +(let ((.def_130 (+ .def_102 .def_129))) +(let ((.def_96 (* .def_79 .def_95))) +(let ((.def_98 (* (- 100.0) .def_96))) +(let ((.def_131 (+ .def_98 .def_130))) +(let ((.def_90 (* .def_80 .def_89))) +(let ((.def_93 (* (- 200.0) .def_90))) +(let ((.def_132 (+ .def_93 .def_131))) +(let ((.def_81 (* m.delta__AT0 .def_80))) +(let ((.def_84 (* (- 2401.0) .def_81))) +(let ((.def_133 (+ .def_84 .def_132))) +(let ((.def_71 (* m.x__AT0 m.x__AT0))) +(let ((.def_122 (* (- 100.0) .def_71))) +(let ((.def_134 (+ .def_122 .def_133))) +(let ((.def_32 (* m.y__AT0 m.y__AT0))) +(let ((.def_120 (* (- 100.0) .def_32))) +(let ((.def_135 (+ .def_120 .def_134))) +(let ((.def_125 (* 4000.0 m.x__AT0))) +(let ((.def_136 (+ .def_125 .def_135))) +(let ((.def_190 (<= 0.0 .def_136))) +(let ((.def_204 (not .def_190))) +(let ((.def_72 (* (- 1.0) .def_71))) +(let ((.def_70 (* (- 1.0) .def_32))) +(let ((.def_73 (+ .def_70 .def_72))) +(let ((.def_75 (* 40.0 m.x__AT0))) +(let ((.def_77 (+ .def_75 .def_73))) +(let ((.def_188 (<= 0.0 .def_77))) +(let ((.def_205 (or .def_188 .def_204))) +(let ((.def_78 (<= .def_77 0.0 ))) +(let ((.def_202 (not .def_78))) +(let ((.def_137 (<= .def_136 0.0 ))) +(let ((.def_203 (or .def_137 .def_202))) +(let ((.def_206 (and .def_203 .def_205))) +(let ((.def_200 (or .def_197 .def_199))) +(let ((.def_201 (not .def_200))) +(let ((.def_207 (or .def_201 .def_206))) +(let ((.def_192 (not .def_137))) +(let ((.def_193 (or .def_78 .def_192))) +(let ((.def_189 (not .def_188))) +(let ((.def_191 (or .def_189 .def_190))) +(let ((.def_194 (and .def_191 .def_193))) +(let ((.def_186 (or .def_177 .def_185))) +(let ((.def_187 (not .def_186))) +(let ((.def_195 (or .def_187 .def_194))) +(let ((.def_208 (and .def_195 .def_207))) +(let ((.def_138 (and .def_78 .def_137))) +(let ((.def_209 (and .def_138 .def_208))) +(let ((.def_426 (and .def_209 .def_425))) +(let ((.def_453 (and .def_426 .def_452))) +(let ((.def_473 (and .def_453 .def_472))) +(let ((.def_48 (+ m.x__AT0 .def_47))) +(let ((.def_53 (<= .def_48 0.0 ))) +(let ((.def_62 (not .def_53))) +(let ((.def_51 (<= m.x__AT0 0.0 ))) +(let ((.def_63 (or .def_51 .def_62))) +(let ((.def_36 (<= 0.0 m.x__AT0))) +(let ((.def_60 (not .def_36))) +(let ((.def_49 (<= 0.0 .def_48))) +(let ((.def_61 (or .def_49 .def_60))) +(let ((.def_64 (and .def_61 .def_63))) +(let ((.def_59 (<= m.speed_x__AT0 0.0 ))) +(let ((.def_65 (or .def_59 .def_64))) +(let ((.def_55 (not .def_49))) +(let ((.def_56 (or .def_36 .def_55))) +(let ((.def_52 (not .def_51))) +(let ((.def_54 (or .def_52 .def_53))) +(let ((.def_57 (and .def_54 .def_56))) +(let ((.def_19 (<= 0.0 m.speed_x__AT0))) +(let ((.def_58 (or .def_19 .def_57))) +(let ((.def_66 (and .def_58 .def_65))) +(let ((.def_50 (and .def_36 .def_49))) +(let ((.def_67 (and .def_50 .def_66))) +(let ((.def_474 (and .def_67 .def_473))) +(let ((.def_41 (and .def_39 .def_40))) +(let ((.def_30 (+ m.x__AT0 (- 20.0) ))) +(let ((.def_31 (* .def_30 .def_30))) +(let ((.def_33 (+ .def_31 .def_32))) +(let ((.def_35 (<= 400.0 .def_33))) +(let ((.def_37 (and .def_35 .def_36))) +(let ((.def_42 (and .def_37 .def_41))) +(let ((.def_28 (or .def_25 .def_27))) +(let ((.def_43 (and .def_28 .def_42))) +(let ((.def_16 (= m.y__AT0 0.0 ))) +(let ((.def_13 (= m.x__AT0 0.0 ))) +(let ((.def_9 (= m.time__AT0 0.0 ))) +(let ((.def_11 (and .def_9 m.event_is_timed__AT0))) +(let ((.def_14 (and .def_11 .def_13))) +(let ((.def_17 (and .def_14 .def_16))) +(let ((.def_20 (and .def_17 .def_19))) +(let ((.def_23 (and .def_20 .def_22))) +(let ((.def_44 (and .def_23 .def_43))) +(let ((.def_5 (<= m.x__AT2 20.0 ))) +(let ((.def_6 (not .def_5))) +(let ((.def_45 (and .def_6 .def_44))) +(let ((.def_475 (and .def_45 .def_474))) +(let ((.def_568 (and .def_475 .def_567))) +(let ((.def_974 (and .def_568 .def_973))) +(let ((.def_1069 (and .def_974 .def_1068))) +(let ((.def_1475 (and .def_1069 .def_1474))) +.def_1475)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) +(check-sat) +(exit) diff --git a/tests/regress/mcsat/nra/simple_ballistics_reach.01.seq_lazy_lemmas_global_2.smt2.gold b/tests/regress/mcsat/nra/simple_ballistics_reach.01.seq_lazy_lemmas_global_2.smt2.gold new file mode 100644 index 000000000..3f65111b0 --- /dev/null +++ b/tests/regress/mcsat/nra/simple_ballistics_reach.01.seq_lazy_lemmas_global_2.smt2.gold @@ -0,0 +1 @@ +unsat From f0ff87a044ef210044515e14729b7b7a563bdb5c Mon Sep 17 00:00:00 2001 From: Dejan Jovanovic Date: Thu, 14 May 2020 11:12:58 -0400 Subject: [PATCH 04/16] tests --- src/mcsat/nra/nra_plugin.c | 6 +++ .../nra/exp-problem-10-2-chunk-0147.smt2 | 28 ++++++++++ .../nra/exp-problem-10-2-chunk-0147.smt2.gold | 1 + tests/regress/mcsat/nra/matrix-1-all-01.smt2 | 51 +++++++++++++++++++ .../mcsat/nra/matrix-1-all-01.smt2.gold | 1 + .../mcsat/nra/sqrt-problem-13-chunk-0024.smt2 | 28 ++++++++++ .../nra/sqrt-problem-13-chunk-0024.smt2.gold | 1 + 7 files changed, 116 insertions(+) create mode 100644 tests/regress/mcsat/nra/exp-problem-10-2-chunk-0147.smt2 create mode 100644 tests/regress/mcsat/nra/exp-problem-10-2-chunk-0147.smt2.gold create mode 100644 tests/regress/mcsat/nra/matrix-1-all-01.smt2 create mode 100644 tests/regress/mcsat/nra/matrix-1-all-01.smt2.gold create mode 100644 tests/regress/mcsat/nra/sqrt-problem-13-chunk-0024.smt2 create mode 100644 tests/regress/mcsat/nra/sqrt-problem-13-chunk-0024.smt2.gold diff --git a/src/mcsat/nra/nra_plugin.c b/src/mcsat/nra/nra_plugin.c index cc0378a11..bd67fdc6e 100644 --- a/src/mcsat/nra/nra_plugin.c +++ b/src/mcsat/nra/nra_plugin.c @@ -1791,6 +1791,12 @@ void nra_plugin_learn(plugin_t* plugin, trail_token_t* prop) { 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); diff --git a/tests/regress/mcsat/nra/exp-problem-10-2-chunk-0147.smt2 b/tests/regress/mcsat/nra/exp-problem-10-2-chunk-0147.smt2 new file mode 100644 index 000000000..66d2e7bb9 --- /dev/null +++ b/tests/regress/mcsat/nra/exp-problem-10-2-chunk-0147.smt2 @@ -0,0 +1,28 @@ +(set-info :smt-lib-version 2.6) +(set-logic QF_NRA) +(set-info :source | +These benchmarks used in the paper: + + Dejan Jovanovic and Leonardo de Moura. Solving Non-Linear Arithmetic. + In IJCAR 2012, published as LNCS volume 7364, pp. 339--354. + +The meti-tarski benchmarks are proof obligations extracted from the +Meti-Tarski project, see: + + B. Akbarpour and L. C. Paulson. MetiTarski: An automatic theorem prover + for real-valued special functions. Journal of Automated Reasoning, + 44(3):175-205, 2010. + +Submitted by Dejan Jovanovic for SMT-LIB. + + +|) +(set-info :category "industrial") +(set-info :status sat) +(declare-fun skoSM1 () Real) +(declare-fun skoSP1 () Real) +(declare-fun skoS () Real) +(declare-fun skoX () Real) +(assert (and (<= (* skoSP1 (+ (* skoSM1 12) (* skoSP1 (* skoSM1 (- 24))))) (* skoSM1 2)) (and (= (+ (- 1) (* skoSP1 skoSP1)) skoX) (and (= (+ 1 (* skoSM1 skoSM1)) skoX) (and (= (* skoS skoS) skoX) (and (not (<= skoX 1)) (and (not (<= skoSP1 0)) (and (not (<= skoSM1 0)) (and (not (<= skoS 0)) (not (<= 5 skoX))))))))))) +(check-sat) +(exit) diff --git a/tests/regress/mcsat/nra/exp-problem-10-2-chunk-0147.smt2.gold b/tests/regress/mcsat/nra/exp-problem-10-2-chunk-0147.smt2.gold new file mode 100644 index 000000000..6b8a2c3d2 --- /dev/null +++ b/tests/regress/mcsat/nra/exp-problem-10-2-chunk-0147.smt2.gold @@ -0,0 +1 @@ +sat diff --git a/tests/regress/mcsat/nra/matrix-1-all-01.smt2 b/tests/regress/mcsat/nra/matrix-1-all-01.smt2 new file mode 100644 index 000000000..e4041df22 --- /dev/null +++ b/tests/regress/mcsat/nra/matrix-1-all-01.smt2 @@ -0,0 +1,51 @@ +(set-info :smt-lib-version 2.6) +(set-logic QF_NRA) +(set-info :source | +From termination analysis of term rewriting. + +Submitted by Harald Roman Zankl + +|) +(set-info :category "industrial") +(set-info :status sat) +(declare-fun x6 () Real) +(declare-fun x13 () Real) +(declare-fun x3 () Real) +(declare-fun x10 () Real) +(declare-fun x0 () Real) +(declare-fun x17 () Real) +(declare-fun x7 () Real) +(declare-fun x14 () Real) +(declare-fun x4 () Real) +(declare-fun x11 () Real) +(declare-fun x1 () Real) +(declare-fun x18 () Real) +(declare-fun x8 () Real) +(declare-fun x15 () Real) +(declare-fun x5 () Real) +(declare-fun x12 () Real) +(declare-fun x2 () Real) +(declare-fun x9 () Real) +(declare-fun x16 () Real) +(assert (>= x6 0)) +(assert (>= x13 0)) +(assert (>= x3 0)) +(assert (>= x10 0)) +(assert (>= x0 0)) +(assert (>= x17 0)) +(assert (>= x7 0)) +(assert (>= x14 0)) +(assert (>= x4 0)) +(assert (>= x11 0)) +(assert (>= x1 0)) +(assert (>= x18 0)) +(assert (>= x8 0)) +(assert (>= x15 0)) +(assert (>= x5 0)) +(assert (>= x12 0)) +(assert (>= x2 0)) +(assert (>= x9 0)) +(assert (>= x16 0)) +(assert (let ((?v_0 (+ x0 (* x2 x3))) (?v_2 (* x2 x4)) (?v_1 (+ x5 (* x6 x7))) (?v_4 (* x12 x3))) (let ((?v_3 (+ (+ x10 (* x11 x3)) ?v_4)) (?v_6 (* x11 x4)) (?v_7 (* x12 x4)) (?v_5 (+ (+ x10 (* x11 x7)) ?v_4))) (let ((?v_17 (and (and (and (and (and (> ?v_0 x0) (>= ?v_0 x0)) (>= ?v_2 x2)) (and (and (and (> ?v_0 ?v_1) (>= ?v_0 ?v_1)) (>= x1 (* x6 x8))) (>= ?v_2 (* x6 x9)))) (and (and (and (> ?v_3 x0) (>= ?v_3 x0)) (>= ?v_6 x1)) (>= ?v_7 x2))) (and (and (and (> ?v_3 ?v_5) (>= ?v_3 ?v_5)) (>= ?v_6 (* x11 x8))) (>= ?v_7 (+ (* x11 x9) ?v_7))))) (?v_8 (+ x13 (* x14 x3))) (?v_9 (+ x7 (* x9 x15))) (?v_11 (+ x13 (* x14 x7))) (?v_10 (+ x7 (* x9 x3))) (?v_13 (* x18 x3))) (let ((?v_12 (+ (+ x16 (* x17 x15)) ?v_13)) (?v_15 (+ x3 (* x4 (+ (+ x16 (* x17 x7)) ?v_13)))) (?v_14 (+ (+ x16 (* x17 x3)) ?v_13)) (?v_16 (* x18 x4))) (and (and (and (and (and (and ?v_17 (and (and (> ?v_8 0) (>= ?v_8 0)) (>= (* x14 x4) 1))) (and (and (> ?v_9 0) (>= ?v_9 0)) (>= x8 1))) (and (and (and (> ?v_10 ?v_11) (>= ?v_10 ?v_11)) (>= x8 (* x14 x8))) (>= (* x9 x4) (* x14 x9)))) (and (> ?v_12 x15) (>= ?v_12 x15))) (and (and (and (> ?v_14 ?v_15) (>= ?v_14 ?v_15)) (>= (* x17 x4) (* x4 (* x17 x8)))) (>= ?v_16 (* x4 (+ (* x17 x9) ?v_16))))) ?v_17)))))) +(check-sat) +(exit) diff --git a/tests/regress/mcsat/nra/matrix-1-all-01.smt2.gold b/tests/regress/mcsat/nra/matrix-1-all-01.smt2.gold new file mode 100644 index 000000000..6b8a2c3d2 --- /dev/null +++ b/tests/regress/mcsat/nra/matrix-1-all-01.smt2.gold @@ -0,0 +1 @@ +sat diff --git a/tests/regress/mcsat/nra/sqrt-problem-13-chunk-0024.smt2 b/tests/regress/mcsat/nra/sqrt-problem-13-chunk-0024.smt2 new file mode 100644 index 000000000..eadeb0079 --- /dev/null +++ b/tests/regress/mcsat/nra/sqrt-problem-13-chunk-0024.smt2 @@ -0,0 +1,28 @@ +(set-info :smt-lib-version 2.6) +(set-logic QF_NRA) +(set-info :source | +These benchmarks used in the paper: + + Dejan Jovanovic and Leonardo de Moura. Solving Non-Linear Arithmetic. + In IJCAR 2012, published as LNCS volume 7364, pp. 339--354. + +The meti-tarski benchmarks are proof obligations extracted from the +Meti-Tarski project, see: + + B. Akbarpour and L. C. Paulson. MetiTarski: An automatic theorem prover + for real-valued special functions. Journal of Automated Reasoning, + 44(3):175-205, 2010. + +Submitted by Dejan Jovanovic for SMT-LIB. + + +|) +(set-info :category "industrial") +(set-info :status sat) +(declare-fun skoSXY () Real) +(declare-fun skoT () Real) +(declare-fun skoX () Real) +(declare-fun skoY () Real) +(assert (and (not (= (+ (* skoSXY (- 1)) (* skoT (* skoT skoSXY))) skoX)) (and (= (+ (* skoSXY skoSXY) (* skoX (- 1))) skoY) (and (<= skoY (/ 33 32)) (and (<= skoX 2) (and (<= (/ 3 2) skoX) (and (<= 1 skoY) (and (<= 0 skoT) (<= 0 skoSXY))))))))) +(check-sat) +(exit) diff --git a/tests/regress/mcsat/nra/sqrt-problem-13-chunk-0024.smt2.gold b/tests/regress/mcsat/nra/sqrt-problem-13-chunk-0024.smt2.gold new file mode 100644 index 000000000..6b8a2c3d2 --- /dev/null +++ b/tests/regress/mcsat/nra/sqrt-problem-13-chunk-0024.smt2.gold @@ -0,0 +1 @@ +sat From 69d16c3d40e385c642ad0826e6104c84beadbd63 Mon Sep 17 00:00:00 2001 From: Dejan Jovanovic Date: Thu, 14 May 2020 15:03:49 -0400 Subject: [PATCH 05/16] for now, learn only at start --- src/mcsat/solver.c | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/src/mcsat/solver.c b/src/mcsat/solver.c index fbf1bafd0..97d88bda1 100644 --- a/src/mcsat/solver.c +++ b/src/mcsat/solver.c @@ -2055,6 +2055,9 @@ void mcsat_solve(mcsat_solver_t* mcsat, const param_t *params) { restart_resource = 0; luby_init(&luby, mcsat->heuristic_params.restart_interval); + // Whether to run learning + bool learning = true; + while (!mcsat->stop_search) { // Do we restart @@ -2068,7 +2071,8 @@ void mcsat_solve(mcsat_solver_t* mcsat, const param_t *params) { mcsat_process_requests(mcsat); // Do propagation - mcsat_propagate(mcsat, true); + mcsat_propagate(mcsat, learning); + learning = false; // If inconsistent, analyze the conflict if (!trail_is_consistent(mcsat->trail)) { From 4acd43c9212d593748ed3e2dcb9a28218d099a34 Mon Sep 17 00:00:00 2001 From: Dejan Jovanovic Date: Fri, 15 May 2020 20:41:41 -0400 Subject: [PATCH 06/16] bound inference and some tests --- src/mcsat/nra/nra_plugin.c | 75 ++++++++++++++++++++++- src/mcsat/nra/nra_plugin_internal.c | 5 ++ src/mcsat/nra/nra_plugin_internal.h | 5 ++ src/mcsat/nra/poly_constraint.c | 39 ++++++++++-- src/mcsat/nra/poly_constraint.h | 3 + tests/regress/mcsat/nra/hong_20.smt2 | 42 +++++++++++++ tests/regress/mcsat/nra/hong_20.smt2.gold | 1 + 7 files changed, 161 insertions(+), 9 deletions(-) create mode 100644 tests/regress/mcsat/nra/hong_20.smt2 create mode 100644 tests/regress/mcsat/nra/hong_20.smt2.gold diff --git a/src/mcsat/nra/nra_plugin.c b/src/mcsat/nra/nra_plugin.c index bd67fdc6e..b439f0c10 100644 --- a/src/mcsat/nra/nra_plugin.c +++ b/src/mcsat/nra/nra_plugin.c @@ -118,10 +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::interval"); + lp_trace_enable("polynomial::bounds"); } // Trace pscs @@ -203,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); } @@ -673,6 +676,60 @@ 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); + poly_constraint_infer_bounds(constraint, !trail_value, m, &lp_variables); + + // 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) { @@ -945,9 +1002,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; + } } } diff --git a/src/mcsat/nra/nra_plugin_internal.c b/src/mcsat/nra/nra_plugin_internal.c index 3596aa7ff..0cb396e35 100644 --- a/src/mcsat/nra/nra_plugin_internal.c +++ b/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) { diff --git a/src/mcsat/nra/nra_plugin_internal.h b/src/mcsat/nra/nra_plugin_internal.h index f9b64651d..cadfc4c54 100644 --- a/src/mcsat/nra/nra_plugin_internal.h +++ b/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); diff --git a/src/mcsat/nra/poly_constraint.c b/src/mcsat/nra/poly_constraint.c index 1089eed96..574a2d513 100644 --- a/src/mcsat/nra/poly_constraint.c +++ b/src/mcsat/nra/poly_constraint.c @@ -286,6 +286,34 @@ lp_feasibility_set_t* poly_constraint_get_feasible_set(const poly_constraint_t* return feasible; } +void poly_constraint_infer_bounds(const poly_constraint_t* cstr, bool negated, lp_interval_assignment_t* m, ivector_t* inferred_vars) { + + // TODO: is it possible to support root constraints + if (poly_constraint_is_root_constraint(cstr)) { + return; + } + + // Infer some bounds + bool something_inferred = lp_polynomial_constraint_infer_bounds(cstr->polynomial, cstr->sgn_condition, negated, m); + if (!something_inferred) { + return; + } + + lp_variable_list_t vars; + lp_variable_list_construct(&vars); + lp_polynomial_get_variables(cstr->polynomial, &vars); + uint32_t var_i; + for (var_i = 0; var_i < vars.list_size; ++ var_i) { + lp_variable_t x_lp = vars.list[var_i]; + const lp_interval_t* x_interval = lp_interval_assignment_get_interval(m, x_lp); + if (x_interval != NULL) { + // something is inferred + ivector_push(inferred_vars, x_lp); + } + } +} + + lp_variable_t poly_constraint_get_top_variable(const poly_constraint_t* cstr) { return lp_polynomial_top_variable(cstr->polynomial); } @@ -552,9 +580,9 @@ const mcsat_value_t* poly_constraint_db_approximate(poly_constraint_db_t* db, va return NULL; } - // Construct the interval assignmetn - lp_interval_assignment_t m; - lp_interval_assignment_construct(&m, nra->lp_data.lp_var_db); + // Reset the interval assignment + lp_interval_assignment_t* m = nra->lp_data.lp_interval_assignment; + lp_interval_assignment_reset(m); // Setup the assignment x -> I(x) lp_variable_list_t vars; @@ -567,14 +595,14 @@ const mcsat_value_t* poly_constraint_db_approximate(poly_constraint_db_t* db, va lp_interval_t x_interval; lp_interval_construct_full(&x_interval); feasible_set_db_approximate_value(nra->feasible_set_db, x, &x_interval); - lp_interval_assignment_set_interval(&m, x_lp, &x_interval); + lp_interval_assignment_set_interval(m, x_lp, &x_interval); lp_interval_destruct(&x_interval); } // Evaluate the polynomial lp_interval_t value; lp_interval_construct_full(&value); - lp_polynomial_interval_value(cstr->polynomial, &m, &value); + lp_polynomial_interval_value(cstr->polynomial, m, &value); lp_sign_condition_t pos = cstr->sgn_condition; lp_sign_condition_t neg = lp_sign_condition_negate(cstr->sgn_condition); @@ -587,7 +615,6 @@ const mcsat_value_t* poly_constraint_db_approximate(poly_constraint_db_t* db, va // Remove temps lp_variable_list_destruct(&vars); - lp_interval_assignment_destruct(&m); return result; } diff --git a/src/mcsat/nra/poly_constraint.h b/src/mcsat/nra/poly_constraint.h index 6b6b638c4..145404727 100644 --- a/src/mcsat/nra/poly_constraint.h +++ b/src/mcsat/nra/poly_constraint.h @@ -52,6 +52,9 @@ void poly_constraint_print_mathematica(const poly_constraint_t* cstr, bool neage /** Get the feasible set of the constraint */ lp_feasibility_set_t* poly_constraint_get_feasible_set(const poly_constraint_t* cstr, const lp_assignment_t* m, bool negated); +/** Infer the bounds for this constraint (inferred_vars are lp_variables) */ +void poly_constraint_infer_bounds(const poly_constraint_t* cstr, bool negated, lp_interval_assignment_t* m, ivector_t* inferred_vars); + /** * Is this a valid constraint in the current order. */ diff --git a/tests/regress/mcsat/nra/hong_20.smt2 b/tests/regress/mcsat/nra/hong_20.smt2 new file mode 100644 index 000000000..ec7a2955e --- /dev/null +++ b/tests/regress/mcsat/nra/hong_20.smt2 @@ -0,0 +1,42 @@ +(set-info :smt-lib-version 2.6) +(set-logic QF_NRA) +(set-info :source |These benchmarks used in the paper: + + Dejan Jovanovic and Leonardo de Moura. Solving Non-Linear Arithmetic. + In IJCAR 2012, published as LNCS volume 7364, pp. 339--354. + +The hong family is a set of crafted benchmarks, a parametrized +generalization of the problem of Hong, sum x_i^2 < 1 and prod x_i > 1. +See: + + H. Hong. Comparison of several decision algorithms for the existential + theory of the reals. 1991. + +Submitted by Dejan Jovanvic for SMT-LIB. +|) +(set-info :category "crafted") +(set-info :status unsat) +(declare-fun x_0 () Real) +(declare-fun x_1 () Real) +(declare-fun x_2 () Real) +(declare-fun x_3 () Real) +(declare-fun x_4 () Real) +(declare-fun x_5 () Real) +(declare-fun x_6 () Real) +(declare-fun x_7 () Real) +(declare-fun x_8 () Real) +(declare-fun x_9 () Real) +(declare-fun x_10 () Real) +(declare-fun x_11 () Real) +(declare-fun x_12 () Real) +(declare-fun x_13 () Real) +(declare-fun x_14 () Real) +(declare-fun x_15 () Real) +(declare-fun x_16 () Real) +(declare-fun x_17 () Real) +(declare-fun x_18 () Real) +(declare-fun x_19 () Real) +(assert (< (+ (* x_0 x_0) (+ (* x_1 x_1) (+ (* x_2 x_2) (+ (* x_3 x_3) (+ (* x_4 x_4) (+ (* x_5 x_5) (+ (* x_6 x_6) (+ (* x_7 x_7) (+ (* x_8 x_8) (+ (* x_9 x_9) (+ (* x_10 x_10) (+ (* x_11 x_11) (+ (* x_12 x_12) (+ (* x_13 x_13) (+ (* x_14 x_14) (+ (* x_15 x_15) (+ (* x_16 x_16) (+ (* x_17 x_17) (+ (* x_18 x_18) (* x_19 x_19)))))))))))))))))))) 1)) +(assert (> (* x_0 (* x_1 (* x_2 (* x_3 (* x_4 (* x_5 (* x_6 (* x_7 (* x_8 (* x_9 (* x_10 (* x_11 (* x_12 (* x_13 (* x_14 (* x_15 (* x_16 (* x_17 (* x_18 x_19))))))))))))))))))) 1)) +(check-sat) +(exit) diff --git a/tests/regress/mcsat/nra/hong_20.smt2.gold b/tests/regress/mcsat/nra/hong_20.smt2.gold new file mode 100644 index 000000000..3f65111b0 --- /dev/null +++ b/tests/regress/mcsat/nra/hong_20.smt2.gold @@ -0,0 +1 @@ +unsat From 6155f749adb607daefbe0c0cafa77aee7d34dcf4 Mon Sep 17 00:00:00 2001 From: Dejan Jovanovic Date: Sat, 16 May 2020 13:00:01 -0400 Subject: [PATCH 07/16] get conflicts from inference k --- src/mcsat/nra/nra_plugin.c | 41 +++++++++++++++++++++------------ src/mcsat/nra/poly_constraint.c | 15 ++++++++---- src/mcsat/nra/poly_constraint.h | 4 ++-- 3 files changed, 38 insertions(+), 22 deletions(-) diff --git a/src/mcsat/nra/nra_plugin.c b/src/mcsat/nra/nra_plugin.c index b439f0c10..95ed431e0 100644 --- a/src/mcsat/nra/nra_plugin.c +++ b/src/mcsat/nra/nra_plugin.c @@ -709,24 +709,35 @@ void nra_plugin_infer_bounds_from_constraint(nra_plugin_t* nra, trail_token_t* p // Compute the bounds lp_interval_assignment_t* m = nra->lp_data.lp_interval_assignment; lp_interval_assignment_reset(m); - poly_constraint_infer_bounds(constraint, !trail_value, m, &lp_variables); - - // 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); + 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)); + } + + // 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); + delete_ivector(&lp_variables); + } } diff --git a/src/mcsat/nra/poly_constraint.c b/src/mcsat/nra/poly_constraint.c index 574a2d513..b6955f0e7 100644 --- a/src/mcsat/nra/poly_constraint.c +++ b/src/mcsat/nra/poly_constraint.c @@ -286,17 +286,20 @@ lp_feasibility_set_t* poly_constraint_get_feasible_set(const poly_constraint_t* return feasible; } -void poly_constraint_infer_bounds(const poly_constraint_t* cstr, bool negated, lp_interval_assignment_t* m, ivector_t* inferred_vars) { +bool poly_constraint_infer_bounds(const poly_constraint_t* cstr, bool negated, lp_interval_assignment_t* m, ivector_t* inferred_vars) { // TODO: is it possible to support root constraints if (poly_constraint_is_root_constraint(cstr)) { - return; + return false; } // Infer some bounds - bool something_inferred = lp_polynomial_constraint_infer_bounds(cstr->polynomial, cstr->sgn_condition, negated, m); - if (!something_inferred) { - return; + int inference_result = lp_polynomial_constraint_infer_bounds(cstr->polynomial, cstr->sgn_condition, negated, m); + if (inference_result == 0) { + return false; + } + if (inference_result == -1) { + return true; } lp_variable_list_t vars; @@ -311,6 +314,8 @@ void poly_constraint_infer_bounds(const poly_constraint_t* cstr, bool negated, l ivector_push(inferred_vars, x_lp); } } + + return false; } diff --git a/src/mcsat/nra/poly_constraint.h b/src/mcsat/nra/poly_constraint.h index 145404727..c12e2e7a4 100644 --- a/src/mcsat/nra/poly_constraint.h +++ b/src/mcsat/nra/poly_constraint.h @@ -52,8 +52,8 @@ void poly_constraint_print_mathematica(const poly_constraint_t* cstr, bool neage /** Get the feasible set of the constraint */ lp_feasibility_set_t* poly_constraint_get_feasible_set(const poly_constraint_t* cstr, const lp_assignment_t* m, bool negated); -/** Infer the bounds for this constraint (inferred_vars are lp_variables) */ -void poly_constraint_infer_bounds(const poly_constraint_t* cstr, bool negated, lp_interval_assignment_t* m, ivector_t* inferred_vars); +/** Infer the bounds for this constraint (inferred_vars are lp_variables). Returns true if conflict detected. */ +bool poly_constraint_infer_bounds(const poly_constraint_t* cstr, bool negated, lp_interval_assignment_t* m, ivector_t* inferred_vars); /** * Is this a valid constraint in the current order. From dd7bf35eeb0211e64617c2b6c228bf117bd1ee26 Mon Sep 17 00:00:00 2001 From: Dejan Jovanovic Date: Sat, 16 May 2020 13:31:19 -0400 Subject: [PATCH 08/16] ... --- src/mcsat/nra/nra_plugin.c | 1 + 1 file changed, 1 insertion(+) diff --git a/src/mcsat/nra/nra_plugin.c b/src/mcsat/nra/nra_plugin.c index 95ed431e0..85b83da6f 100644 --- a/src/mcsat/nra/nra_plugin.c +++ b/src/mcsat/nra/nra_plugin.c @@ -719,6 +719,7 @@ void nra_plugin_infer_bounds_from_constraint(nra_plugin_t* nra, trail_token_t* p 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 From 0871579425526a9b53bd8b47b97cc0a6a33ae1ca Mon Sep 17 00:00:00 2001 From: Dejan Jovanovic Date: Mon, 18 May 2020 13:17:32 -0400 Subject: [PATCH 09/16] use inference explain, test --- src/mcsat/nra/nra_plugin_explain.c | 16 +++++++++-- src/mcsat/nra/poly_constraint.c | 20 ++++++++++++++ src/mcsat/nra/poly_constraint.h | 3 +++ .../mcsat/nra/Chua-1-IL-L-chunk-0046.smt2 | 27 +++++++++++++++++++ .../nra/Chua-1-IL-L-chunk-0046.smt2.gold | 1 + 5 files changed, 65 insertions(+), 2 deletions(-) create mode 100644 tests/regress/mcsat/nra/Chua-1-IL-L-chunk-0046.smt2 create mode 100644 tests/regress/mcsat/nra/Chua-1-IL-L-chunk-0046.smt2.gold diff --git a/src/mcsat/nra/nra_plugin_explain.c b/src/mcsat/nra/nra_plugin_explain.c index 2eb7d9393..aed5c5434 100644 --- a/src/mcsat/nra/nra_plugin_explain.c +++ b/src/mcsat/nra/nra_plugin_explain.c @@ -1027,8 +1027,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 diff --git a/src/mcsat/nra/poly_constraint.c b/src/mcsat/nra/poly_constraint.c index b6955f0e7..a6b4f8e8b 100644 --- a/src/mcsat/nra/poly_constraint.c +++ b/src/mcsat/nra/poly_constraint.c @@ -314,10 +314,30 @@ bool poly_constraint_infer_bounds(const poly_constraint_t* cstr, bool negated, l ivector_push(inferred_vars, x_lp); } } + lp_variable_list_destruct(&vars); return false; } +bool poly_constraint_is_unit(const poly_constraint_t* cstr, const lp_assignment_t* M) { + lp_variable_t x = lp_polynomial_top_variable(cstr->polynomial); + if (lp_assignment_get_value(M, x)->type != LP_VALUE_NONE) { + return false; + } + + lp_variable_list_t vars; + lp_variable_list_construct(&vars); + lp_polynomial_get_variables(cstr->polynomial, &vars); + uint32_t var_i; + for (var_i = 0; var_i < vars.list_size; ++ var_i) { + lp_variable_t x_lp = vars.list[var_i]; + if (x_lp != x && lp_assignment_get_value(M, x_lp)->type == LP_VALUE_NONE) { + return false; + } + } + + return true; +} lp_variable_t poly_constraint_get_top_variable(const poly_constraint_t* cstr) { return lp_polynomial_top_variable(cstr->polynomial); diff --git a/src/mcsat/nra/poly_constraint.h b/src/mcsat/nra/poly_constraint.h index c12e2e7a4..9d14fa622 100644 --- a/src/mcsat/nra/poly_constraint.h +++ b/src/mcsat/nra/poly_constraint.h @@ -86,6 +86,9 @@ lp_variable_t poly_constraint_get_variable(const poly_constraint_t* cstr); /** Get the root index (if a root constraint) */ uint32_t poly_constraint_get_root_index(const poly_constraint_t* cstr); +/** Check if the constraint is unit */ +bool poly_constraint_is_unit(const poly_constraint_t* cstr, const lp_assignment_t* M); + /** Construct the database */ void poly_constraint_db_construct(poly_constraint_db_t* db, nra_plugin_t* nra); diff --git a/tests/regress/mcsat/nra/Chua-1-IL-L-chunk-0046.smt2 b/tests/regress/mcsat/nra/Chua-1-IL-L-chunk-0046.smt2 new file mode 100644 index 000000000..d6ff916be --- /dev/null +++ b/tests/regress/mcsat/nra/Chua-1-IL-L-chunk-0046.smt2 @@ -0,0 +1,27 @@ +(set-info :smt-lib-version 2.6) +(set-logic QF_NRA) +(set-info :source | +These benchmarks used in the paper: + + Dejan Jovanovic and Leonardo de Moura. Solving Non-Linear Arithmetic. + In IJCAR 2012, published as LNCS volume 7364, pp. 339--354. + +The meti-tarski benchmarks are proof obligations extracted from the +Meti-Tarski project, see: + + B. Akbarpour and L. C. Paulson. MetiTarski: An automatic theorem prover + for real-valued special functions. Journal of Automated Reasoning, + 44(3):175-205, 2010. + +Submitted by Dejan Jovanovic for SMT-LIB. + + +|) +(set-info :category "industrial") +(set-info :status sat) +(declare-fun skoC () Real) +(declare-fun skoS () Real) +(declare-fun skoX () Real) +(assert (let ((?v_1 (<= skoX 0)) (?v_0 (* skoC (/ (- 235) 42)))) (and (<= skoS ?v_0) (and (not ?v_1) (and (or (<= ?v_0 skoS) ?v_1) (and (= (* skoS skoS) (+ 1 (* skoC (* skoC (- 1))))) (and (<= skoX 289) (<= 0 skoX)))))))) +(check-sat) +(exit) diff --git a/tests/regress/mcsat/nra/Chua-1-IL-L-chunk-0046.smt2.gold b/tests/regress/mcsat/nra/Chua-1-IL-L-chunk-0046.smt2.gold new file mode 100644 index 000000000..6b8a2c3d2 --- /dev/null +++ b/tests/regress/mcsat/nra/Chua-1-IL-L-chunk-0046.smt2.gold @@ -0,0 +1 @@ +sat From b981eb3ab211ffecf972e7c3df33f05b711a72a1 Mon Sep 17 00:00:00 2001 From: Dejan Jovanovic Date: Mon, 18 May 2020 13:32:08 -0400 Subject: [PATCH 10/16] leak --- src/mcsat/nra/poly_constraint.c | 1 + 1 file changed, 1 insertion(+) diff --git a/src/mcsat/nra/poly_constraint.c b/src/mcsat/nra/poly_constraint.c index a6b4f8e8b..e55b7c7a0 100644 --- a/src/mcsat/nra/poly_constraint.c +++ b/src/mcsat/nra/poly_constraint.c @@ -335,6 +335,7 @@ bool poly_constraint_is_unit(const poly_constraint_t* cstr, const lp_assignment_ return false; } } + lp_variable_list_destruct(&vars); return true; } From 30ea3e4925d80127d4a9691716bf2a9bfec78032 Mon Sep 17 00:00:00 2001 From: Dejan Jovanovic Date: Mon, 18 May 2020 13:33:27 -0400 Subject: [PATCH 11/16] leak --- src/mcsat/nra/poly_constraint.c | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/src/mcsat/nra/poly_constraint.c b/src/mcsat/nra/poly_constraint.c index e55b7c7a0..9b5cebc09 100644 --- a/src/mcsat/nra/poly_constraint.c +++ b/src/mcsat/nra/poly_constraint.c @@ -325,6 +325,8 @@ bool poly_constraint_is_unit(const poly_constraint_t* cstr, const lp_assignment_ return false; } + bool result = true; + lp_variable_list_t vars; lp_variable_list_construct(&vars); lp_polynomial_get_variables(cstr->polynomial, &vars); @@ -332,12 +334,13 @@ bool poly_constraint_is_unit(const poly_constraint_t* cstr, const lp_assignment_ for (var_i = 0; var_i < vars.list_size; ++ var_i) { lp_variable_t x_lp = vars.list[var_i]; if (x_lp != x && lp_assignment_get_value(M, x_lp)->type == LP_VALUE_NONE) { - return false; + result = false; + break; } } lp_variable_list_destruct(&vars); - return true; + return result; } lp_variable_t poly_constraint_get_top_variable(const poly_constraint_t* cstr) { From 828a1be0de4ca2e93e3f90ab083af09d5c74e8d4 Mon Sep 17 00:00:00 2001 From: Dejan Jovanovic Date: Mon, 18 May 2020 13:43:45 -0400 Subject: [PATCH 12/16] leak --- src/mcsat/nra/poly_constraint.c | 1 + 1 file changed, 1 insertion(+) diff --git a/src/mcsat/nra/poly_constraint.c b/src/mcsat/nra/poly_constraint.c index 9b5cebc09..14324f5f7 100644 --- a/src/mcsat/nra/poly_constraint.c +++ b/src/mcsat/nra/poly_constraint.c @@ -644,6 +644,7 @@ const mcsat_value_t* poly_constraint_db_approximate(poly_constraint_db_t* db, va // Remove temps lp_variable_list_destruct(&vars); + lp_interval_destruct(&value); return result; } From c828581d6864be93d8e7dccc03504ef1ff9f63d3 Mon Sep 17 00:00:00 2001 From: Dejan Jovanovic Date: Tue, 19 May 2020 16:22:14 -0400 Subject: [PATCH 13/16] report int conflict properly --- src/mcsat/nra/nra_plugin.c | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/src/mcsat/nra/nra_plugin.c b/src/mcsat/nra/nra_plugin.c index 85b83da6f..20d5576e3 100644 --- a/src/mcsat/nra/nra_plugin.c +++ b/src/mcsat/nra/nra_plugin.c @@ -752,11 +752,13 @@ void nra_plugin_process_unit_constraint(nra_plugin_t* nra, trail_token_t* prop, ctx_trace_term(nra->ctx, variable_db_get_term(nra->ctx->var_db, constraint_var)); } + const mcsat_trail_t* trail = nra->ctx->trail; + // Process if constraint is assigned, or an evaluation constraint bool is_eval_constraint = !variable_db_is_boolean(nra->ctx->var_db, constraint_var); - if (is_eval_constraint || trail_has_value(nra->ctx->trail, constraint_var)) { + if (is_eval_constraint || trail_has_value(trail, constraint_var)) { // Get the constraint value - bool constraint_value = is_eval_constraint || trail_get_value(nra->ctx->trail, constraint_var)->b; + bool constraint_value = is_eval_constraint || trail_get_value(trail, constraint_var)->b; // Get the constraint const poly_constraint_t* constraint = poly_constraint_db_get(nra->constraint_db, constraint_var); @@ -796,12 +798,12 @@ void nra_plugin_process_unit_constraint(nra_plugin_t* nra, trail_token_t* prop, lp_value_construct_none(&v); lp_feasibility_set_pick_value(feasible_set_db_get(nra->feasible_set_db, x), &v); if (!lp_value_is_integer(&v)) { - nra->conflict_variable_int = x; + nra_plugin_report_int_conflict(nra, prop, x); } lp_value_destruct(&v); } // If the value is implied at zero level, propagate it - if (!trail_has_value(nra->ctx->trail, x) && trail_is_at_base_level(nra->ctx->trail)) { + if (trail_is_consistent(trail) && trail_is_at_base_level(trail) && !trail_has_value(trail, x)) { const lp_feasibility_set_t* feasible = feasible_set_db_get(nra->feasible_set_db, x); if (lp_feasibility_set_is_point(feasible)) { lp_value_t x_value; From 41250658e129277cff7dd3234199fac09616be79 Mon Sep 17 00:00:00 2001 From: Dejan Jovanovic Date: Wed, 20 May 2020 16:26:04 -0400 Subject: [PATCH 14/16] Revert "report int conflict properly" This reverts commit c828581d6864be93d8e7dccc03504ef1ff9f63d3. --- src/mcsat/nra/nra_plugin.c | 10 ++++------ 1 file changed, 4 insertions(+), 6 deletions(-) diff --git a/src/mcsat/nra/nra_plugin.c b/src/mcsat/nra/nra_plugin.c index 20d5576e3..85b83da6f 100644 --- a/src/mcsat/nra/nra_plugin.c +++ b/src/mcsat/nra/nra_plugin.c @@ -752,13 +752,11 @@ void nra_plugin_process_unit_constraint(nra_plugin_t* nra, trail_token_t* prop, ctx_trace_term(nra->ctx, variable_db_get_term(nra->ctx->var_db, constraint_var)); } - const mcsat_trail_t* trail = nra->ctx->trail; - // Process if constraint is assigned, or an evaluation constraint bool is_eval_constraint = !variable_db_is_boolean(nra->ctx->var_db, constraint_var); - if (is_eval_constraint || trail_has_value(trail, constraint_var)) { + if (is_eval_constraint || trail_has_value(nra->ctx->trail, constraint_var)) { // Get the constraint value - bool constraint_value = is_eval_constraint || trail_get_value(trail, constraint_var)->b; + bool constraint_value = is_eval_constraint || trail_get_value(nra->ctx->trail, constraint_var)->b; // Get the constraint const poly_constraint_t* constraint = poly_constraint_db_get(nra->constraint_db, constraint_var); @@ -798,12 +796,12 @@ void nra_plugin_process_unit_constraint(nra_plugin_t* nra, trail_token_t* prop, lp_value_construct_none(&v); lp_feasibility_set_pick_value(feasible_set_db_get(nra->feasible_set_db, x), &v); if (!lp_value_is_integer(&v)) { - nra_plugin_report_int_conflict(nra, prop, x); + nra->conflict_variable_int = x; } lp_value_destruct(&v); } // If the value is implied at zero level, propagate it - if (trail_is_consistent(trail) && trail_is_at_base_level(trail) && !trail_has_value(trail, x)) { + if (!trail_has_value(nra->ctx->trail, x) && trail_is_at_base_level(nra->ctx->trail)) { const lp_feasibility_set_t* feasible = feasible_set_db_get(nra->feasible_set_db, x); if (lp_feasibility_set_is_point(feasible)) { lp_value_t x_value; From e25619a1fb0803f774fd4a72d0385e9a663fb8b5 Mon Sep 17 00:00:00 2001 From: Dejan Jovanovic Date: Thu, 21 May 2020 15:54:51 -0400 Subject: [PATCH 15/16] experiment with fourier motzkin --- src/mcsat/nra/nra_plugin_explain.c | 20 +++++++ src/mcsat/nra/poly_constraint.c | 87 ++++++++++++++++++++++++++++++ src/mcsat/nra/poly_constraint.h | 3 ++ 3 files changed, 110 insertions(+) diff --git a/src/mcsat/nra/nra_plugin_explain.c b/src/mcsat/nra/nra_plugin_explain.c index aed5c5434..1be59f0c2 100644 --- a/src/mcsat/nra/nra_plugin_explain.c +++ b/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 (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); diff --git a/src/mcsat/nra/poly_constraint.c b/src/mcsat/nra/poly_constraint.c index 14324f5f7..85b3b5fc4 100644 --- a/src/mcsat/nra/poly_constraint.c +++ b/src/mcsat/nra/poly_constraint.c @@ -26,6 +26,7 @@ #include #include #include +#include /** * A constraint of the form sgn(p(x)) = sgn_conition. @@ -319,6 +320,92 @@ bool poly_constraint_infer_bounds(const poly_constraint_t* cstr, bool negated, l return false; } +bool poly_constraint_resolve_fm(const poly_constraint_t* c0, bool c0_negated, const poly_constraint_t* c1, bool c1_negated, nra_plugin_t* nra, ivector_t* out) { + + lp_polynomial_context_t* ctx = nra->lp_data.lp_ctx; + lp_assignment_t* m = nra->lp_data.lp_assignment; + + if (poly_constraint_is_root_constraint(c0) || poly_constraint_is_root_constraint(c1)) { + return false; + } + + if (ctx_trace_enabled(nra->ctx, "mcsat::nra::explain")) { + ctx_trace_printf(nra->ctx, "c0 %s: ", c0_negated ? "(negated)" : ""); + poly_constraint_print(c0, ctx_trace_out(nra->ctx)); + ctx_trace_printf(nra->ctx, "\n"); + ctx_trace_printf(nra->ctx, "c1 %s: ", c1_negated ? "(negated)" : ""); + poly_constraint_print(c1, ctx_trace_out(nra->ctx)); + ctx_trace_printf(nra->ctx, "\n"); + } + + lp_polynomial_vector_t* assumptions = lp_polynomial_vector_new(ctx); + + lp_sign_condition_t R_sgn_condition; + lp_polynomial_t* R = lp_polynomial_new(ctx); + lp_sign_condition_t c0_sgn_condition = c0_negated ? lp_sign_condition_negate(c0->sgn_condition) : c0->sgn_condition; + lp_sign_condition_t c1_sgn_condition = c1_negated ? lp_sign_condition_negate(c1->sgn_condition) : c1->sgn_condition; + bool ok = lp_polynomial_constraint_resolve_fm(c0->polynomial, c0_sgn_condition, c1->polynomial, c1_sgn_condition, m, R, &R_sgn_condition, assumptions); + if (ok) { + // (C1 && C2 && assumptions && !(p R2 0)) => false + term_manager_t* tm = nra->ctx->tm; + size_t n = lp_polynomial_vector_size(assumptions); + size_t i; + for (i = 0; i < n; ++ i) { + lp_polynomial_t* assumption_p_i = lp_polynomial_vector_at(assumptions, i); + term_t assumption_i_p_term = lp_polynomial_to_yices_term(nra, assumption_p_i); + int assumption_i_p_sgn = lp_polynomial_sgn(assumption_p_i, m); + term_t assumption_i = NULL_TERM; + if (assumption_i_p_sgn < 0) { + assumption_i = mk_arith_term_lt0(tm, assumption_i_p_term); + } else if (assumption_i_p_sgn > 0) { + assumption_i = mk_arith_term_gt0(tm, assumption_i_p_term); + } else { + assumption_i = mk_arith_term_eq0(tm, assumption_i_p_term); + } + if (ctx_trace_enabled(nra->ctx, "mcsat::nra::explain")) { + ctx_trace_printf(nra->ctx, "adding FM assumption: "); + ctx_trace_term(nra->ctx, assumption_i); + } + ivector_push(out, assumption_i); + lp_polynomial_delete(assumption_p_i); + } + term_t R_p_term = lp_polynomial_to_yices_term(nra, R); + term_t R_term = NULL_TERM; + switch (R_sgn_condition) { + case LP_SGN_LT_0: + R_term = mk_arith_term_lt0(tm, R_p_term); + break; + case LP_SGN_LE_0: + R_term = mk_arith_term_leq0(tm, R_p_term); + break; + case LP_SGN_EQ_0: + R_term = mk_arith_term_eq0(tm, R_p_term); + break; + case LP_SGN_NE_0: + R_term = mk_arith_term_neq0(tm, R_p_term); + break; + case LP_SGN_GT_0: + R_term = mk_arith_term_gt0(tm, R_p_term); + break; + case LP_SGN_GE_0: + R_term = mk_arith_term_geq0(tm, R_p_term); + break; + } + R_term = opposite_term(R_term); + if (ctx_trace_enabled(nra->ctx, "mcsat::nra::explain")) { + ctx_trace_printf(nra->ctx, "adding resolvent: "); + ctx_trace_term(nra->ctx, R_term); + } + ivector_push(out, R_term); + } + + lp_polynomial_delete(R); + lp_polynomial_vector_delete(assumptions); + + return ok; +} + + bool poly_constraint_is_unit(const poly_constraint_t* cstr, const lp_assignment_t* M) { lp_variable_t x = lp_polynomial_top_variable(cstr->polynomial); if (lp_assignment_get_value(M, x)->type != LP_VALUE_NONE) { diff --git a/src/mcsat/nra/poly_constraint.h b/src/mcsat/nra/poly_constraint.h index 9d14fa622..d68cb2d91 100644 --- a/src/mcsat/nra/poly_constraint.h +++ b/src/mcsat/nra/poly_constraint.h @@ -89,6 +89,9 @@ uint32_t poly_constraint_get_root_index(const poly_constraint_t* cstr); /** Check if the constraint is unit */ bool poly_constraint_is_unit(const poly_constraint_t* cstr, const lp_assignment_t* M); +/** Try to resolve the two constraints with Fourier-Motzkin resolution */ +bool poly_constraint_resolve_fm(const poly_constraint_t* c0, bool c0_negated, const poly_constraint_t* c1, bool c1_negated, nra_plugin_t* nra, ivector_t* out); + /** Construct the database */ void poly_constraint_db_construct(poly_constraint_db_t* db, nra_plugin_t* nra); From 46bf35adb9201cf4cd5d25dba6d00c2bd7f59c00 Mon Sep 17 00:00:00 2001 From: Dejan Jovanovic Date: Sun, 24 May 2020 14:45:03 -0400 Subject: [PATCH 16/16] don't use FM until understood better --- src/mcsat/nra/nra_plugin_explain.c | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/mcsat/nra/nra_plugin_explain.c b/src/mcsat/nra/nra_plugin_explain.c index 1be59f0c2..7f6bcec65 100644 --- a/src/mcsat/nra/nra_plugin_explain.c +++ b/src/mcsat/nra/nra_plugin_explain.c @@ -1018,7 +1018,7 @@ void nra_plugin_explain_conflict(nra_plugin_t* nra, const int_mset_t* pos, const } // Check if there is a simple Fourier-Motzkin explanation - if (core->size == 2 && lemma_reasons->size == 0) { + 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);