diff --git a/src/ast/rewriter/CMakeLists.txt b/src/ast/rewriter/CMakeLists.txt index 804fbcbed..57924b48a 100644 --- a/src/ast/rewriter/CMakeLists.txt +++ b/src/ast/rewriter/CMakeLists.txt @@ -6,13 +6,13 @@ z3_add_component(rewriter bit2int.cpp bool_rewriter.cpp bv_bounds.cpp - bv_elim2.cpp + bv_elim.cpp bv_rewriter.cpp datatype_rewriter.cpp der.cpp distribute_forall.cpp dl_rewriter.cpp - elim_bounds2.cpp + elim_bounds.cpp enum2bv_rewriter.cpp expr_replacer.cpp expr_safe_replace.cpp diff --git a/src/ast/rewriter/bv_elim2.cpp b/src/ast/rewriter/bv_elim.cpp similarity index 99% rename from src/ast/rewriter/bv_elim2.cpp rename to src/ast/rewriter/bv_elim.cpp index 5b542e59e..270d7deb8 100644 --- a/src/ast/rewriter/bv_elim2.cpp +++ b/src/ast/rewriter/bv_elim.cpp @@ -4,7 +4,7 @@ Copyright (c) 2015 Microsoft Corporation --*/ -#include "ast/rewriter/bv_elim2.h" +#include "ast/rewriter/bv_elim.h" #include "ast/bv_decl_plugin.h" #include "ast/rewriter/var_subst.h" #include "ast/rewriter/rewriter_def.h" diff --git a/src/ast/rewriter/bv_elim2.h b/src/ast/rewriter/bv_elim.h similarity index 96% rename from src/ast/rewriter/bv_elim2.h rename to src/ast/rewriter/bv_elim.h index a4829b207..6468cb8b9 100644 --- a/src/ast/rewriter/bv_elim2.h +++ b/src/ast/rewriter/bv_elim.h @@ -17,8 +17,8 @@ Author: Revision History: --*/ -#ifndef BV_ELIM2_H_ -#define BV_ELIM2_H_ +#ifndef BV_ELIM_H_ +#define BV_ELIM_H_ #include "ast/ast.h" #include "ast/rewriter/rewriter.h" diff --git a/src/ast/rewriter/elim_bounds2.cpp b/src/ast/rewriter/elim_bounds2.cpp deleted file mode 100644 index 9691ade09..000000000 --- a/src/ast/rewriter/elim_bounds2.cpp +++ /dev/null @@ -1,203 +0,0 @@ -/*++ -Copyright (c) 2006 Microsoft Corporation - -Module Name: - - elim_bounds2.cpp - -Abstract: - - - -Author: - - Leonardo de Moura (leonardo) 2008-06-28. - -Revision History: - ---*/ - -#ifndef ELIM_BOUNDS_H_ -#define ELIM_BOUNDS_H_ - -#include "ast/used_vars.h" -#include "util/obj_hashtable.h" -#include "ast/rewriter/var_subst.h" -#include "ast/rewriter/elim_bounds2.h" -#include "ast/ast_pp.h" - -elim_bounds_cfg::elim_bounds_cfg(ast_manager & m): - m(m), - m_util(m) { -} - -/** - \brief Find bounds of the form - - (<= x k) - (<= (+ x (* -1 y)) k) - (<= (+ x (* -1 t)) k) - (<= (+ t (* -1 x)) k) - - x and y are a bound variables, t is a ground term and k is a numeral - - It also detects >=, and the atom can be negated. -*/ -bool elim_bounds_cfg::is_bound(expr * n, var * & lower, var * & upper) { - upper = 0; - lower = 0; - bool neg = false; - if (m.is_not(n)) { - n = to_app(n)->get_arg(0); - neg = true; - } - - expr* l = 0, *r = 0; - bool le = false; - if (m_util.is_le(n, l, r) && m_util.is_numeral(r)) { - n = l; - le = true; - } - else if (m_util.is_ge(n, l, r) && m_util.is_numeral(r)) { - n = l; - le = false; - } - else { - return false; - } - - if (neg) - le = !le; - - if (is_var(n)) { - upper = to_var(n); - } - else if (m_util.is_add(n, l, r)) { - expr * arg1 = l; - expr * arg2 = r; - if (is_var(arg1)) - upper = to_var(arg1); - else if (!is_ground(arg1)) - return false; - rational k; - bool is_int; - if (m_util.is_mul(arg2) && m_util.is_numeral(to_app(arg2)->get_arg(0), k, is_int) && k.is_minus_one()) { - arg2 = to_app(arg2)->get_arg(1); - if (is_var(arg2)) - lower = to_var(arg2); - else if (!is_ground(arg2)) - return false; // not supported - } - else { - return false; // not supported - } - } - else { - return false; - } - - if (!le) - std::swap(upper, lower); - - return true; -} - -bool elim_bounds_cfg::is_bound(expr * n) { - var * lower, * upper; - return is_bound(n, lower, upper); -} - - -bool elim_bounds_cfg::reduce_quantifier(quantifier * q, - expr * n, - expr * const * new_patterns, - expr * const * new_no_patterns, - expr_ref & result, - proof_ref & result_pr) { - if (!q->is_forall()) { - return false; - } - unsigned num_vars = q->get_num_decls(); - ptr_buffer atoms; - if (m.is_or(n)) - atoms.append(to_app(n)->get_num_args(), to_app(n)->get_args()); - else - atoms.push_back(n); - used_vars used_vars; - // collect non-candidates - for (expr * a : atoms) { - if (!is_bound(a)) - used_vars.process(a); - } - if (used_vars.uses_all_vars(q->get_num_decls())) { - return false; - } - // collect candidates - obj_hashtable lowers; - obj_hashtable uppers; - obj_hashtable candidate_set; - ptr_buffer candidates; -#define ADD_CANDIDATE(V) if (!lowers.contains(V) && !uppers.contains(V)) { candidate_set.insert(V); candidates.push_back(V); } - for (expr * a : atoms) { - var * lower = 0; - var * upper = 0; - if (is_bound(a, lower, upper)) { - if (lower != 0 && !used_vars.contains(lower->get_idx()) && lower->get_idx() < num_vars) { - ADD_CANDIDATE(lower); - lowers.insert(lower); - } - if (upper != 0 && !used_vars.contains(upper->get_idx()) && upper->get_idx() < num_vars) { - ADD_CANDIDATE(upper); - uppers.insert(upper); - } - } - } - TRACE("elim_bounds", tout << "candidates:\n"; for (unsigned i = 0; i < candidates.size(); i++) tout << mk_pp(candidates[i], m) << "\n";); - // remove candidates that have lower and upper bounds - - for (var * v : candidates) { - if (lowers.contains(v) && uppers.contains(v)) - candidate_set.erase(v); - } - TRACE("elim_bounds", tout << "candidates after filter:\n"; for (unsigned i = 0; i < candidates.size(); i++) tout << mk_pp(candidates[i], m) << "\n";); - if (candidate_set.empty()) { - return false; - } - // remove bounds that contain variables in candidate_set - unsigned j = 0; - for (unsigned i = 0; i < atoms.size(); ++i) { - expr * a = atoms[i]; - var * lower = 0; - var * upper = 0; - if (is_bound(a, lower, upper) && ((lower != 0 && candidate_set.contains(lower)) || (upper != 0 && candidate_set.contains(upper)))) - continue; - atoms[j] = a; - j++; - } - if (j == atoms.size()) { - return false; - } - atoms.resize(j); - expr * new_body = 0; - switch (atoms.size()) { - case 0: - result = m.mk_false(); - result_pr = m.mk_rewrite(q, result); - TRACE("elim_bounds", tout << mk_pp(q, m) << "\n" << result << "\n";); - return true; - case 1: - new_body = atoms[0]; - break; - default: - new_body = m.mk_or(atoms.size(), atoms.c_ptr()); - break; - } - quantifier_ref new_q(m); - new_q = m.update_quantifier(q, new_body); - elim_unused_vars(m, new_q, params_ref(), result); - result_pr = m.mk_rewrite(q, result); - TRACE("elim_bounds", tout << mk_pp(q, m) << "\n" << result << "\n";); - return true; -} - -#endif /* ELIM_BOUNDS_H_ */ diff --git a/src/ast/rewriter/elim_bounds2.h b/src/ast/rewriter/elim_bounds2.h deleted file mode 100644 index e0bba4e60..000000000 --- a/src/ast/rewriter/elim_bounds2.h +++ /dev/null @@ -1,77 +0,0 @@ -/*++ -Copyright (c) 2006 Microsoft Corporation - -Module Name: - - elim_bounds2.h - -Abstract: - - - -Author: - - Leonardo de Moura (leonardo) 2008-06-28. - -Revision History: - ---*/ -#ifndef ELIM_BOUNDS2_H_ -#define ELIM_BOUNDS2_H_ - -#include "ast/ast.h" -#include "ast/arith_decl_plugin.h" -#include "ast/rewriter/rewriter.h" - -/** - \brief Functor for eliminating irrelevant bounds in quantified formulas. - - Example: - (forall (x Int) (y Int) (or (not (>= y x) (not (>= x 0)) (= (select a x) 1)))) - - The bound (>= y x) is irrelevant and can be eliminated. - - This can be easily proved by using Fourier-Motzkin elimination. - - Limitations & Assumptions: - - It assumes the input formula was already simplified. - - It can only handle bounds in the diff-logic fragment. - - \remark This operation is subsumed by Fourier-Motzkin elimination. -*/ -class elim_bounds_cfg : public default_rewriter_cfg { - ast_manager & m; - arith_util m_util; - bool is_bound(expr * n, var * & lower, var * & upper); - bool is_bound(expr * n); -public: - elim_bounds_cfg(ast_manager & m); - - 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); -}; - -/** - \brief Functor for applying elim_bounds2 in all - universal quantifiers in an expression. - - Assumption: the formula was already skolemized. -*/ -class elim_bounds_rw : public rewriter_tpl { -protected: - elim_bounds_cfg m_cfg; -public: - elim_bounds_rw(ast_manager & m): - rewriter_tpl(m, m.proofs_enabled(), m_cfg), - m_cfg(m) - {} - - virtual ~elim_bounds_rw() {} -}; - -#endif /* ELIM_BOUNDS2_H_ */ - diff --git a/src/ast/simplifier/CMakeLists.txt b/src/ast/simplifier/CMakeLists.txt index 52a44595e..649c0486e 100644 --- a/src/ast/simplifier/CMakeLists.txt +++ b/src/ast/simplifier/CMakeLists.txt @@ -1,21 +1,21 @@ z3_add_component(simplifier SOURCES - arith_simplifier_params.cpp - arith_simplifier_plugin.cpp - array_simplifier_params.cpp - array_simplifier_plugin.cpp - basic_simplifier_plugin.cpp - bv_elim.cpp - bv_simplifier_params.cpp - bv_simplifier_plugin.cpp - datatype_simplifier_plugin.cpp - elim_bounds.cpp - fpa_simplifier_plugin.cpp - maximise_ac_sharing.cpp - poly_simplifier_plugin.cpp - seq_simplifier_plugin.cpp - simplifier.cpp - simplifier_plugin.cpp + arith_simplifier_params.cpp +# arith_simplifier_plugin.cpp + array_simplifier_params.cpp +# array_simplifier_plugin.cpp +# basic_simplifier_plugin.cpp +# bv_elim.cpp + bv_simplifier_params.cpp +# bv_simplifier_plugin.cpp +# datatype_simplifier_plugin.cpp +# elim_bounds.cpp +# fpa_simplifier_plugin.cpp +# maximise_ac_sharing.cpp +# poly_simplifier_plugin.cpp +# seq_simplifier_plugin.cpp +# simplifier.cpp +# simplifier_plugin.cpp COMPONENT_DEPENDENCIES rewriter PYG_FILES diff --git a/src/smt/CMakeLists.txt b/src/smt/CMakeLists.txt index 5c4c6b0b9..385d1aaa0 100644 --- a/src/smt/CMakeLists.txt +++ b/src/smt/CMakeLists.txt @@ -2,7 +2,6 @@ z3_add_component(smt SOURCES arith_eq_adapter.cpp arith_eq_solver.cpp -## asserted_formulas.cpp asserted_formulas_new.cpp cached_var_subst.cpp cost_evaluator.cpp diff --git a/src/smt/asserted_formulas.cpp b/src/smt/asserted_formulas.cpp deleted file mode 100644 index 44ccd0bf6..000000000 --- a/src/smt/asserted_formulas.cpp +++ /dev/null @@ -1,879 +0,0 @@ -/*++ -Copyright (c) 2006 Microsoft Corporation - -Module Name: - - asserted_formulas.cpp - -Abstract: - - - -Author: - - Leonardo de Moura (leonardo) 2008-06-11. - -Revision History: - ---*/ -#include "util/warning.h" -#include "ast/ast_ll_pp.h" -#include "ast/ast_pp.h" -#include "ast/for_each_expr.h" -#include "ast/well_sorted.h" -#include "ast/rewriter/rewriter_def.h" -#include "ast/rewriter/pull_ite_tree.h" -#include "ast/rewriter/push_app_ite.h" -#include "ast/rewriter/inj_axiom.h" -#include "ast/simplifier/arith_simplifier_plugin.h" -#include "ast/simplifier/array_simplifier_plugin.h" -#include "ast/simplifier/datatype_simplifier_plugin.h" -#include "ast/simplifier/fpa_simplifier_plugin.h" -#include "ast/simplifier/seq_simplifier_plugin.h" -#include "ast/simplifier/bv_simplifier_plugin.h" -#include "ast/simplifier/bv_elim.h" -#include "ast/simplifier/elim_bounds.h" -#include "ast/normal_forms/pull_quant.h" -#include "ast/normal_forms/nnf.h" -#include "ast/pattern/pattern_inference.h" -#include "ast/rewriter/der.h" -#include "ast/rewriter/distribute_forall.h" -#include "ast/macros/quasi_macros.h" -#include "smt/asserted_formulas.h" -#include "smt/elim_term_ite.h" - -asserted_formulas::asserted_formulas(ast_manager & m, smt_params & p): - m(m), - m_params(p), - m_pre_simplifier(m), - m_simplifier(m), - m_rewriter(m), - m_defined_names(m), - m_static_features(m), - m_asserted_formulas(m), - m_asserted_formula_prs(m), - m_asserted_qhead(0), - m_macro_manager(m), - m_bit2int(m), - m_bv_sharing(m), - m_inconsistent(false), - m_has_quantifiers(false) { - - m_bsimp = 0; - m_bvsimp = 0; - arith_simplifier_plugin * arith_simp = 0; - setup_simplifier_plugins(m_simplifier, m_bsimp, arith_simp, m_bvsimp); - SASSERT(m_bsimp != 0); - SASSERT(arith_simp != 0); - m_macro_finder = alloc(macro_finder, m, m_macro_manager); - - basic_simplifier_plugin * basic_simp = 0; - bv_simplifier_plugin * bv_simp = 0; - setup_simplifier_plugins(m_pre_simplifier, basic_simp, arith_simp, bv_simp); - m_pre_simplifier.enable_presimp(); -} - -void asserted_formulas::setup() { - switch (m_params.m_lift_ite) { - case LI_FULL: - m_params.m_ng_lift_ite = LI_NONE; - break; - case LI_CONSERVATIVE: - if (m_params.m_ng_lift_ite == LI_CONSERVATIVE) - m_params.m_ng_lift_ite = LI_NONE; - break; - default: - break; - } - - if (m_params.m_relevancy_lvl == 0) - m_params.m_relevancy_lemma = false; -} - -void asserted_formulas::setup_simplifier_plugins(simplifier & s, basic_simplifier_plugin * & bsimp, arith_simplifier_plugin * & asimp, bv_simplifier_plugin * & bvsimp) { - bsimp = alloc(basic_simplifier_plugin, m); - s.register_plugin(bsimp); - asimp = alloc(arith_simplifier_plugin, m, *bsimp, m_params); - s.register_plugin(asimp); - s.register_plugin(alloc(array_simplifier_plugin, m, *bsimp, s, m_params)); - bvsimp = alloc(bv_simplifier_plugin, m, *bsimp, m_params); - s.register_plugin(bvsimp); - s.register_plugin(alloc(datatype_simplifier_plugin, m, *bsimp)); - s.register_plugin(alloc(fpa_simplifier_plugin, m, *bsimp)); - s.register_plugin(alloc(seq_simplifier_plugin, m, *bsimp)); -} - -void asserted_formulas::init(unsigned num_formulas, expr * const * formulas, proof * const * prs) { - SASSERT(m_asserted_formulas.empty()); - SASSERT(m_asserted_formula_prs.empty()); - SASSERT(!m_inconsistent); - SASSERT(m_scopes.empty()); - m_asserted_formulas.append(num_formulas, formulas); - if (m.proofs_enabled()) - m_asserted_formula_prs.append(num_formulas, prs); -} - -bool asserted_formulas::has_bv() const { - // approaximated answer... assume the formula has bit-vectors if the bv_simplifier_plugin was invoked at least once. - return m_bvsimp->reduce_invoked(); -} - -asserted_formulas::~asserted_formulas() { -} - -void asserted_formulas::push_assertion(expr * e, proof * pr, expr_ref_vector & result, proof_ref_vector & result_prs) { - if (inconsistent()) { - SASSERT(!result.empty()); - return; - } - if (m.is_false(e)) - m_inconsistent = true; - ::push_assertion(m, e, pr, result, result_prs); -} - -void asserted_formulas::set_eliminate_and(bool flag) { - if (m_bsimp->eliminate_and() == flag) - return; - TRACE("eliminate_and", tout << "flushing cache...\n";); - flush_cache(); - m_bsimp->set_eliminate_and(flag); -} - - -void asserted_formulas::assert_expr(expr * e, proof * _in_pr) { - if (inconsistent()) - return; - m_has_quantifiers |= ::has_quantifiers(e); - if (!m_params.m_preprocess) { - push_assertion(e, _in_pr, m_asserted_formulas, m_asserted_formula_prs); - return; - } - proof_ref in_pr(_in_pr, m); - expr_ref r1(m); - proof_ref pr1(m); - expr_ref r2(m); - proof_ref pr2(m); - TRACE("assert_expr_before_simp", tout << mk_ll_pp(e, m) << "\n";); - TRACE("assert_expr_bug", tout << mk_pp(e, m) << "\n";); - if (m_params.m_pre_simplifier) { - m_pre_simplifier(e, r1, pr1); - } - else { - r1 = e; - pr1 = 0; - } - set_eliminate_and(false); // do not eliminate and before nnf. - m_simplifier(r1, r2, pr2); - TRACE("assert_expr_bug", tout << "after...\n" << mk_pp(r1, m) << "\n";); - if (m.proofs_enabled()) { - if (e == r2) - pr2 = in_pr; - else - pr2 = m.mk_modus_ponens(in_pr, m.mk_transitivity(pr1, pr2)); - } - TRACE("assert_expr_after_simp", tout << mk_ll_pp(r1, m) << "\n";); - push_assertion(r2, pr2, m_asserted_formulas, m_asserted_formula_prs); - TRACE("asserted_formulas_bug", tout << "after assert_expr\n"; display(tout);); -} - -void asserted_formulas::assert_expr(expr * e) { - if (inconsistent()) - return; - assert_expr(e, m.mk_asserted(e)); -} - -void asserted_formulas::get_assertions(ptr_vector & result) { - result.append(m_asserted_formulas.size(), m_asserted_formulas.c_ptr()); -} - -void asserted_formulas::push_scope() { - SASSERT(inconsistent() || m_asserted_qhead == m_asserted_formulas.size() || m.canceled()); - TRACE("asserted_formulas_scopes", tout << "push:\n"; display(tout);); - m_scopes.push_back(scope()); - m_macro_manager.push_scope(); - scope & s = m_scopes.back(); - s.m_asserted_formulas_lim = m_asserted_formulas.size(); - SASSERT(inconsistent() || s.m_asserted_formulas_lim == m_asserted_qhead || m.canceled()); - s.m_inconsistent_old = m_inconsistent; - m_defined_names.push(); - m_bv_sharing.push_scope(); - commit(); -} - -void asserted_formulas::pop_scope(unsigned num_scopes) { - TRACE("asserted_formulas_scopes", tout << "before pop " << num_scopes << "\n"; display(tout);); - m_bv_sharing.pop_scope(num_scopes); - m_macro_manager.pop_scope(num_scopes); - unsigned new_lvl = m_scopes.size() - num_scopes; - scope & s = m_scopes[new_lvl]; - m_inconsistent = s.m_inconsistent_old; - m_defined_names.pop(num_scopes); - m_asserted_formulas.shrink(s.m_asserted_formulas_lim); - if (m.proofs_enabled()) - m_asserted_formula_prs.shrink(s.m_asserted_formulas_lim); - m_asserted_qhead = s.m_asserted_formulas_lim; - m_scopes.shrink(new_lvl); - flush_cache(); - TRACE("asserted_formulas_scopes", tout << "after pop " << num_scopes << "\n"; display(tout);); -} - -void asserted_formulas::reset() { - m_defined_names.reset(); - m_asserted_qhead = 0; - m_asserted_formulas.reset(); - m_asserted_formula_prs.reset(); - m_macro_manager.reset(); - m_bv_sharing.reset(); - m_inconsistent = false; -} - - -#ifdef Z3DEBUG -bool asserted_formulas::check_well_sorted() const { - for (unsigned i = 0; i < m_asserted_formulas.size(); i++) { - if (!is_well_sorted(m, m_asserted_formulas.get(i))) return false; - } - return true; -} -#endif - -void asserted_formulas::reduce() { - if (inconsistent()) - return; - if (canceled()) { - return; - } - if (m_asserted_qhead == m_asserted_formulas.size()) - return; - if (!m_params.m_preprocess) - return; - - if (m_macro_manager.has_macros()) - expand_macros(); - TRACE("before_reduce", display(tout);); - CASSERT("well_sorted", check_well_sorted()); - - -#define INVOKE(COND, FUNC) if (COND) { FUNC; IF_VERBOSE(10000, verbose_stream() << "total size: " << get_total_size() << "\n";); } TRACE("reduce_step_ll", ast_mark visited; display_ll(tout, visited);); TRACE("reduce_step", display(tout << #FUNC << " ");); CASSERT("well_sorted",check_well_sorted()); if (inconsistent() || canceled()) { TRACE("after_reduce", display(tout);); TRACE("after_reduce_ll", ast_mark visited; display_ll(tout, visited);); return; } - - set_eliminate_and(false); // do not eliminate and before nnf. - INVOKE(m_params.m_propagate_booleans, propagate_booleans()); - INVOKE(m_params.m_propagate_values, propagate_values()); - INVOKE(m_params.m_macro_finder && has_quantifiers(), find_macros()); - INVOKE(m_params.m_nnf_cnf || (m_params.m_mbqi && has_quantifiers()), nnf_cnf()); - INVOKE(/*m_params.m_eliminate_and*/ true, eliminate_and()); - INVOKE(m_params.m_pull_cheap_ite_trees, pull_cheap_ite_trees()); - INVOKE(m_params.m_pull_nested_quantifiers && has_quantifiers(), pull_nested_quantifiers()); - INVOKE(m_params.m_ng_lift_ite != LI_NONE, ng_lift_ite()); - INVOKE(m_params.m_lift_ite != LI_NONE, lift_ite()); - INVOKE(m_params.m_eliminate_term_ite && m_params.m_lift_ite != LI_FULL, eliminate_term_ite()); - INVOKE(m_params.m_refine_inj_axiom && has_quantifiers(), refine_inj_axiom()); - INVOKE(m_params.m_distribute_forall && has_quantifiers(), apply_distribute_forall()); - TRACE("qbv_bug", tout << "after distribute_forall:\n"; display(tout);); - INVOKE(m_params.m_macro_finder && has_quantifiers(), find_macros()); - INVOKE(m_params.m_quasi_macros && has_quantifiers(), apply_quasi_macros()); - INVOKE(m_params.m_simplify_bit2int, apply_bit2int()); - INVOKE(m_params.m_eliminate_bounds && has_quantifiers(), cheap_quant_fourier_motzkin()); - INVOKE(m_params.m_ematching && has_quantifiers(), infer_patterns()); - INVOKE(m_params.m_max_bv_sharing && has_bv(), max_bv_sharing()); - INVOKE(m_params.m_bb_quantifiers, elim_bvs_from_quantifiers()); - // temporary HACK: make sure that arith & bv are list-assoc - // this may destroy some simplification steps such as max_bv_sharing - reduce_asserted_formulas(); - - CASSERT("well_sorted",check_well_sorted()); - - IF_VERBOSE(10, verbose_stream() << "(smt.simplifier-done)\n";); - TRACE("after_reduce", display(tout);); - TRACE("after_reduce_ll", ast_mark visited; display_ll(tout, visited);); - TRACE("macros", m_macro_manager.display(tout);); - flush_cache(); -} - -void asserted_formulas::eliminate_and() { - IF_IVERBOSE(10, verbose_stream() << "(smt.eliminating-and)\n";); - set_eliminate_and(true); - reduce_asserted_formulas(); - TRACE("after_elim_and", display(tout);); -} - -unsigned asserted_formulas::get_formulas_last_level() const { - if (m_scopes.empty()) { - return 0; - } - else { - return m_scopes.back().m_asserted_formulas_lim; - } -} - -void asserted_formulas::collect_static_features() { - if (m_params.m_display_features) { - unsigned sz = m_asserted_formulas.size(); - unsigned head = m_asserted_qhead; - while (head < sz) { - expr * f = m_asserted_formulas.get(head); - head++; - m_static_features.collect(f); - } - m_static_features.display_primitive(std::cout); - m_static_features.display(std::cout); - } -} - -void asserted_formulas::display(std::ostream & out) const { - out << "asserted formulas:\n"; - for (unsigned i = 0; i < m_asserted_formulas.size(); i++) { - if (i == m_asserted_qhead) - out << "[HEAD] ==>\n"; - out << mk_pp(m_asserted_formulas.get(i), m) << "\n"; - } - out << "inconsistent: " << inconsistent() << "\n"; -} - -void asserted_formulas::display_ll(std::ostream & out, ast_mark & pp_visited) const { - if (!m_asserted_formulas.empty()) { - unsigned sz = m_asserted_formulas.size(); - for (unsigned i = 0; i < sz; i++) - ast_def_ll_pp(out, m, m_asserted_formulas.get(i), pp_visited, true, false); - out << "asserted formulas:\n"; - for (unsigned i = 0; i < sz; i++) - out << "#" << m_asserted_formulas[i]->get_id() << " "; - out << "\n"; - } -} - -void asserted_formulas::collect_statistics(statistics & st) const { -} - -void asserted_formulas::reduce_asserted_formulas() { - if (inconsistent()) { - return; - } - expr_ref_vector new_exprs(m); - proof_ref_vector new_prs(m); - unsigned i = m_asserted_qhead; - unsigned sz = m_asserted_formulas.size(); - for (; i < sz && !inconsistent(); i++) { - expr * n = m_asserted_formulas.get(i); - SASSERT(n != 0); - proof * pr = m_asserted_formula_prs.get(i, 0); - expr_ref new_n(m); - proof_ref new_pr(m); - m_simplifier(n, new_n, new_pr); - TRACE("reduce_asserted_formulas", tout << mk_pp(n, m) << " -> " << mk_pp(new_n, m) << "\n";); - if (n == new_n.get()) { - push_assertion(n, pr, new_exprs, new_prs); - } - else { - new_pr = m.mk_modus_ponens(pr, new_pr); - push_assertion(new_n, new_pr, new_exprs, new_prs); - } - if (canceled()) { - return; - } - } - swap_asserted_formulas(new_exprs, new_prs); -} - -void asserted_formulas::swap_asserted_formulas(expr_ref_vector & new_exprs, proof_ref_vector & new_prs) { - SASSERT(!inconsistent() || !new_exprs.empty()); - m_asserted_formulas.shrink(m_asserted_qhead); - m_asserted_formulas.append(new_exprs); - if (m.proofs_enabled()) { - m_asserted_formula_prs.shrink(m_asserted_qhead); - m_asserted_formula_prs.append(new_prs); - } -} - -void asserted_formulas::find_macros_core() { - expr_ref_vector new_exprs(m); - proof_ref_vector new_prs(m); - unsigned sz = m_asserted_formulas.size(); - expr_dependency_ref_vector new_deps(m); - m_macro_finder->operator()(sz - m_asserted_qhead, - m_asserted_formulas.c_ptr() + m_asserted_qhead, - m_asserted_formula_prs.c_ptr() + m_asserted_qhead, - 0, // 0 == No dependency tracking - new_exprs, new_prs, new_deps); - swap_asserted_formulas(new_exprs, new_prs); - reduce_and_solve(); -} - -void asserted_formulas::find_macros() { - IF_IVERBOSE(10, verbose_stream() << "(smt.find-macros)\n";); - TRACE("before_find_macros", display(tout);); - find_macros_core(); - TRACE("after_find_macros", display(tout);); -} - -void asserted_formulas::expand_macros() { - IF_IVERBOSE(10, verbose_stream() << "(smt.expand-macros)\n";); - find_macros_core(); -} - -void asserted_formulas::apply_quasi_macros() { - IF_IVERBOSE(10, verbose_stream() << "(smt.find-quasi-macros)\n";); - TRACE("before_quasi_macros", display(tout);); - expr_ref_vector new_exprs(m); - proof_ref_vector new_prs(m); - expr_dependency_ref_vector new_deps(m); - quasi_macros proc(m, m_macro_manager); - while (proc(m_asserted_formulas.size() - m_asserted_qhead, - m_asserted_formulas.c_ptr() + m_asserted_qhead, - m_asserted_formula_prs.c_ptr() + m_asserted_qhead, - 0, // 0 == No dependency tracking - new_exprs, new_prs, new_deps)) { - swap_asserted_formulas(new_exprs, new_prs); - new_exprs.reset(); - new_prs.reset(); - new_deps.reset(); - } - TRACE("after_quasi_macros", display(tout);); - reduce_and_solve(); -} - -void asserted_formulas::nnf_cnf() { - IF_IVERBOSE(10, verbose_stream() << "(smt.nnf)\n";); - nnf apply_nnf(m, m_defined_names); - expr_ref_vector new_exprs(m); - proof_ref_vector new_prs(m); - expr_ref_vector push_todo(m); - proof_ref_vector push_todo_prs(m); - - unsigned i = m_asserted_qhead; - unsigned sz = m_asserted_formulas.size(); - TRACE("nnf_bug", tout << "i: " << i << " sz: " << sz << "\n";); - for (; i < sz; i++) { - expr * n = m_asserted_formulas.get(i); - TRACE("nnf_bug", tout << "processing:\n" << mk_pp(n, m) << "\n";); - proof * pr = m_asserted_formula_prs.get(i, 0); - expr_ref r1(m); - proof_ref pr1(m); - CASSERT("well_sorted",is_well_sorted(m, n)); - push_todo.reset(); - push_todo_prs.reset(); - apply_nnf(n, push_todo, push_todo_prs, r1, pr1); - CASSERT("well_sorted",is_well_sorted(m, r1)); - pr = m.mk_modus_ponens(pr, pr1); - push_todo.push_back(r1); - push_todo_prs.push_back(pr); - - if (canceled()) { - return; - } - unsigned sz2 = push_todo.size(); - for (unsigned k = 0; k < sz2; k++) { - expr * n = push_todo.get(k); - proof * pr = 0; - m_simplifier(n, r1, pr1); - CASSERT("well_sorted",is_well_sorted(m, r1)); - if (canceled()) { - return; - } - - if (m.proofs_enabled()) - pr = m.mk_modus_ponens(push_todo_prs.get(k), pr1); - else - pr = 0; - push_assertion(r1, pr, new_exprs, new_prs); - } - } - swap_asserted_formulas(new_exprs, new_prs); -} - -#define MK_SIMPLE_SIMPLIFIER(NAME, FUNCTOR_DEF, LABEL, MSG) \ -void asserted_formulas::NAME() { \ - IF_IVERBOSE(10, verbose_stream() << "(smt." << MSG << ")\n";); \ - TRACE(LABEL, tout << "before:\n"; display(tout);); \ - FUNCTOR_DEF; \ - expr_ref_vector new_exprs(m); \ - proof_ref_vector new_prs(m); \ - unsigned i = m_asserted_qhead; \ - unsigned sz = m_asserted_formulas.size(); \ - for (; i < sz; i++) { \ - expr * n = m_asserted_formulas.get(i); \ - proof * pr = m_asserted_formula_prs.get(i, 0); \ - expr_ref new_n(m); \ - functor(n, new_n); \ - TRACE("simplifier_simple_step", tout << mk_pp(n, m) << "\n" << mk_pp(new_n, m) << "\n";); \ - if (n == new_n.get()) { \ - push_assertion(n, pr, new_exprs, new_prs); \ - } \ - else if (m.proofs_enabled()) { \ - proof_ref new_pr(m); \ - new_pr = m.mk_rewrite_star(n, new_n, 0, 0); \ - new_pr = m.mk_modus_ponens(pr, new_pr); \ - push_assertion(new_n, new_pr, new_exprs, new_prs); \ - } \ - else { \ - push_assertion(new_n, 0, new_exprs, new_prs); \ - } \ - } \ - swap_asserted_formulas(new_exprs, new_prs); \ - TRACE(LABEL, display(tout);); \ - reduce_and_solve(); \ - TRACE(LABEL, display(tout);); \ -} - -MK_SIMPLE_SIMPLIFIER(apply_distribute_forall, distribute_forall functor(m), "distribute_forall", "distribute-forall"); - -void asserted_formulas::reduce_and_solve() { - IF_IVERBOSE(10, verbose_stream() << "(smt.reducing)\n";); - flush_cache(); // collect garbage - reduce_asserted_formulas(); -} - -void asserted_formulas::infer_patterns() { - IF_IVERBOSE(10, verbose_stream() << "(smt.pattern-inference)\n";); - TRACE("before_pattern_inference", display(tout);); - pattern_inference_rw infer(m, m_params); - expr_ref_vector new_exprs(m); - proof_ref_vector new_prs(m); - unsigned i = m_asserted_qhead; - unsigned sz = m_asserted_formulas.size(); - for (; i < sz; i++) { - expr * n = m_asserted_formulas.get(i); - proof * pr = m_asserted_formula_prs.get(i, 0); - expr_ref new_n(m); - proof_ref new_pr(m); - infer(n, new_n, new_pr); - if (n == new_n.get()) { - push_assertion(n, pr, new_exprs, new_prs); - } - else if (m.proofs_enabled()) { - new_pr = m.mk_modus_ponens(pr, new_pr); - push_assertion(new_n, new_pr, new_exprs, new_prs); - } - else { - push_assertion(new_n, 0, new_exprs, new_prs); - } - } - swap_asserted_formulas(new_exprs, new_prs); - TRACE("after_pattern_inference", display(tout);); -} - -void asserted_formulas::commit() { - commit(m_asserted_formulas.size()); -} - -void asserted_formulas::commit(unsigned new_qhead) { - m_macro_manager.mark_forbidden(new_qhead - m_asserted_qhead, m_asserted_formulas.c_ptr() + m_asserted_qhead); - m_asserted_qhead = new_qhead; -} - -void asserted_formulas::eliminate_term_ite() { - IF_IVERBOSE(10, verbose_stream() << "(smt.eliminating-ite-term)\n";); - TRACE("before_elim_term_ite", display(tout);); - elim_term_ite elim(m, m_defined_names); - expr_ref_vector new_exprs(m); - proof_ref_vector new_prs(m); - unsigned i = m_asserted_qhead; - unsigned sz = m_asserted_formulas.size(); - for (; i < sz; i++) { - expr * n = m_asserted_formulas.get(i); - proof * pr = m_asserted_formula_prs.get(i, 0); - expr_ref new_n(m); - proof_ref new_pr(m); - elim(n, new_exprs, new_prs, new_n, new_pr); - SASSERT(new_n.get() != 0); - DEBUG_CODE({ - for (unsigned i = 0; i < new_exprs.size(); i++) { - SASSERT(new_exprs.get(i) != 0); - } - }); - if (n == new_n.get()) { - push_assertion(n, pr, new_exprs, new_prs); - } - else if (m.proofs_enabled()) { - new_pr = m.mk_modus_ponens(pr, new_pr); - push_assertion(new_n, new_pr, new_exprs, new_prs); - } - else { - push_assertion(new_n, 0, new_exprs, new_prs); - } - } - swap_asserted_formulas(new_exprs, new_prs); - TRACE("after_elim_term_ite", display(tout);); - reduce_and_solve(); - TRACE("after_elim_term_ite", display(tout);); -} - -void asserted_formulas::propagate_values() { - IF_IVERBOSE(10, verbose_stream() << "(smt.constant-propagation)\n";); - TRACE("propagate_values", tout << "before:\n"; display(tout);); - flush_cache(); - bool found = false; - // Separate the formulas in two sets: C and R - // C is a set which contains formulas of the form - // { x = n }, where x is a variable and n a numeral. - // R contains the rest. - // - // - new_exprs1 is the set C - // - new_exprs2 is the set R - // - // The loop also updates the m_cache. It adds the entries x -> n to it. - expr_ref_vector new_exprs1(m); - proof_ref_vector new_prs1(m); - expr_ref_vector new_exprs2(m); - proof_ref_vector new_prs2(m); - unsigned sz = m_asserted_formulas.size(); - for (unsigned i = 0; i < sz; i++) { - expr_ref n(m_asserted_formulas.get(i), m); - proof_ref pr(m_asserted_formula_prs.get(i, 0), m); - TRACE("simplifier", tout << mk_pp(n, m) << "\n";); - expr* lhs, *rhs; - if (m.is_eq(n, lhs, rhs) && - (m.is_value(lhs) || m.is_value(rhs))) { - if (m.is_value(lhs)) { - std::swap(lhs, rhs); - n = m.mk_eq(lhs, rhs); - pr = m.mk_symmetry(pr); - } - if (!m.is_value(lhs) && !m_simplifier.is_cached(lhs)) { - if (i >= m_asserted_qhead) { - new_exprs1.push_back(n); - if (m.proofs_enabled()) - new_prs1.push_back(pr); - } - TRACE("propagate_values", tout << "found:\n" << mk_pp(lhs, m) << "\n->\n" << mk_pp(rhs, m) << "\n"; - if (pr) tout << "proof: " << mk_pp(pr, m) << "\n";); - m_simplifier.cache_result(lhs, rhs, pr); - found = true; - continue; - } - } - if (i >= m_asserted_qhead) { - new_exprs2.push_back(n); - if (m.proofs_enabled()) - new_prs2.push_back(pr); - } - } - TRACE("propagate_values", tout << "found: " << found << "\n";); - // If C is not empty, then reduce R using the updated simplifier cache with entries - // x -> n for each constraint 'x = n' in C. - if (found) { - unsigned sz = new_exprs2.size(); - for (unsigned i = 0; i < sz; i++) { - expr * n = new_exprs2.get(i); - proof * pr = new_prs2.get(i, 0); - expr_ref new_n(m); - proof_ref new_pr(m); - m_simplifier(n, new_n, new_pr); - if (n == new_n.get()) { - push_assertion(n, pr, new_exprs1, new_prs1); - } - else { - new_pr = m.mk_modus_ponens(pr, new_pr); - push_assertion(new_n, new_pr, new_exprs1, new_prs1); - } - } - swap_asserted_formulas(new_exprs1, new_prs1); - // IMPORTANT: the cache MUST be flushed. This guarantees that all entries - // x->n will be removed from m_cache. If we don't do that, the next transformation - // may simplify constraints in C using these entries, and the variables x in C - // will be (silently) eliminated, and models produced by Z3 will not contain them. - flush_cache(); - } - TRACE("propagate_values", tout << "after:\n"; display(tout);); -} - -void asserted_formulas::propagate_booleans() { - bool cont = true; - bool modified = false; - flush_cache(); - while (cont) { - TRACE("propagate_booleans", tout << "before:\n"; display(tout);); - IF_IVERBOSE(10, verbose_stream() << "(smt.propagate-booleans)\n";); - cont = false; - unsigned i = m_asserted_qhead; - unsigned sz = m_asserted_formulas.size(); -#define PROCESS() { \ - expr * n = m_asserted_formulas.get(i); \ - proof * pr = m_asserted_formula_prs.get(i, 0); \ - expr_ref new_n(m); \ - proof_ref new_pr(m); \ - m_simplifier(n, new_n, new_pr); \ - m_asserted_formulas.set(i, new_n); \ - if (m.proofs_enabled()) { \ - new_pr = m.mk_modus_ponens(pr, new_pr); \ - m_asserted_formula_prs.set(i, new_pr); \ - } \ - if (n != new_n) { \ - cont = true; \ - modified = true; \ - } \ - if (m.is_not(new_n)) \ - m_simplifier.cache_result(to_app(new_n)->get_arg(0), m.mk_false(), m.mk_iff_false(new_pr)); \ - else \ - m_simplifier.cache_result(new_n, m.mk_true(), m.mk_iff_true(new_pr)); \ - } - for (; i < sz; i++) { - PROCESS(); - } - flush_cache(); - TRACE("propagate_booleans", tout << "middle:\n"; display(tout);); - i = sz; - while (i > m_asserted_qhead) { - --i; - PROCESS(); - } - flush_cache(); - TRACE("propagate_booleans", tout << "after:\n"; display(tout);); - } - if (modified) - reduce_asserted_formulas(); -} - -#define MK_SIMPLIFIER(NAME, FUNCTOR, TAG, MSG, REDUCE) \ - bool asserted_formulas::NAME() { \ - IF_IVERBOSE(10, verbose_stream() << "(smt." << MSG << ")\n";); \ - TRACE(TAG, ast_mark visited; display_ll(tout, visited);); \ - FUNCTOR; \ - bool changed = false; \ - expr_ref_vector new_exprs(m); \ - proof_ref_vector new_prs(m); \ - unsigned i = m_asserted_qhead; \ - unsigned sz = m_asserted_formulas.size(); \ - for (; i < sz; i++) { \ - expr * n = m_asserted_formulas.get(i); \ - proof * pr = m_asserted_formula_prs.get(i, 0); \ - expr_ref new_n(m); \ - proof_ref new_pr(m); \ - functor(n, new_n, new_pr); \ - if (n == new_n.get()) { \ - push_assertion(n, pr, new_exprs, new_prs); \ - } \ - else if (m.proofs_enabled()) { \ - changed = true; \ - if (!new_pr) new_pr = m.mk_rewrite(n, new_n); \ - new_pr = m.mk_modus_ponens(pr, new_pr); \ - push_assertion(new_n, new_pr, new_exprs, new_prs); \ - } \ - else { \ - changed = true; \ - push_assertion(new_n, 0, new_exprs, new_prs); \ - } \ - } \ - swap_asserted_formulas(new_exprs, new_prs); \ - TRACE(TAG, ast_mark visited; display_ll(tout, visited);); \ - if (changed && REDUCE) { \ - reduce_and_solve(); \ - TRACE(TAG, ast_mark visited; display_ll(tout, visited);); \ - } \ - return changed; \ - } - -MK_SIMPLIFIER(pull_cheap_ite_trees, pull_cheap_ite_tree_rw functor(m), "pull_cheap_ite_trees", "pull-cheap-ite-trees", false); - -MK_SIMPLIFIER(pull_nested_quantifiers, pull_nested_quant functor(m), "pull_nested_quantifiers", "pull-nested-quantifiers", false); - -proof * asserted_formulas::get_inconsistency_proof() const { - if (!inconsistent()) - return 0; - if (!m.proofs_enabled()) - return 0; - unsigned sz = m_asserted_formulas.size(); - for (unsigned i = 0; i < sz; i++) { - expr * f = m_asserted_formulas.get(i); - if (m.is_false(f)) - return m_asserted_formula_prs.get(i); - } - UNREACHABLE(); - return 0; -} - -void asserted_formulas::refine_inj_axiom() { - IF_IVERBOSE(10, verbose_stream() << "(smt.refine-injectivity)\n";); - TRACE("inj_axiom", display(tout);); - unsigned i = m_asserted_qhead; - unsigned sz = m_asserted_formulas.size(); - for (; i < sz; i++) { - expr * n = m_asserted_formulas.get(i); - proof * pr = m_asserted_formula_prs.get(i, 0); - expr_ref new_n(m); - if (is_quantifier(n) && simplify_inj_axiom(m, to_quantifier(n), new_n)) { - TRACE("inj_axiom", tout << "simplifying...\n" << mk_pp(n, m) << "\n" << mk_pp(new_n, m) << "\n";); - m_asserted_formulas.set(i, new_n); - if (m.proofs_enabled()) { - proof_ref new_pr(m); - new_pr = m.mk_rewrite(n, new_n); - new_pr = m.mk_modus_ponens(pr, new_pr); - m_asserted_formula_prs.set(i, new_pr); - } - } - } - TRACE("inj_axiom", display(tout);); -} - -MK_SIMPLIFIER(apply_bit2int, bit2int& functor = m_bit2int, "bit2int", "propagate-bit-vector-over-integers", true); - -MK_SIMPLIFIER(cheap_quant_fourier_motzkin, elim_bounds_star functor(m), "elim_bounds", "cheap-fourier-motzkin", true); - - - -MK_SIMPLIFIER(elim_bvs_from_quantifiers, bv_elim_star functor(m), "bv_elim", "eliminate-bit-vectors-from-quantifiers", true); - -#define LIFT_ITE(NAME, FUNCTOR, MSG) \ - void asserted_formulas::NAME() { \ - IF_IVERBOSE(10, verbose_stream() << "(smt." << MSG << ")\n";); \ - TRACE("lift_ite", display(tout);); \ - FUNCTOR; \ - unsigned i = m_asserted_qhead; \ - unsigned sz = m_asserted_formulas.size(); \ - for (; i < sz; i++) { \ - expr * n = m_asserted_formulas.get(i); \ - proof * pr = m_asserted_formula_prs.get(i, 0); \ - expr_ref new_n(m); \ - proof_ref new_pr(m); \ - functor(n, new_n, new_pr); \ - TRACE("lift_ite_step", tout << mk_pp(n, m) << "\n";); \ - IF_IVERBOSE(10000, verbose_stream() << "lift before: " << get_num_exprs(n) << ", after: " << get_num_exprs(new_n) << "\n";); \ - m_asserted_formulas.set(i, new_n); \ - if (m.proofs_enabled()) { \ - new_pr = m.mk_modus_ponens(pr, new_pr); \ - m_asserted_formula_prs.set(i, new_pr); \ - } \ - } \ - TRACE("lift_ite", display(tout);); \ - reduce_and_solve(); \ - } - -LIFT_ITE(lift_ite, push_app_ite_rw functor(m, m_params.m_lift_ite == LI_CONSERVATIVE), "lifting ite"); -LIFT_ITE(ng_lift_ite, ng_push_app_ite_rw functor(m, m_params.m_ng_lift_ite == LI_CONSERVATIVE), "lifting ng ite"); - -unsigned asserted_formulas::get_total_size() const { - expr_mark visited; - unsigned r = 0; - unsigned sz = m_asserted_formulas.size(); - for (unsigned i = 0; i < sz; i++) - r += get_num_exprs(m_asserted_formulas.get(i), visited); - return r; -} - -void asserted_formulas::max_bv_sharing() { - IF_IVERBOSE(10, verbose_stream() << "(smt.maximizing-bv-sharing)\n";); - TRACE("bv_sharing", display(tout);); - unsigned i = m_asserted_qhead; - unsigned sz = m_asserted_formulas.size(); - for (; i < sz; i++) { - expr * n = m_asserted_formulas.get(i); - proof * pr = m_asserted_formula_prs.get(i, 0); - expr_ref new_n(m); - proof_ref new_pr(m); - m_bv_sharing(n, new_n, new_pr); - m_asserted_formulas.set(i, new_n); - if (m.proofs_enabled()) { - new_pr = m.mk_modus_ponens(pr, new_pr); - m_asserted_formula_prs.set(i, new_pr); - } - } - reduce_asserted_formulas(); - TRACE("bv_sharing", display(tout);); - -} - -#ifdef Z3DEBUG -void pp(asserted_formulas & f) { - f.display(std::cout); -} -#endif diff --git a/src/smt/asserted_formulas.h b/src/smt/asserted_formulas.h deleted file mode 100644 index 1e15e6300..000000000 --- a/src/smt/asserted_formulas.h +++ /dev/null @@ -1,151 +0,0 @@ -/*++ -Copyright (c) 2006 Microsoft Corporation - -Module Name: - - asserted_formulas.h - -Abstract: - - - -Author: - - Leonardo de Moura (leonardo) 2008-06-11. - -Revision History: - ---*/ -#ifndef ASSERTED_FORMULAS_H_ -#define ASSERTED_FORMULAS_H_ - -#include "util/statistics.h" -#include "ast/static_features.h" -#include "ast/simplifier/simplifier.h" -#include "ast/simplifier/basic_simplifier_plugin.h" -#include "ast/simplifier/maximise_ac_sharing.h" -#include "ast/rewriter/bit2int.h" -#include "ast/macros/macro_manager.h" -#include "ast/macros/macro_finder.h" -#include "ast/normal_forms/defined_names.h" -#include "ast/pattern/pattern_inference.h" -#include "smt/params/smt_params.h" -#include "ast/rewriter/th_rewriter.h" - -class arith_simplifier_plugin; -class bv_simplifier_plugin; - -class asserted_formulas { - ast_manager & m; - smt_params & m_params; - simplifier m_pre_simplifier; - simplifier m_simplifier; - th_rewriter m_rewriter; - basic_simplifier_plugin * m_bsimp; - bv_simplifier_plugin * m_bvsimp; - defined_names m_defined_names; - static_features m_static_features; - expr_ref_vector m_asserted_formulas; // formulas asserted by user - proof_ref_vector m_asserted_formula_prs; // proofs for the asserted formulas. - unsigned m_asserted_qhead; - - macro_manager m_macro_manager; - scoped_ptr m_macro_finder; - - bit2int m_bit2int; - - maximise_bv_sharing m_bv_sharing; - - bool m_inconsistent; - bool m_has_quantifiers; - - struct scope { - unsigned m_asserted_formulas_lim; - bool m_inconsistent_old; - }; - svector m_scopes; - - void setup_simplifier_plugins(simplifier & s, basic_simplifier_plugin * & bsimp, arith_simplifier_plugin * & asimp, bv_simplifier_plugin * & bvsimp); - void reduce_asserted_formulas(); - void swap_asserted_formulas(expr_ref_vector & new_exprs, proof_ref_vector & new_prs); - void find_macros_core(); - void find_macros(); - void expand_macros(); - void apply_quasi_macros(); - void nnf_cnf(); - void infer_patterns(); - void eliminate_term_ite(); - void reduce_and_solve(); - void flush_cache() { m_pre_simplifier.reset(); m_simplifier.reset(); } - void set_eliminate_and(bool flag); - void propagate_values(); - void propagate_booleans(); - bool pull_cheap_ite_trees(); - bool pull_nested_quantifiers(); - void push_assertion(expr * e, proof * pr, expr_ref_vector & result, proof_ref_vector & result_prs); - void eliminate_and(); - void refine_inj_axiom(); - bool cheap_quant_fourier_motzkin(); - void apply_distribute_forall(); - bool apply_bit2int(); - void lift_ite(); - bool elim_bvs_from_quantifiers(); - void ng_lift_ite(); -#ifdef Z3DEBUG - bool check_well_sorted() const; -#endif - unsigned get_total_size() const; - bool has_bv() const; - void max_bv_sharing(); - bool canceled() { return m.canceled(); } - -public: - asserted_formulas(ast_manager & m, smt_params & p); - ~asserted_formulas(); - - void setup(); - void assert_expr(expr * e, proof * in_pr); - void assert_expr(expr * e); - void reset(); - void push_scope(); - void pop_scope(unsigned num_scopes); - bool inconsistent() const { return m_inconsistent; } - proof * get_inconsistency_proof() const; - void reduce(); - unsigned get_num_formulas() const { return m_asserted_formulas.size(); } - unsigned get_formulas_last_level() const; - unsigned get_qhead() const { return m_asserted_qhead; } - void commit(); - void commit(unsigned new_qhead); - expr * get_formula(unsigned idx) const { return m_asserted_formulas.get(idx); } - proof * get_formula_proof(unsigned idx) const { return m.proofs_enabled() ? m_asserted_formula_prs.get(idx) : 0; } - expr * const * get_formulas() const { return m_asserted_formulas.c_ptr(); } - proof * const * get_formula_proofs() const { return m_asserted_formula_prs.c_ptr(); } - void init(unsigned num_formulas, expr * const * formulas, proof * const * prs); - void register_simplifier_plugin(simplifier_plugin * p) { m_simplifier.register_plugin(p); } - // simplifier & get_simplifier() { return m_simplifier; } - th_rewriter& get_rewriter() { return m_rewriter; } - void get_assertions(ptr_vector & result); - bool empty() const { return m_asserted_formulas.empty(); } - void collect_static_features(); - void display(std::ostream & out) const; - void display_ll(std::ostream & out, ast_mark & pp_visited) const; - void collect_statistics(statistics & st) const; - // TODO: improve precision of the following method. - bool has_quantifiers() const { return m_has_quantifiers; } - - // ----------------------------------- - // - // Macros - // - // ----------------------------------- - unsigned get_num_macros() const { return m_macro_manager.get_num_macros(); } - unsigned get_first_macro_last_level() const { return m_macro_manager.get_first_macro_last_level(); } - func_decl * get_macro_func_decl(unsigned i) const { return m_macro_manager.get_macro_func_decl(i); } - func_decl * get_macro_interpretation(unsigned i, expr_ref & interp) const { return m_macro_manager.get_macro_interpretation(i, interp); } - quantifier * get_macro_quantifier(func_decl * f) const { return m_macro_manager.get_macro_quantifier(f); } - void insert_macro(func_decl * f, quantifier * m, proof * pr, expr_dependency * dep) { m_macro_manager.insert(f, m, pr, dep); } -}; - -#endif /* ASSERTED_FORMULAS_H_ */ - diff --git a/src/smt/asserted_formulas_new.cpp b/src/smt/asserted_formulas_new.cpp index 5d4783bf8..8d16ef2cd 100644 --- a/src/smt/asserted_formulas_new.cpp +++ b/src/smt/asserted_formulas_new.cpp @@ -431,7 +431,7 @@ void asserted_formulas_new::propagate_values() { flush_cache(); unsigned num_prop = 0; - while (true) { + while (!inconsistent()) { m_expr2depth.reset(); m_scoped_substitution.push(); unsigned prop = num_prop; @@ -474,6 +474,9 @@ unsigned asserted_formulas_new::propagate_values(unsigned i) { } justified_expr j(m, new_n, new_pr); m_formulas[i] = j; + if (m.is_false(j.get_fml())) { + m_inconsistent = true; + } update_substitution(new_n, new_pr); return n != new_n ? 1 : 0; } @@ -484,13 +487,16 @@ void asserted_formulas_new::update_substitution(expr* n, proof* pr) { compute_depth(lhs); compute_depth(rhs); if (is_gt(lhs, rhs)) { + TRACE("propagate_values", tout << "insert " << mk_pp(lhs, m) << " -> " << mk_pp(rhs, m) << "\n";); m_scoped_substitution.insert(lhs, rhs, pr); return; } if (is_gt(rhs, lhs)) { + TRACE("propagate_values", tout << "insert " << mk_pp(rhs, m) << " -> " << mk_pp(lhs, m) << "\n";); m_scoped_substitution.insert(rhs, lhs, m.mk_symmetry(pr)); return; } + TRACE("propagate_values", tout << "incompatible " << mk_pp(n, m) << "\n";); } if (m.is_not(n, n1)) { m_scoped_substitution.insert(n1, m.mk_false(), m.mk_iff_false(pr)); diff --git a/src/smt/asserted_formulas_new.h b/src/smt/asserted_formulas_new.h index 60af46dea..82f18250d 100644 --- a/src/smt/asserted_formulas_new.h +++ b/src/smt/asserted_formulas_new.h @@ -29,9 +29,9 @@ Revision History: #include "ast/rewriter/pull_ite_tree.h" #include "ast/rewriter/push_app_ite.h" #include "ast/rewriter/inj_axiom.h" -#include "ast/rewriter/bv_elim2.h" +#include "ast/rewriter/bv_elim.h" #include "ast/rewriter/der.h" -#include "ast/rewriter/elim_bounds2.h" +#include "ast/rewriter/elim_bounds.h" #include "ast/macros/macro_manager.h" #include "ast/macros/macro_finder.h" #include "ast/normal_forms/defined_names.h" @@ -210,7 +210,7 @@ class asserted_formulas_new { void apply_quasi_macros(); void nnf_cnf(); void reduce_and_solve(); - void flush_cache() { m_rewriter.reset(); } + void flush_cache() { m_rewriter.reset(); m_rewriter.set_substitution(&m_substitution); } void set_eliminate_and(bool flag); void propagate_values(); unsigned propagate_values(unsigned i); diff --git a/src/smt/elim_term_ite.cpp b/src/smt/elim_term_ite.cpp index d9cfac775..e8b70fc59 100644 --- a/src/smt/elim_term_ite.cpp +++ b/src/smt/elim_term_ite.cpp @@ -19,144 +19,6 @@ Revision History: #include "smt/elim_term_ite.h" #include "ast/ast_smt2_pp.h" -void elim_term_ite::operator()(expr * n, - expr_ref_vector & new_defs, - proof_ref_vector & new_def_proofs, - expr_ref & r, - proof_ref & pr) { - - m_coarse_proofs.reset(); - m_new_defs = &new_defs; - m_new_def_proofs = &new_def_proofs; - reduce_core(n); - expr * r2; - proof * pr2; - get_cached(n, r2, pr2); - r = r2; - switch (m.proof_mode()) { - case PGM_DISABLED: - pr = m.mk_undef_proof(); - break; - case PGM_COARSE: - remove_duplicates(m_coarse_proofs); - pr = n == r2 ? m.mk_oeq_reflexivity(n) : m.mk_apply_defs(n, r, m_coarse_proofs.size(), m_coarse_proofs.c_ptr()); - break; - case PGM_FINE: - pr = pr2 == 0 ? m.mk_oeq_reflexivity(n) : pr2; - break; - } - m_coarse_proofs.reset(); -} - -void elim_term_ite::reduce_core(expr * n) { - m_todo.reset(); - if (!is_cached(n)) { - m_todo.push_back(n); - while (!m_todo.empty()) { - expr * n = m_todo.back(); - if (is_cached(n)) { - m_todo.pop_back(); - } - else if (visit_children(n)) { - m_todo.pop_back(); - reduce1(n); - } - } - } -} - -bool elim_term_ite::visit_children(expr * n) { - bool visited = true; - unsigned j; - switch(n->get_kind()) { - case AST_VAR: - return true; - case AST_APP: - j = to_app(n)->get_num_args(); - while (j > 0) { - --j; - visit(to_app(n)->get_arg(j), visited); - } - return visited; - case AST_QUANTIFIER: - visit(to_quantifier(n)->get_expr(), visited); - return visited; - default: - UNREACHABLE(); - return true; - } -} - -void elim_term_ite::reduce1(expr * n) { - switch (n->get_kind()) { - case AST_VAR: - cache_result(n, n, 0); - break; - case AST_APP: - reduce1_app(to_app(n)); - break; - case AST_QUANTIFIER: - reduce1_quantifier(to_quantifier(n)); - break; - default: - UNREACHABLE(); - } -} - -void elim_term_ite::reduce1_app(app * n) { - m_args.reset(); - - func_decl * decl = n->get_decl(); - proof_ref p1(m); - get_args(n, m_args, p1); - if (!m.fine_grain_proofs()) - p1 = 0; - - expr_ref r(m); - r = m.mk_app(decl, m_args.size(), m_args.c_ptr()); - if (m.is_term_ite(r)) { - expr_ref new_def(m); - proof_ref new_def_pr(m); - app_ref new_r(m); - proof_ref new_pr(m); - if (m_defined_names.mk_name(r, new_def, new_def_pr, new_r, new_pr)) { - CTRACE("elim_term_ite_bug", new_def.get() == 0, tout << mk_ismt2_pp(r, m) << "\n";); - SASSERT(new_def.get() != 0); - m_new_defs->push_back(new_def); - if (m.fine_grain_proofs()) { - m_new_def_proofs->push_back(new_def_pr); - new_pr = m.mk_transitivity(p1, new_pr); - } - else { - // [Leo] This looks fishy... why do we add 0 into m_coarse_proofs when fine_grain_proofs are disabled? - new_pr = 0; - if (m.proofs_enabled()) - m_coarse_proofs.push_back(new_pr); - } - } - else { - SASSERT(new_def.get() == 0); - if (!m.fine_grain_proofs()) - new_pr = 0; - } - cache_result(n, new_r, new_pr); - } - else { - cache_result(n, r, p1); - } -} - -void elim_term_ite::reduce1_quantifier(quantifier * q) { - expr * new_body; - proof * new_body_pr; - get_cached(q->get_expr(), new_body, new_body_pr); - - quantifier * new_q = m.update_quantifier(q, new_body); - proof * p = q == new_q ? 0 : m.mk_oeq_quant_intro(q, new_q, new_body_pr); - cache_result(q, new_q, p); -} - - br_status elim_term_ite_cfg::reduce_app(func_decl* f, unsigned n, expr * const* args, expr_ref& result, proof_ref& result_pr) { if (!m.is_term_ite(f)) { return BR_FAILED; diff --git a/src/smt/elim_term_ite.h b/src/smt/elim_term_ite.h index a57ea1dad..8e8340dc0 100644 --- a/src/smt/elim_term_ite.h +++ b/src/smt/elim_term_ite.h @@ -21,35 +21,8 @@ Revision History: #include "ast/normal_forms/defined_names.h" #include "ast/rewriter/rewriter.h" -#include "ast/simplifier/simplifier.h" #include "ast/justified_expr.h" - -class elim_term_ite : public simplifier { - defined_names & m_defined_names; - proof_ref_vector m_coarse_proofs; - expr_ref_vector * m_new_defs; - proof_ref_vector * m_new_def_proofs; - void reduce_core(expr * n); - bool visit_children(expr * n); - void reduce1(expr * n); - void reduce1_app(app * n); - void reduce1_quantifier(quantifier * q); -public: - elim_term_ite(ast_manager & m, defined_names & d):simplifier(m), m_defined_names(d), m_coarse_proofs(m) { - m_use_oeq = true; - enable_ac_support(false); - } - virtual ~elim_term_ite() {} - void operator()(expr * n, // [IN] - expr_ref_vector & new_defs, // [OUT] new definitions - proof_ref_vector & new_def_proofs, // [OUT] proofs of the new definitions - expr_ref & r, // [OUT] resultant expression - proof_ref & pr // [OUT] proof for (~ n r) - ); -}; - - class elim_term_ite_cfg : public default_rewriter_cfg { ast_manager& m; defined_names & m_defined_names; diff --git a/src/smt/expr_context_simplifier.h b/src/smt/expr_context_simplifier.h index ed15044e7..b412d8646 100644 --- a/src/smt/expr_context_simplifier.h +++ b/src/smt/expr_context_simplifier.h @@ -21,10 +21,10 @@ Revision History: #include "ast/ast.h" #include "util/obj_hashtable.h" -#include "ast/simplifier/basic_simplifier_plugin.h" #include "smt/params/smt_params.h" #include "smt/smt_kernel.h" #include "ast/arith_decl_plugin.h" +#include "ast/rewriter/bool_rewriter.h" class expr_context_simplifier { typedef obj_map context_map; @@ -33,7 +33,7 @@ class expr_context_simplifier { arith_util m_arith; context_map m_context; expr_ref_vector m_trail; - basic_simplifier_plugin m_simp; + bool_rewriter m_simp; expr_mark m_mark; bool m_forward; public: diff --git a/src/smt/params/CMakeLists.txt b/src/smt/params/CMakeLists.txt index c965f0a62..500423dcc 100644 --- a/src/smt/params/CMakeLists.txt +++ b/src/smt/params/CMakeLists.txt @@ -13,6 +13,7 @@ z3_add_component(smt_params ast bit_blaster pattern + simplifier PYG_FILES smt_params_helper.pyg ) diff --git a/src/smt/smt_consequences.cpp b/src/smt/smt_consequences.cpp index 65af3c0bd..0bf2a2939 100644 --- a/src/smt/smt_consequences.cpp +++ b/src/smt/smt_consequences.cpp @@ -16,12 +16,13 @@ Author: Revision History: --*/ -#include "smt/smt_context.h" -#include "ast/ast_util.h" -#include "ast/datatype_decl_plugin.h" -#include "model/model_pp.h" #include "util/max_cliques.h" #include "util/stopwatch.h" +#include "ast/ast_util.h" +#include "ast/ast_pp.h" +#include "ast/datatype_decl_plugin.h" +#include "model/model_pp.h" +#include "smt/smt_context.h" namespace smt { diff --git a/src/smt/smt_quantifier.cpp b/src/smt/smt_quantifier.cpp index 6a2f848d9..22004ee78 100644 --- a/src/smt/smt_quantifier.cpp +++ b/src/smt/smt_quantifier.cpp @@ -16,6 +16,8 @@ Author: Revision History: --*/ +#include "ast/ast_pp.h" +#include "ast/ast_smt2_pp.h" #include "smt/smt_quantifier.h" #include "smt/smt_context.h" #include "smt/smt_quantifier_stat.h" @@ -24,7 +26,6 @@ Revision History: #include "smt/smt_quick_checker.h" #include "smt/mam.h" #include "smt/qi_queue.h" -#include "ast/ast_smt2_pp.h" namespace smt { diff --git a/src/smt/theory_array.cpp b/src/smt/theory_array.cpp index 17eefb361..18fc9f50b 100644 --- a/src/smt/theory_array.cpp +++ b/src/smt/theory_array.cpp @@ -19,6 +19,7 @@ Revision History: #include "smt/smt_context.h" #include "smt/theory_array.h" #include "ast/ast_ll_pp.h" +#include "ast/ast_pp.h" #include "util/stats.h" namespace smt { diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index 124fea910..0c09d0403 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -28,6 +28,7 @@ Revision History: #include "util/optional.h" #include "util/lp/lp_params.hpp" #include "util/inf_rational.h" +#include "ast/ast_pp.h" #include "smt/smt_theory.h" #include "smt/smt_context.h" #include "smt/theory_lra.h" diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index c91882dad..8d6d70a79 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -19,11 +19,12 @@ Revision History: --*/ #include +#include "ast/ast_pp.h" +#include "ast/ast_trail.h" #include "smt/proto_model/value_factory.h" #include "smt/smt_context.h" #include "smt/smt_model_generator.h" #include "smt/theory_seq.h" -#include "ast/ast_trail.h" #include "smt/theory_arith.h" #include "smt/smt_kernel.h" diff --git a/src/smt/theory_str.h b/src/smt/theory_str.h index 5837980df..686fcdd57 100644 --- a/src/smt/theory_str.h +++ b/src/smt/theory_str.h @@ -17,13 +17,14 @@ #ifndef _THEORY_STR_H_ #define _THEORY_STR_H_ +#include "util/trail.h" +#include "ast/ast_pp.h" +#include "ast/arith_decl_plugin.h" +#include "ast/rewriter/th_rewriter.h" #include "smt/smt_theory.h" #include "smt/params/theory_str_params.h" -#include "util/trail.h" -#include "ast/rewriter/th_rewriter.h" #include "smt/proto_model/value_factory.h" #include "smt/smt_model_generator.h" -#include "ast/arith_decl_plugin.h" #include #include #include diff --git a/src/test/CMakeLists.txt b/src/test/CMakeLists.txt index b395c09e6..fbcaec5ef 100644 --- a/src/test/CMakeLists.txt +++ b/src/test/CMakeLists.txt @@ -20,7 +20,6 @@ add_executable(test-z3 bits.cpp bit_vector.cpp buffer.cpp - bv_simplifier_plugin.cpp chashtable.cpp check_assumptions.cpp cnf_backbones.cpp diff --git a/src/test/bv_simplifier_plugin.cpp b/src/test/bv_simplifier_plugin.cpp deleted file mode 100644 index 15ca9fac5..000000000 --- a/src/test/bv_simplifier_plugin.cpp +++ /dev/null @@ -1,326 +0,0 @@ - -/*++ -Copyright (c) 2015 Microsoft Corporation - ---*/ - -#include "ast/simplifier/bv_simplifier_plugin.h" -#include "ast/arith_decl_plugin.h" -#include "ast/ast_pp.h" -#include "ast/reg_decl_plugins.h" - -class tst_bv_simplifier_plugin_cls { - class mgr { - public: - mgr(ast_manager& m) { - reg_decl_plugins(m); - } - }; - ast_manager m_manager; - mgr m_mgr; - bv_simplifier_params m_bv_params; - basic_simplifier_plugin m_bsimp; - arith_util m_arith; - bv_simplifier_plugin m_simp; - bv_util m_bv_util; - family_id m_fid; - - void get_num(expr* e, unsigned bv_size, rational& r) { - unsigned bv_size0; - if (!m_bv_util.is_numeral(e, r, bv_size0)) { - UNREACHABLE(); - } - ENSURE(bv_size == bv_size0); - } - - unsigned u32(expr* e) { - rational r; - std::cout << mk_pp(e,m_manager) << "\n"; - get_num(e, 32, r); - return r.get_unsigned(); - } - - unsigned char u8(expr* e) { - rational r; - get_num(e, 8, r); - return static_cast(r.get_unsigned()); - } - int i32(expr* e) { - return static_cast(u32(e)); - } - - uint64 u64(expr* e) { - rational r; - get_num(e, 64, r); - return r.get_uint64(); - } - - int64 i64(expr* e) { - rational r; - get_num(e, 64, r); - if (r >= power(rational(2), 63)) { - r -= power(rational(2), 64); - } - return r.get_int64(); - } - - bool ast2bool(expr* e) { - if (m_manager.is_true(e)) { - return true; - } - if (m_manager.is_false(e)) { - return false; - } - UNREACHABLE(); - return false; - } - - bool bit2bool(expr* e) { - rational r; - get_num(e, 1, r); - return 0 != r.get_unsigned(); - } - - expr* mk_int(unsigned i) { - return m_arith.mk_numeral(rational(i), true); - } - -public: - - tst_bv_simplifier_plugin_cls() : - m_mgr(m_manager), - m_bsimp(m_manager), - m_arith(m_manager), - m_simp(m_manager, m_bsimp, m_bv_params), - m_bv_util(m_manager), - m_fid(0) { - m_fid = m_manager.mk_family_id("bv"); - } - - ~tst_bv_simplifier_plugin_cls() {} - - void test_num(unsigned a) { - expr_ref e(m_manager), e1(m_manager); - app_ref ar(m_manager); - uint64 a64 = static_cast(a); - - e1 = m_bv_util.mk_numeral(rational(a), 32); - expr* const es[1] = { e1.get() }; - - ar = m_manager.mk_app(m_fid, OP_BNEG, e1.get()); - m_simp.reduce(ar->get_decl(), ar->get_num_args(), ar->get_args(), e); - ENSURE((0-a) == u32(e.get())); - - ar = m_manager.mk_app(m_fid, OP_BNOT, e1.get()); - m_simp.reduce(ar->get_decl(), ar->get_num_args(), ar->get_args(), e); - ENSURE((~a) == u32(e.get())); - - parameter params[2] = { parameter(32), parameter(32) }; - ar = m_manager.mk_app(m_fid, OP_SIGN_EXT, 1, params, 1, es); - m_simp.reduce(ar->get_decl(), ar->get_num_args(), ar->get_args(), e); - ENSURE(((int64)(int)a) == i64(e.get())); - - ar = m_manager.mk_app(m_fid, OP_ZERO_EXT, 1, params, 1, es); - m_simp.reduce(ar->get_decl(), ar->get_num_args(), ar->get_args(), e); - ENSURE(((uint64)a) == u64(e.get())); - - params[0] = parameter(7); - params[1] = parameter(0); - ar = m_manager.mk_app(m_fid, OP_EXTRACT, 2, params, 1, es); - m_simp.reduce(ar->get_decl(), ar->get_num_args(), ar->get_args(), e); - ENSURE(((unsigned char)a) == u8(e.get())); - - params[0] = parameter(2); - ar = m_manager.mk_app(m_fid, OP_REPEAT, 1, params, 1, es); - m_simp.reduce(ar->get_decl(), ar->get_num_args(), ar->get_args(), e); - VERIFY(((a64 << 32) | a64) == u64(e.get())); - - ar = m_manager.mk_app(m_fid, OP_BREDOR, e1.get()); - m_simp.reduce(ar->get_decl(), ar->get_num_args(), ar->get_args(), e); - ENSURE((a != 0) == bit2bool(e.get())); - - ar = m_manager.mk_app(m_fid, OP_BREDAND, e1.get()); - m_simp.reduce(ar->get_decl(), ar->get_num_args(), ar->get_args(), e); - ENSURE((a == 0xFFFFFFFF) == bit2bool(e.get())); - - params[0] = parameter(8); - - ar = m_manager.mk_app(m_fid, OP_ROTATE_LEFT, 1, params, 1, es); - m_simp.reduce(ar->get_decl(), ar->get_num_args(), ar->get_args(), e); - ENSURE(((a << 8) | (a >> 24)) == u32(e.get())); - - ar = m_manager.mk_app(m_fid, OP_ROTATE_RIGHT, 1, params, 1, es); - m_simp.reduce(ar->get_decl(), ar->get_num_args(), ar->get_args(), e); - ENSURE(((a >> 8) | (a << 24)) == u32(e.get())); - - params[0] = parameter(m_manager.mk_sort(m_manager.mk_family_id("arith"), INT_SORT)); - ar = m_manager.mk_app(m_fid, OP_BV2INT, 1, params, 1, es); - expr* es2[1] = { ar.get() }; - params[0] = parameter(32); - ar = m_manager.mk_app(m_fid, OP_INT2BV, 1, params, 1, es2); - m_simp.reduce(ar->get_decl(), ar->get_num_args(), ar->get_args(), e); - ENSURE(a == u32(e.get())); - - ar = m_manager.mk_app(m_fid, OP_BIT0); - m_simp.reduce(ar->get_decl(), ar->get_num_args(), ar->get_args(), e); - VERIFY(!bit2bool(e.get())); - - ar = m_manager.mk_app(m_fid, OP_BIT1); - m_simp.reduce(ar->get_decl(), ar->get_num_args(), ar->get_args(), e); - VERIFY(bit2bool(e.get())); - - } - - void test_pair(unsigned a, unsigned b) { - - expr_ref e(m_manager), e1(m_manager), e2(m_manager); - app_ref ar(m_manager); - int sa = static_cast(a); - int sb = static_cast(b); - uint64 a64 = static_cast(a); - uint64 b64 = static_cast(b); - - e1 = m_bv_util.mk_numeral(rational(a), 32); - e2 = m_bv_util.mk_numeral(rational(b), 32); - expr* const e1e2[] = { e1.get(), e2.get() }; - - - ar = m_manager.mk_app(m_fid, OP_BADD, 2, e1e2); - m_simp.reduce(ar->get_decl(), ar->get_num_args(), ar->get_args(), e); - VERIFY((a + b) == u32(e.get())); - - ar = m_manager.mk_app(m_fid, OP_BSUB, 2, e1e2); - m_simp.reduce(ar->get_decl(), ar->get_num_args(), ar->get_args(), e); - VERIFY((a - b) == u32(e.get())); - - ar = m_manager.mk_app(m_fid, OP_BMUL, 2, e1e2); - m_simp.reduce(ar->get_decl(), ar->get_num_args(), ar->get_args(), e); - VERIFY((a * b) == u32(e.get())); - - ar = m_manager.mk_app(m_fid, OP_BAND, 2, e1e2); - m_simp.reduce(ar->get_decl(), ar->get_num_args(), ar->get_args(), e); - VERIFY((a & b) == u32(e.get())); - - ar = m_manager.mk_app(m_fid, OP_BOR, 2, e1e2); - m_simp.reduce(ar->get_decl(), ar->get_num_args(), ar->get_args(), e); - VERIFY((a | b) == u32(e.get())); - - ar = m_manager.mk_app(m_fid, OP_BNOR, 2, e1e2); - m_simp.reduce(ar->get_decl(), ar->get_num_args(), ar->get_args(), e); - VERIFY(~(a | b) == u32(e.get())); - - ar = m_manager.mk_app(m_fid, OP_BXOR, 2, e1e2); - m_simp.reduce(ar->get_decl(), ar->get_num_args(), ar->get_args(), e); - VERIFY((a ^ b) == u32(e.get())); - - ar = m_manager.mk_app(m_fid, OP_BXNOR, 2, e1e2); - m_simp.reduce(ar->get_decl(), ar->get_num_args(), ar->get_args(), e); - VERIFY((~(a ^ b)) == u32(e.get())); - - ar = m_manager.mk_app(m_fid, OP_BNAND, 2, e1e2); - m_simp.reduce(ar->get_decl(), ar->get_num_args(), ar->get_args(), e); - VERIFY((~(a & b)) == u32(e.get())); - - ar = m_manager.mk_app(m_fid, OP_ULEQ, 2, e1e2); - m_simp.reduce(ar->get_decl(), ar->get_num_args(), ar->get_args(), e); - VERIFY((a <= b) == ast2bool(e.get())); - - ar = m_manager.mk_app(m_fid, OP_UGEQ, 2, e1e2); - m_simp.reduce(ar->get_decl(), ar->get_num_args(), ar->get_args(), e); - VERIFY((a >= b) == ast2bool(e.get())); - - ar = m_manager.mk_app(m_fid, OP_ULT, 2, e1e2); - m_simp.reduce(ar->get_decl(), ar->get_num_args(), ar->get_args(), e); - VERIFY((a < b) == ast2bool(e.get())); - - ar = m_manager.mk_app(m_fid, OP_UGT, 2, e1e2); - m_simp.reduce(ar->get_decl(), ar->get_num_args(), ar->get_args(), e); - VERIFY((a > b) == ast2bool(e.get())); - - ar = m_manager.mk_app(m_fid, OP_SLEQ, 2, e1e2); - m_simp.reduce(ar->get_decl(), ar->get_num_args(), ar->get_args(), e); - VERIFY((sa <= sb) == ast2bool(e.get())); - - ar = m_manager.mk_app(m_fid, OP_SGEQ, 2, e1e2); - m_simp.reduce(ar->get_decl(), ar->get_num_args(), ar->get_args(), e); - VERIFY((sa >= sb) == ast2bool(e.get())); - - ar = m_manager.mk_app(m_fid, OP_SLT, 2, e1e2); - m_simp.reduce(ar->get_decl(), ar->get_num_args(), ar->get_args(), e); - VERIFY((sa < sb) == ast2bool(e.get())); - - ar = m_manager.mk_app(m_fid, OP_SGT, 2, e1e2); - m_simp.reduce(ar->get_decl(), ar->get_num_args(), ar->get_args(), e); - VERIFY((sa > sb) == ast2bool(e.get())); - - ar = m_manager.mk_app(m_fid, OP_BSHL, 2, e1e2); - m_simp.reduce(ar->get_decl(), ar->get_num_args(), ar->get_args(), e); - VERIFY(((b>=32)?0:(a << b)) == u32(e.get())); - - ar = m_manager.mk_app(m_fid, OP_BLSHR, 2, e1e2); - m_simp.reduce(ar->get_decl(), ar->get_num_args(), ar->get_args(), e); - VERIFY(((b>=32)?0:(a >> b)) == u32(e.get())); - - ar = m_manager.mk_app(m_fid, OP_BASHR, 2, e1e2); - m_simp.reduce(ar->get_decl(), ar->get_num_args(), ar->get_args(), e); - - std::cout << "compare: " << sa << " >> " << b << " = " << (sa >> b) << " with " << i32(e.get()) << "\n"; - VERIFY(b >= 32 || ((sa >> b) == i32(e.get()))); - - if (b != 0) { - ar = m_manager.mk_app(m_fid, OP_BSDIV, 2, e1e2); - m_simp.reduce(ar->get_decl(), ar->get_num_args(), ar->get_args(), e); - VERIFY((sa / sb) == i32(e.get())); - - ar = m_manager.mk_app(m_fid, OP_BUDIV, 2, e1e2); - m_simp.reduce(ar->get_decl(), ar->get_num_args(), ar->get_args(), e); - VERIFY((a / b) == u32(e.get())); - - ar = m_manager.mk_app(m_fid, OP_BSREM, 2, e1e2); - m_simp.reduce(ar->get_decl(), ar->get_num_args(), ar->get_args(), e); - //VERIFY((sa % sb) == i32(e.get())); - - ar = m_manager.mk_app(m_fid, OP_BUREM, 2, e1e2); - m_simp.reduce(ar->get_decl(), ar->get_num_args(), ar->get_args(), e); - VERIFY((a % b) == u32(e.get())); - - // TBD: BSMOD. - } - - ar = m_manager.mk_app(m_fid, OP_CONCAT, 2, e1e2); - m_simp.reduce(ar->get_decl(), ar->get_num_args(), ar->get_args(), e); - VERIFY(((a64 << 32) | b64) == u64(e.get())); - - ar = m_manager.mk_app(m_fid, OP_BCOMP, 2, e1e2); - m_simp.reduce(ar->get_decl(), ar->get_num_args(), ar->get_args(), e); - VERIFY((a == b) == bit2bool(e.get())); - } - - void test() { - unsigned_vector nums; - nums.push_back(0); - nums.push_back(1); - nums.push_back(-1); - nums.push_back(2); - nums.push_back(31); - nums.push_back(32); - nums.push_back(33); - nums.push_back(435562); - nums.push_back(-43556211); - // TBD add some random numbers. - - - for (unsigned i = 0; i < nums.size(); ++i) { - test_num(nums[i]); - for (unsigned j = 0; j < nums.size(); ++j) { - test_pair(nums[i], nums[j]); - } - } - } -}; - - -void tst_bv_simplifier_plugin() { - tst_bv_simplifier_plugin_cls tst_cls; - tst_cls.test(); -} diff --git a/src/test/main.cpp b/src/test/main.cpp index 17ac720dc..2c51df601 100644 --- a/src/test/main.cpp +++ b/src/test/main.cpp @@ -166,7 +166,6 @@ int main(int argc, char ** argv) { TST(timeout); TST(proof_checker); TST(simplifier); - TST(bv_simplifier_plugin); TST(bit_blaster); TST(var_subst); TST(simple_parser); diff --git a/src/test/quant_elim.cpp b/src/test/quant_elim.cpp index fec86d164..3674e6b70 100644 --- a/src/test/quant_elim.cpp +++ b/src/test/quant_elim.cpp @@ -6,12 +6,7 @@ Copyright (c) 2015 Microsoft Corporation #include "ast/ast.h" #include "smt/params/smt_params.h" -#include "ast/simplifier/simplifier.h" #include "qe/qe.h" -#include "ast/simplifier/basic_simplifier_plugin.h" -#include "ast/simplifier/arith_simplifier_plugin.h" -#include "ast/simplifier/array_simplifier_plugin.h" -#include "ast/simplifier/bv_simplifier_plugin.h" #include "ast/ast_pp.h" #include "parsers/smt/smtlib.h" #include "parsers/smt/smtparser.h" @@ -38,7 +33,6 @@ static void test_qe(ast_manager& m, lbool expected_outcome, expr* fml, char cons // enable_trace("after_search"); // enable_trace("bv_bit_prop"); - simplifier simp(m); smt_params params; // params.m_quant_elim = true; diff --git a/src/test/sorting_network.cpp b/src/test/sorting_network.cpp index 909ea594e..2984e94e2 100644 --- a/src/test/sorting_network.cpp +++ b/src/test/sorting_network.cpp @@ -220,7 +220,7 @@ static void test_sorting_eq(unsigned n, unsigned k) { TRACE("pb", unsigned sz = solver.size(); for (unsigned i = 0; i < sz; ++i) { - tout << mk_pp(solver.get_formulas()[i], m) << "\n"; + tout << mk_pp(solver.get_formula(i), m) << "\n"; }); model_ref model; solver.get_model(model); @@ -266,7 +266,7 @@ static void test_sorting_le(unsigned n, unsigned k) { TRACE("pb", unsigned sz = solver.size(); for (unsigned i = 0; i < sz; ++i) { - tout << mk_pp(solver.get_formulas()[i], m) << "\n"; + tout << mk_pp(solver.get_formula(i), m) << "\n"; }); model_ref model; solver.get_model(model); @@ -314,7 +314,7 @@ void test_sorting_ge(unsigned n, unsigned k) { TRACE("pb", unsigned sz = solver.size(); for (unsigned i = 0; i < sz; ++i) { - tout << mk_pp(solver.get_formulas()[i], m) << "\n"; + tout << mk_pp(solver.get_formula(i), m) << "\n"; }); model_ref model; solver.get_model(model);