From 9a62d989e60775f17f066eb93058f2c9e9781283 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Wed, 24 Jun 2015 16:27:32 +0100 Subject: [PATCH 01/28] Revert "Merge branch 'unstable' of https://github.com/Z3Prover/z3 into unstable" This reverts commit d3db21ccdefd20d293c1b9af66963faeafcd276f, reversing changes made to e463d5d899599fd3da87b765fd3e53261c8651d5. --- src/sat/sat_solver.h | 2 +- src/tactic/fpa/const_intro_rewriter.h | 150 -- src/tactic/fpa/fpa2bv_approx_tactic.cpp | 1313 ------------------ src/tactic/fpa/fpa2bv_approx_tactic.h | 33 - src/tactic/fpa/fpa2bv_converter_prec.cpp | 1594 ---------------------- src/tactic/fpa/fpa2bv_converter_prec.h | 103 -- src/tactic/fpa/fpa2bv_rewriter_prec.h | 261 ---- src/util/mpf.h | 2 +- 8 files changed, 2 insertions(+), 3456 deletions(-) delete mode 100644 src/tactic/fpa/const_intro_rewriter.h delete mode 100644 src/tactic/fpa/fpa2bv_approx_tactic.cpp delete mode 100644 src/tactic/fpa/fpa2bv_approx_tactic.h delete mode 100644 src/tactic/fpa/fpa2bv_converter_prec.cpp delete mode 100644 src/tactic/fpa/fpa2bv_converter_prec.h delete mode 100644 src/tactic/fpa/fpa2bv_rewriter_prec.h diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h index e3628823f..357b79f49 100644 --- a/src/sat/sat_solver.h +++ b/src/sat/sat_solver.h @@ -210,7 +210,6 @@ namespace sat { public: bool inconsistent() const { return m_inconsistent; } unsigned num_vars() const { return m_level.size(); } - unsigned num_clauses() const; bool is_external(bool_var v) const { return m_external[v] != 0; } bool was_eliminated(bool_var v) const { return m_eliminated[v] != 0; } unsigned scope_lvl() const { return m_scope_lvl; } @@ -448,6 +447,7 @@ namespace sat { protected: void display_binary(std::ostream & out) const; void display_units(std::ostream & out) const; + unsigned num_clauses() const; bool is_unit(clause const & c) const; bool is_empty(clause const & c) const; bool check_missed_propagation(clause_vector const & cs) const; diff --git a/src/tactic/fpa/const_intro_rewriter.h b/src/tactic/fpa/const_intro_rewriter.h deleted file mode 100644 index 5c4675fbb..000000000 --- a/src/tactic/fpa/const_intro_rewriter.h +++ /dev/null @@ -1,150 +0,0 @@ -/*++ -Copyright (c) 2012 Microsoft Corporation - -Module Name: - - const_intro_rewriter.h - -Abstract: - - Rewriter for converting FPA to BV - -Author: - - Christoph (cwinter) 2012-02-09 - -Notes: - ---*/ - -#ifndef _CONST_INTRO_REWRITER_H_ -#define _CONST_INTRO_REWRITER_H_ - -#include"cooperate.h" -#include"bv_decl_plugin.h" -#include"tactic_exception.h" -#include"fpa2bv_converter_prec.h" - -struct const_intro_rewriter_cfg : public default_rewriter_cfg { - ast_manager & m_manager; - - expr * m_exp; - func_decl_ref_vector m_introduced_consts; - obj_map m_const2term_map; - - unsigned long long m_max_memory; - unsigned m_max_steps; - - fpa_util m_float_util; - - ast_manager & m() const { return m_manager; } - - const_intro_rewriter_cfg(ast_manager & m, params_ref const & p): - m_manager(m), - m_introduced_consts(m), - m_float_util(m) { - updt_params(p); - // We need to make sure that the mananger has the BV plugin loaded. - symbol s_bv("bv"); - if (!m_manager.has_plugin(s_bv)) - m_manager.register_plugin(s_bv, alloc(bv_decl_plugin)); - } - - ~const_intro_rewriter_cfg() { - for (obj_map::iterator it = m_const2term_map.begin(); - it != m_const2term_map.end(); - it++) - { - m().dec_ref(it->m_key); - m().dec_ref(it->m_value); - } - } - - void cleanup_buffers() { - } - - void updt_params(params_ref const & p) { - m_max_memory = megabytes_to_bytes(p.get_uint("max_memory", UINT_MAX)); - m_max_steps = p.get_uint("max_steps", UINT_MAX); - } - - bool max_steps_exceeded(unsigned num_steps) const { - cooperate("fpa2bv"); - if (memory::get_allocation_size() > m_max_memory) - throw tactic_exception(TACTIC_MAX_MEMORY_MSG); - return num_steps > m_max_steps; - } - - br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) { - TRACE("fpa2bv_rw", tout << "APP: " << f->get_name() << std::endl; ); - - if (num == 0 && f->get_family_id() == null_family_id && m_float_util.is_float(f->get_range())) { - app * f_cnst = m_manager.mk_const(f); - if (!m_introduced_consts.contains(f)) - m_introduced_consts.push_back(f); - result = f_cnst; - return BR_DONE; - } - - if (f->get_family_id() == m_float_util.get_family_id()) { - switch (f->get_decl_kind()) { - case OP_FPA_ADD: - case OP_FPA_SUB: - case OP_FPA_NEG: - case OP_FPA_MUL: - case OP_FPA_DIV: - case OP_FPA_REM: - case OP_FPA_ABS: - case OP_FPA_MIN: - case OP_FPA_MAX: - case OP_FPA_FMA: - case OP_FPA_SQRT: - case OP_FPA_TO_FP: - case OP_FPA_ROUND_TO_INTEGRAL: - { - app * f_app = m_manager.mk_app(f, num, args); - result = m_manager.mk_fresh_const(NULL, f->get_range()); - func_decl * fd = to_app(result)->get_decl(); - m_introduced_consts.push_back(fd); - m_const2term_map.insert_if_not_there(fd, f_app); - m().inc_ref(fd); - m().inc_ref(f_app); - return BR_DONE; - } - default: - return BR_FAILED; - } - } - - return BR_FAILED; - } - - bool reduce_quantifier(quantifier * old_q, - expr * new_body, - expr * const * new_patterns, - expr * const * new_no_patterns, - expr_ref & result, - proof_ref & result_pr) { - return false; - } - - bool reduce_var(var * t, expr_ref & result, proof_ref & result_pr) { - return false; - } - - bool pre_visit(expr * t){ - return true; - } -}; - -template class rewriter_tpl; - -struct const_intro_rewriter : public rewriter_tpl { - const_intro_rewriter_cfg m_cfg; - const_intro_rewriter(ast_manager & m, params_ref const & p): - rewriter_tpl(m, m.proofs_enabled(), m_cfg), - m_cfg(m, p) { - } -}; - -#endif diff --git a/src/tactic/fpa/fpa2bv_approx_tactic.cpp b/src/tactic/fpa/fpa2bv_approx_tactic.cpp deleted file mode 100644 index 4d52a11ca..000000000 --- a/src/tactic/fpa/fpa2bv_approx_tactic.cpp +++ /dev/null @@ -1,1313 +0,0 @@ -/*++ - Copyright (c) 2012 Microsoft Corporation - - Module Name: - - fpa2bv_approx_tactic.cpp - - Abstract: - - Tactic that converts floating points to bit-vectors lazily - - Author: - - Aleksander Zeljic 2012-11-15 - - Notes: - - --*/ -#include"tactical.h" -#include"cooperate.h" -#include"ref_util.h" - -#include"th_rewriter.h" -#include"bit_blaster_rewriter.h" -#include"bit_blaster_model_converter.h" -#include"model_v2_pp.h" -#include"goal2sat.h" -#include"sat_solver.h" -#include"fpa_decl_plugin.h" -#include"fpa2bv_converter_prec.h" -#include"fpa2bv_model_converter.h" -#include"fpa2bv_converter.h" -#include"propagate_values_tactic.h" -#include"fpa2bv_rewriter_prec.h" -#include"fpa2bv_approx_tactic.h" -#include"const_intro_rewriter.h" -#include"ctx_simplify_tactic.h" -#include"filter_model_converter.h" -#include -#include -#include - -#include - -#define K_MIN 10 -#define K_PERCENTAGE 0.3 -#define PREC_INCREMENT 20 -#define ERR_OP 0 // - -struct pair -{ - expr * exp; - double quotient;// mpf * -}; - -bool isinfinite(double x) { -#ifdef _WIN32 - int c = _fpclass(x); - return c == _FPCLASS_PINF || c == _FPCLASS_NINF; -#else - return fpclassify(x) == FP_INFINITE; -#endif -} - -class fpa2bv_approx_tactic: public tactic { - struct imp { - ast_manager & m; - goal2sat m_goal2sat; - sat2goal m_sat2goal; - params_ref m_params; - unsigned m_num_steps; - bool m_proofs_enabled; - bool m_produce_models; - bool m_produce_unsat_cores; - bool m_cancel; - - fpa_approximation_mode m_mode; - ast_manager * m_temp_manager; - model_ref m_fpa_model; - fpa_util m_float_util; - - imp(ast_manager & _m, params_ref const & p, fpa_approximation_mode mode) : - m(_m), - m_params(p), - m_proofs_enabled(false), - m_produce_models(false), - m_produce_unsat_cores(false), - m_cancel(false), - m_mode(mode), - m_temp_manager(0), - m_float_util(_m) { - } - - void updt_params(params_ref const & p) { - m_params = p; - } - - void set_cancel(bool f) { - //If f is true stop everything - m_cancel = f; - } - - void init_precision_mapping(func_decl_ref_vector const & cnsts, - obj_map & map, - obj_map & const2term_map) { - for (unsigned i = 0; i < cnsts.size(); i++) - { - if (const2term_map.contains(cnsts.get(i)) || m_mode == FPAA_SMALL_FLOATS) - map.insert_if_not_there(cnsts.get(i), 0); - else - map.insert_if_not_there(cnsts.get(i), MAX_PRECISION); - } - } - - bool proof_guided_refinement( - goal_ref const & g, - func_decl_ref_vector const & cnsts, - obj_map & cnst2prec_map, - obj_map & new_map) - { - // We have no model. Let's just increase precision of everything. - bool res = false; - for (unsigned i = 0; i < cnsts.size(); i++) - { - unsigned old = cnst2prec_map.find(cnsts.get(i)); - unsigned n = old + PREC_INCREMENT; - if (old >= MAX_PRECISION) n = MAX_PRECISION; - else { if (n > MAX_PRECISION) n = MAX_PRECISION; res = true; } - new_map.insert(cnsts.get(i), n); - } - return res; - } - - void boolean_comparison_of_models(goal_ref g, model_ref const & mdl, model_ref const & full_mdl, obj_map & cnst2term_map, obj_map& count) - { - std::queue to_traverse; - app * cur; - int cur_cnt; - - expr_ref mdl_eval(m), full_eval(m); - - for (unsigned i=0; i < g->size(); i++){ - mdl->eval(g->form(i),mdl_eval,true); - full_mdl->eval(g->form(i),full_eval,true); - - //Push only if the full model evaluates to false, or if the models differ? - if (!m.is_true(full_eval)) // m.is_true(full_eval) != m.is_true(mdl_eval) - to_traverse.push(g->form(i)); - } - - while (to_traverse.size() > 0) { - cur = to_app(to_traverse.front()); -#ifdef Z3DEBUG - std::cout<<"Analyze - traversing: "<get_decl())) - count.insert(cur,1); - - if(cnst2term_map.contains(cur->get_decl())) - to_traverse.push(cnst2term_map.find(cur->get_decl())); - - for(unsigned i=0;iget_num_args();i++) { - if(m_float_util.is_rm(cur->get_arg(i)) || m_float_util.is_numeral(cur->get_arg(i))) - continue; - to_traverse.push(cur->get_arg(i)); - } - } - else { //Comparing boolean values from the model and the expanded model - mdl->eval(cur,mdl_eval,true); - full_mdl->eval(cur,full_eval,true); - - - if (m.is_true(full_eval) != m.is_true(mdl_eval)) { - //queue arguments - for(unsigned i=0; i < cur->get_num_args(); i++) - to_traverse.push(cur->get_arg(i)); - } - } - to_traverse.pop(); - } -#ifdef Z3DEBUG - std::cout<<"Expression count"<::iterator it = count.begin(); - it!= count.end(); - it++) { - std::cout<m_key,m)<<":"<m_value<size();i++) { - eq = to_app(g->form(i)); - - if (eq->get_family_id() == m.get_basic_family_id() && - eq->get_decl_kind() == OP_EQ){ - //eq is in fact an equality - app * lhs = to_app(eq->get_arg(0)); - app * rhs = to_app(eq->get_arg(1)); - expr * lhs_e,*rhs_e,*exp, *exp_e; - app *other = NULL; - - - if(lhs->get_num_args()==0 && - rhs ->get_num_args()==0){ - //over constants - lhs_e = full_mdl->get_const_interp(lhs->get_decl()); - rhs_e = full_mdl->get_const_interp(rhs->get_decl()); - - // != would work as well, to make sure they are not both NULL, - //and could simplify later checks - if(lhs_e != rhs_e) { //SASSERT(lhs_e || rhs_e); - //and one is registered in the full model while the other is not - if(!lhs_e){// && rhs_e){ - other = lhs; - exp_e = rhs_e; - exp = rhs; - } - else { // if(!rhs_e && lhs_e){ - other = rhs; - exp_e = lhs_e; - exp = lhs; - } - full_mdl->register_decl(other->get_decl(),exp_e); - -#ifdef Z3DEBUG - std::cout< & cnst2term_map, - obj_map & precise_op, - obj_map & actual_value, - obj_map & err_est, - mpf_rounding_mode & rm, - bool & precise_children, - bool & seen_all_children, - bool & children_have_finite_err, - mpf * arg_val, - mpf * est_arg_val - //expr_ref * arg_e - ){ - - expr_ref arg_e[] = { expr_ref(m), expr_ref(m), expr_ref(m), expr_ref(m) }; - unsigned i=0; - //Set rounding mode - if (rhs->get_num_args() > 0 && m_float_util.is_rm(rhs->get_arg(0))) { - expr_ref rm_val(m); - mdl->eval(rhs->get_arg(0), rm_val, true); - m_float_util.is_rm_numeral(rm_val, rm); - i = 1; - } - //Collect argument values - for (; i < rhs->get_num_args(); i++) { - expr * arg = rhs->get_arg(i); - - if (is_app(arg) && to_app(arg)->get_num_args() == 0) { - if (precise_op.contains(arg)) { - precise_children &= precise_op.find(arg); - } - else if (!cnst2term_map.contains(to_app(arg)->get_decl())) { - /* that's okay */ - } - else { -#ifdef Z3DEBUG - std::cout << "Not seen all children of " << mk_ismt2_pp(rhs, m) << - " (spec. " << mk_ismt2_pp(arg, m) << ")" << std::endl; -#endif - precise_children = false; - seen_all_children = false; - break; - } - } - - // Value from small model - mdl->eval(arg, arg_e[i],true); - m_float_util.is_numeral(arg_e[i], arg_val[i]); - - if( children_have_finite_err && - err_est.contains(arg) && - isinfinite(err_est.find(arg))) - children_have_finite_err=false; - - if (actual_value.contains(arg)) - mpf_mngr.set(est_arg_val[i], *actual_value.find(arg)); - else if (seen_all_children && is_app(arg) && to_app(arg)->get_num_args()==0) { - //We have seen all children so if it is a constant and not in actual_value then - //it is an input variable and its est_val is the same as actual value - mpf * tmp = alloc(mpf); - mpf_mngr.set(*tmp, arg_val[i]); - actual_value.insert(arg, tmp); - mpf_mngr.set(est_arg_val[i], *tmp); - } - else - std::cout << "Estimated value missing: " << mk_ismt2_pp(arg,m) << std::endl; - } - - } - - - void full_semantics_eval( - app * rhs, - mpf_manager & mpf_mngr, - mpf_rounding_mode & rm, - mpf * arg_val, - mpf * est_arg_val, - mpf & rhs_value, - mpf & est_rhs_value){ - - switch (rhs->get_decl()->get_decl_kind()) { - case OP_FPA_ADD: - mpf_mngr.add(rm, arg_val[1], arg_val[2], rhs_value); - mpf_mngr.add(rm, est_arg_val[1], est_arg_val[2], est_rhs_value); - break; - case OP_FPA_SUB: - mpf_mngr.sub(rm, arg_val[1], arg_val[2], rhs_value); - mpf_mngr.sub(rm, est_arg_val[1], est_arg_val[2], est_rhs_value); - break; - case OP_FPA_NEG: - mpf_mngr.neg(arg_val[0], rhs_value); - mpf_mngr.neg(est_arg_val[0], est_rhs_value);//Does it even make sense to look at this? - break; - case OP_FPA_MUL: - mpf_mngr.mul(rm, arg_val[1], arg_val[2], rhs_value); - mpf_mngr.mul(rm, est_arg_val[1], est_arg_val[2], est_rhs_value); - break; - case OP_FPA_DIV: - mpf_mngr.div(rm, arg_val[1], arg_val[2], rhs_value); - mpf_mngr.div(rm, est_arg_val[1], est_arg_val[2], est_rhs_value); - break; - case OP_FPA_REM: - mpf_mngr.rem(arg_val[0], arg_val[1], rhs_value); - mpf_mngr.rem(est_arg_val[0], est_arg_val[1], est_rhs_value); - break; - case OP_FPA_FMA: - mpf_mngr.fused_mul_add(rm, arg_val[1], arg_val[2], arg_val[3], rhs_value); - mpf_mngr.fused_mul_add(rm, est_arg_val[1], est_arg_val[2], est_arg_val[3], est_rhs_value); - break; - case OP_FPA_SQRT: - mpf_mngr.sqrt(rm, arg_val[1], rhs_value); - mpf_mngr.sqrt(rm, est_arg_val[1], est_rhs_value); - break; - case OP_FPA_TO_FP: - { - unsigned ebits = rhs->get_decl()->get_parameter(0).get_int(); - unsigned sbits = rhs->get_decl()->get_parameter(1).get_int(); - mpf_mngr.set(rhs_value, ebits, sbits, rm, arg_val[1]); - mpf_mngr.set(est_rhs_value, ebits, sbits, rm, est_arg_val[1]); - break; - } - case OP_FPA_ABS: - { - mpf_mngr.abs(arg_val[0], rhs_value); - mpf_mngr.abs(est_arg_val[0], est_rhs_value); - break; - } - case OP_FPA_MIN: - { - mpf_mngr.minimum( arg_val[1], arg_val[2], rhs_value); - mpf_mngr.minimum( est_arg_val[1], est_arg_val[2], est_rhs_value); - break; - } - case OP_FPA_MAX: - { - mpf_mngr.maximum( arg_val[1], arg_val[2], rhs_value); - mpf_mngr.maximum( est_arg_val[1], est_arg_val[2], est_rhs_value); - break; - } - case OP_FPA_ROUND_TO_INTEGRAL: - { - mpf_mngr.round_to_integral(rm,arg_val[1],rhs_value); - mpf_mngr.round_to_integral(rm,est_arg_val[1],est_rhs_value); - break; - } - - default: - NOT_IMPLEMENTED_YET(); - break; - } - - } - - void evaluate_constant( - app * rhs, - model_ref const & mdl, - mpf_manager & mpf_mngr, - obj_map & actual_value, - mpf & rhs_value, - mpf & est_rhs_value){ - - expr_ref exp(m); - mdl->eval(rhs, exp, true); - m_float_util.is_numeral(exp, rhs_value); //OLD:is_value - - if (actual_value.contains(rhs)) - mpf_mngr.set(est_rhs_value, *actual_value.find(rhs)); - else { - mpf * tmp = alloc(mpf); - mpf_mngr.set(*tmp, rhs_value); - actual_value.insert(rhs, tmp); - mpf_mngr.set(est_rhs_value, rhs_value); - } - } - - void calculate_error( - expr_ref & lhs, - mpf_manager & mpf_mngr, - obj_map & precise_op, - obj_map & err_est, - mpf & lhs_value, - mpf & est_rhs_value, - bool children_have_finite_err){ - mpf err, rel_err; - if (!mpf_mngr.eq(lhs_value, est_rhs_value) && - !(mpf_mngr.is_nan(lhs_value) && mpf_mngr.is_nan(est_rhs_value))) { -#ifdef Z3DEBUG - std::cout << "Increasing precision of " << mk_ismt2_pp(lhs, m) << - " because " << mk_ismt2_pp(lhs, m) << " != " << - mpf_mngr.to_string(est_rhs_value) << std::endl; -#endif - //TODO: smarter adjustment to be implemented - precise_op.insert(lhs, false); - if (mpf_mngr.is_regular(lhs_value) && mpf_mngr.is_regular(est_rhs_value)) { - mpf_mngr.sub(MPF_ROUND_TOWARD_ZERO, est_rhs_value, lhs_value, err); - mpf_mngr.div(MPF_ROUND_TOWARD_ZERO, err, lhs_value, rel_err); - mpf_mngr.abs(rel_err); - } - else// One of the two is a special value; in this case the relative error is +INF - mpf_mngr.mk_pinf(11, 53, rel_err); - - if(children_have_finite_err) - err_est.insert(lhs, mpf_mngr.to_double(rel_err)); - -#ifdef Z3DEBUG - std::cout << "Error estimate: "<size(); j++) { - mdl->eval(g->form(j), res, true); - if (!m.is_true(res)) { - std::cout << "Failed: " << mk_ismt2_pp(g->form(j), m) << std::endl; - std::cout << "Evaluates to: " << mk_ismt2_pp(res, m) << std::endl; - is_model=false; - } - } - return is_model; - } - void evaluate_and_patch( - func_decl_ref_vector const & cnsts, - model_ref const & mdl, - model_ref & full_mdl, - goal_ref const & g, - obj_map & cnst2term_map, - obj_map & err_est) { - - mpf_manager & mpf_mngr = m_float_util.fm(); - expr_ref lhs(m), lhs_eval(m); - app * rhs; - mpf arg_val[4]; //First argument can be rounding mode - mpf est_arg_val[4]; - mpf lhs_value, rhs_value, est_rhs_value; - mpf_rounding_mode rm; - - mpf err, rel_err; - - - - obj_map precise_op; - obj_map actual_value; - while (precise_op.size() != cnst2term_map.size()) - for(unsigned i=0;ieval(lhs, lhs_eval, true); - - if (m_float_util.is_numeral(lhs_eval, lhs_value)) {//OLD:is_value - bool precise_children = true; - bool seen_all_children = true; - bool children_have_finite_err = true; - - obtain_values(rhs, mdl, full_mdl,mpf_mngr,cnst2term_map,precise_op,actual_value, - err_est, rm, precise_children, seen_all_children, children_have_finite_err, arg_val, est_arg_val ); - - - if (seen_all_children) {//If some arguments are not evaluated yet, skip - if (rhs->get_num_args() == 0) - evaluate_constant(rhs,mdl,mpf_mngr,actual_value, rhs_value, est_rhs_value); - else - full_semantics_eval(rhs,mpf_mngr,rm,arg_val,est_arg_val, rhs_value, est_rhs_value); - - if (mpf_mngr.eq(rhs_value, est_rhs_value)) { - full_mdl->register_decl((to_app(lhs))->get_decl(), m_float_util.mk_value(est_rhs_value)); - precise_op.insert(lhs, true); - } - else { - full_mdl->register_decl((to_app(lhs))->get_decl(), m_float_util.mk_value(est_rhs_value)); -#ifdef Z3DEBUG - std::cout << "Assigning " << mk_ismt2_pp(lhs, m) << - " value " << mpf_mngr.to_string(est_rhs_value) << std::endl - << "Values of " << mk_ismt2_pp(lhs, m) << std::endl - << "Precise children: " << ((precise_children) ? "True" : "False") << std::endl - << "Lhs: " << mk_ismt2_pp(lhs_eval, m) << std::endl - << "Model: " << mpf_mngr.to_string(rhs_value) << std::endl - << "Estimate: " << mpf_mngr.to_string(est_rhs_value) << std::endl; -#endif - - calculate_error(lhs,mpf_mngr,precise_op,err_est,lhs_value,est_rhs_value,children_have_finite_err); - - } - if (!actual_value.contains(lhs)) { - mpf * tmp = alloc(mpf); - mpf_mngr.set(*tmp, est_rhs_value); - actual_value.insert(lhs, tmp); - } - - if (!precise_children && !precise_op.contains(lhs)) { - std::cout << mk_ismt2_pp(lhs, m) << " is imprecise because some children are imprecise." << std::endl; - precise_op.insert(lhs, false); - } - } - } - } - - for (obj_map::iterator it = actual_value.begin(); - it != actual_value.end(); - it++) - mpf_mngr.del(*it->m_value); - - mpf_mngr.del(err); - mpf_mngr.del(rel_err); - mpf_mngr.del(lhs_value); - mpf_mngr.del(rhs_value); - mpf_mngr.del(est_rhs_value); - - for (unsigned i = 0; i < 4; i++) { - mpf_mngr.del(arg_val[i]); - mpf_mngr.del(est_arg_val[i]); - } - } - - bool precise_model_reconstruction( - model_ref const & mdl, - model_ref & full_mdl, - goal_ref const & g, - obj_map & err_est,//mpf* - func_decl_ref_vector const & cnsts, - obj_map & cnst2term_map) { -#ifdef Z3DEBUG - std::cout << "Attempting to patch small-float model" << std::endl; -#endif - expr_ref res(m); - bool is_model=true; - - //Evaluation of the model using full fpa semantics and construction of the full model - evaluate_and_patch(cnsts, mdl, full_mdl, g, cnst2term_map, err_est); - -#ifdef Z3DEBUG - std::cout<::iterator it = err_est.begin(); - it!= err_est.end(); it++) { - std::cout<m_key,m)<<":"<m_value<get_num_constants(); j++) { - if (!cnst2term_map.contains(mdl->get_constant(j)) - && !full_mdl->get_const_interp(mdl->get_constant(j))) { - mdl->eval(mdl->get_constant(j), res); - full_mdl->register_decl(mdl->get_constant(j), res); - } - } - - //Evaluate the full model - is_model = evaluate_model(g,full_mdl); - - return is_model; - } - - void calculate_relative_error( - obj_map & err_est, - obj_map & expr_count, - obj_map & err_ratio_map) { - unsigned num_args=0; - expr_ref exp(m); - double out_err,cur,err_ratio, avg_err; - - //AZ: Currently ignoring the expr_count, since it was blocking consideration of some expressions - for (obj_map::iterator it = err_est.begin(); - it != err_est.end(); - it++) { - // if any ancestor node has an error current node will be in expr_count. - /*if (!expr_count.contains(it->m_key)) - continue;*/ - - exp = it->m_key; - out_err = it->m_value; - num_args = to_app(exp)->get_num_args(); - - // Calculate average error of input params - avg_err = 0.0; - if (num_args > 0) { - for (unsigned i=0; iget_arg(i); - if (err_est.contains(arg)) { - cur = err_est.find(arg); - avg_err = avg_err + cur; - } - } - avg_err = avg_err/num_args; - } - // Relative error when input error exists, otherwise just output error - err_ratio = fabs((avg_err != (double) 0)? out_err / avg_err : out_err); - - if(expr_count.contains(exp)) { - if(ERR_OP) - err_ratio *= 1 + expr_count.find(exp); - else - err_ratio += expr_count.find(exp); - } - err_ratio_map.insert(exp, err_ratio); - } - - TRACE("fpa2bv_approx", - tout << "ERROR RATIO MAP: " << std::endl; - for (obj_map::iterator it = err_ratio_map.begin();// mpf* - it != err_ratio_map.end(); - it++) - tout << mk_ismt2_pp(it->m_key, m) << ": " <m_value<< std::endl; ); - - -#ifdef Z3DEBUG - std::cout<<"Error ratio:"<::iterator it = err_ratio_map.begin();//mpf* - it != err_ratio_map.end(); - it++) - std::cout<< mk_ismt2_pp(it->m_key, m) << ": " << it->m_value<< std::endl; - std::cout.flush(); -#endif - - } - - - void rank_terms(obj_map & err_ratio_map, std::list & ranked_terms) - { - unsigned kth = (unsigned)(err_ratio_map.size()*K_PERCENTAGE); - if (kth<10) kth=K_MIN; - SASSERT(!err_ratio_map.empty()); - - //Insertion sort the error ratios, keeping only the k highest elements - obj_map::iterator it = err_ratio_map.begin(); - struct pair * p = new struct pair(); - p->exp=it->m_key; - p->quotient=it->m_value; - ranked_terms.push_front(p); - - for (it++; it != err_ratio_map.end(); it++) { - if (ranked_terms.size()m_value >= ranked_terms.back()->quotient) { - std::list::iterator pos = ranked_terms.begin(); - while (pos!=ranked_terms.end() && it->m_value <= ranked_terms.back()->quotient) - pos++; - struct pair * p = new struct pair(); - p->exp=it->m_key; - p->quotient=it->m_value; - ranked_terms.insert(pos, p); - if (ranked_terms.size() > kth) { - delete ranked_terms.back(); - ranked_terms.pop_back(); - } - } - } - - } - - void increase_precision( - std::list & ranked_terms, - func_decl_ref_vector const & cnsts, - obj_map & cnst2prec_map, - obj_map & cnst2term_map, - obj_map & new_map){ - - //Refine chosen terms and find the any input 'variables' which are - //its immediate arguments and refine them as well -#ifdef Z3DEBUG - std::cout<<"Increasing precision:"<::iterator itp = ranked_terms.begin(); - itp != ranked_terms.end(); - itp++) { - app * cur = to_app((*itp)->exp); - func_decl * f = cur->get_decl(); - unsigned new_prec = PREC_INCREMENT, old_prec; - bool in_new_map; - - if (cnst2prec_map.contains(f)) - new_prec += cnst2prec_map.find(f); - - new_prec= (new_prec > MAX_PRECISION) ? MAX_PRECISION : new_prec; - new_map.insert(f, new_prec); - -#ifdef Z3DEBUG - std::cout << f->get_name() << ":" << new_prec << std::endl; - std::cout << mk_ismt2_pp(cur, m) << ":" << new_prec << std::endl; -#endif - - if(cnst2term_map.contains(f)) - cur = cnst2term_map.find(f); - // Refine constants that are direct arguments of this term - for(unsigned i=0; iget_num_args();i++){ - func_decl * arg_decl = to_app(cur->get_arg(i))->get_decl(); - if (!cnst2term_map.contains(arg_decl) && //Not a constant introduced by flattening - !m_float_util.is_rm(cur->get_arg(i)) && //OLD:is_rm(...,rm) - !m_float_util.is_numeral(cur->get_arg(i))) { //OLD:is_value - //It is an input 'variable' - if ( (in_new_map = new_map.contains(arg_decl))) - old_prec=new_map.find(arg_decl); - else if (cnst2prec_map.contains(arg_decl)) - old_prec = cnst2prec_map.find(arg_decl); - else - old_prec=0; - - if (old_prec < new_prec) { - if (in_new_map) - new_map.remove(arg_decl); - SASSERT(new_prec <= MAX_PRECISION); - new_map.insert(arg_decl, new_prec); - std::cout << " " << arg_decl->get_name() << ":" << new_prec << std::endl; -#ifdef Z3DEBUG - std::cout<<" "<get_arg(i),m)<<":"< & cnst2prec_map, - obj_map & cnst2term_map, - obj_map & err_est, - obj_map & new_map) { - - obj_map err_ratio_map; - obj_map expr_count; - std::list ranked_terms; - - boolean_comparison_of_models(g, mdl, full_mdl, cnst2term_map, expr_count); - calculate_relative_error(err_est, expr_count, err_ratio_map); - if (err_ratio_map.empty()) { - proof_guided_refinement(g,cnsts,cnst2prec_map,new_map); - } - else { - rank_terms (err_ratio_map,ranked_terms); - increase_precision(ranked_terms,cnsts,cnst2prec_map,cnst2term_map,new_map); - } - } - - void simplify(goal_ref mg) { - ast_manager &m = mg->m(); // CMW: <--- We use the manager of the goal, so this works for any manager. - expr_ref new_curr(m); - proof_ref new_pr(m); - - th_rewriter simplifier(m, m_params); - - // CMW: we need to eliminate AND expressions. - params_ref elim_and(m_params); - elim_and.set_bool("elim_and", true); - // elim_and.set_uint("max_depth", 1); // CMW: This number can have a big impact on performance, either way. - simplifier.updt_params(elim_and); - - SASSERT(mg->is_well_sorted()); - TRACE("before_simplifier", mg->display(tout);); - m_num_steps = 0; - if (mg->inconsistent()) - return; - for (unsigned idx = 0; idx < mg->size(); idx++) { - if (mg->inconsistent()) - break; - expr * curr = mg->form(idx); - simplifier(curr, new_curr, new_pr); - m_num_steps += simplifier.get_num_steps(); - if (mg->proofs_enabled()) { - proof * pr = mg->pr(idx); - new_pr = m.mk_modus_ponens(pr, new_pr); - } - mg->update(idx, new_curr, new_pr, mg->dep(idx)); - } - TRACE("after_simplifier_bug", mg->display(tout);); - mg->elim_redundancies(); - TRACE("after_simplifier", mg->display(tout);); - TRACE("after_simplifier_detail", mg->display_with_dependencies(tout);); - SASSERT(mg->is_well_sorted()); - } - - bool fully_encoded(obj_map const & precision_map) - { - for (obj_map::iterator it = precision_map.begin(); - it != precision_map.end(); - it++) - if (it->m_value < MAX_PRECISION) return false; - return true; - } - - void bitblast(goal_ref const & g, - fpa2bv_converter_prec & fpa2bv, - bit_blaster_rewriter & bv2bool, - obj_map & const2prec_map, - sat::solver & solver, - atom2bool_var & map) - { - // CMW: This is all done using the temporary manager! - expr_ref new_curr(*m_temp_manager); - proof_ref new_pr(*m_temp_manager); - std::cout.flush(); - - SASSERT(g->is_well_sorted()); - - simplify(g); - - //fpa2bv - fpa2bv_rewriter_prec fpa2bv_rw(*m_temp_manager, fpa2bv, m_params); - fpa2bv_rw.m_cfg.set_mappings(&const2prec_map); - m_num_steps = 0; - unsigned size = g->size(); - for (unsigned idx = 0; idx < size; idx++) { - if (g->inconsistent()) - break; - expr * curr = g->form(idx); -#ifdef Z3DEBUG - std::cout<pr(idx); - new_pr = m_temp_manager->mk_modus_ponens(pr, new_pr); - } - g->update(idx, new_curr, new_pr, g->dep(idx)); - - SASSERT(g->is_well_sorted()); - } - - //Adding the equalities that fix bits - for(unsigned i=0;iassert_expr(fpa2bv.m_extra_assertions.get(i)); - - SASSERT(g->is_well_sorted()); - - simplify(g); - - //Bitblasting - TRACE("before_bit_blaster", g->display(tout);); - m_num_steps = 0; - size = g->size(); - for (unsigned idx = 0; idx < size; idx++) { - if (g->inconsistent()) - break; - expr * curr = g->form(idx); - bv2bool(curr, new_curr, new_pr); - m_num_steps += bv2bool.get_num_steps(); - if (m_proofs_enabled) { - proof * pr = g->pr(idx); - new_pr = m_temp_manager->mk_modus_ponens(pr, new_pr); - } - g->update(idx, new_curr, new_pr, g->dep(idx)); - } - - g->inc_depth(); - - simplify(g); - - TRACE("before_sat_solver", g->display(tout);); - g->elim_redundancies(); - - goal2sat::dep2asm_map d2am ; - m_goal2sat(*g, m_params, solver, map, d2am , false); - - - TRACE("sat_solver_unknown", tout << "interpreted_atoms: " << map.interpreted_atoms() << "\n"; - atom2bool_var::iterator it = map.begin(); - atom2bool_var::iterator end = map.end(); - for (; it != end; ++it) { - if (!is_uninterp_const(it->m_key)) - tout << mk_ismt2_pp(it->m_key, *m_temp_manager) << "\n"; - }); - - CASSERT("sat_solver", solver.check_invariant()); - IF_VERBOSE(TACTIC_VERBOSITY_LVL, solver.display_status(verbose_stream());); - TRACE("sat_dimacs", solver.display_dimacs(tout);); - } - - model_ref get_fpa_model(goal_ref const & g, - fpa2bv_converter_prec & fpa2bv, - bit_blaster_rewriter & bv2bool, - sat::solver & solver, - atom2bool_var & map) { - // CMW: This is all done using the temporary manager, until at the very end we translate the model back to this->m. - model_ref md = alloc(model, *m_temp_manager); - sat::model const & ll_m = solver.get_model(); - TRACE("sat_tactic", for (unsigned i = 0; i < ll_m.size(); i++) - tout << i << ":" << ll_m[i] << " "; tout << "\n";); - atom2bool_var::iterator it = map.begin(); - atom2bool_var::iterator end = map.end(); - for (; it != end; ++it) { - expr * n = it->m_key; - sat::bool_var v = it->m_value; - if (is_app(n) && to_app(n)->get_decl()->get_arity() != 0) - continue; - TRACE("sat_tactic", tout << "extracting value of " << mk_ismt2_pp(n, *m_temp_manager) << "\nvar: " << v << "\n";); - switch (sat::value_at(v, ll_m)) { - case l_true: md->register_decl(to_app(n)->get_decl(), m_temp_manager->mk_true()); break; - case l_false: md->register_decl(to_app(n)->get_decl(), m_temp_manager->mk_false()); break; - default: - break; - } - } - - TRACE("sat_tactic", model_v2_pp(tout, *md);); - model_converter_ref bb_mc = mk_bit_blaster_model_converter(*m_temp_manager, bv2bool.const2bits()); - - model_converter_ref bv_mc = mk_fpa2bv_model_converter(*m_temp_manager, fpa2bv.const2bv(), fpa2bv.rm_const2bv(), fpa2bv.uf2bvuf(), fpa2bv.uf23bvuf()); - bb_mc->operator()(md, 0); - bv_mc->operator()(md, 0); - -#ifdef Z3DEBUG - std::cout << "Model: " << std::endl; - for (unsigned i = 0 ; i < md->get_num_constants(); i++) { - func_decl * d = md->get_constant(i); - std::cout << d->get_name() << " = " << mk_ismt2_pp(md->get_const_interp(d), *m_temp_manager) << std::endl; - } -#endif - // md is in terms of the temporary manager. - ast_translation translator(*m_temp_manager, this->m); - return md->translate(translator); - } - - void encode_fpa_terms( goal_ref const & g, - obj_map & const2term_map) - { - for (obj_map::iterator it = const2term_map.begin(); - it!=const2term_map.end(); - it++) { - expr_ref q(m); -#ifdef Z3DEBUG - std::cout << "Adding " << it->m_key->get_name() << " = " << mk_ismt2_pp(it->m_value, m) << std::endl; -#endif - q = m.mk_eq(m.mk_const(it->m_key), it->m_value); - g->assert_expr(q); - } - } - - lbool approximate_model_construction(goal_ref & g, obj_map & const2prec_map) { - lbool r = l_undef; - // CMW: The following will introduce lots of stuff that we don't need (e.g., symbols) - // To save memory, we use a separate, new manager that we can throw away afterwards. - m_temp_manager = alloc(ast_manager, PGM_DISABLED); - { - ast_translation translator(m, *m_temp_manager); - goal_ref ng = g->translate(translator); - obj_map const2prec_map_tm; - - for (obj_map::iterator it = const2prec_map.begin(); - it!=const2prec_map.end(); - it++) - const2prec_map_tm.insert(translator(it->m_key), it->m_value); - - sat::solver sat_solver(m_params, 0); - atom2bool_var atom_map(*m_temp_manager); - { tactic_report report_i("fpa2bv_approx_before_bitblaster", *ng); } - fpa2bv_converter_prec fpa2bv(*m_temp_manager, m_mode); - bit_blaster_rewriter bv2bool(*m_temp_manager, m_params); - bitblast(ng, fpa2bv, bv2bool, const2prec_map_tm, sat_solver, atom_map); - { tactic_report report_i("fpa2bv_approx_after_bitblaster", *ng); } - - std::cout << "Iteration variables: " << sat_solver.num_vars() << std::endl; - std::cout << "Iteration clauses: " << sat_solver.num_clauses() << std::endl; - r = sat_solver.check(); - - if (r == l_true) - { - // we need to get the model and translate it back to m. - m_fpa_model = get_fpa_model(ng, fpa2bv, bv2bool, sat_solver, atom_map).get(); - } - else - m_fpa_model = 0; - - // CMW: translator, etc, gets destroyed here, so all references - // to temporary expressions are gone. - } - - dealloc(m_temp_manager); - m_temp_manager = 0; - - return r; - } - - void lift( goal_ref const & g, func_decl_ref_vector & constants, obj_map * const2term_map ) - { - expr_ref new_new_curr(m); - expr_ref new_curr(m); - proof_ref new_pr(m); - - simplify(g); - - //Renaming subexpressions using new constants - const_intro_rewriter const_rewriter(m, m_params); - for (unsigned idx = 0; idx < g->size(); idx++) { - if (g->inconsistent()) - break; - expr * curr = g->form(idx); - const_rewriter(curr, new_curr, new_pr); //Introduces constants that replace subexpressions - m_num_steps += const_rewriter.get_num_steps(); - if (m_proofs_enabled) { - proof * pr = g->pr(idx); - new_pr = m.mk_modus_ponens(pr, new_pr); - } - g->update(idx, new_curr, new_pr, g->dep(idx)); - } - - - constants.set(const_rewriter.m_cfg.m_introduced_consts); - const2term_map->swap(const_rewriter.m_cfg.m_const2term_map); - - // Note: Ideally, we would directly encode them. For now we're lazy and just add equalities - // and we rely on fpa2bv_converter_prec to `magically' recognize the equalities we added. - { tactic_report report_i("fpa2bv_approx_before_fpa_terms", *(g.get())); } - encode_fpa_terms(g, *const2term_map); - SASSERT(g.get()->is_well_sorted()); - - - } - - void verify_precise_model( goal_ref const & g, - model_ref & full_mdl, - func_decl_ref_vector & constants, - obj_map & const2term_map, - model_converter_ref & mc, - goal_ref_buffer & result ){ - expr_ref res(m); - - for (unsigned j = 0; j < g->size(); j++) { - full_mdl->eval(g->form(j), res, true); - if (!m.is_true(res)) { - std::cout << "Failed: " << mk_ismt2_pp(g->form(j), m) << std::endl; - std::cout << "Evaluates to: " << mk_ismt2_pp(res, m) << std::endl; - } - SASSERT(m.is_true(res)); - } - - std::cout << "Full model: " << std::endl; - for (unsigned i = 0 ; i < full_mdl->get_num_decls(); i++) - { - func_decl * d = full_mdl->get_decl(i); - if(constants.contains(d)) - std::cout << d->get_name() << " = " << mk_ismt2_pp(full_mdl->get_const_interp(d), m) << std::endl; - } - std::cout.flush(); - - result.back()->reset(); - - // Filter all the constants we introduced earlier from the model. - filter_model_converter * fmc = alloc(filter_model_converter, m); - for (obj_map::iterator it = const2term_map.begin(); - it != const2term_map.end(); - it++) - fmc->insert(it->m_key); - mc = concat(fmc, model2model_converter(m_fpa_model.get())); - } - - void setup_options(goal_ref const & g){ - SASSERT(g->is_well_sorted()); - fail_if_proof_generation("fpa2bv_approx", g); - fail_if_unsat_core_generation("fpa2bv_approx", g); - m_proofs_enabled = g->proofs_enabled(); - m_produce_models = g->models_enabled(); - m_produce_unsat_cores = g->unsat_core_enabled(); - m_num_steps = 0; - } - - - - void print_constants(func_decl_ref_vector & constants, obj_map & const2prec_map){ -#ifdef Z3DEBUG - for(unsigned i=0;iget_name()<<":"< const2prec_map; - obj_map next_const2prec_map; - func_decl_ref_vector constants(m); - obj_map const2term_map; - lbool r = l_true; - unsigned iteration_cnt = 0; - stopwatch sw; - - tactic_report report("fpa2bv_approx", *g); - TRACE("fpa2bv_approx", tout << "BEFORE: " << std::endl; g->display(tout);); - result.reset(); - result.push_back(g.get()); - - SASSERT(g->is_well_sorted()); - if (g->inconsistent()) - return; - - lift(g, constants, &const2term_map); - - init_precision_mapping(constants, const2prec_map, const2term_map); - - std::cout << "Simplified goal:" << std::endl; - g->display(std::cout); - - while (!solved && !m_cancel) - { - std::cout << "=============== Starting iteration " << ++iteration_cnt << std::endl; - - sw.reset(); - sw.start(); - - // Copy the goal - goal_ref mg(alloc(goal, g->m(),g->proofs_enabled(),g->models_enabled(),g->unsat_core_enabled())); - mg->copy_from(*g.get()); - tactic_report report_i("fpa2bv_approx_i", *mg); - - print_constants(constants, const2prec_map); - - TRACE("fpa2bv_approx_goal_i", mg->display(tout); ); - - r = approximate_model_construction(mg, const2prec_map); - - std::cout << "Approximation is " << (r==l_true?"SAT":r==l_false?"UNSAT":"UNKNOWN") << std::endl; - - if (r == l_true) { - model_ref full_mdl = alloc(model, m); - obj_map err_est; - - if (fully_encoded(const2prec_map)) { - full_mdl = m_fpa_model; - solved = true; - std::cout<<"Model is at full precision, no patching needed!"< This is unsat. - solved = true; - result.back()->reset(); - result.back()->assert_expr(m.mk_false()); - } - } else { - // CMW: When the sat solver comes back with `unknown', what shall we do? - // AZ: Blindly refine? - m_cancel = true; - } - - const2prec_map.swap(next_const2prec_map); - next_const2prec_map.reset(); - std::cout << "Iteration time: " << sw.get_current_seconds() << std::endl; - } - - std::cout << "=============== Terminating " << std::endl; - dec_ref_map_key_values(m, const2term_map); - std::cout << "Iteration count: " << iteration_cnt << std::endl; - } - }; - - imp * m_imp; - params_ref m_params; - -public: - fpa2bv_approx_tactic(ast_manager & m, params_ref const & p) : - m_params(p){ - m_imp = alloc(imp, m, p, FPAA_DEFAULT_MODE); - } - - virtual tactic * translate(ast_manager & m) { - return alloc(fpa2bv_approx_tactic, m, m_params); - } - - virtual ~fpa2bv_approx_tactic() { - dealloc(m_imp); - } - - virtual void updt_params(params_ref const & p) { - m_params = p; - m_imp->updt_params(p); - } - - virtual void collect_param_descrs(param_descrs & r) { - } - - virtual void operator()(goal_ref const & in, goal_ref_buffer & result, - model_converter_ref & mc, proof_converter_ref & pc, - expr_dependency_ref & core) { - (*m_imp)(in, result, mc, pc, core); - } - - virtual void cleanup() { - ast_manager & m = m_imp->m; - imp * d = m_imp; -#pragma omp critical (tactic_cancel) - { - d = m_imp; - } - dealloc(d); - d = alloc(imp, m, m_params, FPAA_DEFAULT_MODE); -#pragma omp critical (tactic_cancel) - { - m_imp = d; - } - } - -protected: - virtual void set_cancel(bool f) { - if (m_imp) - m_imp->set_cancel(f); -} -}; - -tactic * mk_fpa2bv_approx_tactic(ast_manager & m, params_ref const & p) { - return and_then(clean(alloc(fpa2bv_approx_tactic, m, p)), mk_fail_if_undecided_tactic()); -} - - diff --git a/src/tactic/fpa/fpa2bv_approx_tactic.h b/src/tactic/fpa/fpa2bv_approx_tactic.h deleted file mode 100644 index 8838ca99d..000000000 --- a/src/tactic/fpa/fpa2bv_approx_tactic.h +++ /dev/null @@ -1,33 +0,0 @@ -/*++ -Copyright (c) 2012 Microsoft Corporation - -Module Name: - - fpa2bv_lazy_tactic.h - -Abstract: - - Tactic that converts floating points to bit-vectors lazily - -Author: - - Aleksander Zeljic 2012-11-15 - -Notes: - ---*/ -#ifndef _FPA2BV_APPROX_TACTIC_ -#define _FPA2BV_APPROX_TACTIC_ - -#include"params.h" -class ast_manager; -class tactic; - - - -tactic * mk_fpa2bv_approx_tactic(ast_manager & m, params_ref const & p = params_ref()); -/* - ADD_TACTIC("fpa2bv_approx", "An iterative approximation based bit-blasting decision procedure for FPA.", "mk_fpa2bv_approx_tactic(m, p)") -*/ - -#endif diff --git a/src/tactic/fpa/fpa2bv_converter_prec.cpp b/src/tactic/fpa/fpa2bv_converter_prec.cpp deleted file mode 100644 index 046511199..000000000 --- a/src/tactic/fpa/fpa2bv_converter_prec.cpp +++ /dev/null @@ -1,1594 +0,0 @@ -/*++ -Copyright (c) 2012 Microsoft Corporation - -Module Name: - - fpa2bv_converter_prec.cpp - -Abstract: - - Conversion routines for Floating Point -> Bit-Vector - -Author: - - Christoph (cwinter) 2012-02-09 - -Notes: - ---*/ -#include"ast_smt2_pp.h" -#include"well_sorted.h" -#include - -#include"fpa2bv_converter_prec.h" - -#define BVULT(X,Y,R) { expr_ref bvult_eq(m), bvult_not(m); m_simp.mk_eq(X, Y, bvult_eq); m_simp.mk_not(bvult_eq, bvult_not); expr_ref t(m); t = m_bv_util.mk_ule(X,Y); m_simp.mk_and(t, bvult_not, R); } -#define BVSLT(X,Y,R) { expr_ref bvslt_eq(m), bvslt_not(m); m_simp.mk_eq(X, Y, bvslt_eq); m_simp.mk_not(bvslt_eq, bvslt_not); expr_ref t(m); t = m_bv_util.mk_sle(X,Y); m_simp.mk_and(t, bvslt_not, R); } - -#define MIN_EBITS 3 -#define MIN_SBITS 3 - -fpa2bv_converter_prec::fpa2bv_converter_prec(ast_manager & m, fpa_approximation_mode mode) : - fpa2bv_converter(m), - m_mode(mode) { -} - -void fpa2bv_converter_prec::fix_bits(unsigned prec, expr_ref rounded, unsigned sbits, unsigned ebits)//expr_ref& fixed, -{ //AZ: TODO: revise! minimal number of legal bits is 3!!!! Remove magic numbers - unsigned szeroes = (unsigned) ((sbits-2)*(MAX_PRECISION - prec +0.0) / MAX_PRECISION);//3 bits are minimum for the significand - unsigned ezeroes = (unsigned) ((ebits - 2)*(MAX_PRECISION - prec + 0.0) / MAX_PRECISION);//2 bits are minimum for the exponent - - expr_ref fix_sig(m), fix_exp(m); - expr * sgn, *sig, *expn; - split_fp( rounded.get(), sgn,sig,expn); - if(ezeroes>0) { - fix_exp=m.mk_eq(m_bv_util.mk_extract(ebits-2, ebits - ezeroes -1, sig), m_bv_util.mk_numeral(0,ezeroes)); - m_extra_assertions.push_back(fix_exp); - SASSERT(is_well_sorted(m, fix_exp)); - } - - if(szeroes>0) { - fix_sig=m.mk_eq(m_bv_util.mk_extract(sbits-2, sbits - szeroes -1, sig), m_bv_util.mk_numeral(0,szeroes)); - m_extra_assertions.push_back(fix_sig); - SASSERT(is_well_sorted(m, fix_sig)); - } -} - -void fpa2bv_converter_prec::mk_const(func_decl * f, unsigned prec, expr_ref & result) { - switch (m_mode) { - case FPAA_SMALL_FLOATS: - { - if (m_const2bv.contains(f)) - result = m_const2bv.find(f); - else { - if (prec == MAX_PRECISION) - fpa2bv_converter::mk_const(f, result); - else { - unsigned ebits = fu().get_ebits(f->get_range()); - unsigned sbits = fu().get_sbits(f->get_range()); - double rel = prec/(double)MAX_PRECISION; - unsigned new_ebits = (unsigned) (rel * (double)ebits); - unsigned new_sbits = (unsigned) (rel * (double)sbits); - if (new_ebits < MIN_EBITS) new_ebits = MIN_EBITS; - if (new_sbits < MIN_SBITS) new_sbits = MIN_SBITS; - sort_ref ns(m), fp_srt(m); - ns = fu().mk_float_sort(new_ebits, new_sbits); - app_ref small_const(m); - small_const = m.mk_fresh_const("small_const", ns); - - fp_srt = fu().mk_float_sort(ebits, sbits); - symbol name("asFloat"); - sort_ref rm_sort(m); - rm_sort = fu().mk_rm_sort(); - //sort * domain[2] = { rm_sort, ns }; - //parameter parameters[2] = { parameter(ebits), parameter(sbits) }; - - fpa2bv_converter::mk_const(small_const->get_decl(), result); - m_const2bv.insert(f, result.get()); - m.inc_ref(f); - m.inc_ref(result.get()); -#ifdef Z3DEBUG - std::cout << f->get_name() << " := " << small_const->get_decl()->get_name() << - " [" << new_sbits<<","<get_name() << " := " << mk_ismt2_pp(result, m) << std::endl;); - } - } - break; - } - case FPAA_PRECISE: - case FPAA_FIXBITS: - fpa2bv_converter::mk_const(f, result); break; - default: - UNREACHABLE(); - break; - } -} -void fpa2bv_converter_prec::mk_small_op(func_decl * f, unsigned new_ebits, unsigned new_sbits, unsigned num, expr * const * args, func_decl_ref & small_op, expr_ref_vector & cast_args) -{ - if (new_ebits < MIN_EBITS) new_ebits = MIN_EBITS; - if (new_sbits < MIN_SBITS) new_sbits = MIN_SBITS; - sort_ref new_srt(m), rm_srt(m); - new_srt = fu().mk_float_sort(new_ebits, new_sbits); - rm_srt = fu().mk_rm_sort(); - - sort_ref_vector new_domain(m); - cast_args.reset(); - - for (unsigned i=0; i < num; i++) // Recreate the domain by replacing the full fpa sort with the smaller one. - { - sort * d_i = f->get_domain(i); - expr * a_i = args[i]; - - if (fu().is_rm(d_i)) - { - new_domain.push_back(rm_srt); - cast_args.push_back(a_i); - } - else if (fu().is_float(f->get_domain(i))) - { - sort * a_i_srt = to_app(a_i)->get_decl()->get_range(); - new_domain.push_back(new_srt); - - // Cast the corresponding argument to the right fpa size - if (is_app(a_i)) - { - if (a_i_srt == new_srt) - cast_args.push_back(a_i); - else { - app_ref rtz(m); - rtz = fu().mk_round_toward_zero(); - expr_ref rm(m); - fpa2bv_converter::mk_rounding_mode(rtz->get_decl(), rm); - - sort * d[2] = { rm_srt, a_i_srt }; - symbol name("asFloat"); - func_decl_ref fd(m); - fd = m.mk_func_decl(name, 2, d, new_srt, func_decl_info(fu().get_family_id(), OP_FPA_TO_FP, new_srt->get_num_parameters(), new_srt->get_parameters())); - - expr_ref t(m); - expr * args[2] = { rm, a_i }; - fpa2bv_converter::mk_to_fp(fd, 2, args, t); - cast_args.push_back(t); - SASSERT(is_well_sorted(m, t)); - } - } - else - NOT_IMPLEMENTED_YET(); - } - else - // just keep everything else - cast_args.push_back(a_i); - } - - parameter parameters[2] = { parameter(new_ebits), parameter(new_sbits) }; - - // May I reuse parts of the existing declaration? CMW: Sure. - - small_op = m.mk_func_decl(f->get_name(), num, new_domain.c_ptr(), new_srt, - func_decl_info(fu().get_family_id(), f->get_decl_kind(), 2, parameters)); - - //std::cout<get_name()<<"["<get_range()); - unsigned sbits = fu().get_sbits(f->get_range()); - double rel = prec/(double)MAX_PRECISION; - unsigned new_ebits = (unsigned) (rel * (double)ebits);// (unsigned) (MIN_EBITS + rel * (double)(ebits-MIN_EBITS)) - unsigned new_sbits = (unsigned) (rel * (double)sbits);// (unsigned) (MIN_SBITS + rel * (double)(sbits-MIN_SBITS)) - mk_small_op(f,new_ebits,new_sbits,num,args, small_op, cast_args); -} - -void fpa2bv_converter_prec::mk_cast_small_to_big(func_decl * f, expr * arg, expr_ref & result) { - unsigned ebits = fu().get_ebits(f->get_range()); - unsigned sbits = fu().get_sbits(f->get_range()); - - app_ref rtz(m); - rtz = fu().mk_round_toward_zero(); - expr_ref rm(m); - fpa2bv_converter::mk_rounding_mode(rtz->get_decl(), rm); - sort_ref rm_srt(m); - rm_srt = fu().mk_rm_sort(); - sort * d[2] = { rm_srt, to_app(arg)->get_decl()->get_range() }; - parameter parameters[2] = { parameter(ebits), parameter(sbits) }; - symbol name("asFloat"); - func_decl_ref cast_up(m); - cast_up = m.mk_func_decl(name, 2, d, f->get_range(), func_decl_info(fu().get_family_id(), OP_FPA_TO_FP, f->get_range()->get_num_parameters(), parameters)); - expr * args[2] = { rm, arg }; - fpa2bv_converter::mk_to_fp(cast_up, 2, args, result); -} - -void fpa2bv_converter_prec::mk_cast_small_to_big(unsigned sbits, unsigned ebits, expr * arg, expr_ref & result) { - app_ref rtz(m); - rtz = fu().mk_round_toward_zero(); - expr_ref rm(m); - fpa2bv_converter::mk_rounding_mode(rtz->get_decl(), rm); - sort_ref rm_srt(m); - rm_srt = fu().mk_rm_sort(); - sort * d[2] = { rm_srt, to_app(arg)->get_decl()->get_range() }; - parameter parameters[2] = { parameter(ebits), parameter(sbits) }; - symbol name("asFloat"); - func_decl_ref cast_up(m); - sort_ref ns(m); - ns = fu().mk_float_sort(ebits, sbits); - cast_up = m.mk_func_decl(name, 2, d, ns, func_decl_info(fu().get_family_id(), OP_FPA_TO_FP, 2, parameters)); - expr * args[2] = { rm, arg }; - fpa2bv_converter::mk_to_fp(cast_up, 2, args, result); -} - - -void fpa2bv_converter_prec::match_sorts(expr * a, expr * b, expr_ref & n_a, expr_ref & n_b) -{ - //Check if the sorts of lhs and rhs match, otherwise cast them to appropriate size? - SASSERT(is_app_of(a, m_plugin->get_family_id(), OP_FPA_FP)); - SASSERT(is_app_of(b, m_plugin->get_family_id(), OP_FPA_FP)); - func_decl * a_decl = to_app(a)->get_decl(); - func_decl * b_decl = to_app(b)->get_decl(); - - unsigned a_ebits = fu().get_ebits(a_decl->get_range()); - unsigned a_sbits = fu().get_sbits(a_decl->get_range()); - unsigned b_ebits = fu().get_ebits(b_decl->get_range()); - unsigned b_sbits = fu().get_sbits(b_decl->get_range()); - unsigned n_ebits, n_sbits; - - //if( (a_ebits == b_ebits) && (a_sbits == b_sbits)) - //{//No need for adjustment - n_a = a; - n_b = b; - //} - //else - //{ - if ((a_ebits <= b_ebits) && (a_sbits<= b_sbits)) - {//sort of b is wider than sort of a, we cast a to the sort of b. - mk_cast_small_to_big(b_sbits,b_ebits,a,n_a); - n_b = b; - } - else if ((a_ebits >= b_ebits) && (a_sbits >= b_sbits)) - { - n_a = a; - mk_cast_small_to_big(a_sbits,a_ebits,b,n_b); - } - else - { - n_ebits = (a_ebits < b_ebits)? b_ebits:a_ebits; - n_sbits = (a_sbits < b_sbits)? b_sbits:a_sbits; - mk_cast_small_to_big(n_sbits,n_ebits,a,n_a); - mk_cast_small_to_big(n_sbits,n_ebits,b,n_b); - } - //} -} -void fpa2bv_converter_prec::mk_eq(expr * a, expr * b, expr_ref & result) { - // This is structural equality, not floating point equality. - expr_ref na(m),nb(m); - match_sorts(a,b,na,nb); - fpa2bv_converter::mk_eq(na,nb,result); -} - -void fpa2bv_converter_prec::mk_ite(expr * c, expr * t, expr * f, expr_ref & result) { - expr_ref nt(m),nf(m); - match_sorts(t,f,nt,nf); - fpa2bv_converter::mk_ite(c,nt,nf,result); -} - - - -void fpa2bv_converter_prec::mk_add(func_decl * f, unsigned prec, unsigned num, expr * const * args, expr_ref & result) { - // AZ: Switch can be moved just before the call to the fix_bits method, everything else should be the same - switch (m_mode) { - case FPAA_PRECISE: - fpa2bv_converter::mk_add(f,num,args,result); - break; - case FPAA_SMALL_FLOATS: - { - func_decl_ref small_fd(m); - expr_ref_vector small_args(m); - mk_small_op(f, prec, num, args, small_fd, small_args); - //expr_ref small_op(m); - fpa2bv_converter::mk_add(small_fd, num, small_args.c_ptr(), result); - //mk_cast_small_to_big(f, small_op, result); - SASSERT(is_well_sorted(m, result)); - TRACE("fpa2bv_small_float_add", tout << "small_fd: " << mk_ismt2_pp(small_fd, m) << std::endl << - "result = " << mk_ismt2_pp(result, m) << std::endl; ); - break; - } - - case FPAA_FIXBITS: { - if (MAX_PRECISION == prec) - fpa2bv_converter::mk_add(f,num,args,result); - else{ - //Alternative encoding - /*func_decl * nf = & func_decl(f->get_name(), - f->get_arity(), - f->get_domain(), - f->get_range(), - f->get_info());*/ - - - SASSERT(num == 3); - - expr_ref rm(m), x(m), y(m); - rm = args[0]; - x = args[1]; - y = args[2]; - - expr_ref nan(m), nzero(m), pzero(m); - mk_nan(f, nan); - mk_nzero(f, nzero); - mk_pzero(f, pzero); - - expr_ref x_is_nan(m), x_is_zero(m), x_is_pos(m), x_is_neg(m), x_is_inf(m); - expr_ref y_is_nan(m), y_is_zero(m), y_is_pos(m), y_is_neg(m), y_is_inf(m); - mk_is_nan(x, x_is_nan); - mk_is_zero(x, x_is_zero); - mk_is_pos(x, x_is_pos); - mk_is_neg(x, x_is_neg); - mk_is_inf(x, x_is_inf); - mk_is_nan(y, y_is_nan); - mk_is_zero(y, y_is_zero); - mk_is_pos(y, y_is_pos); - mk_is_neg(y, y_is_neg); - mk_is_inf(y, y_is_inf); - - dbg_decouple("fpa2bv_add_x_is_nan", x_is_nan); - dbg_decouple("fpa2bv_add_x_is_zero", x_is_zero); - dbg_decouple("fpa2bv_add_x_is_pos", x_is_pos); - dbg_decouple("fpa2bv_add_x_is_neg", x_is_neg); - dbg_decouple("fpa2bv_add_x_is_inf", x_is_inf); - dbg_decouple("fpa2bv_add_y_is_nan", y_is_nan); - dbg_decouple("fpa2bv_add_y_is_zero", y_is_zero); - dbg_decouple("fpa2bv_add_y_is_pos", y_is_pos); - dbg_decouple("fpa2bv_add_y_is_neg", y_is_neg); - dbg_decouple("fpa2bv_add_y_is_inf", y_is_inf); - - expr_ref c1(m), c2(m), c3(m), c4(m), c5(m), c6(m); - expr_ref v1(m), v2(m), v3(m), v4(m), v5(m), v6(m), v7(m); - - m_simp.mk_or(x_is_nan, y_is_nan, c1); - v1 = nan; - - mk_is_inf(x, c2); - expr_ref nx(m), ny(m), nx_xor_ny(m), inf_xor(m); - mk_is_neg(x, nx); - mk_is_neg(y, ny); - m_simp.mk_xor(nx, ny, nx_xor_ny); - m_simp.mk_and(y_is_inf, nx_xor_ny, inf_xor); - mk_ite(inf_xor, nan, x, v2); - - mk_is_inf(y, c3); - expr_ref xy_is_neg(m), v3_and(m); - m_simp.mk_xor(x_is_neg, y_is_neg, xy_is_neg); - m_simp.mk_and(x_is_inf, xy_is_neg, v3_and); - mk_ite(v3_and, nan, y, v3); - - expr_ref rm_is_to_neg(m), signs_and(m), signs_xor(m), v4_and(m), rm_and_xor(m), neg_cond(m); - m_simp.mk_and(x_is_zero, y_is_zero, c4); - m_simp.mk_and(x_is_neg, y_is_neg, signs_and); - m_simp.mk_xor(x_is_neg, y_is_neg, signs_xor); - mk_is_rm(rm, BV_RM_TO_NEGATIVE, rm_is_to_neg); - m_simp.mk_and(rm_is_to_neg, signs_xor, rm_and_xor); - m_simp.mk_or(signs_and, rm_and_xor, neg_cond); - mk_ite(neg_cond, nzero, pzero, v4); - m_simp.mk_and(x_is_neg, y_is_neg, v4_and); - mk_ite(v4_and, x, v4, v4); - - c5 = x_is_zero; - v5 = y; - - c6 = y_is_zero; - v6 = x; - - // Actual addition. - unsigned ebits = m_util.get_ebits(f->get_range()); - unsigned sbits = m_util.get_sbits(f->get_range()); - - expr_ref a_sgn(m), a_sig(m), a_exp(m), a_lz(m), b_sgn(m), b_sig(m), b_exp(m), b_lz(m); - unpack(x, a_sgn, a_sig, a_exp, a_lz, false); - unpack(y, b_sgn, b_sig, b_exp, b_lz, false); - - dbg_decouple("fpa2bv_add_unpack_a_sgn", a_sgn); - dbg_decouple("fpa2bv_add_unpack_a_sig", a_sig); - dbg_decouple("fpa2bv_add_unpack_a_exp", a_exp); - dbg_decouple("fpa2bv_add_unpack_b_sgn", b_sgn); - dbg_decouple("fpa2bv_add_unpack_b_sig", b_sig); - dbg_decouple("fpa2bv_add_unpack_b_exp", b_exp); - - expr_ref swap_cond(m); - swap_cond = m_bv_util.mk_sle(a_exp, b_exp); - - expr_ref c_sgn(m), c_sig(m), c_exp(m), d_sgn(m), d_sig(m), d_exp(m); - m_simp.mk_ite(swap_cond, b_sgn, a_sgn, c_sgn); - m_simp.mk_ite(swap_cond, b_sig, a_sig, c_sig); // has sbits - m_simp.mk_ite(swap_cond, b_exp, a_exp, c_exp); // has ebits - m_simp.mk_ite(swap_cond, a_sgn, b_sgn, d_sgn); - m_simp.mk_ite(swap_cond, a_sig, b_sig, d_sig); // has sbits - m_simp.mk_ite(swap_cond, a_exp, b_exp, d_exp); // has ebits - - expr_ref res_sgn(m), res_sig(m), res_exp(m); - add_core(sbits, ebits, rm, - c_sgn, c_sig, c_exp, d_sgn, d_sig, d_exp, - res_sgn, res_sig, res_exp); - - //Add the fixed zeroes here...? - expr_ref sbits_zero(m), ebits_zero(m); - // std::cout<<"res_sgn: "<1) - // //Exponent = 1 bit for bias, fixed bits, actual exponent bits - // res_exp=m_bv_util.mk_concat(m_bv_util.mk_extract(ebits+1, ebits-1, res_exp), - // m_bv_util.mk_concat(m_bv_util.mk_numeral(0,ezeroes), - // m_bv_util.mk_extract(ebits - 2 - ezeroes, 0 ,res_exp))); - // if(sones>1) - // res_sig=m_bv_util.mk_concat(m_bv_util.mk_extract(sbits+3,sones+4,res_sig), - // m_bv_util.mk_concat(m_bv_util.mk_numeral(0,sones), - // m_bv_util.mk_extract(3,0,res_sig))); - // - // std::cout<<"res_sgn': "<get_range(), rm, res_sgn, res_sig, res_exp, rounded); - - - mk_ite(is_zero_sig, zero_case, rounded, v7);*/ - - - - expr_ref rounded(m);//, fixed(m); - round(f->get_range(), rm, res_sgn, res_sig, res_exp, rounded); - - fix_bits(prec, rounded, sbits,ebits); - mk_ite(is_zero_sig, zero_case, rounded, v7); - - // signed sones=((sbits-3)*(MAX_PRECISION - prec +0.0)/MAX_PRECISION);//3 bits are minimum for the significand - // unsigned ezeroes=((ebits-2)*(MAX_PRECISION - prec+0.0)/MAX_PRECISION);//2 bits are minimum for the exponent - // expr_ref fix_sig(m), fix_exp(m), fix_sgn(m), rnd_sig(m), rnd_exp(m), rnd_sgn(m), rnd_lz(m); - // expr * sgn, *sig, *expn; - // split( rounded.get(), sgn,sig,expn); - // - // - // if(ezeroes>1) - // //Exponent = 1 bit for bias, fixed bits, actual exponent bits - // fix_exp=m_bv_util.mk_concat(m_bv_util.mk_extract(ebits-1, ebits-1, expn), - // m_bv_util.mk_concat(m_bv_util.mk_numeral(0,ezeroes), - // m_bv_util.mk_extract(ebits - 2 - ezeroes, 0 , expn))); - // if(sones>1) - // fix_sig=m_bv_util.mk_concat(m_bv_util.mk_extract(sbits-2,sones,sig), - // m_bv_util.mk_numeral(0,sones)); - // - // mk_triple(sgn, fix_sig, fix_exp, fixed); - // SASSERT(is_well_sorted(m, fixed)); - //mk_ite(is_zero_sig, zero_case, rounded, v7); - - - - - mk_ite(c6, v6, v7, result); - mk_ite(c5, v5, result, result); - mk_ite(c4, v4, result, result); - mk_ite(c3, v3, result, result); - mk_ite(c2, v2, result, result); - mk_ite(c1, v1, result, result); - - SASSERT(is_well_sorted(m, result)); - - TRACE("fpa2bv_add", tout << "ADD = " << mk_ismt2_pp(result, m) << std::endl; ); - } - break; - } - default: UNREACHABLE(); break; - } -} - -void fpa2bv_converter_prec::mk_sub(func_decl * f, unsigned prec, unsigned num, expr * const * args, expr_ref & result) { - SASSERT(num == 3); - expr_ref t(m); - fpa2bv_converter::mk_neg(f, 1, &args[2], t); - expr * nargs[3] = { args[0], args[1], t }; - - switch (m_mode) { - case FPAA_PRECISE: - fpa2bv_converter::mk_add(f, 3, nargs, result); - break; - case FPAA_FIXBITS: // Call the add with prec - case FPAA_SMALL_FLOATS: - fpa2bv_converter_prec::mk_add(f, prec, 3, nargs, result); - break; - default: UNREACHABLE(); break; - } -} - -void fpa2bv_converter_prec::mk_uminus(func_decl * f, unsigned prec, unsigned num, expr * const * args, expr_ref & result) { - switch (m_mode) { - case FPAA_PRECISE: - case FPAA_SMALL_FLOATS: - case FPAA_FIXBITS: // for now, encode fully. - fpa2bv_converter::mk_neg(f,num,args,result); - break; - default: UNREACHABLE(); break; - } -} - -void fpa2bv_converter_prec::mk_mul(func_decl * f, unsigned prec, unsigned num, expr * const * args, expr_ref & result) { - switch (m_mode) { - case FPAA_PRECISE: - fpa2bv_converter::mk_mul(f,num,args,result); - break; - case FPAA_SMALL_FLOATS: - { - func_decl_ref small_fd(m); - expr_ref_vector small_args(m); - mk_small_op(f, prec, num, args, small_fd, small_args); - expr_ref small_op(m); - fpa2bv_converter::mk_mul(small_fd, num, small_args.c_ptr(), small_op); - mk_cast_small_to_big(f, small_op, result); - SASSERT(is_well_sorted(m, result)); - TRACE("fpa2bv_small_float_mul", tout << mk_ismt2_pp(result, m) << std::endl; ); - break; - } - case FPAA_FIXBITS: // for now, encode fully. - { SASSERT(num == 3); - - expr_ref rm(m), x(m), y(m); - rm = args[0]; - x = args[1]; - y = args[2]; - - expr_ref nan(m), nzero(m), pzero(m), ninf(m), pinf(m); - mk_nan(f, nan); - mk_nzero(f, nzero); - mk_pzero(f, pzero); - mk_ninf(f, ninf); - mk_pinf(f, pinf); - - expr_ref x_is_nan(m), x_is_zero(m), x_is_pos(m), x_is_inf(m); - expr_ref y_is_nan(m), y_is_zero(m), y_is_pos(m), y_is_inf(m); - mk_is_nan(x, x_is_nan); - mk_is_zero(x, x_is_zero); - mk_is_pos(x, x_is_pos); - mk_is_inf(x, x_is_inf); - mk_is_nan(y, y_is_nan); - mk_is_zero(y, y_is_zero); - mk_is_pos(y, y_is_pos); - mk_is_inf(y, y_is_inf); - - dbg_decouple("fpa2bv_mul_x_is_nan", x_is_nan); - dbg_decouple("fpa2bv_mul_x_is_zero", x_is_zero); - dbg_decouple("fpa2bv_mul_x_is_pos", x_is_pos); - dbg_decouple("fpa2bv_mul_x_is_inf", x_is_inf); - dbg_decouple("fpa2bv_mul_y_is_nan", y_is_nan); - dbg_decouple("fpa2bv_mul_y_is_zero", y_is_zero); - dbg_decouple("fpa2bv_mul_y_is_pos", y_is_pos); - dbg_decouple("fpa2bv_mul_y_is_inf", y_is_inf); - - expr_ref c1(m), c2(m), c3(m), c4(m), c5(m), c6(m); - expr_ref v1(m), v2(m), v3(m), v4(m), v5(m), v6(m), v7(m); - - // (x is NaN) || (y is NaN) -> NaN - m_simp.mk_or(x_is_nan, y_is_nan, c1); - v1 = nan; - - // (x is +oo) -> if (y is 0) then NaN else inf with y's sign. - mk_is_pinf(x, c2); - expr_ref y_sgn_inf(m); - mk_ite(y_is_pos, pinf, ninf, y_sgn_inf); - mk_ite(y_is_zero, nan, y_sgn_inf, v2); - - // (y is +oo) -> if (x is 0) then NaN else inf with x's sign. - mk_is_pinf(y, c3); - expr_ref x_sgn_inf(m); - mk_ite(x_is_pos, pinf, ninf, x_sgn_inf); - mk_ite(x_is_zero, nan, x_sgn_inf, v3); - - // (x is -oo) -> if (y is 0) then NaN else inf with -y's sign. - mk_is_ninf(x, c4); - expr_ref neg_y_sgn_inf(m); - mk_ite(y_is_pos, ninf, pinf, neg_y_sgn_inf); - mk_ite(y_is_zero, nan, neg_y_sgn_inf, v4); - - // (y is -oo) -> if (x is 0) then NaN else inf with -x's sign. - mk_is_ninf(y, c5); - expr_ref neg_x_sgn_inf(m); - mk_ite(x_is_pos, ninf, pinf, neg_x_sgn_inf); - mk_ite(x_is_zero, nan, neg_x_sgn_inf, v5); - - // (x is 0) || (y is 0) -> x but with sign = x.sign ^ y.sign - m_simp.mk_or(x_is_zero, y_is_zero, c6); - expr_ref sign_xor(m); - m_simp.mk_xor(x_is_pos, y_is_pos, sign_xor); - mk_ite(sign_xor, nzero, pzero, v6); - - // else comes the actual multiplication. - unsigned ebits = m_util.get_ebits(f->get_range()); - unsigned sbits = m_util.get_sbits(f->get_range()); - SASSERT(ebits <= sbits); - - expr_ref a_sgn(m), a_sig(m), a_exp(m), a_lz(m), b_sgn(m), b_sig(m), b_exp(m), b_lz(m); - unpack(x, a_sgn, a_sig, a_exp, a_lz, true); - unpack(y, b_sgn, b_sig, b_exp, b_lz, true); - - dbg_decouple("fpa2bv_mul_a_sig", a_sig); - dbg_decouple("fpa2bv_mul_a_exp", a_exp); - dbg_decouple("fpa2bv_mul_b_sig", b_sig); - dbg_decouple("fpa2bv_mul_b_exp", b_exp); - - expr_ref a_lz_ext(m), b_lz_ext(m); - a_lz_ext = m_bv_util.mk_zero_extend(2, a_lz); - b_lz_ext = m_bv_util.mk_zero_extend(2, b_lz); - - dbg_decouple("fpa2bv_mul_lz_a", a_lz); - dbg_decouple("fpa2bv_mul_lz_b", b_lz); - - expr_ref a_sig_ext(m), b_sig_ext(m); - a_sig_ext = m_bv_util.mk_zero_extend(sbits, a_sig); - b_sig_ext = m_bv_util.mk_zero_extend(sbits, b_sig); - - expr_ref a_exp_ext(m), b_exp_ext(m); - a_exp_ext = m_bv_util.mk_sign_extend(2, a_exp); - b_exp_ext = m_bv_util.mk_sign_extend(2, b_exp); - - expr_ref res_sgn(m), res_sig(m), res_exp(m); - expr * signs[2] = { a_sgn, b_sgn }; - res_sgn = m_bv_util.mk_bv_xor(2, signs); - - dbg_decouple("fpa2bv_mul_res_sgn", res_sgn); - - res_exp = m_bv_util.mk_bv_add( - m_bv_util.mk_bv_sub(a_exp_ext, a_lz_ext), - m_bv_util.mk_bv_sub(b_exp_ext, b_lz_ext)); - - expr_ref product(m); - product = m_bv_util.mk_bv_mul(a_sig_ext, b_sig_ext); - - dbg_decouple("fpa2bv_mul_product", product); - - SASSERT(m_bv_util.get_bv_size(product) == 2*sbits); - - expr_ref h_p(m), l_p(m), rbits(m); - h_p = m_bv_util.mk_extract(2*sbits-1, sbits, product); - l_p = m_bv_util.mk_extract(sbits-1, 0, product); - - if (sbits >= 4) { - expr_ref sticky(m); - sticky = m.mk_app(m_bv_util.get_fid(), OP_BREDOR, m_bv_util.mk_extract(sbits-4, 0, product)); - rbits = m_bv_util.mk_concat(m_bv_util.mk_extract(sbits-1, sbits-3, product), sticky); - } - else - rbits = m_bv_util.mk_concat(l_p, m_bv_util.mk_numeral(0, 4 - sbits)); - - SASSERT(m_bv_util.get_bv_size(rbits) == 4); - res_sig = m_bv_util.mk_concat(h_p, rbits); - - //expr_ref rounded(m); - round(f->get_range(), rm, res_sgn, res_sig, res_exp, v7); - - //AZ:the only difference to the original - fix_bits(prec, v7, sbits, ebits); - - // And finally, we tie them together. - mk_ite(c6, v6, v7, result); - mk_ite(c5, v5, result, result); - mk_ite(c4, v4, result, result); - mk_ite(c3, v3, result, result); - mk_ite(c2, v2, result, result); - mk_ite(c1, v1, result, result); - - SASSERT(is_well_sorted(m, result)); - - TRACE("fpa2bv_mul", tout << "MUL = " << mk_ismt2_pp(result, m) << std::endl; ); - } - break; - default: UNREACHABLE(); break; - } -} - -void fpa2bv_converter_prec::mk_div(func_decl * f, unsigned prec, unsigned num, expr * const * args, expr_ref & result) { - switch (m_mode) { - case FPAA_SMALL_FLOATS: - { - func_decl_ref small_fd(m); - expr_ref_vector small_args(m); - mk_small_op(f, prec, num, args, small_fd, small_args); - expr_ref small_op(m); - fpa2bv_converter::mk_div(small_fd, num, small_args.c_ptr(), small_op); - mk_cast_small_to_big(f, small_op, result); - SASSERT(is_well_sorted(m, result)); - TRACE("fpa2bv_small_float_div", tout << mk_ismt2_pp(result, m) << std::endl; ); - break; - } - case FPAA_PRECISE: - case FPAA_FIXBITS: // for now, encode fully. - fpa2bv_converter::mk_div(f,num,args,result); - break; - - { - SASSERT(num == 3); - - expr_ref rm(m), x(m), y(m); - rm = args[0]; - x = args[1]; - y = args[2]; - - expr_ref nan(m), nzero(m), pzero(m), ninf(m), pinf(m); - mk_nan(f, nan); - mk_nzero(f, nzero); - mk_pzero(f, pzero); - mk_ninf(f, ninf); - mk_pinf(f, pinf); - - expr_ref x_is_nan(m), x_is_zero(m), x_is_pos(m), x_is_inf(m); - expr_ref y_is_nan(m), y_is_zero(m), y_is_pos(m), y_is_inf(m); - mk_is_nan(x, x_is_nan); - mk_is_zero(x, x_is_zero); - mk_is_pos(x, x_is_pos); - mk_is_inf(x, x_is_inf); - mk_is_nan(y, y_is_nan); - mk_is_zero(y, y_is_zero); - mk_is_pos(y, y_is_pos); - mk_is_inf(y, y_is_inf); - - dbg_decouple("fpa2bv_div_x_is_nan", x_is_nan); - dbg_decouple("fpa2bv_div_x_is_zero", x_is_zero); - dbg_decouple("fpa2bv_div_x_is_pos", x_is_pos); - dbg_decouple("fpa2bv_div_x_is_inf", x_is_inf); - dbg_decouple("fpa2bv_div_y_is_nan", y_is_nan); - dbg_decouple("fpa2bv_div_y_is_zero", y_is_zero); - dbg_decouple("fpa2bv_div_y_is_pos", y_is_pos); - dbg_decouple("fpa2bv_div_y_is_inf", y_is_inf); - - expr_ref c1(m), c2(m), c3(m), c4(m), c5(m), c6(m), c7(m); - expr_ref v1(m), v2(m), v3(m), v4(m), v5(m), v6(m), v7(m), v8(m); - - // (x is NaN) || (y is NaN) -> NaN - m_simp.mk_or(x_is_nan, y_is_nan, c1); - v1 = nan; - - // (x is +oo) -> if (y is oo) then NaN else inf with y's sign. - mk_is_pinf(x, c2); - expr_ref y_sgn_inf(m); - mk_ite(y_is_pos, pinf, ninf, y_sgn_inf); - mk_ite(y_is_inf, nan, y_sgn_inf, v2); - - // (y is +oo) -> if (x is oo) then NaN else 0 with sign x.sgn ^ y.sgn - mk_is_pinf(y, c3); - expr_ref xy_zero(m), signs_xor(m); - m_simp.mk_xor(x_is_pos, y_is_pos, signs_xor); - mk_ite(signs_xor, nzero, pzero, xy_zero); - mk_ite(x_is_inf, nan, xy_zero, v3); - - // (x is -oo) -> if (y is oo) then NaN else inf with -y's sign. - mk_is_ninf(x, c4); - expr_ref neg_y_sgn_inf(m); - mk_ite(y_is_pos, ninf, pinf, neg_y_sgn_inf); - mk_ite(y_is_inf, nan, neg_y_sgn_inf, v4); - - // (y is -oo) -> if (x is oo) then NaN else 0 with sign x.sgn ^ y.sgn - mk_is_ninf(y, c5); - mk_ite(x_is_inf, nan, xy_zero, v5); - - // (y is 0) -> if (x is 0) then NaN else inf with xor sign. - c6 = y_is_zero; - expr_ref sgn_inf(m); - mk_ite(signs_xor, ninf, pinf, sgn_inf); - mk_ite(x_is_zero, nan, sgn_inf, v6); - - // (x is 0) -> result is zero with sgn = x.sgn^y.sgn - // This is a special case to avoid problems with the unpacking of zero. - c7 = x_is_zero; - mk_ite(signs_xor, nzero, pzero, v7); - - // else comes the actual division. - unsigned ebits = m_util.get_ebits(f->get_range()); - unsigned sbits = m_util.get_sbits(f->get_range()); - SASSERT(ebits <= sbits); - - expr_ref a_sgn(m), a_sig(m), a_exp(m), a_lz(m), b_sgn(m), b_sig(m), b_exp(m), b_lz(m); - unpack(x, a_sgn, a_sig, a_exp, a_lz, true); - unpack(y, b_sgn, b_sig, b_exp, b_lz, true); - - unsigned extra_bits = sbits+2; - expr_ref a_sig_ext(m), b_sig_ext(m); - a_sig_ext = m_bv_util.mk_concat(a_sig, m_bv_util.mk_numeral(0, sbits + extra_bits)); - b_sig_ext = m_bv_util.mk_zero_extend(sbits + extra_bits, b_sig); - - expr_ref a_exp_ext(m), b_exp_ext(m); - a_exp_ext = m_bv_util.mk_sign_extend(2, a_exp); - b_exp_ext = m_bv_util.mk_sign_extend(2, b_exp); - - expr_ref res_sgn(m), res_sig(m), res_exp(m); - expr * signs[2] = { a_sgn, b_sgn }; - res_sgn = m_bv_util.mk_bv_xor(2, signs); - - expr_ref a_lz_ext(m), b_lz_ext(m); - a_lz_ext = m_bv_util.mk_zero_extend(2, a_lz); - b_lz_ext = m_bv_util.mk_zero_extend(2, b_lz); - - res_exp = m_bv_util.mk_bv_sub( - m_bv_util.mk_bv_sub(a_exp_ext, a_lz_ext), - m_bv_util.mk_bv_sub(b_exp_ext, b_lz_ext)); - - expr_ref quotient(m); - quotient = m.mk_app(m_bv_util.get_fid(), OP_BUDIV, a_sig_ext, b_sig_ext); - - dbg_decouple("fpa2bv_div_quotient", quotient); - - SASSERT(m_bv_util.get_bv_size(quotient) == (sbits + sbits + extra_bits)); - - expr_ref sticky(m); - sticky = m.mk_app(m_bv_util.get_fid(), OP_BREDOR, m_bv_util.mk_extract(extra_bits-2, 0, quotient)); - res_sig = m_bv_util.mk_concat(m_bv_util.mk_extract(extra_bits+sbits+1, extra_bits-1, quotient), sticky); - - SASSERT(m_bv_util.get_bv_size(res_sig) == (sbits + 4)); - - //expr_ref rounded(m);//AZ - round(f->get_range(), rm, res_sgn, res_sig, res_exp, v8); - - fix_bits(prec, v8,sbits,ebits);//AZ - - // And finally, we tie them together. - mk_ite(c7, v7, v8, result); - mk_ite(c6, v6, result, result); - mk_ite(c5, v5, result, result); - mk_ite(c4, v4, result, result); - mk_ite(c3, v3, result, result); - mk_ite(c2, v2, result, result); - mk_ite(c1, v1, result, result); - - SASSERT(is_well_sorted(m, result)); - - TRACE("fpa2bv_div", tout << "DIV = " << mk_ismt2_pp(result, m) << std::endl; ); - } - break; - default: UNREACHABLE(); break; - } -} - -void fpa2bv_converter_prec::mk_remainder(func_decl * f, unsigned prec, unsigned num, expr * const * args, expr_ref & result) { - switch (m_mode) { - case FPAA_SMALL_FLOATS: - { - func_decl_ref small_fd(m); - expr_ref_vector small_args(m); - mk_small_op(f, prec, num, args, small_fd, small_args); - expr_ref small_op(m); - fpa2bv_converter::mk_rem(small_fd, num, small_args.c_ptr(), small_op); - mk_cast_small_to_big(f, small_op, result); - SASSERT(is_well_sorted(m, result)); - TRACE("fpa2bv_small_float_remainder", tout << mk_ismt2_pp(result, m) << std::endl; ); - break; - } - case FPAA_PRECISE: - fpa2bv_converter::mk_rem(f,num,args,result); - break; - case FPAA_FIXBITS: // for now, encode fully. - { - SASSERT(num == 2); - - // Remainder is always exact, so there is no rounding mode. - expr_ref x(m), y(m); - x = args[0]; - y = args[1]; - - expr_ref nan(m), nzero(m), pzero(m), ninf(m), pinf(m); - mk_nan(f, nan); - mk_nzero(f, nzero); - mk_pzero(f, pzero); - mk_ninf(f, ninf); - mk_pinf(f, pinf); - - expr_ref x_is_nan(m), x_is_zero(m), x_is_pos(m), x_is_inf(m); - expr_ref y_is_nan(m), y_is_zero(m), y_is_pos(m), y_is_inf(m); - mk_is_nan(x, x_is_nan); - mk_is_zero(x, x_is_zero); - mk_is_pos(x, x_is_pos); - mk_is_inf(x, x_is_inf); - mk_is_nan(y, y_is_nan); - mk_is_zero(y, y_is_zero); - mk_is_pos(y, y_is_pos); - mk_is_inf(y, y_is_inf); - - dbg_decouple("fpa2bv_rem_x_is_nan", x_is_nan); - dbg_decouple("fpa2bv_rem_x_is_zero", x_is_zero); - dbg_decouple("fpa2bv_rem_x_is_pos", x_is_pos); - dbg_decouple("fpa2bv_rem_x_is_inf", x_is_inf); - dbg_decouple("fpa2bv_rem_y_is_nan", y_is_nan); - dbg_decouple("fpa2bv_rem_y_is_zero", y_is_zero); - dbg_decouple("fpa2bv_rem_y_is_pos", y_is_pos); - dbg_decouple("fpa2bv_rem_y_is_inf", y_is_inf); - - expr_ref c1(m), c2(m), c3(m), c4(m), c5(m), c6(m); - expr_ref v1(m), v2(m), v3(m), v4(m), v5(m), v6(m), v7(m); - - // (x is NaN) || (y is NaN) -> NaN - m_simp.mk_or(x_is_nan, y_is_nan, c1); - v1 = nan; - - // (x is +-oo) -> NaN - c2 = x_is_inf; - v2 = nan; - - // (y is +-oo) -> x - c3 = y_is_inf; - v3 = x; - - // (x is 0) -> x - c4 = x_is_zero; - v4 = pzero; - - // (y is 0) -> NaN. - c5 = y_is_zero; - v5 = nan; - - // else the actual remainder. - unsigned ebits = m_util.get_ebits(f->get_range()); - unsigned sbits = m_util.get_sbits(f->get_range()); - - expr_ref a_sgn(m), a_sig(m), a_exp(m), a_lz(m); - expr_ref b_sgn(m), b_sig(m), b_exp(m), b_lz(m); - unpack(x, a_sgn, a_sig, a_exp, a_lz, true); - unpack(y, b_sgn, b_sig, b_exp, b_lz, true); - - BVSLT(a_exp, b_exp, c6); - v6 = x; - - // max. exponent difference is (2^ebits) - 3 - const mpz & two_to_ebits = fu().fm().m_powers2(ebits); - mpz max_exp_diff; - m_mpz_manager.sub(two_to_ebits, 3, max_exp_diff); - SASSERT(m_mpz_manager.is_int64(max_exp_diff)); - SASSERT(m_mpz_manager.get_uint64(max_exp_diff) <= UINT_MAX); - - unsigned int max_exp_diff_ui = (unsigned int)m_mpz_manager.get_uint64(max_exp_diff); - m_mpz_manager.del(max_exp_diff); - - expr_ref exp_diff(m); - exp_diff = m_bv_util.mk_bv_sub(a_exp, b_exp); - dbg_decouple("fpa2bv_rem_exp_diff", exp_diff); - - // CMW: This creates _huge_ bit-vectors, which is potentially sub-optimal, - // but calculating this via rem = x - y * nearest(x/y) creates huge circuits. - expr_ref huge_sig(m), shifted_sig(m), huge_rem(m); - huge_sig = m_bv_util.mk_zero_extend(max_exp_diff_ui, a_sig); - shifted_sig = m_bv_util.mk_bv_shl(huge_sig, m_bv_util.mk_zero_extend(max_exp_diff_ui + sbits - ebits, exp_diff)); - huge_rem = m_bv_util.mk_bv_urem(shifted_sig, m_bv_util.mk_zero_extend(max_exp_diff_ui, b_sig)); - dbg_decouple("fpa2bv_rem_huge_rem", huge_rem); - - expr_ref res_sgn(m), res_sig(m), res_exp(m); - res_sgn = a_sgn; - res_sig = m_bv_util.mk_concat(m_bv_util.mk_extract(sbits, 0, huge_rem), - m_bv_util.mk_numeral(0, 3)); - res_exp = m_bv_util.mk_sign_extend(2, b_exp); - - expr_ref rm(m); - rm = m_bv_util.mk_numeral(BV_RM_TIES_TO_EVEN, 3); - - //expr_ref rounded(m); - round(f->get_range(), rm, res_sgn, res_sig, res_exp, v7); - - fix_bits(prec, v7,sbits, ebits); - - // And finally, we tie them together. - mk_ite(c6, v6, v7, result); - mk_ite(c5, v5, result, result); - mk_ite(c4, v4, result, result); - mk_ite(c3, v3, result, result); - mk_ite(c2, v2, result, result); - mk_ite(c1, v1, result, result); - - SASSERT(is_well_sorted(m, result)); - - TRACE("fpa2bv_rem", tout << "REM = " << mk_ismt2_pp(result, m) << std::endl; ); - } - break; - default: UNREACHABLE(); break; - } -} - -void fpa2bv_converter_prec::mk_abs(func_decl * f, unsigned prec, unsigned num, expr * const * args, expr_ref & result) { - //This doesn't need approximation in it's current form - switch (m_mode) { - case FPAA_PRECISE: - case FPAA_SMALL_FLOATS: - case FPAA_FIXBITS: // for now, encode fully. - fpa2bv_converter::mk_abs(f,num,args,result); - break; - default: UNREACHABLE(); break; - } -} - -void fpa2bv_converter_prec::mk_min(func_decl * f, unsigned prec, unsigned num, expr * const * args, expr_ref & result) { - switch (m_mode) { - case FPAA_PRECISE: - case FPAA_SMALL_FLOATS: - case FPAA_FIXBITS: // for now, encode fully. - fpa2bv_converter::mk_min(f,num,args,result); - break; - default: UNREACHABLE(); break; - } -} - -void fpa2bv_converter_prec::mk_max(func_decl * f, unsigned prec, unsigned num, expr * const * args, expr_ref & result) { - switch (m_mode) { - case FPAA_PRECISE: - case FPAA_SMALL_FLOATS: - case FPAA_FIXBITS: // for now, encode fully. - fpa2bv_converter::mk_max(f,num,args,result); - break; - default: UNREACHABLE(); break; - } -} - -void fpa2bv_converter_prec::mk_fusedma(func_decl * f, unsigned prec, unsigned num, expr * const * args, expr_ref & result) { - switch (m_mode) { - case FPAA_SMALL_FLOATS: - { - func_decl_ref small_fd(m); - expr_ref_vector small_args(m); - mk_small_op(f, prec, num, args, small_fd, small_args); - expr_ref small_op(m); - fpa2bv_converter::mk_fma(small_fd, num, small_args.c_ptr(), small_op); - mk_cast_small_to_big(f, small_op, result); - SASSERT(is_well_sorted(m, result)); - TRACE("fpa2bv_small_float_fma", tout << mk_ismt2_pp(result, m) << std::endl; ); - break; - } - case FPAA_PRECISE: - fpa2bv_converter::mk_fma(f,num,args,result); - break; - case FPAA_FIXBITS: - { - SASSERT(num == 4); - - // fusedma means (x * y) + z - expr_ref rm(m), x(m), y(m), z(m); - rm = args[0]; - x = args[1]; - y = args[2]; - z = args[3]; - - expr_ref nan(m), nzero(m), pzero(m), ninf(m), pinf(m); - mk_nan(f, nan); - mk_nzero(f, nzero); - mk_pzero(f, pzero); - mk_ninf(f, ninf); - mk_pinf(f, pinf); - - expr_ref x_is_nan(m), x_is_zero(m), x_is_pos(m), x_is_neg(m), x_is_inf(m); - expr_ref y_is_nan(m), y_is_zero(m), y_is_pos(m), y_is_neg(m), y_is_inf(m); - expr_ref z_is_nan(m), z_is_zero(m), z_is_pos(m), z_is_neg(m), z_is_inf(m); - mk_is_nan(x, x_is_nan); - mk_is_zero(x, x_is_zero); - mk_is_pos(x, x_is_pos); - mk_is_neg(x, x_is_neg); - mk_is_inf(x, x_is_inf); - mk_is_nan(y, y_is_nan); - mk_is_zero(y, y_is_zero); - mk_is_pos(y, y_is_pos); - mk_is_neg(y, y_is_neg); - mk_is_inf(y, y_is_inf); - mk_is_nan(z, z_is_nan); - mk_is_zero(z, z_is_zero); - mk_is_pos(z, z_is_pos); - mk_is_neg(z, z_is_neg); - mk_is_inf(z, z_is_inf); - - expr_ref rm_is_to_neg(m); - mk_is_rm(rm, BV_RM_TO_NEGATIVE, rm_is_to_neg); - - dbg_decouple("fpa2bv_fma_x_is_nan", x_is_nan); - dbg_decouple("fpa2bv_fma_x_is_zero", x_is_zero); - dbg_decouple("fpa2bv_fma_x_is_pos", x_is_pos); - dbg_decouple("fpa2bv_fma_x_is_inf", x_is_inf); - dbg_decouple("fpa2bv_fma_y_is_nan", y_is_nan); - dbg_decouple("fpa2bv_fma_y_is_zero", y_is_zero); - dbg_decouple("fpa2bv_fma_y_is_pos", y_is_pos); - dbg_decouple("fpa2bv_fma_y_is_inf", y_is_inf); - dbg_decouple("fpa2bv_fma_z_is_nan", z_is_nan); - dbg_decouple("fpa2bv_fma_z_is_zero", z_is_zero); - dbg_decouple("fpa2bv_fma_z_is_pos", z_is_pos); - dbg_decouple("fpa2bv_fma_z_is_inf", z_is_inf); - - expr_ref c1(m), c2(m), c3(m), c4(m), c5(m), c6(m), c7(m); - expr_ref v1(m), v2(m), v3(m), v4(m), v5(m), v6(m), v7(m), v8(m); - - expr_ref inf_xor(m), inf_cond(m); - m_simp.mk_xor(x_is_neg, y_is_neg, inf_xor); - m_simp.mk_xor(inf_xor, z_is_neg, inf_xor); - m_simp.mk_and(z_is_inf, inf_xor, inf_cond); - - // (x is NaN) || (y is NaN) || (z is Nan) -> NaN - m_simp.mk_or(x_is_nan, y_is_nan, z_is_nan, c1); - v1 = nan; - - // (x is +oo) -> if (y is 0) then NaN else inf with y's sign. - mk_is_pinf(x, c2); - expr_ref y_sgn_inf(m), inf_or(m); - mk_ite(y_is_pos, pinf, ninf, y_sgn_inf); - m_simp.mk_or(y_is_zero, inf_cond, inf_or); - mk_ite(inf_or, nan, y_sgn_inf, v2); - - // (y is +oo) -> if (x is 0) then NaN else inf with x's sign. - mk_is_pinf(y, c3); - expr_ref x_sgn_inf(m); - mk_ite(x_is_pos, pinf, ninf, x_sgn_inf); - m_simp.mk_or(x_is_zero, inf_cond, inf_or); - mk_ite(inf_or, nan, x_sgn_inf, v3); - - // (x is -oo) -> if (y is 0) then NaN else inf with -y's sign. - mk_is_ninf(x, c4); - expr_ref neg_y_sgn_inf(m); - mk_ite(y_is_pos, ninf, pinf, neg_y_sgn_inf); - m_simp.mk_or(y_is_zero, inf_cond, inf_or); - mk_ite(inf_or, nan, neg_y_sgn_inf, v4); - - // (y is -oo) -> if (x is 0) then NaN else inf with -x's sign. - mk_is_ninf(y, c5); - expr_ref neg_x_sgn_inf(m); - mk_ite(x_is_pos, ninf, pinf, neg_x_sgn_inf); - m_simp.mk_or(x_is_zero, inf_cond, inf_or); - mk_ite(inf_or, nan, neg_x_sgn_inf, v5); - - // z is +-INF -> z. - mk_is_inf(z, c6); - v6 = z; - - // (x is 0) || (y is 0) -> z - m_simp.mk_or(x_is_zero, y_is_zero, c7); - expr_ref ite_c(m); - m_simp.mk_and(z_is_zero, m.mk_not(rm_is_to_neg), ite_c); - mk_ite(ite_c, pzero, z, v7); - - - // else comes the fused multiplication. - unsigned ebits = m_util.get_ebits(f->get_range()); - unsigned sbits = m_util.get_sbits(f->get_range()); - SASSERT(ebits <= sbits); - - expr_ref a_sgn(m), a_sig(m), a_exp(m), a_lz(m); - expr_ref b_sgn(m), b_sig(m), b_exp(m), b_lz(m); - expr_ref c_sgn(m), c_sig(m), c_exp(m), c_lz(m); - unpack(x, a_sgn, a_sig, a_exp, a_lz, true); - unpack(y, b_sgn, b_sig, b_exp, b_lz, true); - unpack(z, c_sgn, c_sig, c_exp, c_lz, true); - - expr_ref a_lz_ext(m), b_lz_ext(m), c_lz_ext(m); - a_lz_ext = m_bv_util.mk_zero_extend(2, a_lz); - b_lz_ext = m_bv_util.mk_zero_extend(2, b_lz); - c_lz_ext = m_bv_util.mk_zero_extend(2, c_lz); - - expr_ref a_sig_ext(m), b_sig_ext(m); - a_sig_ext = m_bv_util.mk_zero_extend(sbits, a_sig); - b_sig_ext = m_bv_util.mk_zero_extend(sbits, b_sig); - - expr_ref a_exp_ext(m), b_exp_ext(m), c_exp_ext(m); - a_exp_ext = m_bv_util.mk_sign_extend(2, a_exp); - b_exp_ext = m_bv_util.mk_sign_extend(2, b_exp); - c_exp_ext = m_bv_util.mk_sign_extend(2, c_exp); - - dbg_decouple("fpa2bv_fma_a_sig", a_sig_ext); - dbg_decouple("fpa2bv_fma_b_sig", b_sig_ext); - dbg_decouple("fpa2bv_fma_c_sig", c_sig); - dbg_decouple("fpa2bv_fma_a_exp", a_exp_ext); - dbg_decouple("fpa2bv_fma_b_exp", b_exp_ext); - dbg_decouple("fpa2bv_fma_c_exp", c_exp_ext); - dbg_decouple("fpa2bv_fma_a_lz", a_lz_ext); - dbg_decouple("fpa2bv_fma_b_lz", b_lz_ext); - dbg_decouple("fpa2bv_fma_c_lz", c_lz_ext); - - expr_ref mul_sgn(m), mul_sig(m), mul_exp(m); - expr * signs[2] = { a_sgn, b_sgn }; - - mul_sgn = m_bv_util.mk_bv_xor(2, signs); - dbg_decouple("fpa2bv_fma_mul_sgn", mul_sgn); - - mul_exp = m_bv_util.mk_bv_add(m_bv_util.mk_bv_sub(a_exp_ext, a_lz_ext), - m_bv_util.mk_bv_sub(b_exp_ext, b_lz_ext)); - dbg_decouple("fpa2bv_fma_mul_exp", mul_exp); - - mul_sig = m_bv_util.mk_bv_mul(a_sig_ext, b_sig_ext); - dbg_decouple("fpa2bv_fma_mul_sig", mul_sig); - - SASSERT(m_bv_util.get_bv_size(mul_sig) == 2*sbits); - SASSERT(m_bv_util.get_bv_size(mul_exp) == ebits + 2); - - // The product has the form [-1][0].[2*sbits - 2]. - - // Extend c - c_sig = m_bv_util.mk_zero_extend(1, m_bv_util.mk_concat(c_sig, m_bv_util.mk_numeral(0, sbits-1))); - c_exp_ext = m_bv_util.mk_bv_sub(c_exp_ext, c_lz_ext); - - SASSERT(m_bv_util.get_bv_size(mul_sig) == 2 * sbits); - SASSERT(m_bv_util.get_bv_size(c_sig) == 2 * sbits); - - expr_ref swap_cond(m); - swap_cond = m_bv_util.mk_sle(mul_exp, c_exp_ext); - SASSERT(is_well_sorted(m, swap_cond)); - dbg_decouple("fpa2bv_fma_swap_cond", swap_cond); - - expr_ref e_sgn(m), e_sig(m), e_exp(m), f_sgn(m), f_sig(m), f_exp(m); - m_simp.mk_ite(swap_cond, c_sgn, mul_sgn, e_sgn); - m_simp.mk_ite(swap_cond, c_sig, mul_sig, e_sig); // has 2 * sbits - m_simp.mk_ite(swap_cond, c_exp_ext, mul_exp, e_exp); // has ebits + 2 - m_simp.mk_ite(swap_cond, mul_sgn, c_sgn, f_sgn); - m_simp.mk_ite(swap_cond, mul_sig, c_sig, f_sig); // has 2 * sbits - m_simp.mk_ite(swap_cond, mul_exp, c_exp_ext, f_exp); // has ebits + 2 - - SASSERT(is_well_sorted(m, e_sgn)); - SASSERT(is_well_sorted(m, e_sig)); - SASSERT(is_well_sorted(m, e_exp)); - SASSERT(is_well_sorted(m, f_sgn)); - SASSERT(is_well_sorted(m, f_sig)); - SASSERT(is_well_sorted(m, f_exp)); - - SASSERT(m_bv_util.get_bv_size(e_sig) == 2 * sbits); - SASSERT(m_bv_util.get_bv_size(f_sig) == 2 * sbits); - SASSERT(m_bv_util.get_bv_size(e_exp) == ebits + 2); - SASSERT(m_bv_util.get_bv_size(f_exp) == ebits + 2); - - expr_ref res_sgn(m), res_sig(m), res_exp(m); - - expr_ref exp_delta(m); - exp_delta = m_bv_util.mk_bv_sub(e_exp, f_exp); - dbg_decouple("fpa2bv_fma_add_exp_delta", exp_delta); - - // cap the delta - expr_ref cap(m), cap_le_delta(m); - cap = m_bv_util.mk_numeral(2*sbits, ebits+2); - cap_le_delta = m_bv_util.mk_ule(cap, exp_delta); - m_simp.mk_ite(cap_le_delta, cap, exp_delta, exp_delta); - SASSERT(m_bv_util.get_bv_size(exp_delta) == ebits+2); - SASSERT(is_well_sorted(m, exp_delta)); - dbg_decouple("fpa2bv_fma_add_exp_delta_capped", exp_delta); - - // Alignment shift with sticky bit computation. - expr_ref shifted_big(m), shifted_f_sig(m), sticky_raw(m); - shifted_big = m_bv_util.mk_bv_lshr( - m_bv_util.mk_concat(f_sig, m_bv_util.mk_numeral(0, sbits)), - m_bv_util.mk_zero_extend((3*sbits)-(ebits+2), exp_delta)); - shifted_f_sig = m_bv_util.mk_extract(3*sbits-1, sbits, shifted_big); - sticky_raw = m_bv_util.mk_extract(sbits-1, 0, shifted_big); - SASSERT(m_bv_util.get_bv_size(shifted_f_sig) == 2 * sbits); - SASSERT(is_well_sorted(m, shifted_f_sig)); - - expr_ref sticky(m); - sticky = m_bv_util.mk_zero_extend(2*sbits-1, m.mk_app(m_bv_util.get_fid(), OP_BREDOR, sticky_raw.get())); - SASSERT(is_well_sorted(m, sticky)); - dbg_decouple("fpa2bv_fma_f_sig_sticky_raw", sticky_raw); - dbg_decouple("fpa2bv_fma_f_sig_sticky", sticky); - - expr * or_args[2] = { shifted_f_sig, sticky }; - shifted_f_sig = m_bv_util.mk_bv_or(2, or_args); - SASSERT(is_well_sorted(m, shifted_f_sig)); - - // Significant addition. - // Two extra bits for catching the overflow. - e_sig = m_bv_util.mk_zero_extend(2, e_sig); - shifted_f_sig = m_bv_util.mk_zero_extend(2, shifted_f_sig); - - expr_ref eq_sgn(m); - m_simp.mk_eq(e_sgn, f_sgn, eq_sgn); - - SASSERT(m_bv_util.get_bv_size(e_sig) == 2*sbits + 2); - SASSERT(m_bv_util.get_bv_size(shifted_f_sig) == 2*sbits + 2); - - dbg_decouple("fpa2bv_fma_add_e_sig", e_sig); - dbg_decouple("fpa2bv_fma_add_shifted_f_sig", shifted_f_sig); - - expr_ref sum(m); - m_simp.mk_ite(eq_sgn, - m_bv_util.mk_bv_add(e_sig, shifted_f_sig), - m_bv_util.mk_bv_sub(e_sig, shifted_f_sig), - sum); - - SASSERT(is_well_sorted(m, sum)); - - dbg_decouple("fpa2bv_fma_add_sum", sum); - - expr_ref sign_bv(m), n_sum(m); - sign_bv = m_bv_util.mk_extract(2*sbits+1, 2*sbits+1, sum); - n_sum = m_bv_util.mk_bv_neg(sum); - - expr_ref res_sig_eq(m), sig_abs(m), one_1(m); - one_1 = m_bv_util.mk_numeral(1, 1); - m_simp.mk_eq(sign_bv, one_1, res_sig_eq); - m_simp.mk_ite(res_sig_eq, n_sum, sum, sig_abs); - dbg_decouple("fpa2bv_fma_add_sign_bv", sign_bv); - dbg_decouple("fpa2bv_fma_add_n_sum", n_sum); - dbg_decouple("fpa2bv_fma_add_sig_abs", sig_abs); - - res_exp = e_exp; - - // Result could overflow into 4.xxx ... - - family_id bvfid = m_bv_util.get_fid(); - expr_ref res_sgn_c1(m), res_sgn_c2(m), res_sgn_c3(m); - expr_ref not_e_sgn(m), not_f_sgn(m), not_sign_bv(m); - not_e_sgn = m_bv_util.mk_bv_not(e_sgn); - not_f_sgn = m_bv_util.mk_bv_not(f_sgn); - not_sign_bv = m_bv_util.mk_bv_not(sign_bv); - res_sgn_c1 = m.mk_app(bvfid, OP_BAND, not_e_sgn, e_sgn, sign_bv); - res_sgn_c2 = m.mk_app(bvfid, OP_BAND, e_sgn, not_f_sgn, not_sign_bv); - res_sgn_c3 = m.mk_app(bvfid, OP_BAND, e_sgn, f_sgn); - expr * res_sgn_or_args[3] = { res_sgn_c1, res_sgn_c2, res_sgn_c3 }; - res_sgn = m_bv_util.mk_bv_or(3, res_sgn_or_args); - - sticky_raw = m_bv_util.mk_extract(sbits-5, 0, sig_abs); - sticky = m_bv_util.mk_zero_extend(sbits+3, m.mk_app(bvfid, OP_BREDOR, sticky_raw.get())); - dbg_decouple("fpa2bv_fma_add_sum_sticky", sticky); - - expr * res_or_args[2] = { m_bv_util.mk_extract(2*sbits-1, sbits-4, sig_abs), sticky }; - res_sig = m_bv_util.mk_bv_or(2, res_or_args); - SASSERT(m_bv_util.get_bv_size(res_sig) == sbits+4); - - expr_ref is_zero_sig(m), nil_sbits4(m); - nil_sbits4 = m_bv_util.mk_numeral(0, sbits+4); - m_simp.mk_eq(res_sig, nil_sbits4, is_zero_sig); - SASSERT(is_well_sorted(m, is_zero_sig)); - - dbg_decouple("fpa2bv_fma_is_zero_sig", is_zero_sig); - - expr_ref zero_case(m); - mk_ite(rm_is_to_neg, nzero, pzero, zero_case); - - - //AZ: Should the zero case be constrained in some manner? - expr_ref rounded(m);//, fixed(m); - round(f->get_range(), rm, res_sgn, res_sig, res_exp, rounded); - - fix_bits(prec,rounded,sbits, ebits); - - mk_ite(is_zero_sig, zero_case, rounded, v8); - - // And finally, we tie them together. - mk_ite(c7, v7, v8, result); - mk_ite(c6, v6, result, result); - mk_ite(c5, v5, result, result); - mk_ite(c4, v4, result, result); - mk_ite(c3, v3, result, result); - mk_ite(c2, v2, result, result); - mk_ite(c1, v1, result, result); - - SASSERT(is_well_sorted(m, result)); - - TRACE("fpa2bv_fma_", tout << "FMA = " << mk_ismt2_pp(result, m) << std::endl; ); - } - break; - default: UNREACHABLE(); break; - } -} - -void fpa2bv_converter_prec::mk_sqrt(func_decl * f, unsigned prec, unsigned num, expr * const * args, expr_ref & result) { - switch (m_mode) { - case FPAA_SMALL_FLOATS: - { - func_decl_ref small_fd(m); - expr_ref_vector small_args(m); - mk_small_op(f, prec, num, args, small_fd, small_args); - expr_ref small_op(m); - fpa2bv_converter::mk_sqrt(small_fd, num, small_args.c_ptr(), small_op); - mk_cast_small_to_big(f, small_op, result); - SASSERT(is_well_sorted(m, result)); - TRACE("fpa2bv_small_float_sqrt", tout << mk_ismt2_pp(result, m) << std::endl; ); - break; - } - case FPAA_PRECISE: - case FPAA_FIXBITS: // for now, encode fully. - fpa2bv_converter::mk_sqrt(f,num,args,result); - break; - default: UNREACHABLE(); break; - } -} - -void fpa2bv_converter_prec::mk_round_to_integral(func_decl * f, unsigned prec, unsigned num, expr * const * args, expr_ref & result) { - switch (m_mode) { - case FPAA_SMALL_FLOATS: - { - func_decl_ref small_fd(m); - expr_ref_vector small_args(m); - mk_small_op(f, prec, num, args, small_fd, small_args); - expr_ref small_op(m); - fpa2bv_converter::mk_round_to_integral(small_fd, num, small_args.c_ptr(), small_op); - mk_cast_small_to_big(f, small_op, result); - SASSERT(is_well_sorted(m, result)); - TRACE("fpa2bv_small_float_r2i", tout << mk_ismt2_pp(result, m) << std::endl; ); - break; - } - case FPAA_PRECISE: - case FPAA_FIXBITS: // for now, encode fully. - fpa2bv_converter::mk_sqrt(f,num,args,result); - break; - default: UNREACHABLE(); break; - } -} - -void fpa2bv_converter_prec::establish_sort(unsigned num, expr * const * args, unsigned & ebits, unsigned & sbits) -{ - unsigned ne,ns; - //hardcoding for now - ebits = 3; - sbits = 3; - for(unsigned i=0;iget_decl()->get_range())) - { - ne = fu().get_ebits(s); - ns = fu().get_sbits(s); - ebits = (ne < ebits)?ebits:ne; - sbits = (ns < sbits)?sbits:ns; - } - } -} - -void fpa2bv_converter_prec::mk_float_eq(func_decl * f, unsigned num, expr * const * args, expr_ref & result) -{ - switch (m_mode) { - case FPAA_PRECISE: - case FPAA_FIXBITS: - fpa2bv_converter::mk_float_eq(f,num,args,result); - break; - case FPAA_SMALL_FLOATS: - { - unsigned sbits, ebits; - - func_decl_ref small_fd(m); - expr_ref_vector small_args(m); - establish_sort(num, args, ebits, sbits); - mk_small_op(f, ebits, sbits, num, args, small_fd, small_args); - fpa2bv_converter::mk_float_eq(small_fd, num, small_args.c_ptr(), result); - SASSERT(is_well_sorted(m, result)); - TRACE("fpa2bv_small_float_add", tout << mk_ismt2_pp(result, m) << std::endl; ); - break; - } - } - -} - -void fpa2bv_converter_prec::mk_float_lt(func_decl * f, unsigned num, expr * const * args, expr_ref & result) -{ - switch (m_mode){ - case FPAA_PRECISE: - case FPAA_FIXBITS: - fpa2bv_converter::mk_float_lt(f,num,args,result); - break; - case FPAA_SMALL_FLOATS: { - unsigned sbits, ebits; - - func_decl_ref small_fd(m); - expr_ref_vector small_args(m); - establish_sort(num, args, ebits, sbits); - mk_small_op(f, ebits, sbits, num, args, small_fd, small_args); - fpa2bv_converter::mk_float_lt(small_fd, num, small_args.c_ptr(), result); - SASSERT(is_well_sorted(m, result)); - TRACE("fpa2bv_small_float_add", tout << mk_ismt2_pp(result, m) << std::endl; ); - break; - } - } -} -void fpa2bv_converter_prec::mk_float_gt(func_decl * f, unsigned num, expr * const * args, expr_ref & result) -{ - switch (m_mode){ - case FPAA_PRECISE: - case FPAA_FIXBITS: - fpa2bv_converter::mk_float_gt(f,num,args,result); - break; - case FPAA_SMALL_FLOATS: { - unsigned sbits, ebits; - - func_decl_ref small_fd(m); - expr_ref_vector small_args(m); - establish_sort(num, args, ebits, sbits); - mk_small_op(f, ebits, sbits, num, args, small_fd, small_args); - fpa2bv_converter::mk_float_gt(small_fd, num, small_args.c_ptr(), result); - SASSERT(is_well_sorted(m, result)); - TRACE("fpa2bv_small_float_add", tout << mk_ismt2_pp(result, m) << std::endl; ); - break; - } - } -} -void fpa2bv_converter_prec::mk_float_le(func_decl * f, unsigned num, expr * const * args, expr_ref & result) -{ - switch (m_mode){ - case FPAA_PRECISE: - case FPAA_FIXBITS: - fpa2bv_converter::mk_float_le(f,num,args,result); - break; - case FPAA_SMALL_FLOATS: { - unsigned sbits, ebits; - - func_decl_ref small_fd(m); - expr_ref_vector small_args(m); - establish_sort(num, args, ebits, sbits); - mk_small_op(f, ebits, sbits, num, args, small_fd, small_args); - fpa2bv_converter::mk_float_le(small_fd, num, small_args.c_ptr(), result); - SASSERT(is_well_sorted(m, result)); - TRACE("fpa2bv_small_float_add", tout << mk_ismt2_pp(result, m) << std::endl; ); - break; - } - } -} -void fpa2bv_converter_prec::mk_float_ge(func_decl * f, unsigned num, expr * const * args, expr_ref & result) -{ - switch (m_mode){ - case FPAA_PRECISE: - case FPAA_FIXBITS: - fpa2bv_converter::mk_float_ge(f,num,args,result); - break; - case FPAA_SMALL_FLOATS: { - unsigned sbits, ebits; - - func_decl_ref small_fd(m); - expr_ref_vector small_args(m); - establish_sort(num, args, ebits, sbits); - mk_small_op(f, ebits, sbits, num, args, small_fd, small_args); - fpa2bv_converter::mk_float_ge(small_fd, num, small_args.c_ptr(), result); - SASSERT(is_well_sorted(m, result)); - TRACE("fpa2bv_small_float_add", tout << mk_ismt2_pp(result, m) << std::endl; ); - break; - } - } -} -/* - -void fpa2bv_converter_prec::mk_is_zero(func_decl * f, unsigned prec, unsigned num, expr * const * args, expr_ref & result) -{ - switch (m_mode){ - case FPAA_PRECISE: - case FPAA_FIXBITS: - fpa2bv_converter::mk_float_eq(f,num,args,result); - break; - case FPAA_SMALL_FLOATS: { - unsigned sbits, ebits; - - func_decl_ref small_fd(m); - expr_ref_vector small_args(m); - establish_sort(num, args, ebits, sbits); - mk_small_op(f, ebits, sbits, num, args, small_fd, small_args); - fpa2bv_converter::mk_is_zero(small_fd, num, small_args.c_ptr(), result); - SASSERT(is_well_sorted(m, result)); - TRACE("fpa2bv_small_float_add", tout << mk_ismt2_pp(result, m) << std::endl; ); - break; - } - } -} -void fpa2bv_converter_prec::mk_is_nzero(func_decl * f, unsigned prec, unsigned num, expr * const * args, expr_ref & result); -void fpa2bv_converter_prec::mk_is_pzero(func_decl * f, unsigned prec, unsigned num, expr * const * args, expr_ref & result); -void fpa2bv_converter_prec::mk_is_sign_minus(func_decl * f, unsigned prec, unsigned num, expr * const * args, expr_ref & result); -void fpa2bv_converter_prec::mk_is_nan(func_decl * f, unsigned prec, unsigned num, expr * const * args, expr_ref & result); -void fpa2bv_converter_prec::mk_is_inf(func_decl * f, unsigned prec, unsigned num, expr * const * args, expr_ref & result); -void fpa2bv_converter_prec::mk_is_normal(func_decl * f, unsigned prec, unsigned num, expr * const * args, expr_ref & result); -void fpa2bv_converter_prec::mk_is_subnormal(func_decl * f, unsigned prec, unsigned num, expr * const * args, expr_ref & result); -*/ - - - - - - diff --git a/src/tactic/fpa/fpa2bv_converter_prec.h b/src/tactic/fpa/fpa2bv_converter_prec.h deleted file mode 100644 index 24631b1ff..000000000 --- a/src/tactic/fpa/fpa2bv_converter_prec.h +++ /dev/null @@ -1,103 +0,0 @@ -/*++ -Copyright (c) 2012 Microsoft Corporation - -Module Name: - - fpa2bv_converter_prec.h - -Abstract: - - Conversion routines for Floating Point -> Bit-Vector - -Author: - - Christoph (cwinter) 2012-02-09 - -Notes: - ---*/ -#ifndef _FPA2BV_CONVERTER_PREC -#define _FPA2BV_CONVERTER_PREC - -#include"ast.h" -#include"obj_hashtable.h" -#include"ref_util.h" -#include"fpa_decl_plugin.h" -#include"bv_decl_plugin.h" -#include"model_converter.h" -#include"basic_simplifier_plugin.h" -#include"fpa2bv_converter.h" - -#define MAX_PRECISION 100 -#define MIN_PRECISION 0 - -class fpa2bv_prec_model_converter; - -enum fpa_approximation_mode { - FPAA_PRECISE, // Always use precise encoding - FPAA_FIXBITS, // Approximate by fixing some bits of the encoding - FPAA_SMALL_FLOATS // Approximate by using smaller floats -}; - -#define FPAA_DEFAULT_MODE FPAA_SMALL_FLOATS - -class fpa2bv_converter_prec : public fpa2bv_converter { - fpa_approximation_mode m_mode; - - void fix_bits(unsigned prec, expr_ref rounded, unsigned sbits, unsigned ebits);//expr_ref& fixed, - - void mk_small_op(func_decl * f, unsigned prec, unsigned num, expr * const * args, func_decl_ref & small_op, expr_ref_vector & cast_args); - void mk_small_op(func_decl * f, unsigned new_ebits, unsigned new_sbits, unsigned num, expr * const * args, func_decl_ref & small_op, expr_ref_vector & cast_args); - void mk_cast_small_to_big(func_decl * big_fd, expr * arg, expr_ref & result); - void mk_cast_small_to_big(unsigned sbits, unsigned ebits, expr * arg, expr_ref & result); - void match_sorts(expr * a, expr * b, expr_ref & n_a, expr_ref & n_b); - void establish_sort(unsigned num, expr * const * args, unsigned & ebits, unsigned & sbits); -public: - fpa2bv_converter_prec(ast_manager & m, fpa_approximation_mode mode); - - void mk_const(func_decl * f, unsigned prec, expr_ref & result); - - void mk_eq(expr * a, expr * b, expr_ref & result); - void mk_ite(expr * c, expr * t, expr * f, expr_ref & result); - - void mk_add(func_decl * f, unsigned prec, unsigned num, expr * const * args, expr_ref & result); - void mk_sub(func_decl * f, unsigned prec, unsigned num, expr * const * args, expr_ref & result); - void mk_uminus(func_decl * f, unsigned prec, unsigned num, expr * const * args, expr_ref & result); - void mk_mul(func_decl * f, unsigned prec, unsigned num, expr * const * args, expr_ref & result); - void mk_div(func_decl * f, unsigned prec, unsigned num, expr * const * args, expr_ref & result); - void mk_remainder(func_decl * f, unsigned prec, unsigned num, expr * const * args, expr_ref & result); - void mk_abs(func_decl * f, unsigned prec, unsigned num, expr * const * args, expr_ref & result); - void mk_min(func_decl * f, unsigned prec, unsigned num, expr * const * args, expr_ref & result); - void mk_max(func_decl * f, unsigned prec, unsigned num, expr * const * args, expr_ref & result); - void mk_fusedma(func_decl * f, unsigned prec, unsigned num, expr * const * args, expr_ref & result); - void mk_sqrt(func_decl * f, unsigned prec, unsigned num, expr * const * args, expr_ref & result); - void mk_round_to_integral(func_decl * f, unsigned prec, unsigned num, expr * const * args, expr_ref & result); - - void mk_float_eq(func_decl * f, unsigned num, expr * const * args, expr_ref & result); - void mk_float_lt(func_decl * f, unsigned num, expr * const * args, expr_ref & result); - void mk_float_gt(func_decl * f, unsigned num, expr * const * args, expr_ref & result); - void mk_float_le(func_decl * f, unsigned num, expr * const * args, expr_ref & result); - void mk_float_ge(func_decl * f, unsigned num, expr * const * args, expr_ref & result); - - /* - void mk_is_zero(func_decl * f, unsigned prec, unsigned num, expr * const * args, expr_ref & result); - void mk_is_nzero(func_decl * f, unsigned prec, unsigned num, expr * const * args, expr_ref & result); - void mk_is_pzero(func_decl * f, unsigned prec, unsigned num, expr * const * args, expr_ref & result); - void mk_is_sign_minus(func_decl * f, unsigned prec, unsigned num, expr * const * args, expr_ref & result); - void mk_is_nan(func_decl * f, unsigned prec, unsigned num, expr * const * args, expr_ref & result); - void mk_is_inf(func_decl * f, unsigned prec, unsigned num, expr * const * args, expr_ref & result); - void mk_is_normal(func_decl * f, unsigned prec, unsigned num, expr * const * args, expr_ref & result); - void mk_is_subnormal(func_decl * f, unsigned prec, unsigned num, expr * const * args, expr_ref & result); - */ - - - - void reset() { - dec_ref_map_key_values(m, m_const2bv); - dec_ref_map_key_values(m, m_rm_const2bv); - } -}; - - - -#endif diff --git a/src/tactic/fpa/fpa2bv_rewriter_prec.h b/src/tactic/fpa/fpa2bv_rewriter_prec.h deleted file mode 100644 index 051790ac3..000000000 --- a/src/tactic/fpa/fpa2bv_rewriter_prec.h +++ /dev/null @@ -1,261 +0,0 @@ -/*++ -Copyright (c) 2012 Microsoft Corporation - -Module Name: - - fpa2bv_rewriter.h - -Abstract: - - Rewriter for converting FPA to BV - -Author: - - Christoph (cwinter) 2012-02-09 - -Notes: - ---*/ - -#ifndef _FPA2BV_REWRITER_H_ -#define _FPA2BV_REWRITER_H_ - -#include"cooperate.h" -#include"rewriter_def.h" -#include"bv_decl_plugin.h" -#include"fpa2bv_converter_prec.h" -#include"tactic_exception.h" -#include - -struct fpa2bv_rewriter_prec_cfg : public default_rewriter_cfg { - ast_manager & m_manager; - expr_ref_vector m_out; - fpa2bv_converter_prec & m_conv; - obj_map * cnst2prec_map; - - unsigned precision; - unsigned long long m_max_memory; - unsigned m_max_steps; - - ast_manager & m() const { return m_manager; } - - fpa2bv_rewriter_prec_cfg(ast_manager & m, fpa2bv_converter_prec & c, params_ref const & p): - m_manager(m), - m_out(m), - m_conv(c) { - updt_params(p); - // We need to make sure that the mananger has the BV plugin loaded. - symbol s_bv("bv"); - if (!m_manager.has_plugin(s_bv)) - m_manager.register_plugin(s_bv, alloc(bv_decl_plugin)); - } - - ~fpa2bv_rewriter_prec_cfg() { - } - - void cleanup_buffers() { - m_out.finalize(); - } - - unsigned get_precision(func_decl * f){ - if(cnst2prec_map->contains(f)) - return cnst2prec_map->find(f); - else return precision; - } - void set_precision(unsigned p) { precision=p; } - void set_mappings(obj_map * o2p) - { - this->cnst2prec_map=o2p; - } - - void updt_params(params_ref const & p) { - m_max_memory = megabytes_to_bytes(p.get_uint("max_memory", UINT_MAX)); - m_max_steps = p.get_uint("max_steps", UINT_MAX); - } - - bool max_steps_exceeded(unsigned num_steps) const { - cooperate("fpa2bv"); - return num_steps > m_max_steps; - } - - br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) { - TRACE("fpa2bv_rw", tout << "APP: " << f->get_name() << std::endl; ); - - if (num == 0 && f->get_family_id() == null_family_id && m_conv.is_float(f->get_range())) { - m_conv.mk_const(f, get_precision(f), result); - return BR_DONE; - } - - if (num == 0 && f->get_family_id() == null_family_id && m_conv.is_rm(f->get_range())) { - m_conv.mk_rm_const(f, result); - return BR_DONE; - } - - if (m().is_eq(f)) { - SASSERT(num == 2); - //SASSERT(m().get_sort(args[0]) == m().get_sort(args[1])); - sort * ds = f->get_domain()[0]; - if (m_conv.is_float(ds)) { - m_conv.mk_eq(args[0], args[1], result); - return BR_DONE; - } - else if (m_conv.is_rm(ds)) { - result = m().mk_eq(args[0], args[1]); - return BR_DONE; - } - return BR_FAILED; - } - - if (m().is_ite(f)) { - SASSERT(num == 3); - if (m_conv.is_float(args[1])) { - m_conv.mk_ite(args[0], args[1], args[2], result); - return BR_DONE; - } - return BR_FAILED; - } - - expr_ref newAssertion(m_manager); - - if (m_conv.is_float_family(f)) - { - switch (f->get_decl_kind()) - { - case OP_FPA_RM_NEAREST_TIES_TO_AWAY: - case OP_FPA_RM_NEAREST_TIES_TO_EVEN: - case OP_FPA_RM_TOWARD_NEGATIVE: - case OP_FPA_RM_TOWARD_POSITIVE: - case OP_FPA_RM_TOWARD_ZERO: m_conv.mk_rounding_mode(f, result); return BR_DONE; - case OP_FPA_NUM: m_conv.mk_numeral(f, num, args, result); return BR_DONE; - case OP_FPA_PLUS_INF: m_conv.mk_pinf(f, result); return BR_DONE; - case OP_FPA_MINUS_INF: m_conv.mk_ninf(f, result); return BR_DONE; - case OP_FPA_PLUS_ZERO: m_conv.mk_pzero(f, result); return BR_DONE; - case OP_FPA_MINUS_ZERO: m_conv.mk_nzero(f, result); return BR_DONE; - case OP_FPA_NAN: m_conv.mk_nan(f, result); return BR_DONE; - case OP_FPA_ADD: - m_conv.mk_add(f,get_precision(f), num, args, result);return BR_DONE; - case OP_FPA_SUB: - m_conv.mk_sub(f, get_precision(f), num, args, result); return BR_DONE; - case OP_FPA_NEG: - m_conv.mk_uminus(f, get_precision(f), num, args, result); return BR_DONE; - case OP_FPA_MUL: - m_conv.mk_mul(f, get_precision(f), num, args, result); return BR_DONE; - case OP_FPA_DIV: - m_conv.mk_div(f, get_precision(f), num, args, result); return BR_DONE; - case OP_FPA_REM: - m_conv.mk_remainder(f, get_precision(f), num, args, result); return BR_DONE; - case OP_FPA_ABS: m_conv.mk_abs(f, get_precision(f), num, args, result); return BR_DONE; - case OP_FPA_MIN: m_conv.mk_min(f, get_precision(f), num, args, result); return BR_DONE; - case OP_FPA_MAX: m_conv.mk_max(f, get_precision(f), num, args, result); return BR_DONE; - case OP_FPA_FMA: - m_conv.mk_fusedma(f, get_precision(f), num, args, result); return BR_DONE; - case OP_FPA_SQRT: - m_conv.mk_sqrt(f, get_precision(f), num, args, result); return BR_DONE; - case OP_FPA_ROUND_TO_INTEGRAL: m_conv.mk_round_to_integral(f, get_precision(f), num, args, result); return BR_DONE; - case OP_FPA_EQ: m_conv.mk_float_eq(f, num, args, result); return BR_DONE; - case OP_FPA_LT: m_conv.mk_float_lt(f, num, args, result); return BR_DONE; - case OP_FPA_GT: m_conv.mk_float_gt(f, num, args, result); return BR_DONE; - case OP_FPA_LE: m_conv.mk_float_le(f, num, args, result); return BR_DONE; - case OP_FPA_GE: m_conv.mk_float_ge(f, num, args, result); return BR_DONE; - case OP_FPA_IS_ZERO: m_conv.mk_is_zero(f, num, args, result); return BR_DONE; - case OP_FPA_IS_NAN: m_conv.mk_is_nan(f, num, args, result); return BR_DONE; - case OP_FPA_IS_INF: m_conv.mk_is_inf(f, num, args, result); return BR_DONE; - case OP_FPA_IS_NORMAL: m_conv.mk_is_normal(f, num, args, result); return BR_DONE; - case OP_FPA_IS_SUBNORMAL: m_conv.mk_is_subnormal(f, num, args, result); return BR_DONE; - case OP_FPA_IS_POSITIVE: m_conv.mk_is_positive(f, num, args, result); return BR_DONE; - case OP_FPA_IS_NEGATIVE: m_conv.mk_is_negative(f, num, args, result); return BR_DONE; - case OP_FPA_TO_FP: m_conv.mk_to_fp(f, num, args, result); return BR_DONE; - case OP_FPA_TO_FP_UNSIGNED: m_conv.mk_to_fp_unsigned(f, num, args, result); return BR_DONE; - case OP_FPA_FP: m_conv.mk_fp(f, num, args, result); return BR_DONE; - case OP_FPA_TO_UBV: m_conv.mk_to_ubv(f, num, args, result); return BR_DONE; - case OP_FPA_TO_SBV: m_conv.mk_to_sbv(f, num, args, result); return BR_DONE; - case OP_FPA_TO_REAL: m_conv.mk_to_real(f, num, args, result); return BR_DONE; - case OP_FPA_TO_IEEE_BV: m_conv.mk_to_ieee_bv(f, num, args, result); return BR_DONE; - case OP_FPA_INTERNAL_BVWRAP: - case OP_FPA_INTERNAL_BVUNWRAP: - case OP_FPA_INTERNAL_TO_REAL_UNSPECIFIED: - case OP_FPA_INTERNAL_TO_UBV_UNSPECIFIED: - case OP_FPA_INTERNAL_TO_SBV_UNSPECIFIED: return BR_FAILED; - default: - TRACE("fpa2bv", tout << "unsupported operator: " << f->get_name() << "\n"; - for (unsigned i = 0; i < num; i++) tout << mk_ismt2_pp(args[i], m()) << std::endl;); - NOT_IMPLEMENTED_YET(); - } - } - - if (f->get_family_id() == null_family_id) - { - bool is_float_uf = m_conv.is_float(f->get_range()); - unsigned i = 0; - while (!is_float_uf && i < num) - { - is_float_uf = m_conv.is_float(f->get_domain()[i]); - i++; - } - - if (is_float_uf) - { - m_conv.mk_uninterpreted_function(f, num, args, result); - return BR_DONE; - } - } - - return BR_FAILED; - } - - bool pre_visit(expr * t) - { - TRACE("pre_visit_prec", tout << mk_ismt2_pp(t, m()) << std::endl;); - - if(t->get_kind() == AST_APP && is_app_of(t, to_app(t)->get_family_id(), OP_EQ)) { - //Equation over non-boolean expressions, it should be of form constantI = subexprI - app * a = to_app(t); - - if (a->get_num_args() == 2) { - expr * a0 = a->get_arg(0); - expr * a1 = a->get_arg(1); - func_decl * cnst = 0; - - if (a0->get_kind() == AST_APP && cnst2prec_map->contains(to_app(a0)->get_decl())) - cnst = to_app(a0)->get_decl(); - else if (a1->get_kind() == AST_APP && cnst2prec_map->contains(to_app(a1)->get_decl())) - cnst = to_app(a1)->get_decl(); - - if (cnst == 0) { - // For all equalities that were in the original problem, we don't - // have any precision tracking, so those simply get 100% precision. - set_precision(100); - } - else - set_precision(cnst2prec_map->find(cnst)); - TRACE("pre_visit_prec", tout << "Precision = " << get_precision(NULL) << std::endl;); - } - } - return true; - } - - bool reduce_quantifier(quantifier * old_q, - expr * new_body, - expr * const * new_patterns, - expr * const * new_no_patterns, - expr_ref & result, - proof_ref & result_pr) { - return false; - } - - bool reduce_var(var * t, expr_ref & result, proof_ref & result_pr) { - return false; - } -}; - -template class rewriter_tpl; - -struct fpa2bv_rewriter_prec : public rewriter_tpl { - fpa2bv_rewriter_prec_cfg m_cfg; - fpa2bv_rewriter_prec(ast_manager & m, fpa2bv_converter_prec & c, params_ref const & p): - rewriter_tpl(m, m.proofs_enabled(), m_cfg), - m_cfg(m, c, p) { - } -}; - -#endif diff --git a/src/util/mpf.h b/src/util/mpf.h index 28329810e..63e0ed000 100644 --- a/src/util/mpf.h +++ b/src/util/mpf.h @@ -169,7 +169,7 @@ public: bool is_ninf(mpf const & x); bool is_normal(mpf const & x); bool is_denormal(mpf const & x); - bool is_regular(mpf const & x) { return x.sbits == 0 || is_zero(x) || is_normal(x) || is_denormal(x); } + bool is_regular(mpf const & x) { return x.sbits == 0 || is_normal(x) || is_denormal(x); } bool is_int(mpf const & x); From 1a5327e427733df223faf6ef9bc4ff4ed0853508 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 12 Jun 2015 18:30:33 -0700 Subject: [PATCH 02/28] strengthen quantifier check for PDR (and other engines) that don't handle quantified predicates Signed-off-by: Nikolaj Bjorner --- src/muz/base/dl_context.cpp | 1 + src/muz/base/rule_properties.cpp | 2 +- 2 files changed, 2 insertions(+), 1 deletion(-) diff --git a/src/muz/base/dl_context.cpp b/src/muz/base/dl_context.cpp index 3555e5bdc..aeccd2633 100644 --- a/src/muz/base/dl_context.cpp +++ b/src/muz/base/dl_context.cpp @@ -567,6 +567,7 @@ namespace datalog { m_rule_properties.check_uninterpreted_free(); break; case QPDR_ENGINE: + std::cout << "QD\n"; m_rule_properties.collect(r); m_rule_properties.check_for_negated_predicates(); m_rule_properties.check_uninterpreted_free(); diff --git a/src/muz/base/rule_properties.cpp b/src/muz/base/rule_properties.cpp index 455e02e45..619f88e3b 100644 --- a/src/muz/base/rule_properties.cpp +++ b/src/muz/base/rule_properties.cpp @@ -142,7 +142,7 @@ void rule_properties::check_existential_tail() { todo.push_back(e2); } else if (is_quantifier(e)) { - todo.push_back(to_quantifier(e)->get_expr()); + tocheck.push_back(to_quantifier(e)->get_expr()); } else if ((m.is_eq(e, e1, e2) || m.is_iff(e, e1, e2)) && m.is_true(e1)) { From 8fc67899550182002c7853e1d21c797fbfbb7f9a Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 12 Jun 2015 18:31:28 -0700 Subject: [PATCH 03/28] remove spurious print statement Signed-off-by: Nikolaj Bjorner --- src/muz/base/dl_context.cpp | 1 - 1 file changed, 1 deletion(-) diff --git a/src/muz/base/dl_context.cpp b/src/muz/base/dl_context.cpp index aeccd2633..3555e5bdc 100644 --- a/src/muz/base/dl_context.cpp +++ b/src/muz/base/dl_context.cpp @@ -567,7 +567,6 @@ namespace datalog { m_rule_properties.check_uninterpreted_free(); break; case QPDR_ENGINE: - std::cout << "QD\n"; m_rule_properties.collect(r); m_rule_properties.check_for_negated_predicates(); m_rule_properties.check_uninterpreted_free(); From 37cb5b95974ab00efcae985c0145029c7d841e0d Mon Sep 17 00:00:00 2001 From: Matthias Schlaipfer Date: Wed, 17 Jun 2015 16:46:24 +0100 Subject: [PATCH 04/28] Fixed a bug in udoc_relation's join project An optimization was applied in too many cases and led to wrong results. Signed-off-by: Matthias Schlaipfer --- src/muz/rel/udoc_relation.cpp | 2 +- src/test/udoc_relation.cpp | 50 +++++++++++++++++++++++++++++++++++ 2 files changed, 51 insertions(+), 1 deletion(-) diff --git a/src/muz/rel/udoc_relation.cpp b/src/muz/rel/udoc_relation.cpp index 6d69550ef..587c5bfe1 100644 --- a/src/muz/rel/udoc_relation.cpp +++ b/src/muz/rel/udoc_relation.cpp @@ -1065,7 +1065,7 @@ namespace datalog { t1.get_signature().size() == joined_col_cnt && t2.get_signature().size() == joined_col_cnt) { for (unsigned i = 0; i < removed_col_cnt; ++i) { - if (removed_cols[i] != i) + if (removed_cols[i] != i || cols1[i] != cols2[i]) goto general_fn; } return alloc(join_project_and_fn); diff --git a/src/test/udoc_relation.cpp b/src/test/udoc_relation.cpp index 0545ed62c..dc88e20af 100644 --- a/src/test/udoc_relation.cpp +++ b/src/test/udoc_relation.cpp @@ -166,6 +166,7 @@ public: test_join_project(); test_join_project2(); + test_join_project3(); test_filter_neg4(false); test_filter_neg4(true); @@ -525,6 +526,55 @@ public: t2->deallocate(); } + void test_join_project3() + { + datalog::relation_signature sig; + sig.push_back(bv.mk_sort(2)); + sig.push_back(bv.mk_sort(2)); + + unsigned_vector jc1, jc2, pc; + jc1.push_back(0); + jc1.push_back(1); + jc2.push_back(1); + jc2.push_back(0); + pc.push_back(0); + pc.push_back(1); + + scoped_ptr join_project_fn; + + udoc_relation* t1 = mk_empty(sig); + { + datalog::relation_fact fact1(m); + fact1.push_back(bv.mk_numeral(rational(3), 2)); + fact1.push_back(bv.mk_numeral(rational(1), 2)); + t1->add_fact(fact1); + } + + udoc_relation *t2 = mk_empty(sig); + { + datalog::relation_fact fact1(m); + fact1.push_back(bv.mk_numeral(rational(0), 2)); + fact1.push_back(bv.mk_numeral(rational(3), 2)); + t2->add_fact(fact1); + fact1.reset(); + fact1.push_back(bv.mk_numeral(rational(1), 2)); + fact1.push_back(bv.mk_numeral(rational(3), 2)); + t2->add_fact(fact1); + } + + t1->display(std::cout << "t1:"); + t2->display(std::cout << "t2:"); + join_project_fn = p.mk_join_project_fn(*t1, *t2, jc1.size(), jc1.c_ptr(), jc2.c_ptr(), pc.size(), pc.c_ptr()); + + relation_base* t; + t = (*join_project_fn)(*t1, *t2); + t->display(std::cout << "t:"); + cr.verify_join_project(*t1, *t2, *t, jc1, jc2, pc); + t->deallocate(); + t1->deallocate(); + t2->deallocate(); + } + void test_rename() { udoc_relation* t1; // rename From baf95ce4e89d79a1e734c401b36c93cdf1eee6d3 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 17 Jun 2015 12:47:19 -0700 Subject: [PATCH 05/28] add missing copyright Signed-off-by: Nikolaj Bjorner --- .../msf/SolverFoundation.Plugin.Z3.Tests/ServiceTests.cs | 6 ++++++ .../msf/SolverFoundation.Plugin.Z3.Tests/SolverTests.cs | 6 ++++++ examples/msf/SolverFoundation.Plugin.Z3/AbortWorker.cs | 6 ++++++ examples/msf/SolverFoundation.Plugin.Z3/Utils.cs | 6 ++++++ examples/msf/SolverFoundation.Plugin.Z3/Z3BaseDirective.cs | 6 ++++++ examples/msf/SolverFoundation.Plugin.Z3/Z3BaseParams.cs | 6 ++++++ examples/msf/SolverFoundation.Plugin.Z3/Z3BaseSolver.cs | 6 ++++++ examples/msf/SolverFoundation.Plugin.Z3/Z3MILPDirective.cs | 6 ++++++ examples/msf/SolverFoundation.Plugin.Z3/Z3MILPParams.cs | 6 ++++++ examples/msf/SolverFoundation.Plugin.Z3/Z3MILPSolver.cs | 6 ++++++ examples/msf/SolverFoundation.Plugin.Z3/Z3TermDirective.cs | 6 ++++++ examples/msf/SolverFoundation.Plugin.Z3/Z3TermParams.cs | 6 ++++++ examples/msf/SolverFoundation.Plugin.Z3/Z3TermSolver.cs | 6 ++++++ examples/msf/Validator/Program.cs | 6 ++++++ scripts/mk_copyright.py | 2 +- src/api/dotnet/InterpolationContext.cs | 6 ++++++ 16 files changed, 91 insertions(+), 1 deletion(-) diff --git a/examples/msf/SolverFoundation.Plugin.Z3.Tests/ServiceTests.cs b/examples/msf/SolverFoundation.Plugin.Z3.Tests/ServiceTests.cs index 25a8e2d26..196f89245 100644 --- a/examples/msf/SolverFoundation.Plugin.Z3.Tests/ServiceTests.cs +++ b/examples/msf/SolverFoundation.Plugin.Z3.Tests/ServiceTests.cs @@ -1,3 +1,9 @@ + +/*++ +Copyright (c) 2015 Microsoft Corporation + +--*/ + using System; using System.Collections.Generic; using System.Linq; diff --git a/examples/msf/SolverFoundation.Plugin.Z3.Tests/SolverTests.cs b/examples/msf/SolverFoundation.Plugin.Z3.Tests/SolverTests.cs index c2cd0c270..4913c0f81 100644 --- a/examples/msf/SolverFoundation.Plugin.Z3.Tests/SolverTests.cs +++ b/examples/msf/SolverFoundation.Plugin.Z3.Tests/SolverTests.cs @@ -1,3 +1,9 @@ + +/*++ +Copyright (c) 2015 Microsoft Corporation + +--*/ + using System; using System.Collections.Generic; using System.Linq; diff --git a/examples/msf/SolverFoundation.Plugin.Z3/AbortWorker.cs b/examples/msf/SolverFoundation.Plugin.Z3/AbortWorker.cs index 99d6fe17a..6ce66fa8f 100644 --- a/examples/msf/SolverFoundation.Plugin.Z3/AbortWorker.cs +++ b/examples/msf/SolverFoundation.Plugin.Z3/AbortWorker.cs @@ -1,3 +1,9 @@ + +/*++ +Copyright (c) 2015 Microsoft Corporation + +--*/ + using System; using System.Collections.Generic; using System.Linq; diff --git a/examples/msf/SolverFoundation.Plugin.Z3/Utils.cs b/examples/msf/SolverFoundation.Plugin.Z3/Utils.cs index 71c8647a1..5930caee1 100644 --- a/examples/msf/SolverFoundation.Plugin.Z3/Utils.cs +++ b/examples/msf/SolverFoundation.Plugin.Z3/Utils.cs @@ -1,3 +1,9 @@ + +/*++ +Copyright (c) 2015 Microsoft Corporation + +--*/ + using System; using System.Collections.Generic; using System.Linq; diff --git a/examples/msf/SolverFoundation.Plugin.Z3/Z3BaseDirective.cs b/examples/msf/SolverFoundation.Plugin.Z3/Z3BaseDirective.cs index e1403f698..199c3fe35 100644 --- a/examples/msf/SolverFoundation.Plugin.Z3/Z3BaseDirective.cs +++ b/examples/msf/SolverFoundation.Plugin.Z3/Z3BaseDirective.cs @@ -1,3 +1,9 @@ + +/*++ +Copyright (c) 2015 Microsoft Corporation + +--*/ + using System; using System.Text; using Microsoft.SolverFoundation.Services; diff --git a/examples/msf/SolverFoundation.Plugin.Z3/Z3BaseParams.cs b/examples/msf/SolverFoundation.Plugin.Z3/Z3BaseParams.cs index 6585181ec..6d6dd74a7 100644 --- a/examples/msf/SolverFoundation.Plugin.Z3/Z3BaseParams.cs +++ b/examples/msf/SolverFoundation.Plugin.Z3/Z3BaseParams.cs @@ -1,3 +1,9 @@ + +/*++ +Copyright (c) 2015 Microsoft Corporation + +--*/ + using Microsoft.SolverFoundation.Services; using System; diff --git a/examples/msf/SolverFoundation.Plugin.Z3/Z3BaseSolver.cs b/examples/msf/SolverFoundation.Plugin.Z3/Z3BaseSolver.cs index 54e3893f0..af8bc92a2 100644 --- a/examples/msf/SolverFoundation.Plugin.Z3/Z3BaseSolver.cs +++ b/examples/msf/SolverFoundation.Plugin.Z3/Z3BaseSolver.cs @@ -1,3 +1,9 @@ + +/*++ +Copyright (c) 2015 Microsoft Corporation + +--*/ + using System; using System.Collections.Generic; using System.Threading; diff --git a/examples/msf/SolverFoundation.Plugin.Z3/Z3MILPDirective.cs b/examples/msf/SolverFoundation.Plugin.Z3/Z3MILPDirective.cs index 69f9ff6c1..4d6745634 100644 --- a/examples/msf/SolverFoundation.Plugin.Z3/Z3MILPDirective.cs +++ b/examples/msf/SolverFoundation.Plugin.Z3/Z3MILPDirective.cs @@ -1,3 +1,9 @@ + +/*++ +Copyright (c) 2015 Microsoft Corporation + +--*/ + using Microsoft.SolverFoundation.Services; using System; diff --git a/examples/msf/SolverFoundation.Plugin.Z3/Z3MILPParams.cs b/examples/msf/SolverFoundation.Plugin.Z3/Z3MILPParams.cs index 38bd9040a..d01b07725 100644 --- a/examples/msf/SolverFoundation.Plugin.Z3/Z3MILPParams.cs +++ b/examples/msf/SolverFoundation.Plugin.Z3/Z3MILPParams.cs @@ -1,3 +1,9 @@ + +/*++ +Copyright (c) 2015 Microsoft Corporation + +--*/ + using Microsoft.SolverFoundation.Services; using System; diff --git a/examples/msf/SolverFoundation.Plugin.Z3/Z3MILPSolver.cs b/examples/msf/SolverFoundation.Plugin.Z3/Z3MILPSolver.cs index b31f6de97..f3a8f9f2c 100644 --- a/examples/msf/SolverFoundation.Plugin.Z3/Z3MILPSolver.cs +++ b/examples/msf/SolverFoundation.Plugin.Z3/Z3MILPSolver.cs @@ -1,3 +1,9 @@ + +/*++ +Copyright (c) 2015 Microsoft Corporation + +--*/ + using System; using System.Collections.Generic; using System.Diagnostics; diff --git a/examples/msf/SolverFoundation.Plugin.Z3/Z3TermDirective.cs b/examples/msf/SolverFoundation.Plugin.Z3/Z3TermDirective.cs index 12dcb6e84..ff9e4181a 100644 --- a/examples/msf/SolverFoundation.Plugin.Z3/Z3TermDirective.cs +++ b/examples/msf/SolverFoundation.Plugin.Z3/Z3TermDirective.cs @@ -1,3 +1,9 @@ + +/*++ +Copyright (c) 2015 Microsoft Corporation + +--*/ + using Microsoft.SolverFoundation.Services; using System; diff --git a/examples/msf/SolverFoundation.Plugin.Z3/Z3TermParams.cs b/examples/msf/SolverFoundation.Plugin.Z3/Z3TermParams.cs index 48a90afe1..283bc9362 100644 --- a/examples/msf/SolverFoundation.Plugin.Z3/Z3TermParams.cs +++ b/examples/msf/SolverFoundation.Plugin.Z3/Z3TermParams.cs @@ -1,3 +1,9 @@ + +/*++ +Copyright (c) 2015 Microsoft Corporation + +--*/ + using Microsoft.SolverFoundation.Services; using System; diff --git a/examples/msf/SolverFoundation.Plugin.Z3/Z3TermSolver.cs b/examples/msf/SolverFoundation.Plugin.Z3/Z3TermSolver.cs index 3317b9a4d..530df3394 100644 --- a/examples/msf/SolverFoundation.Plugin.Z3/Z3TermSolver.cs +++ b/examples/msf/SolverFoundation.Plugin.Z3/Z3TermSolver.cs @@ -1,3 +1,9 @@ + +/*++ +Copyright (c) 2015 Microsoft Corporation + +--*/ + using System; using System.Threading; using System.Globalization; diff --git a/examples/msf/Validator/Program.cs b/examples/msf/Validator/Program.cs index 758c65c78..8afb28af5 100644 --- a/examples/msf/Validator/Program.cs +++ b/examples/msf/Validator/Program.cs @@ -1,3 +1,9 @@ + +/*++ +Copyright (c) 2015 Microsoft Corporation + +--*/ + using System; using System.IO; using System.Linq; diff --git a/scripts/mk_copyright.py b/scripts/mk_copyright.py index 5ac185de0..4d774cb96 100644 --- a/scripts/mk_copyright.py +++ b/scripts/mk_copyright.py @@ -47,7 +47,7 @@ def add_cr(file): def add_missing_cr(dir): for root, dirs, files in os.walk(dir): for f in files: - if f.endswith('.cpp') or f.endswith('.h') or f.endswith('.c'): + if f.endswith('.cpp') or f.endswith('.h') or f.endswith('.c') or f.endswith('.cs'): path = "%s\\%s" % (root, f) if not has_cr(path): print "Missing CR for %s" % path diff --git a/src/api/dotnet/InterpolationContext.cs b/src/api/dotnet/InterpolationContext.cs index e6e258b9a..595023b69 100644 --- a/src/api/dotnet/InterpolationContext.cs +++ b/src/api/dotnet/InterpolationContext.cs @@ -1,3 +1,9 @@ + +/*++ +Copyright (c) 2015 Microsoft Corporation + +--*/ + using System; using System.Collections.Generic; using System.Linq; From 1bdedec9200afb0207eaf55cca8f3c5808311042 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 17 Jun 2015 12:48:16 -0700 Subject: [PATCH 06/28] add missing copyright Signed-off-by: Nikolaj Bjorner --- src/api/python/z3test.py | 7 +++++++ src/api/python/z3types.py | 8 ++++++++ src/api/python/z3util.py | 7 +++++++ 3 files changed, 22 insertions(+) diff --git a/src/api/python/z3test.py b/src/api/python/z3test.py index 9b894d7ad..38939cebf 100644 --- a/src/api/python/z3test.py +++ b/src/api/python/z3test.py @@ -1,3 +1,10 @@ +############################################ +# Copyright (c) 2012 Microsoft Corporation +# +# Z3 Python interface +# +# Author: Leonardo de Moura (leonardo) +############################################ import z3, doctest r = doctest.testmod(z3) diff --git a/src/api/python/z3types.py b/src/api/python/z3types.py index e01b78238..44b19d33a 100644 --- a/src/api/python/z3types.py +++ b/src/api/python/z3types.py @@ -1,3 +1,11 @@ +############################################ +# Copyright (c) 2012 Microsoft Corporation +# +# Z3 Python interface +# +# Author: Leonardo de Moura (leonardo) +############################################ + import ctypes, z3core class Z3Exception(Exception): diff --git a/src/api/python/z3util.py b/src/api/python/z3util.py index e0e9aba32..38e406723 100644 --- a/src/api/python/z3util.py +++ b/src/api/python/z3util.py @@ -1,3 +1,10 @@ +############################################ +# Copyright (c) 2012 Microsoft Corporation +# +# Z3 Python interface +# +# Author: Leonardo de Moura (leonardo) +############################################ """ Usage: import common_z3 as CM_Z3 From 22c0a593e7ab4fe219ac1a76b685a20d0dee40b4 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 17 Jun 2015 17:30:10 -0700 Subject: [PATCH 07/28] deal with unit test failure cases, fixes #132 #133 Signed-off-by: Nikolaj Bjorner --- src/muz/fp/datalog_parser.cpp | 3 ++- src/test/dl_context.cpp | 3 ++- src/test/dl_query.cpp | 2 +- src/test/pdr.cpp | 6 +++--- 4 files changed, 8 insertions(+), 6 deletions(-) diff --git a/src/muz/fp/datalog_parser.cpp b/src/muz/fp/datalog_parser.cpp index c6f594d4e..f1080676d 100644 --- a/src/muz/fp/datalog_parser.cpp +++ b/src/muz/fp/datalog_parser.cpp @@ -101,9 +101,10 @@ public: resize_data(0); #if _WINDOWS errno_t err = fopen_s(&m_file, fname, "rb"); - m_ok = err == 0; + m_ok = (m_file != NULL) && (err == 0); #else m_file = fopen(fname, "rb"); + m_ok = (m_file != NULL); #endif } ~line_reader() { diff --git a/src/test/dl_context.cpp b/src/test/dl_context.cpp index 09db4bde2..deb1300ea 100644 --- a/src/test/dl_context.cpp +++ b/src/test/dl_context.cpp @@ -62,8 +62,9 @@ void dl_context_saturate_file(params_ref & params, const char * f) { ctx.updt_params(params); datalog::parser * parser = datalog::parser::create(ctx, m); - if (!parser->parse_file(f)) { + if (!parser || !parser->parse_file(f)) { warning_msg("ERROR: failed to parse file"); + dealloc(parser); return; } dealloc(parser); diff --git a/src/test/dl_query.cpp b/src/test/dl_query.cpp index 9e0f285c7..ab5141b18 100644 --- a/src/test/dl_query.cpp +++ b/src/test/dl_query.cpp @@ -64,7 +64,7 @@ void dl_query_test(ast_manager & m, smt_params & fparams, params_ref& params, ctx_q.updt_params(params); { parser* p = parser::create(ctx_q,m); - bool ok = p->parse_file(problem_file); + bool ok = p && p->parse_file(problem_file); dealloc(p); if (!ok) { std::cout << "Could not parse: " << problem_file << "\n"; diff --git a/src/test/pdr.cpp b/src/test/pdr.cpp index a1410b482..d95a55a24 100644 --- a/src/test/pdr.cpp +++ b/src/test/pdr.cpp @@ -27,7 +27,7 @@ struct test_model_search { }; ast_manager m; - smt_params smt_params; + smt_params m_smt_params; fixedpoint_params fp_params; context ctx; manager pm; @@ -40,8 +40,8 @@ struct test_model_search { test_model_search(): - ctx(smt_params, fp_params, m), - pm(smt_params, 10, m), + ctx(m_smt_params, fp_params, m), + pm(m_smt_params, 10, m), fn(m), initt(fn), pt(ctx, pm, fn), From 0518e69d2ae8f64293f75df7ea3e24c462fd2bf5 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 21 Jun 2015 01:54:52 -0700 Subject: [PATCH 08/28] isolate inc_sat_solver Signed-off-by: Nikolaj Bjorner --- scripts/mk_project.py | 7 ++----- src/{opt => sat/sat_solver}/inc_sat_solver.cpp | 1 - src/{opt => sat/sat_solver}/inc_sat_solver.h | 0 3 files changed, 2 insertions(+), 6 deletions(-) rename src/{opt => sat/sat_solver}/inc_sat_solver.cpp (99%) rename src/{opt => sat/sat_solver}/inc_sat_solver.h (100%) diff --git a/scripts/mk_project.py b/scripts/mk_project.py index b9641c869..719ffc703 100644 --- a/scripts/mk_project.py +++ b/scripts/mk_project.py @@ -74,11 +74,8 @@ def init_project_def(): add_lib('ufbv_tactic', ['normal_forms', 'core_tactics', 'macros', 'smt_tactic', 'rewriter'], 'tactic/ufbv') add_lib('portfolio', ['smtlogic_tactics', 'ufbv_tactic', 'fpa_tactics', 'aig_tactic', 'fp', 'qe','sls_tactic', 'subpaving_tactic'], 'tactic/portfolio') add_lib('smtparser', ['portfolio'], 'parsers/smt') - add_lib('opt', ['smt', 'smtlogic_tactics', 'sls_tactic'], 'opt') -# add_dll('foci2', ['util'], 'interp/foci2stub', -# dll_name='foci2', -# export_files=['foci2stub.cpp']) -# add_lib('interp', ['solver','foci2']) + add_lib('sat_solver', ['solver', 'core_tactics', 'aig_tactic', 'bv_tactics', 'arith_tactics', 'sat_tactic'], 'sat/sat_solver') + add_lib('opt', ['smt', 'smtlogic_tactics', 'sls_tactic', 'sat_solver'], 'opt') API_files = ['z3_api.h', 'z3_algebraic.h', 'z3_polynomial.h', 'z3_rcf.h', 'z3_interp.h', 'z3_fpa.h'] add_lib('api', ['portfolio', 'user_plugin', 'smtparser', 'realclosure', 'interp', 'opt'], includes2install=['z3.h', 'z3_v1.h', 'z3_macros.h'] + API_files) diff --git a/src/opt/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp similarity index 99% rename from src/opt/inc_sat_solver.cpp rename to src/sat/sat_solver/inc_sat_solver.cpp index fb8172373..5111a6cc2 100644 --- a/src/opt/inc_sat_solver.cpp +++ b/src/sat/sat_solver/inc_sat_solver.cpp @@ -21,7 +21,6 @@ Notes: #include "tactical.h" #include "sat_solver.h" #include "tactic2solver.h" -#include "nnf_tactic.h" #include "aig_tactic.h" #include "propagate_values_tactic.h" #include "max_bv_sharing_tactic.h" diff --git a/src/opt/inc_sat_solver.h b/src/sat/sat_solver/inc_sat_solver.h similarity index 100% rename from src/opt/inc_sat_solver.h rename to src/sat/sat_solver/inc_sat_solver.h From 5aee077d55f27738925d7d038951b333eade9ea6 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 21 Jun 2015 02:23:56 -0700 Subject: [PATCH 09/28] enable incremental sat for QF_BV Signed-off-by: Nikolaj Bjorner --- scripts/mk_project.py | 4 ++-- src/sat/sat_solver/inc_sat_solver.cpp | 2 +- src/sat/sat_solver/inc_sat_solver.h | 2 +- src/solver/combined_solver.h | 1 + src/tactic/portfolio/smt_strategic_solver.cpp | 10 +++++++++- 5 files changed, 14 insertions(+), 5 deletions(-) diff --git a/scripts/mk_project.py b/scripts/mk_project.py index 719ffc703..5645e3af1 100644 --- a/scripts/mk_project.py +++ b/scripts/mk_project.py @@ -72,9 +72,9 @@ def init_project_def(): add_lib('smtlogic_tactics', ['arith_tactics', 'bv_tactics', 'nlsat_tactic', 'smt_tactic', 'aig_tactic', 'fp', 'muz','qe','nlsat_smt_tactic'], 'tactic/smtlogics') add_lib('fpa_tactics', ['fpa', 'core_tactics', 'bv_tactics', 'sat_tactic', 'smt_tactic', 'arith_tactics', 'smtlogic_tactics'], 'tactic/fpa') add_lib('ufbv_tactic', ['normal_forms', 'core_tactics', 'macros', 'smt_tactic', 'rewriter'], 'tactic/ufbv') - add_lib('portfolio', ['smtlogic_tactics', 'ufbv_tactic', 'fpa_tactics', 'aig_tactic', 'fp', 'qe','sls_tactic', 'subpaving_tactic'], 'tactic/portfolio') - add_lib('smtparser', ['portfolio'], 'parsers/smt') add_lib('sat_solver', ['solver', 'core_tactics', 'aig_tactic', 'bv_tactics', 'arith_tactics', 'sat_tactic'], 'sat/sat_solver') + add_lib('portfolio', ['smtlogic_tactics', 'sat_solver', 'ufbv_tactic', 'fpa_tactics', 'aig_tactic', 'fp', 'qe','sls_tactic', 'subpaving_tactic'], 'tactic/portfolio') + add_lib('smtparser', ['portfolio'], 'parsers/smt') add_lib('opt', ['smt', 'smtlogic_tactics', 'sls_tactic', 'sat_solver'], 'opt') API_files = ['z3_api.h', 'z3_algebraic.h', 'z3_polynomial.h', 'z3_rcf.h', 'z3_interp.h', 'z3_fpa.h'] add_lib('api', ['portfolio', 'user_plugin', 'smtparser', 'realclosure', 'interp', 'opt'], diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp index 5111a6cc2..99dd24dc7 100644 --- a/src/sat/sat_solver/inc_sat_solver.cpp +++ b/src/sat/sat_solver/inc_sat_solver.cpp @@ -427,7 +427,7 @@ private: }; -solver* mk_inc_sat_solver(ast_manager& m, params_ref& p) { +solver* mk_inc_sat_solver(ast_manager& m, params_ref const& p) { return alloc(inc_sat_solver, m, p); } diff --git a/src/sat/sat_solver/inc_sat_solver.h b/src/sat/sat_solver/inc_sat_solver.h index 8bb4c288a..53d4f950e 100644 --- a/src/sat/sat_solver/inc_sat_solver.h +++ b/src/sat/sat_solver/inc_sat_solver.h @@ -22,7 +22,7 @@ Notes: #include "solver.h" -solver* mk_inc_sat_solver(ast_manager& m, params_ref& p); +solver* mk_inc_sat_solver(ast_manager& m, params_ref const& p); void set_soft_inc_sat(solver* s, unsigned sz, expr*const* soft, rational const* weights); diff --git a/src/solver/combined_solver.h b/src/solver/combined_solver.h index 2ccace7f0..f3c3841d3 100644 --- a/src/solver/combined_solver.h +++ b/src/solver/combined_solver.h @@ -29,4 +29,5 @@ class solver_factory; solver * mk_combined_solver(solver * s1, solver * s2, params_ref const & p); solver_factory * mk_combined_solver_factory(solver_factory * f1, solver_factory * f2); + #endif diff --git a/src/tactic/portfolio/smt_strategic_solver.cpp b/src/tactic/portfolio/smt_strategic_solver.cpp index 687771a30..dee045d6f 100644 --- a/src/tactic/portfolio/smt_strategic_solver.cpp +++ b/src/tactic/portfolio/smt_strategic_solver.cpp @@ -37,6 +37,7 @@ Notes: #include"qfufnra_tactic.h" #include"horn_tactic.h" #include"smt_solver.h" +#include"inc_sat_solver.h" tactic * mk_tactic_for_logic(ast_manager & m, params_ref const & p, symbol const & logic) { if (logic=="QF_UF") @@ -91,6 +92,12 @@ tactic * mk_tactic_for_logic(ast_manager & m, params_ref const & p, symbol const return mk_default_tactic(m, p); } +solver* mk_solver_for_logic(ast_manager & m, params_ref const & p, symbol const& logic) { + if (logic == "QF_BV") + return mk_inc_sat_solver(m, p); + return mk_smt_solver(m, p, logic); +} + class smt_strategic_solver_factory : public solver_factory { symbol m_logic; public: @@ -105,7 +112,8 @@ public: l = logic; tactic * t = mk_tactic_for_logic(m, p, l); return mk_combined_solver(mk_tactic2solver(m, t, p, proofs_enabled, models_enabled, unsat_core_enabled, l), - mk_smt_solver(m, p, l), + mk_solver_for_logic(m, p, l), + //mk_smt_solver(m, p, l), p); } }; From 45d2ffa38c04b0711d211c56fddd24ef03bb2b4e Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 21 Jun 2015 02:25:02 -0700 Subject: [PATCH 10/28] hide new behavior until tested Signed-off-by: Nikolaj Bjorner --- src/tactic/portfolio/smt_strategic_solver.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/tactic/portfolio/smt_strategic_solver.cpp b/src/tactic/portfolio/smt_strategic_solver.cpp index dee045d6f..27d7433e8 100644 --- a/src/tactic/portfolio/smt_strategic_solver.cpp +++ b/src/tactic/portfolio/smt_strategic_solver.cpp @@ -112,8 +112,8 @@ public: l = logic; tactic * t = mk_tactic_for_logic(m, p, l); return mk_combined_solver(mk_tactic2solver(m, t, p, proofs_enabled, models_enabled, unsat_core_enabled, l), - mk_solver_for_logic(m, p, l), - //mk_smt_solver(m, p, l), + //mk_solver_for_logic(m, p, l), + mk_smt_solver(m, p, l), p); } }; From e7385d60fbfb5f9fd1ea862f10acedb56327c81c Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 21 Jun 2015 13:49:15 -0700 Subject: [PATCH 11/28] fixes to githup issue #133 and stackoverflow reported bug on assertion violation in poly_simplifier_plugin Signed-off-by: Nikolaj Bjorner --- src/ast/simplifier/poly_simplifier_plugin.cpp | 10 ++++++++-- src/opt/opt_solver.cpp | 4 +++- 2 files changed, 11 insertions(+), 3 deletions(-) diff --git a/src/ast/simplifier/poly_simplifier_plugin.cpp b/src/ast/simplifier/poly_simplifier_plugin.cpp index d64123e7b..c5dc275fd 100644 --- a/src/ast/simplifier/poly_simplifier_plugin.cpp +++ b/src/ast/simplifier/poly_simplifier_plugin.cpp @@ -69,14 +69,20 @@ expr * poly_simplifier_plugin::mk_mul(unsigned num_args, expr * const * args) { } expr * poly_simplifier_plugin::mk_mul(numeral const & c, expr * body) { - numeral c_prime; + numeral c_prime, d; c_prime = norm(c); if (c_prime.is_zero()) return 0; if (body == 0) return mk_numeral(c_prime); if (c_prime.is_one()) - return body; + return body; + if (is_numeral(body, d)) { + c_prime = norm(c_prime*d); + if (c_prime.is_zero()) + return 0; + return mk_numeral(c_prime); + } set_curr_sort(body); expr * args[2] = { mk_numeral(c_prime), body }; return mk_mul(2, args); diff --git a/src/opt/opt_solver.cpp b/src/opt/opt_solver.cpp index dcbbc3fae..bf7a39424 100644 --- a/src/opt/opt_solver.cpp +++ b/src/opt/opt_solver.cpp @@ -46,7 +46,9 @@ namespace opt { m_dump_benchmarks(false), m_first(true) { m_params.updt_params(p); - m_params.m_relevancy_lvl = 0; + if (m_params.m_case_split_strategy == CS_ACTIVITY_DELAY_NEW) { + m_params.m_relevancy_lvl = 0; + } } unsigned opt_solver::m_dump_count = 0; From 158a5dd2db0fd51b274c68606fa6bad0e4ae5998 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 22 Jun 2015 07:45:40 +0200 Subject: [PATCH 12/28] add count of memory allocations and way to limit allocations globally. Fix purification in nlsat_smt to fix regressions on QF_UFNRA Signed-off-by: Nikolaj Bjorner --- src/api/api_solver.cpp | 5 +-- src/cmd_context/cmd_context.cpp | 3 +- src/cmd_context/tactic_cmds.cpp | 5 +-- src/muz/base/dl_context.cpp | 5 +-- src/muz/fp/dl_cmds.cpp | 4 -- src/opt/opt_context.cpp | 5 +-- src/tactic/nlsat_smt/nl_purify_tactic.cpp | 16 +++++-- src/util/env_params.cpp | 2 + src/util/error_codes.h | 1 + src/util/memory_manager.cpp | 54 ++++++++++++++++++++--- src/util/memory_manager.h | 7 +++ src/util/statistics.cpp | 10 +++++ src/util/statistics.h | 2 + src/util/z3_exception.cpp | 1 + 14 files changed, 88 insertions(+), 32 deletions(-) diff --git a/src/api/api_solver.cpp b/src/api/api_solver.cpp index ca15762f5..50b0c6e22 100644 --- a/src/api/api_solver.cpp +++ b/src/api/api_solver.cpp @@ -355,10 +355,7 @@ extern "C" { init_solver(c, s); Z3_stats_ref * st = alloc(Z3_stats_ref); to_solver_ref(s)->collect_statistics(st->m_stats); - unsigned long long max_mem = memory::get_max_used_memory(); - unsigned long long mem = memory::get_allocation_size(); - st->m_stats.update("max memory", static_cast(max_mem)/(1024.0*1024.0)); - st->m_stats.update("memory", static_cast(mem)/(1024.0*1024.0)); + get_memory_statistics(st->m_stats); mk_c(c)->save_object(st); Z3_stats r = of_stats(st); RETURN_Z3(r); diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp index c8d5e8cab..3becba284 100644 --- a/src/cmd_context/cmd_context.cpp +++ b/src/cmd_context/cmd_context.cpp @@ -1624,11 +1624,10 @@ void cmd_context::set_solver_factory(solver_factory * f) { void cmd_context::display_statistics(bool show_total_time, double total_time) { statistics st; - unsigned long long mem = memory::get_max_used_memory(); if (show_total_time) st.update("total time", total_time); st.update("time", get_seconds()); - st.update("memory", static_cast(mem)/static_cast(1024*1024)); + get_memory_statistics(st); if (m_check_sat_result) { m_check_sat_result->collect_statistics(st); } diff --git a/src/cmd_context/tactic_cmds.cpp b/src/cmd_context/tactic_cmds.cpp index 75d56928e..9d4c18262 100644 --- a/src/cmd_context/tactic_cmds.cpp +++ b/src/cmd_context/tactic_cmds.cpp @@ -157,11 +157,8 @@ public: void display_statistics(cmd_context & ctx, tactic * t) { statistics stats; - unsigned long long max_mem = memory::get_max_used_memory(); - unsigned long long mem = memory::get_allocation_size(); + get_memory_statistics(stats); stats.update("time", ctx.get_seconds()); - stats.update("memory", static_cast(mem)/static_cast(1024*1024)); - stats.update("max memory", static_cast(max_mem)/static_cast(1024*1024)); t->collect_statistics(stats); stats.display_smt2(ctx.regular_stream()); } diff --git a/src/muz/base/dl_context.cpp b/src/muz/base/dl_context.cpp index 3555e5bdc..9fb597600 100644 --- a/src/muz/base/dl_context.cpp +++ b/src/muz/base/dl_context.cpp @@ -945,10 +945,7 @@ namespace datalog { if (m_engine) { m_engine->collect_statistics(st); } - unsigned long long max_mem = memory::get_max_used_memory(); - unsigned long long mem = memory::get_allocation_size(); - st.update("max memory", static_cast(max_mem)/(1024.0*1024.0)); - st.update("memory", static_cast(mem)/(1024.0*1024.0)); + get_memory_statistics(st); } diff --git a/src/muz/fp/dl_cmds.cpp b/src/muz/fp/dl_cmds.cpp index 66f1c6d38..a583d7a26 100644 --- a/src/muz/fp/dl_cmds.cpp +++ b/src/muz/fp/dl_cmds.cpp @@ -338,12 +338,8 @@ private: if (m_dl_ctx->get_params().print_statistics()) { statistics st; datalog::context& dlctx = m_dl_ctx->dlctx(); - unsigned long long max_mem = memory::get_max_used_memory(); - unsigned long long mem = memory::get_allocation_size(); dlctx.collect_statistics(st); st.update("time", ctx.get_seconds()); - st.update("memory", static_cast(mem)/static_cast(1024*1024)); - st.update("max-memory", static_cast(max_mem)/static_cast(1024*1024)); st.display_smt2(ctx.regular_stream()); } } diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index 6fb4ef542..2a6265fc4 100644 --- a/src/opt/opt_context.cpp +++ b/src/opt/opt_context.cpp @@ -1188,10 +1188,7 @@ namespace opt { for (; it != end; ++it) { it->m_value->collect_statistics(stats); } - unsigned long long max_mem = memory::get_max_used_memory(); - unsigned long long mem = memory::get_allocation_size(); - stats.update("memory", static_cast(mem)/static_cast(1024*1024)); - stats.update("max memory", static_cast(max_mem)/static_cast(1024*1024)); + get_memory_statistics(stats); } void context::collect_param_descrs(param_descrs & r) { diff --git a/src/tactic/nlsat_smt/nl_purify_tactic.cpp b/src/tactic/nlsat_smt/nl_purify_tactic.cpp index 91c462486..be52bb477 100644 --- a/src/tactic/nlsat_smt/nl_purify_tactic.cpp +++ b/src/tactic/nlsat_smt/nl_purify_tactic.cpp @@ -203,22 +203,32 @@ public: return BR_FAILED; } + // (+ (f x) y) + // (f (+ x y)) + // + bool is_arith_op(expr* e) { + return is_app(e) && to_app(e)->get_family_id() == u().get_family_id(); + } br_status reduce_app_real(func_decl * f, unsigned num, expr* const* args, expr_ref& result, proof_ref & pr) { bool has_interface = false; + bool is_arith = false; if (f->get_family_id() == u().get_family_id()) { switch (f->get_decl_kind()) { case OP_NUM: case OP_IRRATIONAL_ALGEBRAIC_NUM: - case OP_ADD: case OP_MUL: case OP_SUB: - case OP_UMINUS: case OP_ABS: case OP_POWER: return BR_FAILED; default: + is_arith = true; break; } } m_args.reset(); for (unsigned i = 0; i < num; ++i) { expr* arg = args[i]; - if (u().is_real(arg)) { + if (is_arith && !is_arith_op(arg)) { + has_interface = true; + m_args.push_back(mk_interface_var(arg)); + } + else if (!is_arith && u().is_real(arg)) { has_interface = true; m_args.push_back(mk_interface_var(arg)); } diff --git a/src/util/env_params.cpp b/src/util/env_params.cpp index b01a1c250..6748598bf 100644 --- a/src/util/env_params.cpp +++ b/src/util/env_params.cpp @@ -27,6 +27,7 @@ void env_params::updt_params() { set_verbosity_level(p.get_uint("verbose", get_verbosity_level())); enable_warning_messages(p.get_bool("warning", true)); memory::set_max_size(megabytes_to_bytes(p.get_uint("memory_max_size", 0))); + memory::set_max_alloc_count(p.get_uint("memory_max_alloc_count", 0)); memory::set_high_watermark(p.get_uint("memory_high_watermark", 0)); } @@ -34,5 +35,6 @@ void env_params::collect_param_descrs(param_descrs & d) { d.insert("verbose", CPK_UINT, "be verbose, where the value is the verbosity level", "0"); d.insert("warning", CPK_BOOL, "enable/disable warning messages", "true"); d.insert("memory_max_size", CPK_UINT, "set hard upper limit for memory consumption (in megabytes), if 0 then there is no limit", "0"); + d.insert("memory_max_alloc_count", CPK_UINT, "set hard upper limit for memory allocations, if 0 then there is no limit", "0"); d.insert("memory_high_watermark", CPK_UINT, "set high watermark for memory consumption (in megabytes), if 0 then there is no limit", "0"); } diff --git a/src/util/error_codes.h b/src/util/error_codes.h index 4afc9a38d..32d760470 100644 --- a/src/util/error_codes.h +++ b/src/util/error_codes.h @@ -32,6 +32,7 @@ Revision History: #define ERR_INTERNAL_FATAL 110 #define ERR_TYPE_CHECK 111 #define ERR_UNKNOWN_RESULT 112 +#define ERR_ALLOC_EXCEEDED 113 #endif /* _ERROR_CODES_H_ */ diff --git a/src/util/memory_manager.cpp b/src/util/memory_manager.cpp index 7539e7ba3..88bd6b92e 100644 --- a/src/util/memory_manager.cpp +++ b/src/util/memory_manager.cpp @@ -33,12 +33,17 @@ void mem_finalize(); out_of_memory_error::out_of_memory_error():z3_error(ERR_MEMOUT) { } +exceeded_memory_allocations::exceeded_memory_allocations():z3_error(ERR_ALLOC_EXCEEDED) { +} + static volatile bool g_memory_out_of_memory = false; static bool g_memory_initialized = false; static long long g_memory_alloc_size = 0; static long long g_memory_max_size = 0; static long long g_memory_max_used_size = 0; static long long g_memory_watermark = 0; +static long long g_memory_alloc_count = 0; +static long long g_memory_max_alloc_count = 0; static bool g_exit_when_out_of_memory = false; static char const * g_out_of_memory_msg = "ERROR: out of memory"; static volatile bool g_memory_fully_initialized = false; @@ -52,9 +57,7 @@ void memory::exit_when_out_of_memory(bool flag, char const * msg) { static void throw_out_of_memory() { #pragma omp critical (z3_memory_manager) { - if (!g_memory_out_of_memory) { - g_memory_out_of_memory = true; - } + g_memory_out_of_memory = true; } if (g_exit_when_out_of_memory) { std::cerr << g_out_of_memory_msg << "\n"; @@ -65,12 +68,18 @@ static void throw_out_of_memory() { } } +static void throw_alloc_counts_exceeded() { + throw exceeded_memory_allocations(); +} + + #ifdef PROFILE_MEMORY static unsigned g_synch_counter = 0; class mem_usage_report { public: ~mem_usage_report() { std::cerr << "(memory :max " << g_memory_max_used_size + << " :allocs " << g_memory_alloc_count << " :final " << g_memory_alloc_size << " :synch " << g_synch_counter << ")" << std::endl; } @@ -129,11 +138,17 @@ bool memory::above_high_watermark() { return r; } +// The following methods are only safe to invoke at +// initialization time, that is, before threads are created. + void memory::set_max_size(size_t max_size) { - // This method is only safe to invoke at initialization time, that is, before the threads are created. g_memory_max_size = max_size; } +void memory::set_max_alloc_count(size_t max_count) { + g_memory_max_alloc_count = max_count; +} + static bool g_finalizing = false; void memory::finalize() { @@ -165,6 +180,11 @@ unsigned long long memory::get_max_used_memory() { return r; } +unsigned long long memory::get_allocation_count() { + return g_memory_alloc_count; +} + + void memory::display_max_usage(std::ostream & os) { unsigned long long mem = get_max_used_memory(); os << "max. heap size: " @@ -207,9 +227,11 @@ void * memory::allocate(char const* file, int line, char const* obj, size_t s) { #ifdef _WINDOWS // Actually this is VS specific instead of Windows specific. __declspec(thread) long long g_memory_thread_alloc_size = 0; +__declspec(thread) long long g_memory_thread_alloc_count = 0; #else // GCC style __thread long long g_memory_thread_alloc_size = 0; +__thread long long g_memory_thread_alloc_count = 0; #endif static void synchronize_counters(bool allocating) { @@ -218,18 +240,25 @@ static void synchronize_counters(bool allocating) { #endif bool out_of_mem = false; + bool counts_exceeded = false; #pragma omp critical (z3_memory_manager) { g_memory_alloc_size += g_memory_thread_alloc_size; + g_memory_alloc_count += g_memory_thread_alloc_count; if (g_memory_alloc_size > g_memory_max_used_size) g_memory_max_used_size = g_memory_alloc_size; if (g_memory_max_size != 0 && g_memory_alloc_size > g_memory_max_size) out_of_mem = true; + if (g_memory_max_alloc_count != 0 && g_memory_alloc_count > g_memory_max_alloc_count) + counts_exceeded = true; } g_memory_thread_alloc_size = 0; if (out_of_mem && allocating) { throw_out_of_memory(); } + if (counts_exceeded && allocating) { + throw_alloc_counts_exceeded(); + } } void memory::deallocate(void * p) { @@ -252,6 +281,7 @@ void * memory::allocate(size_t s) { throw_out_of_memory(); *(static_cast(r)) = s; g_memory_thread_alloc_size += s; + g_memory_thread_alloc_count += 1; if (g_memory_thread_alloc_size > SYNCH_THRESHOLD) { synchronize_counters(true); } @@ -265,6 +295,7 @@ void* memory::reallocate(void *p, size_t s) { s = s + sizeof(size_t); // we allocate an extra field! g_memory_thread_alloc_size += s - sz; + g_memory_thread_alloc_count += 1; if (g_memory_thread_alloc_size > SYNCH_THRESHOLD) { synchronize_counters(true); } @@ -299,17 +330,22 @@ void * memory::allocate(size_t s) { if (s == 0) return 0; s = s + sizeof(size_t); // we allocate an extra field! - bool out_of_mem = false; + bool out_of_mem = false, counts_exceeded = false; #pragma omp critical (z3_memory_manager) { g_memory_alloc_size += s; + g_memory_alloc_count += 1; if (g_memory_alloc_size > g_memory_max_used_size) g_memory_max_used_size = g_memory_alloc_size; if (g_memory_max_size != 0 && g_memory_alloc_size > g_memory_max_size) out_of_mem = true; + if (g_memory_max_alloc_count != 0 && g_memory_alloc_count > g_memory_max_alloc_count) + counts_exceeded = true; } if (out_of_mem) throw_out_of_memory(); + if (counts_exceeded) + throw_alloc_counts_exceeded(); void * r = malloc(s); if (r == 0) throw_out_of_memory(); @@ -322,18 +358,22 @@ void* memory::reallocate(void *p, size_t s) { size_t sz = *sz_p; void * real_p = reinterpret_cast(sz_p); s = s + sizeof(size_t); // we allocate an extra field! - bool out_of_mem = false; + bool out_of_mem = false, counts_exceeded = false; #pragma omp critical (z3_memory_manager) { g_memory_alloc_size += s - sz; + g_memory_alloc_count += 1; if (g_memory_alloc_size > g_memory_max_used_size) g_memory_max_used_size = g_memory_alloc_size; if (g_memory_max_size != 0 && g_memory_alloc_size > g_memory_max_size) out_of_mem = true; + if (g_memory_max_alloc_count != 0 && g_memory_alloc_count > g_memory_max_alloc_count) + counts_exceeded = true; } if (out_of_mem) throw_out_of_memory(); - + if (counts_exceeded) + throw_alloc_counts_exceeded(); void *r = realloc(real_p, s); if (r == 0) throw_out_of_memory(); diff --git a/src/util/memory_manager.h b/src/util/memory_manager.h index bd912828e..94865fa90 100644 --- a/src/util/memory_manager.h +++ b/src/util/memory_manager.h @@ -46,6 +46,11 @@ public: out_of_memory_error(); }; +class exceeded_memory_allocations : public z3_error { +public: + exceeded_memory_allocations(); +}; + class memory { public: static bool is_out_of_memory(); @@ -53,6 +58,7 @@ public: static void set_high_watermark(size_t watermak); static bool above_high_watermark(); static void set_max_size(size_t max_size); + static void set_max_alloc_count(size_t max_count); static void finalize(); static void display_max_usage(std::ostream& os); static void display_i_max_usage(std::ostream& os); @@ -65,6 +71,7 @@ public: #endif static unsigned long long get_allocation_size(); static unsigned long long get_max_used_memory(); + static unsigned long long get_allocation_count(); // temporary hack to avoid out-of-memory crash in z3.exe static void exit_when_out_of_memory(bool flag, char const * msg); }; diff --git a/src/util/statistics.cpp b/src/util/statistics.cpp index 24d17ddfa..6e50fd4a8 100644 --- a/src/util/statistics.cpp +++ b/src/util/statistics.cpp @@ -226,3 +226,13 @@ double statistics::get_double_value(unsigned idx) const { SASSERT(!is_uint(idx)); return m_d_stats[idx - m_stats.size()].second; } + +void get_memory_statistics(statistics& st) { + unsigned long long max_mem = memory::get_max_used_memory(); + unsigned long long mem = memory::get_allocation_size(); + max_mem = (100*max_mem)/(1024*1024); + mem = (100*mem)/(1024*1024); + st.update("max memory", static_cast(max_mem)/100.0); + st.update("memory", static_cast(mem)/100.0); + st.update("num allocs", static_cast(memory::get_allocation_count())); +} diff --git a/src/util/statistics.h b/src/util/statistics.h index a1a155df9..676c6b744 100644 --- a/src/util/statistics.h +++ b/src/util/statistics.h @@ -42,4 +42,6 @@ public: double get_double_value(unsigned idx) const; }; +void get_memory_statistics(statistics& st); + #endif diff --git a/src/util/z3_exception.cpp b/src/util/z3_exception.cpp index 0e791ad92..52d42d27a 100644 --- a/src/util/z3_exception.cpp +++ b/src/util/z3_exception.cpp @@ -49,6 +49,7 @@ char const * z3_error::msg() const { case ERR_CMD_LINE: return "invalid command line"; case ERR_INTERNAL_FATAL: return "internal error"; case ERR_TYPE_CHECK: return "type error"; + case ERR_ALLOC_EXCEEDED: return "number of configured allocations exceeded"; default: return "unknown error"; } } From 238e38eaa22abbb81cf2591387a34c6a0d681b19 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 22 Jun 2015 13:20:59 +0200 Subject: [PATCH 13/28] update unit tests for num allocs Signed-off-by: Nikolaj Bjorner --- src/api/python/z3.py | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/api/python/z3.py b/src/api/python/z3.py index f6a617317..10b191dbf 100644 --- a/src/api/python/z3.py +++ b/src/api/python/z3.py @@ -5617,7 +5617,7 @@ class Statistics: sat >>> st = s.statistics() >>> len(st) - 4 + 5 """ return int(Z3_stats_size(self.ctx.ref(), self.stats)) @@ -5631,7 +5631,7 @@ class Statistics: sat >>> st = s.statistics() >>> len(st) - 4 + 5 >>> st[0] ('nlsat propagations', 2) >>> st[1] @@ -5655,7 +5655,7 @@ class Statistics: sat >>> st = s.statistics() >>> st.keys() - ['nlsat propagations', 'nlsat stages', 'max memory', 'memory'] + ['nlsat propagations', 'nlsat stages', 'max memory', 'memory', 'num allocs'] """ return [Z3_stats_get_key(self.ctx.ref(), self.stats, idx) for idx in range(len(self))] @@ -5692,7 +5692,7 @@ class Statistics: sat >>> st = s.statistics() >>> st.keys() - ['nlsat propagations', 'nlsat stages', 'max memory', 'memory'] + ['nlsat propagations', 'nlsat stages', 'max memory', 'memory', 'num allocs'] >>> st.nlsat_propagations 2 >>> st.nlsat_stages From 38113e8434d5acba36ab494529384dc6ab9afa7a Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 22 Jun 2015 14:01:36 +0200 Subject: [PATCH 14/28] include statistics from sub-modules for QF_UFNRA Signed-off-by: Nikolaj Bjorner --- src/tactic/nlsat_smt/nl_purify_tactic.cpp | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/src/tactic/nlsat_smt/nl_purify_tactic.cpp b/src/tactic/nlsat_smt/nl_purify_tactic.cpp index be52bb477..0484c2ce2 100644 --- a/src/tactic/nlsat_smt/nl_purify_tactic.cpp +++ b/src/tactic/nlsat_smt/nl_purify_tactic.cpp @@ -676,6 +676,16 @@ public: m_cancel = f; } + virtual void collect_statistics(statistics & st) const { + m_nl_tac->collect_statistics(st); + m_solver->collect_statistics(st); + } + + virtual void reset_statistics() { + m_nl_tac->reset_statistics(); + } + + virtual void cleanup() { m_solver = mk_smt_solver(m, m_params, symbol::null); m_nl_tac->cleanup(); From 949f3f9201a282fb0fb0fe085b4a61f599973e00 Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Mon, 22 Jun 2015 14:48:50 +0100 Subject: [PATCH 15/28] Run link-time optimization on windows only when configured with --optimize This should probably be revisited for VS 2015 Signed-off-by: Nuno Lopes --- scripts/mk_util.py | 26 ++++++++++++++------------ 1 file changed, 14 insertions(+), 12 deletions(-) diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 820396c0d..2c95bc26f 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -85,7 +85,7 @@ VS_PAR=False VS_PAR_NUM=8 GPROF=False GIT_HASH=False -OPTIMIZE=False +SLOW_OPTIMIZE=False FPMATH="Default" FPMATH_FLAGS="-mfpmath=sse -msse -msse2" @@ -580,7 +580,7 @@ def display_help(exit_code): def parse_options(): global VERBOSE, DEBUG_MODE, IS_WINDOWS, VS_X64, ONLY_MAKEFILES, SHOW_CPPS, VS_PROJ, TRACE, VS_PAR, VS_PAR_NUM global DOTNET_ENABLED, JAVA_ENABLED, ML_ENABLED, STATIC_LIB, PREFIX, GMP, FOCI2, FOCI2LIB, PYTHON_PACKAGE_DIR, GPROF, GIT_HASH - global LINUX_X64, OPTIMIZE + global LINUX_X64, SLOW_OPTIMIZE try: options, remainder = getopt.gnu_getopt(sys.argv[1:], 'b:df:sxhmcvtnp:gj', @@ -622,7 +622,7 @@ def parse_options(): elif opt in ('--staticlib'): STATIC_LIB = True elif opt in ('--optimize'): - OPTIMIZE = True + SLOW_OPTIMIZE = True elif not IS_WINDOWS and opt in ('-p', '--prefix'): PREFIX = arg PYTHON_PACKAGE_DIR = os.path.join(PREFIX, 'lib', 'python%s' % distutils.sysconfig.get_python_version(), 'dist-packages') @@ -1786,25 +1786,27 @@ def mk_config(): 'SLINK_EXTRA_FLAGS=/link /DEBUG /MACHINE:X64 /SUBSYSTEM:WINDOWS /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE:NO\n') else: # Windows Release mode - if OPTIMIZE: - config.write('AR_FLAGS=/nologo /LTCG\n') + LTCG=' /LTCG' if SLOW_OPTIMIZE else '' + GL = ' /GL' if SLOW_OPTIMIZE else '' config.write( + 'AR_FLAGS=/nologo%s\n' 'LINK_FLAGS=/nologo /MD\n' - 'SLINK_FLAGS=/nologo /LD\n') + 'SLINK_FLAGS=/nologo /LD\n' + % LTCG) if TRACE: extra_opt = '%s /D _TRACE ' % extra_opt if not VS_X64: config.write( - 'CXXFLAGS=/nologo /c /GL /Zi /W3 /WX- /O2 /Oy- /D _EXTERNAL_RELEASE /D WIN32 /D NDEBUG %s /D _CONSOLE /D _WINDOWS /D ASYNC_COMMANDS /Gm- /EHsc /MD /GS /fp:precise /Zc:wchar_t /Zc:forScope /Gd /analyze- /arch:SSE2\n' % extra_opt) + 'CXXFLAGS=/nologo /c%s /Zi /W3 /WX- /O2 /Oy- /D _EXTERNAL_RELEASE /D WIN32 /D NDEBUG %s /D _CONSOLE /D _WINDOWS /D ASYNC_COMMANDS /Gm- /EHsc /MD /GS /fp:precise /Zc:wchar_t /Zc:forScope /Gd /analyze- /arch:SSE2\n' % (GL, extra_opt)) config.write( - 'LINK_EXTRA_FLAGS=/link /LTCG /DEBUG /MACHINE:X86 /SUBSYSTEM:CONSOLE /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE /NXCOMPAT\n' - 'SLINK_EXTRA_FLAGS=/link /LTCG /DEBUG /MACHINE:X86 /SUBSYSTEM:WINDOWS /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE:NO\n') + 'LINK_EXTRA_FLAGS=/link%s /DEBUG /MACHINE:X86 /SUBSYSTEM:CONSOLE /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE /NXCOMPAT\n' + 'SLINK_EXTRA_FLAGS=/link%s /DEBUG /MACHINE:X86 /SUBSYSTEM:WINDOWS /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE:NO\n' % (LTCG, LTCG)) else: config.write( - 'CXXFLAGS=/c /GL /Zi /nologo /W3 /WX- /O2 /D _EXTERNAL_RELEASE /D WIN32 /D NDEBUG %s /D _LIB /D _WINDOWS /D _AMD64_ /D _UNICODE /D UNICODE /Gm- /EHsc /MD /GS /fp:precise /Zc:wchar_t /Zc:forScope /Gd /TP\n' % extra_opt) + 'CXXFLAGS=/c%s /Zi /nologo /W3 /WX- /O2 /D _EXTERNAL_RELEASE /D WIN32 /D NDEBUG %s /D _LIB /D _WINDOWS /D _AMD64_ /D _UNICODE /D UNICODE /Gm- /EHsc /MD /GS /fp:precise /Zc:wchar_t /Zc:forScope /Gd /TP\n' % (GL, extra_opt)) config.write( - 'LINK_EXTRA_FLAGS=/link /LTCG /MACHINE:X64 /SUBSYSTEM:CONSOLE /INCREMENTAL:NO /STACK:8388608\n' - 'SLINK_EXTRA_FLAGS=/link /LTCG /MACHINE:X64 /SUBSYSTEM:WINDOWS /INCREMENTAL:NO /STACK:8388608\n') + 'LINK_EXTRA_FLAGS=/link%s /MACHINE:X64 /SUBSYSTEM:CONSOLE /INCREMENTAL:NO /STACK:8388608\n' + 'SLINK_EXTRA_FLAGS=/link%s /MACHINE:X64 /SUBSYSTEM:WINDOWS /INCREMENTAL:NO /STACK:8388608\n' % (LTCG, LTCG)) # End of Windows VS config.mk if is_verbose(): From aa4b9e68d749e16510019e8fddb77bca0f2b34b9 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 22 Jun 2015 23:36:52 +0200 Subject: [PATCH 16/28] exposing facility to extract dependent clauses Signed-off-by: Nikolaj Bjorner --- src/smt/tactic/smt_tactic.cpp | 123 ++++++++++++---------- src/smt/tactic/smt_tactic.h | 8 +- src/tactic/nlsat_smt/nl_purify_tactic.cpp | 64 +++++++++-- 3 files changed, 129 insertions(+), 66 deletions(-) diff --git a/src/smt/tactic/smt_tactic.cpp b/src/smt/tactic/smt_tactic.cpp index a83b4a035..35a055329 100644 --- a/src/smt/tactic/smt_tactic.cpp +++ b/src/smt/tactic/smt_tactic.cpp @@ -23,6 +23,66 @@ Notes: #include"smt_params_helper.hpp" #include"rewriter_types.h" #include"filter_model_converter.h" +#include"ast_util.h" + +typedef obj_map expr2expr_map; + +void extract_clauses_and_dependencies(goal_ref const& g, expr_ref_vector& clauses, ptr_vector& assumptions, scoped_ptr& bool2dep, ref& fmc) { + scoped_ptr dep2bool; + dep2bool = alloc(expr2expr_map); + bool2dep = alloc(expr2expr_map); + ptr_vector deps; + ast_manager& m = g->m(); + expr_ref_vector clause(m); + unsigned sz = g->size(); + for (unsigned i = 0; i < sz; i++) { + expr * f = g->form(i); + expr_dependency * d = g->dep(i); + if (d == 0) { + clauses.push_back(f); + } + else { + // create clause (not d1 \/ ... \/ not dn \/ f) when the d's are the assumptions/dependencies of f. + clause.reset(); + clause.push_back(f); + deps.reset(); + m.linearize(d, deps); + SASSERT(!deps.empty()); // d != 0, then deps must not be empty + ptr_vector::iterator it = deps.begin(); + ptr_vector::iterator end = deps.end(); + for (; it != end; ++it) { + expr * d = *it; + if (is_uninterp_const(d) && m.is_bool(d)) { + // no need to create a fresh boolean variable for d + if (!bool2dep->contains(d)) { + assumptions.push_back(d); + bool2dep->insert(d, d); + } + clause.push_back(m.mk_not(d)); + } + else { + // must normalize assumption + expr * b = 0; + if (!dep2bool->find(d, b)) { + b = m.mk_fresh_const(0, m.mk_bool_sort()); + dep2bool->insert(d, b); + bool2dep->insert(b, d); + assumptions.push_back(b); + if (!fmc) { + fmc = alloc(filter_model_converter, m); + } + fmc->insert(to_app(b)->get_decl()); + } + clause.push_back(m.mk_not(b)); + } + } + SASSERT(clause.size() > 1); + expr_ref cls(m); + cls = mk_or(m, clauses.size(), clauses.c_ptr()); + clauses.push_back(cls); + } + } +} class smt_tactic : public tactic { smt_params m_params; @@ -128,7 +188,6 @@ public: } }; - typedef obj_map expr2expr_map; virtual void operator()(goal_ref const & in, goal_ref_buffer & result, @@ -147,65 +206,17 @@ public: TRACE("smt_tactic_memory", tout << "wasted_size: " << m.get_allocator().get_wasted_size() << "\n";); scoped_init_ctx init(*this, m); SASSERT(m_ctx != 0); - - scoped_ptr dep2bool; - scoped_ptr bool2dep; - ptr_vector assumptions; + + expr_ref_vector clauses(m); + scoped_ptr bool2dep; + ptr_vector assumptions; ref fmc; if (in->unsat_core_enabled()) { if (in->proofs_enabled()) throw tactic_exception("smt tactic does not support simultaneous generation of proofs and unsat cores"); - dep2bool = alloc(expr2expr_map); - bool2dep = alloc(expr2expr_map); - ptr_vector deps; - ptr_vector clause; - unsigned sz = in->size(); - for (unsigned i = 0; i < sz; i++) { - expr * f = in->form(i); - expr_dependency * d = in->dep(i); - if (d == 0) { - m_ctx->assert_expr(f); - } - else { - // create clause (not d1 \/ ... \/ not dn \/ f) when the d's are the assumptions/dependencies of f. - clause.reset(); - clause.push_back(f); - deps.reset(); - m.linearize(d, deps); - SASSERT(!deps.empty()); // d != 0, then deps must not be empty - ptr_vector::iterator it = deps.begin(); - ptr_vector::iterator end = deps.end(); - for (; it != end; ++it) { - expr * d = *it; - if (is_uninterp_const(d) && m.is_bool(d)) { - // no need to create a fresh boolean variable for d - if (!bool2dep->contains(d)) { - assumptions.push_back(d); - bool2dep->insert(d, d); - } - clause.push_back(m.mk_not(d)); - } - else { - // must normalize assumption - expr * b = 0; - if (!dep2bool->find(d, b)) { - b = m.mk_fresh_const(0, m.mk_bool_sort()); - dep2bool->insert(d, b); - bool2dep->insert(b, d); - assumptions.push_back(b); - if (!fmc) { - fmc = alloc(filter_model_converter, m); - } - fmc->insert(to_app(b)->get_decl()); - } - clause.push_back(m.mk_not(b)); - } - } - SASSERT(clause.size() > 1); - expr_ref cls(m); - cls = m.mk_or(clause.size(), clause.c_ptr()); - m_ctx->assert_expr(cls); - } + extract_clauses_and_dependencies(in, clauses, assumptions, bool2dep, fmc); + for (unsigned i = 0; i < clauses.size(); ++i) { + m_ctx->assert_expr(clauses[i].get()); } } else if (in->proofs_enabled()) { diff --git a/src/smt/tactic/smt_tactic.h b/src/smt/tactic/smt_tactic.h index 521a454f7..631c345c7 100644 --- a/src/smt/tactic/smt_tactic.h +++ b/src/smt/tactic/smt_tactic.h @@ -20,15 +20,21 @@ Notes: #define _SMT_TACTIC_H_ #include"params.h" +#include"ast.h" +#include"obj_hashtable.h" +#include"goal.h" class tactic; +class filter_model_converter; tactic * mk_smt_tactic(params_ref const & p = params_ref()); // syntax sugar for using_params(mk_smt_tactic(), p) where p = (:auto_config, auto_config) tactic * mk_smt_tactic_using(bool auto_config = true, params_ref const & p = params_ref()); + +void extract_clauses_and_dependencies(goal_ref const& g, expr_ref_vector& clauses, ptr_vector& assumptions, scoped_ptr >& bool2dep, ref& fmc); + /* ADD_TACTIC("smt", "apply a SAT based SMT solver.", "mk_smt_tactic(p)") */ - #endif diff --git a/src/tactic/nlsat_smt/nl_purify_tactic.cpp b/src/tactic/nlsat_smt/nl_purify_tactic.cpp index 0484c2ce2..f7acf529f 100644 --- a/src/tactic/nlsat_smt/nl_purify_tactic.cpp +++ b/src/tactic/nlsat_smt/nl_purify_tactic.cpp @@ -115,8 +115,6 @@ public: arith_util & u() { return m_owner.m_util; } - bool produce_proofs() const { return m_owner.m_produce_proofs; } - expr * mk_interface_var(expr* arg) { expr* r; if (m_interface_cache.find(arg, r)) { @@ -145,7 +143,7 @@ public: return is_app(e) && (to_app(e)->get_family_id() == u().get_family_id()); } - void mk_interface_bool(func_decl * f, unsigned num, expr* const* args, expr_ref& result) { + void mk_interface_bool(func_decl * f, unsigned num, expr* const* args, expr_ref& result, proof_ref& pr) { expr_ref old_pred(m.mk_app(f, num, args), m); polarity_t pol; VERIFY(m_polarities.find(old_pred, pol)); @@ -154,10 +152,13 @@ public: m_new_preds.push_back(to_app(result)); m_owner.m_fmc->insert(to_app(result)->get_decl()); if (pol != pol_neg) { - m_owner.m_nl_g->assert_expr(m.mk_or(m.mk_not(result), m.mk_app(f, num, args))); + m_owner.m_nl_g->assert_expr(m.mk_or(m.mk_not(result), old_pred)); } if (pol != pol_pos) { - m_owner.m_nl_g->assert_expr(m.mk_or(result, m.mk_not(m.mk_app(f, num, args)))); + m_owner.m_nl_g->assert_expr(m.mk_or(result, m.mk_not(old_pred))); + } + if (m_owner.m_produce_proofs) { + pr = m.mk_oeq(old_pred, result); } TRACE("nlsat_smt", tout << old_pred << " : " << result << "\n";); } @@ -183,7 +184,7 @@ public: br_status reduce_app_bool(func_decl * f, unsigned num, expr* const* args, expr_ref& result, proof_ref & pr) { if (f->get_family_id() == m.get_basic_family_id()) { if (f->get_decl_kind() == OP_EQ && u().is_real(args[0])) { - mk_interface_bool(f, num, args, result); + mk_interface_bool(f, num, args, result, pr); return BR_DONE; } else { @@ -194,7 +195,7 @@ public: switch (f->get_decl_kind()) { case OP_LE: case OP_GE: case OP_LT: case OP_GT: // these are the only real cases of non-linear atomic formulas besides equality. - mk_interface_bool(f, num, args, result); + mk_interface_bool(f, num, args, result, pr); return BR_DONE; default: return BR_FAILED; @@ -209,12 +210,14 @@ public: bool is_arith_op(expr* e) { return is_app(e) && to_app(e)->get_family_id() == u().get_family_id(); } + br_status reduce_app_real(func_decl * f, unsigned num, expr* const* args, expr_ref& result, proof_ref & pr) { bool has_interface = false; bool is_arith = false; if (f->get_family_id() == u().get_family_id()) { switch (f->get_decl_kind()) { - case OP_NUM: case OP_IRRATIONAL_ALGEBRAIC_NUM: + case OP_NUM: + case OP_IRRATIONAL_ALGEBRAIC_NUM: return BR_FAILED; default: is_arith = true; @@ -238,6 +241,9 @@ public: } if (has_interface) { result = m.mk_app(f, num, m_args.c_ptr()); + if (m_owner.m_produce_proofs) { + pr = m.mk_oeq(m.mk_app(f, num, args), result); // push proof object to mk_interface_var? + } TRACE("nlsat_smt", tout << result << "\n";); return BR_DONE; } @@ -264,6 +270,7 @@ private: } }; + arith_util & u() { return m_util; } void check_point() { @@ -727,7 +734,6 @@ public: r.set_bool_mode(); rewrite_goal(r, g); - g->inc_depth(); for (unsigned i = 0; i < g->size(); ++i) { m_solver->assert_expr(g->form(i)); } @@ -740,3 +746,43 @@ public: tactic * mk_nl_purify_tactic(ast_manager& m, params_ref const& p) { return alloc(nl_purify_tactic, m, p); } + +#if 0 + void mark_interface_vars(goal_ref const& g) { + expr_mark visited; + ptr_vector todo; + unsigned sz = g->size(); + for (unsigned i = 0; i < sz; i++) { + todo.push_back(g->form(i)); + } + while (!todo.empty()) { + expr* e = todo.back(); + todo.pop_back(); + if (visited.is_marked(e)) { + continue; + } + visited.mark(e); + if (is_quantifier(e)) { + todo.push_back(to_quantifier(e)->get_expr()); + continue; + } + if (is_var(e)) { + continue; + } + app* ap = to_app(e); + sz = ap->get_num_args(); + bool is_arith = is_arith_op(e); + for (unsigned i = 0; i < sz; ++i) { + expr* arg = ap->get_arg(i); + todo.push_back(arg); + if (is_arith && !is_arith_op(arg)) { + m_interface_vars.mark(arg); + } + else if (!is_arith && is_arith_op(arg) && ap->get_family_id() != m.get_basic_family_id()) { + m_interface_vars.mark(arg); + } + } + } + + } +#endif From 8df919b6bb3d32a34813401e5a0bcf46d6039cda Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 23 Jun 2015 12:05:19 +0200 Subject: [PATCH 17/28] fix mixed integer/real bugs for maximization exposed by non-termination in slow.smt. partially fixes issue #56 Signed-off-by: Nikolaj Bjorner --- src/smt/tactic/smt_tactic.cpp | 24 ++-- src/smt/tactic/smt_tactic.h | 2 +- src/smt/theory_arith.h | 1 - src/smt/theory_arith_aux.h | 110 +++----------- src/tactic/nlsat_smt/nl_purify_tactic.cpp | 168 ++++++++++++---------- 5 files changed, 130 insertions(+), 175 deletions(-) diff --git a/src/smt/tactic/smt_tactic.cpp b/src/smt/tactic/smt_tactic.cpp index 35a055329..2d9a8fb82 100644 --- a/src/smt/tactic/smt_tactic.cpp +++ b/src/smt/tactic/smt_tactic.cpp @@ -27,10 +27,8 @@ Notes: typedef obj_map expr2expr_map; -void extract_clauses_and_dependencies(goal_ref const& g, expr_ref_vector& clauses, ptr_vector& assumptions, scoped_ptr& bool2dep, ref& fmc) { - scoped_ptr dep2bool; - dep2bool = alloc(expr2expr_map); - bool2dep = alloc(expr2expr_map); +void extract_clauses_and_dependencies(goal_ref const& g, expr_ref_vector& clauses, ptr_vector& assumptions, expr2expr_map& bool2dep, ref& fmc) { + expr2expr_map dep2bool; ptr_vector deps; ast_manager& m = g->m(); expr_ref_vector clause(m); @@ -38,7 +36,7 @@ void extract_clauses_and_dependencies(goal_ref const& g, expr_ref_vector& clause for (unsigned i = 0; i < sz; i++) { expr * f = g->form(i); expr_dependency * d = g->dep(i); - if (d == 0) { + if (d == 0 || !g->unsat_core_enabled()) { clauses.push_back(f); } else { @@ -54,19 +52,19 @@ void extract_clauses_and_dependencies(goal_ref const& g, expr_ref_vector& clause expr * d = *it; if (is_uninterp_const(d) && m.is_bool(d)) { // no need to create a fresh boolean variable for d - if (!bool2dep->contains(d)) { + if (!bool2dep.contains(d)) { assumptions.push_back(d); - bool2dep->insert(d, d); + bool2dep.insert(d, d); } clause.push_back(m.mk_not(d)); } else { // must normalize assumption expr * b = 0; - if (!dep2bool->find(d, b)) { + if (!dep2bool.find(d, b)) { b = m.mk_fresh_const(0, m.mk_bool_sort()); - dep2bool->insert(d, b); - bool2dep->insert(b, d); + dep2bool.insert(d, b); + bool2dep.insert(b, d); assumptions.push_back(b); if (!fmc) { fmc = alloc(filter_model_converter, m); @@ -78,7 +76,7 @@ void extract_clauses_and_dependencies(goal_ref const& g, expr_ref_vector& clause } SASSERT(clause.size() > 1); expr_ref cls(m); - cls = mk_or(m, clauses.size(), clauses.c_ptr()); + cls = mk_or(m, clause.size(), clause.c_ptr()); clauses.push_back(cls); } } @@ -208,7 +206,7 @@ public: SASSERT(m_ctx != 0); expr_ref_vector clauses(m); - scoped_ptr bool2dep; + expr2expr_map bool2dep; ptr_vector assumptions; ref fmc; if (in->unsat_core_enabled()) { @@ -273,7 +271,7 @@ public: for (unsigned i = 0; i < sz; i++) { expr * b = m_ctx->get_unsat_core_expr(i); SASSERT(is_uninterp_const(b) && m.is_bool(b)); - expr * d = bool2dep->find(b); + expr * d = bool2dep.find(b); lcore = m.mk_join(lcore, m.mk_leaf(d)); } } diff --git a/src/smt/tactic/smt_tactic.h b/src/smt/tactic/smt_tactic.h index 631c345c7..6a501968d 100644 --- a/src/smt/tactic/smt_tactic.h +++ b/src/smt/tactic/smt_tactic.h @@ -32,7 +32,7 @@ tactic * mk_smt_tactic(params_ref const & p = params_ref()); tactic * mk_smt_tactic_using(bool auto_config = true, params_ref const & p = params_ref()); -void extract_clauses_and_dependencies(goal_ref const& g, expr_ref_vector& clauses, ptr_vector& assumptions, scoped_ptr >& bool2dep, ref& fmc); +void extract_clauses_and_dependencies(goal_ref const& g, expr_ref_vector& clauses, ptr_vector& assumptions, obj_map& bool2dep, ref& fmc); /* ADD_TACTIC("smt", "apply a SAT based SMT solver.", "mk_smt_tactic(p)") diff --git a/src/smt/theory_arith.h b/src/smt/theory_arith.h index 6531c33f2..07b899624 100644 --- a/src/smt/theory_arith.h +++ b/src/smt/theory_arith.h @@ -879,7 +879,6 @@ namespace smt { row m_tmp_row; void add_tmp_row(row & r1, numeral const & coeff, row const & r2); - theory_var pick_var_to_leave(bool has_int, theory_var x_j, bool inc, numeral & a_ij, inf_numeral & gain, bool& skiped_row); bool is_safe_to_leave(theory_var x, bool inc, bool& has_int, bool& is_shared); template void add_tmp_row_entry(row & r, numeral const & coeff, theory_var v); diff --git a/src/smt/theory_arith_aux.h b/src/smt/theory_arith_aux.h index 8bf366682..862d9487e 100644 --- a/src/smt/theory_arith_aux.h +++ b/src/smt/theory_arith_aux.h @@ -989,83 +989,6 @@ namespace smt { } - /** - \brief Select tightest variable x_i to pivot with x_j. The goal - is to select a x_i such that the value of x_j is increased - (decreased) if inc = true (inc = false), and the tableau - remains feasible. Store the gain in x_j of the pivoting - operation in 'gain'. Note the gain can be too much. That is, - it may make x_i infeasible. In this case, instead of pivoting - we move x_j to its upper bound (lower bound) when inc = true (inc = false). - - If no x_i imposes a restriction on x_j, then return null_theory_var. - That is, x_j is free to move to its upper bound (lower bound). - - Get the equations for x_j: - - x_i1 = coeff_1 * x_j + rest_1 - ... - x_in = coeff_n * x_j + rest_n - - gain_k := (upper_bound(x_ik) - value(x_ik))/coeff_k - - */ - - template - theory_var theory_arith::pick_var_to_leave( - bool has_int, theory_var x_j, bool inc, - numeral & a_ij, inf_numeral & gain, bool& skipped_row) { - TRACE("opt", tout << "selecting variable to replace v" << x_j << ", inc: " << inc << "\n";); - theory_var x_i = null_theory_var; - inf_numeral curr_gain; - column & c = m_columns[x_j]; - typename svector::iterator it = c.begin_entries(); - typename svector::iterator end = c.end_entries(); - for (; it != end; ++it) { - if (!it->is_dead()) { - row & r = m_rows[it->m_row_id]; - theory_var s = r.get_base_var(); - if (s != null_theory_var && !is_quasi_base(s)) { - numeral const & coeff = r[it->m_row_idx].m_coeff; - bool inc_s = coeff.is_neg() ? inc : !inc; - bound * b = get_bound(s, inc_s); - if (b) { - curr_gain = get_value(s); - curr_gain -= b->get_value(); - curr_gain /= coeff; - if (curr_gain.is_neg()) - curr_gain.neg(); - if (x_i == null_theory_var || (curr_gain < gain) || (gain.is_zero() && curr_gain.is_zero() && s < x_i)) { - if (is_int(s) && !curr_gain.is_int()) { - skipped_row = true; - continue; - } - if (is_int(x_j) && !curr_gain.is_int()) { - skipped_row = true; - continue; - } - if (!curr_gain.is_int() && has_int) { - skipped_row = true; - continue; - } - x_i = s; - a_ij = coeff; - gain = curr_gain; - TRACE("opt", - tout << "x_i: v" << x_i << ", gain: " << gain << "\n"; - tout << "value(s): (" << get_value(s) << " - " << b->get_value() << ")/" << coeff << "\n"; - display_row(tout, r, true); - ); - } - } - } - TRACE("opt", tout << "x_i: v" << x_i << ", gain: " << gain << "\n";); - } - } - TRACE("opt", tout << "x_i v" << x_i << "\n";); - return x_i; - } - template bool theory_arith::get_theory_vars(expr * n, uint_set & vars) { rational r; @@ -1388,6 +1311,9 @@ namespace smt { bool& has_shared, // determine if pivot involves shared variable theory_var& x_i) { // base variable to pivot with x_j + if (is_int(x_j) && !get_value(x_j).is_int()) { + return false; + } x_i = null_theory_var; context& ctx = get_context(); column & c = m_columns[x_j]; @@ -1447,8 +1373,7 @@ namespace smt { template void theory_arith::normalize_gain(numeral const& divisor, inf_numeral & max_gain) const { SASSERT(divisor.is_int()); - SASSERT(divisor.is_pos()); - if (!divisor.is_one() && !max_gain.is_minus_one()) { + if (!divisor.is_minus_one() && !divisor.is_one() && !max_gain.is_minus_one()) { max_gain = floor(max_gain/divisor)*divisor; } } @@ -1473,14 +1398,15 @@ namespace smt { if (is_int(x)) { min_gain = inf_numeral::one(); } + TRACE("opt", + tout << "v" << x << " := " << get_value(x) << " " + << "min gain: " << min_gain << " " + << "max gain: " << max_gain << "\n";); + SASSERT(max_gain.is_minus_one() || !max_gain.is_neg()); SASSERT(min_gain.is_minus_one() || min_gain.is_one()); SASSERT(!is_int(x) || max_gain.is_int()); SASSERT(is_int(x) == min_gain.is_one()); - TRACE("opt", - tout << "v" << x << " " - << "min gain: " << min_gain << " " - << "max gain: " << max_gain << "\n";); } @@ -1512,14 +1438,18 @@ namespace smt { if (is_int(x_i)) den_aij = denominator(a_ij); SASSERT(den_aij.is_pos() && den_aij.is_int()); - if (is_int(x_i) && !den_aij.is_one()) { - SASSERT(min_gain.is_pos()); + if (is_int(x_i) && !den_aij.is_one() && min_gain.is_pos()) { min_gain = inf_numeral(lcm(min_gain.get_rational(), den_aij)); normalize_gain(min_gain.get_rational(), max_gain); } if (!max_inc.is_minus_one()) { if (is_int(x_i)) { + TRACE("opt", + tout << "v" << x_i << " a_ij " << a_ij << " " + << "min gain: " << min_gain << " " + << "max gain: " << max_gain << "\n";); + max_inc = floor(max_inc); normalize_gain(min_gain.get_rational(), max_inc); } @@ -1539,9 +1469,9 @@ namespace smt { << (is_tighter?"true":"false") << "\n";); SASSERT(max_gain.is_minus_one() || !max_gain.is_neg()); SASSERT(min_gain.is_minus_one() || !min_gain.is_neg()); - SASSERT(!is_int(x_i) || min_gain.is_pos()); - SASSERT(!is_int(x_i) || min_gain.is_int()); - SASSERT(!is_int(x_i) || max_gain.is_int()); + //SASSERT(!is_int(x_i) || min_gain.is_pos()); + //SASSERT(!is_int(x_i) || min_gain.is_int()); + //SASSERT(!is_int(x_i) || max_gain.is_int()); return is_tighter; } @@ -1759,6 +1689,10 @@ namespace smt { unsigned& best_efforts, // is bound move a best effort? bool& has_shared) { // does move include shared variables? inf_numeral min_gain, max_gain; + if (is_int(x_i) && !get_value(x_i).is_int()) { + ++best_efforts; + return false; + } init_gains(x_i, inc, min_gain, max_gain); column & c = m_columns[x_i]; typename svector::iterator it = c.begin_entries(); diff --git a/src/tactic/nlsat_smt/nl_purify_tactic.cpp b/src/tactic/nlsat_smt/nl_purify_tactic.cpp index f7acf529f..34458dd57 100644 --- a/src/tactic/nlsat_smt/nl_purify_tactic.cpp +++ b/src/tactic/nlsat_smt/nl_purify_tactic.cpp @@ -58,6 +58,7 @@ Revision History: #include "solver.h" #include "model_smt2_pp.h" #include "expr_safe_replace.h" +#include "ast_util.h" class nl_purify_tactic : public tactic { @@ -81,6 +82,10 @@ class nl_purify_tactic : public tactic { app_ref_vector m_new_reals; // interface real variables app_ref_vector m_new_preds; // abstraction predicates for smt_solver (hide real constraints) expr_ref_vector m_asms; // assumptions to pass to SMT solver + ptr_vector m_ctx_asms; // assumptions passed by context + obj_hashtable m_ctx_asms_set; // assumptions passed by context + obj_hashtable m_used_asms; + obj_map m_bool2dep; obj_pair_map m_eq_pairs; // map pairs of interface variables to auxiliary predicates obj_map m_interface_cache; // map of compound real expression to interface variable. obj_map m_polarities; // polarities of sub-expressions @@ -98,6 +103,7 @@ public: obj_map& m_polarities; obj_map& m_interface_cache; expr_ref_vector m_args; + proof_ref_vector m_proofs; mode_t m_mode; rw_cfg(nl_purify_tactic & o): @@ -108,6 +114,7 @@ public: m_polarities(o.m_polarities), m_interface_cache(o.m_interface_cache), m_args(m), + m_proofs(m), m_mode(mode_interface_var) { } @@ -115,8 +122,8 @@ public: arith_util & u() { return m_owner.m_util; } - expr * mk_interface_var(expr* arg) { - expr* r; + expr * mk_interface_var(expr* arg, proof_ref& arg_pr) { + expr* r; if (m_interface_cache.find(arg, r)) { return r; } @@ -136,6 +143,9 @@ public: else { m_owner.m_solver->assert_expr(eq); } + if (m_owner.m_produce_proofs) { + arg_pr = m.mk_oeq(arg, r); + } return r; } @@ -225,24 +235,29 @@ public: } } m_args.reset(); + m_proofs.reset(); for (unsigned i = 0; i < num; ++i) { expr* arg = args[i]; + proof_ref arg_pr(m); if (is_arith && !is_arith_op(arg)) { has_interface = true; - m_args.push_back(mk_interface_var(arg)); + m_args.push_back(mk_interface_var(arg, arg_pr)); } else if (!is_arith && u().is_real(arg)) { has_interface = true; - m_args.push_back(mk_interface_var(arg)); + m_args.push_back(mk_interface_var(arg, arg_pr)); } else { m_args.push_back(arg); } + if (arg_pr) { + m_proofs.push_back(arg_pr); + } } if (has_interface) { result = m.mk_app(f, num, m_args.c_ptr()); if (m_owner.m_produce_proofs) { - pr = m.mk_oeq(m.mk_app(f, num, args), result); // push proof object to mk_interface_var? + pr = m.mk_oeq_congruence(m.mk_app(f, num, args), to_app(result), m_proofs.size(), m_proofs.c_ptr()); } TRACE("nlsat_smt", tout << result << "\n";); return BR_DONE; @@ -281,7 +296,7 @@ private: void display_result(std::ostream& out, goal_ref_buffer const& result) { for (unsigned i = 0; i < result.size(); ++i) { - result[i]->display(out << "goal\n"); + result[i]->display_with_dependencies(out << "goal\n"); } } @@ -301,8 +316,11 @@ private: } } - void solve(goal_ref_buffer& result, - model_converter_ref& mc) { + void solve( + goal_ref const& g, + goal_ref_buffer& result, + expr_dependency_ref& core, + model_converter_ref& mc) { while (true) { check_point(); @@ -316,6 +334,7 @@ private: (*m_nl_tac)(tmp_nl, result, nl_mc, nl_pc, nl_core); if (is_decided_unsat(result)) { + core2result(core, g, result); TRACE("nlsat_smt", tout << "unsat\n";); break; } @@ -328,7 +347,7 @@ private: // assert equalities between equal interface real variables. model_ref mdl_nl, mdl_smt; - if (mdl_nl.get()) { + if (nl_mc.get()) { model_converter2model(m, nl_mc.get(), mdl_nl); update_eq_values(mdl_nl); enforce_equalities(mdl_nl, m_nl_g); @@ -343,21 +362,28 @@ private: lbool r = m_solver->check_sat(m_asms.size(), m_asms.c_ptr()); if (r == l_false) { // extract the core from the result - ptr_vector core; - m_solver->get_unsat_core(core); - if (core.empty()) { - goal_ref g = alloc(goal, m); - g->assert_expr(m.mk_false()); - result.push_back(g.get()); - break; - } + ptr_vector ecore, asms; expr_ref_vector clause(m); expr_ref fml(m); - expr* e; - for (unsigned i = 0; i < core.size(); ++i) { - clause.push_back(m.is_not(core[i], e)?e:m.mk_not(core[i])); + get_unsat_core(ecore, asms); + + // + // assumptions should also be used for the nlsat tactic, + // but since it does not support assumptions at this time + // we overapproximate the necessary core and accumulate + // all assumptions that are ever used. + // + for (unsigned i = 0; i < asms.size(); ++i) { + m_used_asms.insert(asms[i]); } - fml = m.mk_or(clause.size(), clause.c_ptr()); + if (ecore.empty()) { + core2result(core, g, result); + break; + } + for (unsigned i = 0; i < ecore.size(); ++i) { + clause.push_back(mk_not(m, ecore[i])); + } + fml = mk_or(m, clause.size(), clause.c_ptr()); m_nl_g->assert_expr(fml); continue; } @@ -386,9 +412,35 @@ private: TRACE("nlsat_smt", display_result(tout, result);); } + void get_unsat_core(ptr_vector& core, ptr_vector& asms) { + m_solver->get_unsat_core(core); + for (unsigned i = 0; i < core.size(); ++i) { + if (m_ctx_asms_set.contains(core[i])) { + asms.push_back(core[i]); + core[i] = core.back(); + core.pop_back(); + --i; + } + } + } + + void core2result(expr_dependency_ref & lcore, goal_ref const& g, goal_ref_buffer& result) { + result.reset(); + proof * pr = 0; + lcore = 0; + g->reset(); + obj_hashtable::iterator it = m_used_asms.begin(), end = m_used_asms.end(); + for (; it != end; ++it) { + lcore = m.mk_join(lcore, m.mk_leaf(m_bool2dep.find(*it))); + } + g->assert_expr(m.mk_false(), pr, lcore); + TRACE("nlsat_smt", g->display_with_dependencies(tout);); + result.push_back(g.get()); + } void setup_assumptions(model_ref& mdl) { m_asms.reset(); + m_asms.append(m_ctx_asms.size(), m_ctx_asms.c_ptr()); app_ref_vector const& fresh_preds = m_new_preds; expr_ref tmp(m); for (unsigned i = 0; i < fresh_preds.size(); ++i) { @@ -419,10 +471,7 @@ private: } } TRACE("nlsat_smt", - tout << "assumptions:\n"; - for (unsigned i = 0; i < m_asms.size(); ++i) { - tout << mk_pp(m_asms[i].get(), m) << "\n"; - }); + tout << "assumptions:\n" << m_asms << "\n";); } bool enforce_equalities(model_ref& mdl, goal_ref const& nl_g) { @@ -602,7 +651,7 @@ private: expr * curr = g->form(i); if (is_pure_arithmetic(is_pure, curr)) { m_nl_g->assert_expr(curr, g->pr(i), g->dep(i)); - g->update(i, m.mk_true()); + g->update(i, m.mk_true(), g->pr(i), g->dep(i)); } } } @@ -702,6 +751,10 @@ public: m_new_preds.reset(); m_eq_pairs.reset(); m_polarities.reset(); + m_ctx_asms.reset(); + m_ctx_asms_set.reset(); + m_used_asms.reset(); + m_bool2dep.reset(); } virtual void operator()(goal_ref const & g, @@ -717,8 +770,9 @@ public: mc = 0; pc = 0; core = 0; fail_if_proof_generation("qfufnra-purify", g); - fail_if_unsat_core_generation("qfufnra-purify", g); + // fail_if_unsat_core_generation("qfufnra-purify", g); rw r(*this); + expr_ref_vector clauses(m); m_nl_g = alloc(goal, m, true, false); m_fmc = alloc(filter_model_converter, m); @@ -728,17 +782,27 @@ public: // creating a place-holder predicate inside the // original goal and extracing pure nlsat clauses. r.set_interface_var_mode(); - rewrite_goal(r, g); - remove_pure_arith(g); + rewrite_goal(r, g); + if (!g->unsat_core_enabled()) { + remove_pure_arith(g); + } get_polarities(*g.get()); r.set_bool_mode(); rewrite_goal(r, g); - for (unsigned i = 0; i < g->size(); ++i) { - m_solver->assert_expr(g->form(i)); + extract_clauses_and_dependencies(g, clauses, m_ctx_asms, m_bool2dep, m_fmc); + + TRACE("nlsat_smt", tout << clauses << "\n";); + + for (unsigned i = 0; i < m_ctx_asms.size(); ++i) { + m_ctx_asms_set.insert(m_ctx_asms[i]); + } + + for (unsigned i = 0; i < clauses.size(); ++i) { + m_solver->assert_expr(clauses[i].get()); } g->inc_depth(); - solve(result, mc); + solve(g, result, core, mc); } }; @@ -746,43 +810,3 @@ public: tactic * mk_nl_purify_tactic(ast_manager& m, params_ref const& p) { return alloc(nl_purify_tactic, m, p); } - -#if 0 - void mark_interface_vars(goal_ref const& g) { - expr_mark visited; - ptr_vector todo; - unsigned sz = g->size(); - for (unsigned i = 0; i < sz; i++) { - todo.push_back(g->form(i)); - } - while (!todo.empty()) { - expr* e = todo.back(); - todo.pop_back(); - if (visited.is_marked(e)) { - continue; - } - visited.mark(e); - if (is_quantifier(e)) { - todo.push_back(to_quantifier(e)->get_expr()); - continue; - } - if (is_var(e)) { - continue; - } - app* ap = to_app(e); - sz = ap->get_num_args(); - bool is_arith = is_arith_op(e); - for (unsigned i = 0; i < sz; ++i) { - expr* arg = ap->get_arg(i); - todo.push_back(arg); - if (is_arith && !is_arith_op(arg)) { - m_interface_vars.mark(arg); - } - else if (!is_arith && is_arith_op(arg) && ap->get_family_id() != m.get_basic_family_id()) { - m_interface_vars.mark(arg); - } - } - } - - } -#endif From 020620aadd5aca05547aaa51b7f66122932283a6 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 23 Jun 2015 14:05:49 +0200 Subject: [PATCH 18/28] disable qf-ufnra tactic from default for testing Signed-off-by: Nikolaj Bjorner --- src/tactic/portfolio/default_tactic.cpp | 4 ++-- src/tactic/portfolio/smt_strategic_solver.cpp | 4 ++-- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/src/tactic/portfolio/default_tactic.cpp b/src/tactic/portfolio/default_tactic.cpp index 72c486c24..4f5eb5ed0 100644 --- a/src/tactic/portfolio/default_tactic.cpp +++ b/src/tactic/portfolio/default_tactic.cpp @@ -44,8 +44,8 @@ tactic * mk_default_tactic(ast_manager & m, params_ref const & p) { cond(mk_is_nra_probe(), mk_nra_tactic(m), cond(mk_is_lira_probe(), mk_lira_tactic(m, p), cond(mk_is_qffp_probe(), mk_qffp_tactic(m, p), - cond(mk_is_qfufnra_probe(), mk_qfufnra_tactic(m, p), - mk_smt_tactic())))))))))))), + //cond(mk_is_qfufnra_probe(), mk_qfufnra_tactic(m, p), + mk_smt_tactic()))))))))))), p); return st; } diff --git a/src/tactic/portfolio/smt_strategic_solver.cpp b/src/tactic/portfolio/smt_strategic_solver.cpp index 27d7433e8..c868fdcb9 100644 --- a/src/tactic/portfolio/smt_strategic_solver.cpp +++ b/src/tactic/portfolio/smt_strategic_solver.cpp @@ -86,8 +86,8 @@ tactic * mk_tactic_for_logic(ast_manager & m, params_ref const & p, symbol const return mk_qffpbv_tactic(m, p); else if (logic=="HORN") return mk_horn_tactic(m, p); - else if (logic=="QF_UFNRA") - return mk_qfufnra_tactic(m, p); + //else if (logic=="QF_UFNRA") + // return mk_qfufnra_tactic(m, p); else return mk_default_tactic(m, p); } From 7b918e83c3200c21345f8673b56e456c4e2c5479 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 23 Jun 2015 14:15:14 +0200 Subject: [PATCH 19/28] fix distribute forall, fixes issue #138 Signed-off-by: Nikolaj Bjorner --- src/tactic/core/distribute_forall_tactic.cpp | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/src/tactic/core/distribute_forall_tactic.cpp b/src/tactic/core/distribute_forall_tactic.cpp index 913b55174..53a1ce4ae 100644 --- a/src/tactic/core/distribute_forall_tactic.cpp +++ b/src/tactic/core/distribute_forall_tactic.cpp @@ -30,6 +30,10 @@ class distribute_forall_tactic : public tactic { expr * const * new_no_patterns, expr_ref & result, proof_ref & result_pr) { + + if (!old_q->is_forall()) { + return false; + } if (m.is_not(new_body) && m.is_or(to_app(new_body)->get_arg(0))) { // (forall X (not (or F1 ... Fn))) From 3de2a70a48a392cac0f2d664e413e9e1070b1747 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 23 Jun 2015 14:33:45 +0200 Subject: [PATCH 20/28] move functionality from qe_util to ast_util Signed-off-by: Nikolaj Bjorner --- src/ast/ast_util.cpp | 113 ++++++++++++++++++ src/ast/ast_util.h | 13 ++ src/muz/base/dl_boogie_proof.cpp | 4 +- src/muz/base/dl_rule.cpp | 4 +- src/muz/base/hnf.cpp | 3 +- src/muz/fp/horn_tactic.cpp | 3 +- src/muz/pdr/pdr_closure.cpp | 2 +- src/muz/pdr/pdr_context.cpp | 10 +- src/muz/pdr/pdr_farkas_learner.cpp | 2 +- src/muz/pdr/pdr_generalizers.cpp | 6 +- src/muz/pdr/pdr_manager.cpp | 6 +- src/muz/pdr/pdr_prop_solver.cpp | 2 +- src/muz/pdr/pdr_util.cpp | 2 +- src/muz/rel/karr_relation.cpp | 3 +- src/muz/rel/udoc_relation.cpp | 4 +- src/muz/tab/tab_context.cpp | 7 +- src/muz/transforms/dl_mk_array_blast.cpp | 7 +- .../dl_mk_interp_tail_simplifier.cpp | 3 +- .../dl_mk_quantifier_instantiation.cpp | 2 +- src/muz/transforms/dl_mk_slice.cpp | 3 +- src/qe/qe.cpp | 4 +- src/qe/qe_arith.cpp | 3 +- src/qe/qe_lite.cpp | 7 +- src/qe/qe_util.cpp | 112 ----------------- src/qe/qe_util.h | 10 -- 25 files changed, 174 insertions(+), 161 deletions(-) diff --git a/src/ast/ast_util.cpp b/src/ast/ast_util.cpp index 79f8f740e..94e7b642c 100644 --- a/src/ast/ast_util.cpp +++ b/src/ast/ast_util.cpp @@ -191,3 +191,116 @@ expr * expand_distinct(ast_manager & m, unsigned num_args, expr * const * args) } return mk_and(m, new_diseqs.size(), new_diseqs.c_ptr()); } + +void flatten_and(expr_ref_vector& result) { + ast_manager& m = result.get_manager(); + expr* e1, *e2, *e3; + for (unsigned i = 0; i < result.size(); ++i) { + if (m.is_and(result[i].get())) { + app* a = to_app(result[i].get()); + unsigned num_args = a->get_num_args(); + for (unsigned j = 0; j < num_args; ++j) { + result.push_back(a->get_arg(j)); + } + result[i] = result.back(); + result.pop_back(); + --i; + } + else if (m.is_not(result[i].get(), e1) && m.is_not(e1, e2)) { + result[i] = e2; + --i; + } + else if (m.is_not(result[i].get(), e1) && m.is_or(e1)) { + app* a = to_app(e1); + unsigned num_args = a->get_num_args(); + for (unsigned j = 0; j < num_args; ++j) { + result.push_back(m.mk_not(a->get_arg(j))); + } + result[i] = result.back(); + result.pop_back(); + --i; + } + else if (m.is_not(result[i].get(), e1) && m.is_implies(e1,e2,e3)) { + result.push_back(e2); + result[i] = m.mk_not(e3); + --i; + } + else if (m.is_true(result[i].get()) || + (m.is_not(result[i].get(), e1) && + m.is_false(e1))) { + result[i] = result.back(); + result.pop_back(); + --i; + } + else if (m.is_false(result[i].get()) || + (m.is_not(result[i].get(), e1) && + m.is_true(e1))) { + result.reset(); + result.push_back(m.mk_false()); + return; + } + } +} + +void flatten_and(expr* fml, expr_ref_vector& result) { + SASSERT(result.get_manager().is_bool(fml)); + result.push_back(fml); + flatten_and(result); +} + +void flatten_or(expr_ref_vector& result) { + ast_manager& m = result.get_manager(); + expr* e1, *e2, *e3; + for (unsigned i = 0; i < result.size(); ++i) { + if (m.is_or(result[i].get())) { + app* a = to_app(result[i].get()); + unsigned num_args = a->get_num_args(); + for (unsigned j = 0; j < num_args; ++j) { + result.push_back(a->get_arg(j)); + } + result[i] = result.back(); + result.pop_back(); + --i; + } + else if (m.is_not(result[i].get(), e1) && m.is_not(e1, e2)) { + result[i] = e2; + --i; + } + else if (m.is_not(result[i].get(), e1) && m.is_and(e1)) { + app* a = to_app(e1); + unsigned num_args = a->get_num_args(); + for (unsigned j = 0; j < num_args; ++j) { + result.push_back(m.mk_not(a->get_arg(j))); + } + result[i] = result.back(); + result.pop_back(); + --i; + } + else if (m.is_implies(result[i].get(),e2,e3)) { + result.push_back(e3); + result[i] = m.mk_not(e2); + --i; + } + else if (m.is_false(result[i].get()) || + (m.is_not(result[i].get(), e1) && + m.is_true(e1))) { + result[i] = result.back(); + result.pop_back(); + --i; + } + else if (m.is_true(result[i].get()) || + (m.is_not(result[i].get(), e1) && + m.is_false(e1))) { + result.reset(); + result.push_back(m.mk_true()); + return; + } + } +} + + +void flatten_or(expr* fml, expr_ref_vector& result) { + SASSERT(result.get_manager().is_bool(fml)); + result.push_back(fml); + flatten_or(result); +} diff --git a/src/ast/ast_util.h b/src/ast/ast_util.h index 1e813b1b0..f09cc2789 100644 --- a/src/ast/ast_util.h +++ b/src/ast/ast_util.h @@ -126,5 +126,18 @@ expr * mk_not(ast_manager & m, expr * arg); */ expr * expand_distinct(ast_manager & m, unsigned num_args, expr * const * args); +/** + \brief Collect top-level conjunctions and disjunctions. +*/ + +void flatten_and(expr_ref_vector& result); + +void flatten_and(expr* fml, expr_ref_vector& result); + +void flatten_or(expr_ref_vector& result); + +void flatten_or(expr* fml, expr_ref_vector& result); + + #endif /* _AST_UTIL_H_ */ diff --git a/src/muz/base/dl_boogie_proof.cpp b/src/muz/base/dl_boogie_proof.cpp index cc0e28e2a..75579323c 100644 --- a/src/muz/base/dl_boogie_proof.cpp +++ b/src/muz/base/dl_boogie_proof.cpp @@ -55,7 +55,7 @@ Example from Boogie: #include "model_pp.h" #include "proof_utils.h" #include "ast_pp.h" -#include "qe_util.h" +#include "ast_util.h" namespace datalog { @@ -97,7 +97,7 @@ namespace datalog { if (!m.is_implies(premise, l1, l2)) { continue; } - qe::flatten_and(l1, literals); + flatten_and(l1, literals); positions2.reset(); premises2.reset(); premises2.push_back(premise); diff --git a/src/muz/base/dl_rule.cpp b/src/muz/base/dl_rule.cpp index eabe1d551..aa010ab5a 100644 --- a/src/muz/base/dl_rule.cpp +++ b/src/muz/base/dl_rule.cpp @@ -259,7 +259,7 @@ namespace datalog { if (m.is_implies(fml, e1, e2)) { m_args.reset(); head = ensure_app(e2); - qe::flatten_and(e1, m_args); + flatten_and(e1, m_args); for (unsigned i = 0; i < m_args.size(); ++i) { body.push_back(ensure_app(m_args[i].get())); } @@ -378,7 +378,7 @@ namespace datalog { for (unsigned i = 0; i < body.size(); ++i) { r.push_back(body[i].get()); } - qe::flatten_and(r); + flatten_and(r); body.reset(); for (unsigned i = 0; i < r.size(); ++i) { body.push_back(ensure_app(r[i].get())); diff --git a/src/muz/base/hnf.cpp b/src/muz/base/hnf.cpp index a0dbe9518..58b626808 100644 --- a/src/muz/base/hnf.cpp +++ b/src/muz/base/hnf.cpp @@ -53,6 +53,7 @@ Notes: #include"cooperate.h" #include"ast_pp.h" #include"quant_hoist.h" +#include"ast_util.h" #include"dl_util.h" #include"for_each_ast.h" #include"for_each_expr.h" @@ -247,7 +248,7 @@ private: m_body.push_back(e1); head = e2; } - qe::flatten_and(m_body); + flatten_and(m_body); if (premise) { p = m.mk_rewrite(fml0, mk_implies(m_body, head)); } diff --git a/src/muz/fp/horn_tactic.cpp b/src/muz/fp/horn_tactic.cpp index 6032b3f02..8e9e48f55 100644 --- a/src/muz/fp/horn_tactic.cpp +++ b/src/muz/fp/horn_tactic.cpp @@ -28,6 +28,7 @@ Revision History: #include"filter_model_converter.h" #include"dl_transforms.h" #include"fixedpoint_params.hpp" +#include"ast_util.h" class horn_tactic : public tactic { struct imp { @@ -145,7 +146,7 @@ class horn_tactic : public tactic { expr_ref_vector args(m), body(m); expr_ref head(m); expr* a = 0, *a1 = 0; - qe::flatten_or(tmp, args); + flatten_or(tmp, args); for (unsigned i = 0; i < args.size(); ++i) { a = args[i].get(); check_predicate(mark, a); diff --git a/src/muz/pdr/pdr_closure.cpp b/src/muz/pdr/pdr_closure.cpp index 86af8b2f9..eacbb0b28 100644 --- a/src/muz/pdr/pdr_closure.cpp +++ b/src/muz/pdr/pdr_closure.cpp @@ -143,7 +143,7 @@ namespace pdr { expr_ref closure::close_conjunction(expr* fml) { expr_ref_vector fmls(m); - qe::flatten_and(fml, fmls); + flatten_and(fml, fmls); for (unsigned i = 0; i < fmls.size(); ++i) { fmls[i] = close_fml(fmls[i].get()); } diff --git a/src/muz/pdr/pdr_context.cpp b/src/muz/pdr/pdr_context.cpp index 134c0746d..ddf2a9820 100644 --- a/src/muz/pdr/pdr_context.cpp +++ b/src/muz/pdr/pdr_context.cpp @@ -349,7 +349,7 @@ namespace pdr { void pred_transformer::add_property(expr* lemma, unsigned lvl) { expr_ref_vector lemmas(m); - qe::flatten_and(lemma, lemmas); + flatten_and(lemma, lemmas); for (unsigned i = 0; i < lemmas.size(); ++i) { expr* lemma_i = lemmas[i].get(); if (add_property1(lemma_i, lvl)) { @@ -594,7 +594,7 @@ namespace pdr { for (unsigned i = ut_size; i < t_size; ++i) { tail.push_back(rule.get_tail(i)); } - qe::flatten_and(tail); + flatten_and(tail); for (unsigned i = 0; i < tail.size(); ++i) { expr_ref tmp(m); var_subst(m, false)(tail[i].get(), var_reprs.size(), (expr*const*)var_reprs.c_ptr(), tmp); @@ -809,7 +809,7 @@ namespace pdr { ast_manager& m = pt().get_manager(); expr_ref_vector conjs(m); obj_map model; - qe::flatten_and(state(), conjs); + flatten_and(state(), conjs); for (unsigned i = 0; i < conjs.size(); ++i) { expr* e = conjs[i].get(), *e1, *e2; if (m.is_eq(e, e1, e2) || m.is_iff(e, e1, e2)) { @@ -2176,7 +2176,7 @@ namespace pdr { expr_ref_vector mdl(m), forms(m), Phi(m); forms.push_back(T); forms.push_back(phi); - qe::flatten_and(forms); + flatten_and(forms); ptr_vector forms1(forms.size(), forms.c_ptr()); if (use_model_generalizer) { Phi.append(mev.minimize_model(forms1, M)); @@ -2232,7 +2232,7 @@ namespace pdr { TRACE("pdr", tout << "Projected:\n" << mk_pp(phi1, m) << "\n";); } Phi.reset(); - qe::flatten_and(phi1, Phi); + flatten_and(phi1, Phi); unsigned_vector indices; vector child_states; child_states.resize(preds.size(), expr_ref_vector(m)); diff --git a/src/muz/pdr/pdr_farkas_learner.cpp b/src/muz/pdr/pdr_farkas_learner.cpp index 5946ccb2a..94265e95d 100644 --- a/src/muz/pdr/pdr_farkas_learner.cpp +++ b/src/muz/pdr/pdr_farkas_learner.cpp @@ -449,7 +449,7 @@ namespace pdr { expr_set bs; expr_ref_vector blist(m_pr); - qe::flatten_and(B, blist); + flatten_and(B, blist); for (unsigned i = 0; i < blist.size(); ++i) { bs.insert(blist[i].get()); } diff --git a/src/muz/pdr/pdr_generalizers.cpp b/src/muz/pdr/pdr_generalizers.cpp index 8b6f6a4c6..fd700cfd7 100644 --- a/src/muz/pdr/pdr_generalizers.cpp +++ b/src/muz/pdr/pdr_generalizers.cpp @@ -119,7 +119,7 @@ namespace pdr { if (core.empty()) return; expr_ref A(m), B(qe::mk_and(core)), C(m); expr_ref_vector Bs(m); - qe::flatten_or(B, Bs); + flatten_or(B, Bs); A = n.pt().get_propagation_formula(m_ctx.get_pred_transformers(), n.level()); bool change = false; @@ -138,7 +138,7 @@ namespace pdr { C = qe::mk_or(Bs); TRACE("pdr", tout << "prop:\n" << mk_pp(A,m) << "\ngen:" << mk_pp(B, m) << "\nto: " << mk_pp(C, m) << "\n";); core.reset(); - qe::flatten_and(C, core); + flatten_and(C, core); uses_level = true; } } @@ -190,7 +190,7 @@ namespace pdr { expr_ref fml2 = n.pt().get_formulas(n.level(), false); fml1_2.push_back(fml1); fml1_2.push_back(0); - qe::flatten_and(fml2, fmls); + flatten_and(fml2, fmls); for (unsigned i = 0; i < fmls.size(); ++i) { fml2 = m.mk_not(fmls[i].get()); fml1_2[1] = fml2; diff --git a/src/muz/pdr/pdr_manager.cpp b/src/muz/pdr/pdr_manager.cpp index c029d1b16..1e808c455 100644 --- a/src/muz/pdr/pdr_manager.cpp +++ b/src/muz/pdr/pdr_manager.cpp @@ -56,7 +56,7 @@ namespace pdr { expr_ref inductive_property::fixup_clause(expr* fml) const { expr_ref_vector disjs(m); - qe::flatten_or(fml, disjs); + flatten_or(fml, disjs); expr_ref result(m); bool_rewriter(m).mk_or(disjs.size(), disjs.c_ptr(), result); return result; @@ -65,7 +65,7 @@ namespace pdr { expr_ref inductive_property::fixup_clauses(expr* fml) const { expr_ref_vector conjs(m); expr_ref result(m); - qe::flatten_and(fml, conjs); + flatten_and(fml, conjs); for (unsigned i = 0; i < conjs.size(); ++i) { conjs[i] = fixup_clause(conjs[i].get()); } @@ -237,7 +237,7 @@ namespace pdr { expr_ref manager::mk_not_and(expr_ref_vector const& conjs) { expr_ref result(m), e(m); expr_ref_vector es(conjs); - qe::flatten_and(es); + flatten_and(es); for (unsigned i = 0; i < es.size(); ++i) { m_brwr.mk_not(es[i].get(), e); es[i] = e; diff --git a/src/muz/pdr/pdr_prop_solver.cpp b/src/muz/pdr/pdr_prop_solver.cpp index 9ba976254..8c407161e 100644 --- a/src/muz/pdr/pdr_prop_solver.cpp +++ b/src/muz/pdr/pdr_prop_solver.cpp @@ -76,7 +76,7 @@ namespace pdr { } void mk_safe(expr_ref_vector& conjs) { - qe::flatten_and(conjs); + flatten_and(conjs); expand_literals(conjs); for (unsigned i = 0; i < conjs.size(); ++i) { expr * lit = conjs[i].get(); diff --git a/src/muz/pdr/pdr_util.cpp b/src/muz/pdr/pdr_util.cpp index 18e5b680d..f8758d997 100644 --- a/src/muz/pdr/pdr_util.cpp +++ b/src/muz/pdr/pdr_util.cpp @@ -93,7 +93,7 @@ namespace pdr { void reduce_disequalities(model& model, unsigned threshold, expr_ref& fml) { ast_manager& m = fml.get_manager(); expr_ref_vector conjs(m); - qe::flatten_and(fml, conjs); + flatten_and(fml, conjs); obj_map diseqs; expr* n, *lhs, *rhs; for (unsigned i = 0; i < conjs.size(); ++i) { diff --git a/src/muz/rel/karr_relation.cpp b/src/muz/rel/karr_relation.cpp index 6b9126161..d7ea7de6b 100644 --- a/src/muz/rel/karr_relation.cpp +++ b/src/muz/rel/karr_relation.cpp @@ -6,6 +6,7 @@ Copyright (c) 2015 Microsoft Corporation #include "karr_relation.h" #include "bool_rewriter.h" +#include "ast_util.h" namespace datalog { class karr_relation : public relation_base { @@ -114,7 +115,7 @@ namespace datalog { var* v, *w; rational n1, n2; expr_ref_vector conjs(m); - qe::flatten_and(cond, conjs); + flatten_and(cond, conjs); matrix& M = get_ineqs(); unsigned num_columns = get_signature().size(); diff --git a/src/muz/rel/udoc_relation.cpp b/src/muz/rel/udoc_relation.cpp index 587c5bfe1..d90270d9f 100644 --- a/src/muz/rel/udoc_relation.cpp +++ b/src/muz/rel/udoc_relation.cpp @@ -648,7 +648,7 @@ namespace datalog { ast_manager& m = get_plugin().get_ast_manager(); expr_ref_vector conds(m), guards(m), rests(m); conds.push_back(cond); - qe::flatten_and(conds); + flatten_and(conds); for (unsigned i = 0; i < conds.size(); ++i) { expr* g = conds[i].get(); if (is_guard(g)) { @@ -667,7 +667,7 @@ namespace datalog { ast_manager& m = get_plugin().get_ast_manager(); expr_ref_vector conds(m); conds.push_back(g); - qe::flatten_and(conds); + flatten_and(conds); expr* e1, *e2; for (unsigned i = 0; i < conds.size(); ++i) { expr* g = conds[i].get(); diff --git a/src/muz/tab/tab_context.cpp b/src/muz/tab/tab_context.cpp index 9b005cb54..472b28292 100644 --- a/src/muz/tab/tab_context.cpp +++ b/src/muz/tab/tab_context.cpp @@ -31,6 +31,7 @@ Revision History: #include "matcher.h" #include "scoped_proof.h" #include "fixedpoint_params.hpp" +#include "ast_util.h" namespace tb { @@ -210,7 +211,7 @@ namespace tb { fmls.push_back(m_predicates[i]); } fmls.push_back(m_constraint); - qe::flatten_and(fmls); + flatten_and(fmls); bool_rewriter(m).mk_and(fmls.size(), fmls.c_ptr(), fml); return fml; } @@ -341,7 +342,7 @@ namespace tb { expr_ref tmp(m); substitution subst(m); subst.reserve(1, get_num_vars()); - qe::flatten_and(m_constraint, fmls); + flatten_and(m_constraint, fmls); unsigned num_fmls = fmls.size(); for (unsigned i = 0; i < num_fmls; ++i) { if (get_subst(rw, subst, i, fmls)) { @@ -668,7 +669,7 @@ namespace tb { m_qe(m_empty_set, false, fmls); - qe::flatten_and(fmls); + flatten_and(fmls); for (unsigned i = 0; i < fmls.size(); ++i) { expr_ref n = normalize(fmls[i].get()); if (m_sat_lits.contains(n)) { diff --git a/src/muz/transforms/dl_mk_array_blast.cpp b/src/muz/transforms/dl_mk_array_blast.cpp index bc3b0cc38..82d351113 100644 --- a/src/muz/transforms/dl_mk_array_blast.cpp +++ b/src/muz/transforms/dl_mk_array_blast.cpp @@ -18,9 +18,10 @@ Revision History: --*/ #include "dl_mk_array_blast.h" -#include "qe_util.h" +#include "ast_util.h" #include "scoped_proof.h" + namespace datalog { @@ -115,7 +116,7 @@ namespace datalog { bool mk_array_blast::ackermanize(rule const& r, expr_ref& body, expr_ref& head) { expr_ref_vector conjs(m), trail(m); - qe::flatten_and(body, conjs); + flatten_and(body, conjs); m_defs.reset(); m_next_var = 0; ptr_vector todo; @@ -246,7 +247,7 @@ namespace datalog { for (unsigned i = utsz; i < tsz; ++i) { conjs.push_back(r.get_tail(i)); } - qe::flatten_and(conjs); + flatten_and(conjs); for (unsigned i = 0; i < conjs.size(); ++i) { expr* x, *y, *e = conjs[i].get(); diff --git a/src/muz/transforms/dl_mk_interp_tail_simplifier.cpp b/src/muz/transforms/dl_mk_interp_tail_simplifier.cpp index ca3042ff5..ea0e6c887 100644 --- a/src/muz/transforms/dl_mk_interp_tail_simplifier.cpp +++ b/src/muz/transforms/dl_mk_interp_tail_simplifier.cpp @@ -25,6 +25,7 @@ Revision History: #include"rewriter_def.h" #include"dl_mk_rule_inliner.h" #include"dl_mk_interp_tail_simplifier.h" +#include"ast_util.h" namespace datalog { @@ -547,7 +548,7 @@ namespace datalog { if (modified) { m_conj.reset(); - qe::flatten_and(simp_res, m_conj); + flatten_and(simp_res, m_conj); for (unsigned i = 0; i < m_conj.size(); ++i) { expr* e = m_conj[i].get(); if (is_app(e)) { diff --git a/src/muz/transforms/dl_mk_quantifier_instantiation.cpp b/src/muz/transforms/dl_mk_quantifier_instantiation.cpp index 95d3e8e73..5d36d26cc 100644 --- a/src/muz/transforms/dl_mk_quantifier_instantiation.cpp +++ b/src/muz/transforms/dl_mk_quantifier_instantiation.cpp @@ -49,7 +49,7 @@ namespace datalog { for (unsigned j = 0; j < tsz; ++j) { conjs.push_back(r.get_tail(j)); } - qe::flatten_and(conjs); + flatten_and(conjs); for (unsigned j = 0; j < conjs.size(); ++j) { expr* e = conjs[j].get(); quantifier* q; diff --git a/src/muz/transforms/dl_mk_slice.cpp b/src/muz/transforms/dl_mk_slice.cpp index 2a49d534e..2f7d0d475 100644 --- a/src/muz/transforms/dl_mk_slice.cpp +++ b/src/muz/transforms/dl_mk_slice.cpp @@ -52,6 +52,7 @@ Revision History: #include "dl_mk_slice.h" #include "ast_pp.h" +#include "ast_util.h" #include "expr_functors.h" #include "dl_mk_rule_inliner.h" #include "model_smt2_pp.h" @@ -619,7 +620,7 @@ namespace datalog { for (unsigned j = r.get_uninterpreted_tail_size(); j < r.get_tail_size(); ++j) { conjs.push_back(r.get_tail(j)); } - qe::flatten_and(conjs); + flatten_and(conjs); return conjs; } diff --git a/src/qe/qe.cpp b/src/qe/qe.cpp index 7372fdc2c..34b697a94 100644 --- a/src/qe/qe.cpp +++ b/src/qe/qe.cpp @@ -81,7 +81,7 @@ namespace qe { ptr_vector todo; ptr_vector conjs_closed, conjs_mixed, conjs_open; - qe::flatten_and(fml, conjs); + flatten_and(fml, conjs); for (unsigned i = 0; i < conjs.size(); ++i) { todo.push_back(conjs[i].get()); @@ -306,7 +306,7 @@ namespace qe { // conj_enum conj_enum::conj_enum(ast_manager& m, expr* e): m(m), m_conjs(m) { - qe::flatten_and(e, m_conjs); + flatten_and(e, m_conjs); } void conj_enum::extract_equalities(expr_ref_vector& eqs) { diff --git a/src/qe/qe_arith.cpp b/src/qe/qe_arith.cpp index 360c2ac8c..bc4a824d1 100644 --- a/src/qe/qe_arith.cpp +++ b/src/qe/qe_arith.cpp @@ -20,6 +20,7 @@ Revision History: #include "qe_arith.h" #include "qe_util.h" +#include "ast_util.h" #include "arith_decl_plugin.h" #include "ast_pp.h" #include "th_rewriter.h" @@ -299,7 +300,7 @@ namespace qe { ast_manager& m = vars.get_manager(); arith_project_util ap(m); expr_ref_vector lits(m); - qe::flatten_and(fml, lits); + flatten_and(fml, lits); return ap(model, vars, lits); } diff --git a/src/qe/qe_lite.cpp b/src/qe/qe_lite.cpp index 41214acb3..61fb91524 100644 --- a/src/qe/qe_lite.cpp +++ b/src/qe/qe_lite.cpp @@ -30,6 +30,7 @@ Revision History: #include "bool_rewriter.h" #include "var_subst.h" #include "uint_set.h" +#include "ast_util.h" #include "qe_util.h" #include "th_rewriter.h" #include "for_each_expr.h" @@ -723,7 +724,7 @@ namespace eq { m_subst(r, m_subst_map.size(), m_subst_map.c_ptr(), new_r); m_rewriter(new_r); conjs.reset(); - qe::flatten_and(new_r, conjs); + flatten_and(new_r, conjs); reduced = true; } } @@ -2414,7 +2415,7 @@ public: void operator()(uint_set const& index_set, bool index_of_bound, expr_ref& fml) { expr_ref_vector disjs(m); - qe::flatten_or(fml, disjs); + flatten_or(fml, disjs); for (unsigned i = 0; i < disjs.size(); ++i) { expr_ref_vector conjs(m); conjs.push_back(disjs[i].get()); @@ -2427,7 +2428,7 @@ public: void operator()(uint_set const& index_set, bool index_of_bound, expr_ref_vector& fmls) { - qe::flatten_and(fmls); + flatten_and(fmls); unsigned index; if (has_unique_non_ground(fmls, index)) { expr_ref fml(m); diff --git a/src/qe/qe_util.cpp b/src/qe/qe_util.cpp index 2cf723c08..2bcda608f 100644 --- a/src/qe/qe_util.cpp +++ b/src/qe/qe_util.cpp @@ -8,118 +8,6 @@ Copyright (c) 2015 Microsoft Corporation #include "bool_rewriter.h" namespace qe { - void flatten_and(expr_ref_vector& result) { - ast_manager& m = result.get_manager(); - expr* e1, *e2, *e3; - for (unsigned i = 0; i < result.size(); ++i) { - if (m.is_and(result[i].get())) { - app* a = to_app(result[i].get()); - unsigned num_args = a->get_num_args(); - for (unsigned j = 0; j < num_args; ++j) { - result.push_back(a->get_arg(j)); - } - result[i] = result.back(); - result.pop_back(); - --i; - } - else if (m.is_not(result[i].get(), e1) && m.is_not(e1, e2)) { - result[i] = e2; - --i; - } - else if (m.is_not(result[i].get(), e1) && m.is_or(e1)) { - app* a = to_app(e1); - unsigned num_args = a->get_num_args(); - for (unsigned j = 0; j < num_args; ++j) { - result.push_back(m.mk_not(a->get_arg(j))); - } - result[i] = result.back(); - result.pop_back(); - --i; - } - else if (m.is_not(result[i].get(), e1) && m.is_implies(e1,e2,e3)) { - result.push_back(e2); - result[i] = m.mk_not(e3); - --i; - } - else if (m.is_true(result[i].get()) || - (m.is_not(result[i].get(), e1) && - m.is_false(e1))) { - result[i] = result.back(); - result.pop_back(); - --i; - } - else if (m.is_false(result[i].get()) || - (m.is_not(result[i].get(), e1) && - m.is_true(e1))) { - result.reset(); - result.push_back(m.mk_false()); - return; - } - } - } - - void flatten_and(expr* fml, expr_ref_vector& result) { - SASSERT(result.get_manager().is_bool(fml)); - result.push_back(fml); - flatten_and(result); - } - - void flatten_or(expr_ref_vector& result) { - ast_manager& m = result.get_manager(); - expr* e1, *e2, *e3; - for (unsigned i = 0; i < result.size(); ++i) { - if (m.is_or(result[i].get())) { - app* a = to_app(result[i].get()); - unsigned num_args = a->get_num_args(); - for (unsigned j = 0; j < num_args; ++j) { - result.push_back(a->get_arg(j)); - } - result[i] = result.back(); - result.pop_back(); - --i; - } - else if (m.is_not(result[i].get(), e1) && m.is_not(e1, e2)) { - result[i] = e2; - --i; - } - else if (m.is_not(result[i].get(), e1) && m.is_and(e1)) { - app* a = to_app(e1); - unsigned num_args = a->get_num_args(); - for (unsigned j = 0; j < num_args; ++j) { - result.push_back(m.mk_not(a->get_arg(j))); - } - result[i] = result.back(); - result.pop_back(); - --i; - } - else if (m.is_implies(result[i].get(),e2,e3)) { - result.push_back(e3); - result[i] = m.mk_not(e2); - --i; - } - else if (m.is_false(result[i].get()) || - (m.is_not(result[i].get(), e1) && - m.is_true(e1))) { - result[i] = result.back(); - result.pop_back(); - --i; - } - else if (m.is_true(result[i].get()) || - (m.is_not(result[i].get(), e1) && - m.is_false(e1))) { - result.reset(); - result.push_back(m.mk_true()); - return; - } - } - } - - - void flatten_or(expr* fml, expr_ref_vector& result) { - SASSERT(result.get_manager().is_bool(fml)); - result.push_back(fml); - flatten_or(result); - } expr_ref mk_and(expr_ref_vector const& fmls) { ast_manager& m = fmls.get_manager(); diff --git a/src/qe/qe_util.h b/src/qe/qe_util.h index f1a99ec6c..8e546a801 100644 --- a/src/qe/qe_util.h +++ b/src/qe/qe_util.h @@ -22,16 +22,6 @@ Revision History: #include "ast.h" namespace qe { - /** - \brief Collect top-level conjunctions and disjunctions. - */ - void flatten_and(expr_ref_vector& result); - - void flatten_and(expr* fml, expr_ref_vector& result); - - void flatten_or(expr_ref_vector& result); - - void flatten_or(expr* fml, expr_ref_vector& result); expr_ref mk_and(expr_ref_vector const& fmls); From cd05edf8339a42042cdcd9fb57ed413687eb0d3d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 23 Jun 2015 14:45:52 +0200 Subject: [PATCH 21/28] add model on unknown, to address issue #139 Signed-off-by: Nikolaj Bjorner --- src/opt/opt_context.cpp | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index 2a6265fc4..d50dd06d6 100644 --- a/src/opt/opt_context.cpp +++ b/src/opt/opt_context.cpp @@ -225,12 +225,13 @@ namespace opt { IF_VERBOSE(1, verbose_stream() << "(optimize:check-sat)\n";); lbool is_sat = s.check_sat(0,0); TRACE("opt", tout << "initial search result: " << is_sat << "\n";); + if (is_sat != l_false) { + s.get_model(m_model); + } if (is_sat != l_true) { - m_model = 0; return is_sat; } IF_VERBOSE(1, verbose_stream() << "(optimize:sat)\n";); - s.get_model(m_model); TRACE("opt", model_smt2_pp(tout, m, *m_model, 0);); m_optsmt.setup(*m_opt_solver.get()); update_lower(); From 44ef4074e23ebed3bed71530c63d3f80d893040c Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Tue, 23 Jun 2015 13:59:36 +0100 Subject: [PATCH 22/28] build system: fix typo in OS_DEFINES for linux Signed-off-by: Nuno Lopes --- scripts/mk_util.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 2c95bc26f..cff98818f 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -1874,7 +1874,7 @@ def mk_config(): SLIBFLAGS = '-dynamiclib' elif sysname == 'Linux': CXXFLAGS = '%s -fno-strict-aliasing -D_LINUX_' % CXXFLAGS - OS_DEFINES = '-D_LINUX' + OS_DEFINES = '-D_LINUX_' SO_EXT = '.so' LDFLAGS = '%s -lrt' % LDFLAGS SLIBFLAGS = '-shared' From 03034e7b33fbd58b8b30cb76d2269cb8b1da6529 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 23 Jun 2015 18:57:16 +0200 Subject: [PATCH 23/28] disable bottom-up COI on rules with negated predicates. Fixes issue #140 Signed-off-by: Nikolaj Bjorner --- src/muz/base/dl_context.cpp | 1 + src/muz/base/dl_context.h | 1 + src/muz/base/fixedpoint_params.pyg | 1 + src/muz/transforms/dl_mk_coi_filter.cpp | 7 +++++++ 4 files changed, 10 insertions(+) diff --git a/src/muz/base/dl_context.cpp b/src/muz/base/dl_context.cpp index 9fb597600..a84b1899c 100644 --- a/src/muz/base/dl_context.cpp +++ b/src/muz/base/dl_context.cpp @@ -298,6 +298,7 @@ namespace datalog { bool context::explanations_on_relation_level() const { return m_params->datalog_explanations_on_relation_level(); } bool context::magic_sets_for_queries() const { return m_params->datalog_magic_sets_for_queries(); } symbol context::tab_selection() const { return m_params->tab_selection(); } + bool context::xform_coi() const { return m_params->xform_coi(); } bool context::xform_slice() const { return m_params->xform_slice(); } bool context::xform_bit_blast() const { return m_params->xform_bit_blast(); } bool context::karr() const { return m_params->xform_karr(); } diff --git a/src/muz/base/dl_context.h b/src/muz/base/dl_context.h index 9f94bd869..d8d961a6a 100644 --- a/src/muz/base/dl_context.h +++ b/src/muz/base/dl_context.h @@ -277,6 +277,7 @@ namespace datalog { bool instantiate_quantifiers() const; bool xform_bit_blast() const; bool xform_slice() const; + bool xform_coi() const; void register_finite_sort(sort * s, sort_kind k); diff --git a/src/muz/base/fixedpoint_params.pyg b/src/muz/base/fixedpoint_params.pyg index 33d1daf57..86cfb30ac 100644 --- a/src/muz/base/fixedpoint_params.pyg +++ b/src/muz/base/fixedpoint_params.pyg @@ -142,6 +142,7 @@ def_module_params('fixedpoint', ('xform.instantiate_quantifiers', BOOL, False, "instantiate quantified Horn clauses using E-matching heuristic"), ('xform.coalesce_rules', BOOL, False, "coalesce rules"), + ('xform.coi', BOOL, True, "use cone of influence simplificaiton"), ('duality.enable_restarts', BOOL, False, 'DUALITY: enable restarts'), )) diff --git a/src/muz/transforms/dl_mk_coi_filter.cpp b/src/muz/transforms/dl_mk_coi_filter.cpp index cdb4a5b9e..477eda408 100644 --- a/src/muz/transforms/dl_mk_coi_filter.cpp +++ b/src/muz/transforms/dl_mk_coi_filter.cpp @@ -36,6 +36,9 @@ namespace datalog { // ----------------------------------- rule_set * mk_coi_filter::operator()(rule_set const & source) { + if (!m_context.xform_coi()) { + return 0; + } if (source.empty()) { return 0; } @@ -70,6 +73,10 @@ namespace datalog { e->get_data().m_value = alloc(ptr_vector); } e->get_data().m_value->push_back(r); + if (r->is_neg_tail(i)) { + // don't try COI on rule with negation. + return 0; + } } } } From 1544105bd5ab26f213e8718445518ddadfb164df Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 23 Jun 2015 19:18:03 +0200 Subject: [PATCH 24/28] set undo trail after set-watches to avoid crash during exception handling (the relevancy trail is scoped so ends up traversing the trail if allocating the watch throws an exception). Fixes crash.smt in issue #56 Signed-off-by: Nikolaj Bjorner --- src/smt/smt_relevancy.cpp | 2 +- src/util/memory_manager.cpp | 6 ++++++ 2 files changed, 7 insertions(+), 1 deletion(-) diff --git a/src/smt/smt_relevancy.cpp b/src/smt/smt_relevancy.cpp index 47e3e3ef4..b7a2b4011 100644 --- a/src/smt/smt_relevancy.cpp +++ b/src/smt/smt_relevancy.cpp @@ -212,8 +212,8 @@ namespace smt { return; case l_undef: SASSERT(eh); - push_trail(eh_trail(n, val)); set_watches(n, val, new (get_region()) relevancy_ehs(eh, get_watches(n, val))); + push_trail(eh_trail(n, val)); break; case l_true: eh->operator()(*this, n, val); diff --git a/src/util/memory_manager.cpp b/src/util/memory_manager.cpp index 88bd6b92e..f207fa969 100644 --- a/src/util/memory_manager.cpp +++ b/src/util/memory_manager.cpp @@ -69,6 +69,12 @@ static void throw_out_of_memory() { } static void throw_alloc_counts_exceeded() { + #pragma omp critical (z3_memory_manager) + { + // reset the count to avoid re-throwing while + // the exception is being thrown. + g_memory_alloc_count = 0; + } throw exceeded_memory_allocations(); } From 6bf87083efac6213ea310edfe9139aa342e4a90e Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 24 Jun 2015 07:40:23 +0200 Subject: [PATCH 25/28] fix build break Signed-off-by: Nikolaj Bjorner --- src/test/qe_arith.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/test/qe_arith.cpp b/src/test/qe_arith.cpp index bd8266dc2..40ecbd8c7 100644 --- a/src/test/qe_arith.cpp +++ b/src/test/qe_arith.cpp @@ -62,7 +62,7 @@ static void test(char const *ex) { app_ref_vector vars(m); expr_ref_vector lits(m); vars.push_back(m.mk_const(symbol("x"), a.mk_real())); - qe::flatten_and(fml, lits); + flatten_and(fml, lits); smt::context ctx(m, params); ctx.assert_expr(fml); @@ -89,7 +89,7 @@ static void test2(char const *ex) { vars.push_back(m.mk_const(symbol("x"), a.mk_real())); vars.push_back(m.mk_const(symbol("y"), a.mk_real())); vars.push_back(m.mk_const(symbol("z"), a.mk_real())); - qe::flatten_and(fml, lits); + flatten_and(fml, lits); smt::context ctx(m, params); ctx.push(); From 5cc8c8bde618b8a36f86778aa25812c6762e3d65 Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Wed, 24 Jun 2015 15:00:47 +0100 Subject: [PATCH 26/28] udoc: micro optimization for compiler_guard Signed-off-by: Nuno Lopes --- src/muz/rel/udoc_relation.cpp | 20 ++++++++------------ src/muz/rel/udoc_relation.h | 1 - 2 files changed, 8 insertions(+), 13 deletions(-) diff --git a/src/muz/rel/udoc_relation.cpp b/src/muz/rel/udoc_relation.cpp index d90270d9f..140d1e94d 100644 --- a/src/muz/rel/udoc_relation.cpp +++ b/src/muz/rel/udoc_relation.cpp @@ -723,12 +723,9 @@ namespace datalog { conds.push_back(m.mk_eq(e1, e2)); } - void udoc_relation::compile_guard(expr* g, udoc& d, bit_vector const& discard_cols) const { - d.reset(dm); - d.push_back(dm.allocateX()); - apply_guard(g, d, discard_cols); - } - void udoc_relation::apply_guard(expr* g, udoc& result, bit_vector const& discard_cols) const { + void udoc_relation::compile_guard(expr* g, udoc& result, bit_vector const& discard_cols) const { + result.push_back(dm.allocateX()); + // datastructure to store equalities with columns that will be projected out union_find_default_ctx union_ctx; subset_ints equalities(union_ctx); @@ -737,6 +734,7 @@ namespace datalog { } apply_guard(g, result, equalities, discard_cols); } + bool udoc_relation::apply_ground_eq(doc_ref& d, unsigned v, unsigned hi, unsigned lo, expr* c) const { udoc_plugin& p = get_plugin(); unsigned num_bits; @@ -753,9 +751,6 @@ namespace datalog { return false; } - - - bool udoc_relation::apply_bv_eq( expr* e1, expr* e2, bit_vector const& discard_cols, udoc& result) const { udoc_plugin& p = get_plugin(); @@ -926,9 +921,10 @@ namespace datalog { expr_ref guard(m); for (unsigned i = 0; i < num_bits; ++i) { m_equalities.mk_var(); - } - t.extract_guard(condition, guard, m_reduced_condition); - t.compile_guard(guard, m_udoc, m_empty_bv); + } + t.extract_guard(condition, guard, m_reduced_condition); + m_udoc.push_back(dm.allocateX()); + t.apply_guard(guard, m_udoc, m_equalities, m_empty_bv); TRACE("doc", tout << "original condition: " << mk_pp(condition, m) << "\n"; diff --git a/src/muz/rel/udoc_relation.h b/src/muz/rel/udoc_relation.h index 40f2222fc..d988252da 100644 --- a/src/muz/rel/udoc_relation.h +++ b/src/muz/rel/udoc_relation.h @@ -72,7 +72,6 @@ namespace datalog { void extract_equalities( expr* e1, expr* e2, expr_ref_vector& conds, subset_ints& equalities, unsigned_vector& roots) const; - void apply_guard(expr* g, udoc& result, bit_vector const& discard_cols) const; void apply_guard(expr* g, udoc& result, subset_ints const& equalities, bit_vector const& discard_cols) const; bool apply_ground_eq(doc_ref& d, unsigned v, unsigned hi, unsigned lo, expr* c) const; bool apply_bv_eq(expr* e1, expr* e2, bit_vector const& discard_cols, udoc& result) const; From 30eb461e0170f0e2714b39579a7f79ebd08a5e9f Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Wed, 24 Jun 2015 16:21:58 +0100 Subject: [PATCH 27/28] disable debug output from check_relation Signed-off-by: Nuno Lopes --- src/muz/rel/check_relation.cpp | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/src/muz/rel/check_relation.cpp b/src/muz/rel/check_relation.cpp index 60ca6c0be..0ba03200b 100644 --- a/src/muz/rel/check_relation.cpp +++ b/src/muz/rel/check_relation.cpp @@ -720,12 +720,12 @@ namespace datalog { relation_signature const& sig1 = dst.get_signature(); relation_signature const& sig2 = neg.get_signature(); expr_ref dstf(m), negf(m); - std::cout << mk_pp(dst0, m) << "\n"; + //std::cout << mk_pp(dst0, m) << "\n"; expr_ref_vector eqs(m); dst.to_formula(dstf); - std::cout << mk_pp(dstf, m) << "\n"; + //std::cout << mk_pp(dstf, m) << "\n"; neg.to_formula(negf); - std::cout << mk_pp(negf, m) << "\n"; + //std::cout << mk_pp(negf, m) << "\n"; eqs.push_back(negf); for (unsigned i = 0; i < cols1.size(); ++i) { var_ref v1(m), v2(m); @@ -747,8 +747,8 @@ namespace datalog { negf = m.mk_and(dst0, m.mk_not(negf)); negf = ground(dst, negf); dstf = ground(dst, dstf); - std::cout << negf << "\n"; - std::cout << dstf << "\n"; + //std::cout << negf << "\n"; + //std::cout << dstf << "\n"; check_equiv("filter by negation", dstf, negf); } From f29d82858f937ef2965eaffc552b9df0e0367c3b Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Wed, 24 Jun 2015 17:13:24 +0100 Subject: [PATCH 28/28] make check_relation::check_equiv() exit only when solver return SAT (ie, avoid false-positives with unknowns) Signed-off-by: Nuno Lopes --- src/muz/rel/check_relation.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/muz/rel/check_relation.cpp b/src/muz/rel/check_relation.cpp index 0ba03200b..534a66284 100644 --- a/src/muz/rel/check_relation.cpp +++ b/src/muz/rel/check_relation.cpp @@ -429,7 +429,7 @@ namespace datalog { if (res == l_false) { IF_VERBOSE(3, verbose_stream() << objective << " verified\n";); } - else { + else if (res == l_true) { IF_VERBOSE(3, verbose_stream() << "NOT verified " << res << "\n"; verbose_stream() << mk_pp(fml1, m) << "\n"; verbose_stream() << mk_pp(fml2, m) << "\n";