From 026c81ba29224cb358cba5727af7f0399ffeac80 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 22 Nov 2012 16:20:02 -0800 Subject: [PATCH] Simplified asserted_formulas. From now on, we should use tactics for qe, der, solve, etc. Signed-off-by: Leonardo de Moura --- .../params2front_end_params.cpp | 2 - src/front_end_params/preprocessor_params.h | 36 +- src/muz_qe/dl_smt_relation.cpp | 12 +- src/smt/arith_solver_plugin.cpp | 104 --- src/smt/arith_solver_plugin.h | 34 - src/smt/asserted_formulas.cpp | 597 +----------------- src/smt/asserted_formulas.h | 44 +- src/smt/expr_context_simplifier.cpp | 2 - src/smt/smt_context.h | 13 - src/smt/smt_model_generator.cpp | 73 --- src/smt/smt_model_generator.h | 3 +- src/smt/smt_setup.cpp | 20 - src/smt/solver_plugin.h | 51 -- src/smt/tactic/smt_tactic.cpp | 2 +- src/test/quant_elim.cpp | 2 +- 15 files changed, 20 insertions(+), 975 deletions(-) delete mode 100644 src/smt/arith_solver_plugin.cpp delete mode 100644 src/smt/arith_solver_plugin.h delete mode 100644 src/smt/solver_plugin.h diff --git a/src/front_end_params/params2front_end_params.cpp b/src/front_end_params/params2front_end_params.cpp index 35a7175d5..a2bae371c 100644 --- a/src/front_end_params/params2front_end_params.cpp +++ b/src/front_end_params/params2front_end_params.cpp @@ -27,7 +27,6 @@ Revision History: the new strategy framework. */ void params2front_end_params(params_ref const & s, front_end_params & t) { - t.m_quant_elim = s.get_bool(":elim-quant", t.m_quant_elim); t.m_relevancy_lvl = s.get_uint(":relevancy", t.m_relevancy_lvl); TRACE("qi_cost", s.display(tout); tout << "\n";); t.m_qi_cost = s.get_str(":qi-cost", t.m_qi_cost.c_str()); @@ -40,7 +39,6 @@ void params2front_end_params(params_ref const & s, front_end_params & t) { t.m_well_sorted_check = s.get_bool(":check-sorts", t.m_well_sorted_check); t.m_qi_eager_threshold = s.get_double(":qi-eager-threshold", t.m_qi_eager_threshold); t.m_qi_lazy_threshold = s.get_double(":qi-lazy-threshold", t.m_qi_lazy_threshold); - t.m_solver = s.get_bool(":solver", t.m_solver); t.m_preprocess = s.get_bool(":preprocess", t.m_preprocess); t.m_hi_div0 = s.get_bool(":hi-div0", t.m_hi_div0); t.m_auto_config = s.get_bool(":auto-config", t.m_auto_config); diff --git a/src/front_end_params/preprocessor_params.h b/src/front_end_params/preprocessor_params.h index 1b582ff83..d2ba0bd43 100644 --- a/src/front_end_params/preprocessor_params.h +++ b/src/front_end_params/preprocessor_params.h @@ -31,13 +31,6 @@ enum lift_ite_kind { LI_FULL }; -enum q_arith_kind { - QA_NONE, - QA_COOPER, - QA_OMEGA, - QA_ALTERNATE -}; - struct preprocessor_params : public nnf_params, public cnf_params, public pattern_inference_params, public bit_blaster_params, public bv_simplifier_params { lift_ite_kind m_lift_ite; @@ -48,25 +41,19 @@ struct preprocessor_params : public nnf_params, public cnf_params, public patter bool m_eliminate_and; // represent (and a b) as (not (or (not a) (not b))) bool m_reverse_implies; // translate (implies a b) into (or b (not a)) bool m_macro_finder; - bool m_solver; bool m_propagate_values; bool m_propagate_booleans; - bool m_context_simplifier; - bool m_strong_context_simplifier; bool m_refine_inj_axiom; bool m_eliminate_bounds; - bool m_quant_elim; - bool m_nlquant_elim; - bool m_der; bool m_simplify_bit2int; bool m_nnf_cnf; bool m_distribute_forall; bool m_reduce_args; - bool m_pre_demod; bool m_quasi_macros; bool m_restricted_quasi_macros; bool m_max_bv_sharing; bool m_pre_simplifier; + bool m_nlquant_elim; public: preprocessor_params(): @@ -77,25 +64,19 @@ public: m_eliminate_term_ite(false), m_eliminate_and(true), m_macro_finder(false), - m_solver(false), m_propagate_values(true), m_propagate_booleans(false), // TODO << check peformance - m_context_simplifier(false), - m_strong_context_simplifier(false), m_refine_inj_axiom(true), m_eliminate_bounds(false), - m_quant_elim(false), - m_nlquant_elim(false), - m_der(false), m_simplify_bit2int(false), m_nnf_cnf(true), m_distribute_forall(false), m_reduce_args(false), - m_pre_demod(false), m_quasi_macros(false), m_restricted_quasi_macros(false), m_max_bv_sharing(true), - m_pre_simplifier(true) { + m_pre_simplifier(true), + m_nlquant_elim(false) { } void register_params(ini_params & p) { @@ -109,27 +90,16 @@ public: p.register_bool_param("ELIM_TERM_ITE", m_eliminate_term_ite, "eliminate term if-then-else in the preprocessor"); p.register_bool_param("ELIM_AND", m_eliminate_and, "represent (and a b) as (not (or (not a) (not b)))"); p.register_bool_param("MACRO_FINDER", m_macro_finder, "try to find universally quantified formulas that can be viewed as macros"); - p.register_bool_param("SOLVER", m_solver, "enable solver during preprocessing step", true); p.register_bool_param("PROPAGATE_VALUES", m_propagate_values, "propagate values during preprocessing step"); p.register_bool_param("PROPAGATE_BOOLEANS", m_propagate_booleans, "propagate boolean values during preprocessing step"); p.register_bool_param("PULL_CHEAP_ITE_TREES", m_pull_cheap_ite_trees); p.register_bool_param("PULL_NESTED_QUANTIFIERS", m_pull_nested_quantifiers, "eliminate nested quantifiers by moving nested quantified variables to the outermost quantifier, it is unnecessary if the formula is converted into CNF"); - p.register_bool_param("CONTEXT_SIMPLIFIER", m_context_simplifier, - "Simplify Boolean sub-expressions if they already appear in context", true); - p.register_bool_param("STRONG_CONTEXT_SIMPLIFIER", m_strong_context_simplifier, - "Simplify Boolean sub-expressions by using full satisfiability queries", true); p.register_bool_param("REFINE_INJ_AXIOM", m_refine_inj_axiom); p.register_bool_param("ELIM_BOUNDS", m_eliminate_bounds, "cheap Fourier-Motzkin"); - p.register_bool_param("ELIM_QUANTIFIERS", m_quant_elim, - "Use quantifier elimination procedures on Boolean, Bit-vector, Arithmetic and Array variables", true); - p.register_bool_param("ELIM_NLARITH_QUANTIFIERS", m_nlquant_elim, - "Eliminate non-linear quantifiers", true); - p.register_bool_param("DER", m_der); p.register_bool_param("BIT2INT", m_simplify_bit2int, "hoist bit2int conversions over arithmetical expressions"); p.register_bool_param("DISTRIBUTE_FORALL", m_distribute_forall); p.register_bool_param("REDUCE_ARGS", m_reduce_args); - p.register_bool_param("PRE_DEMODULATOR", m_pre_demod, "apply demodulators during preprocessing step"); p.register_bool_param("QUASI_MACROS", m_quasi_macros); p.register_bool_param("RESTRICTED_QUASI_MACROS", m_restricted_quasi_macros); p.register_bool_param("BV_MAX_SHARING", m_max_bv_sharing); diff --git a/src/muz_qe/dl_smt_relation.cpp b/src/muz_qe/dl_smt_relation.cpp index 381b8f434..55d3f7199 100644 --- a/src/muz_qe/dl_smt_relation.cpp +++ b/src/muz_qe/dl_smt_relation.cpp @@ -130,7 +130,9 @@ namespace datalog { IF_VERBOSE(10, verbose_stream() << "Checking emptiness...\n"; ); front_end_params& params = get_plugin().get_fparams(); - flet flet2(params.m_der, true); + // [Leo]: asserted_formulas do not have support for der. + // We should use the tactics der. + // flet flet2(params.m_der, true); smt::kernel ctx(m, params); expr_ref tmp(m); instantiate(r, tmp); @@ -181,9 +183,13 @@ namespace datalog { fml_free = m.mk_and(facts, m.mk_not(get_relation())); instantiate(fml_free, fml_inst); front_end_params& params = get_plugin().get_fparams(); - flet flet0(params.m_quant_elim, true); + // [Leo]: asserted_formulas do not have support for qe nor der. + // We should use the tactics qe and der. + // BTW, qe at asserted_formulas was disabled when we moved to codeplex, but the field m_quant_elim was not deleted. + // + // flet flet0(params.m_quant_elim, true); flet flet1(params.m_nnf_cnf, false); - flet flet2(params.m_der, true); + // flet flet2(params.m_der, true); smt::kernel ctx(m, params); ctx.assert_expr(fml_inst); lbool result = ctx.check(); diff --git a/src/smt/arith_solver_plugin.cpp b/src/smt/arith_solver_plugin.cpp deleted file mode 100644 index d39185b4b..000000000 --- a/src/smt/arith_solver_plugin.cpp +++ /dev/null @@ -1,104 +0,0 @@ -/*++ -Copyright (c) 2006 Microsoft Corporation - -Module Name: - - arith_solver_plugin.cpp - -Abstract: - - - -Author: - - Leonardo de Moura (leonardo) 2008-06-30. - -Revision History: - ---*/ -#include"arith_solver_plugin.h" -#include"ast_pp.h" - -arith_solver_plugin::arith_solver_plugin(arith_simplifier_plugin & simp): - solver_plugin(symbol("arith"), simp.get_manager()), - m_simplifier(simp) { -} - -bool arith_solver_plugin::solve(expr * lhs, expr * rhs, expr_mark const & forbidden, app_ref & var, expr_ref & subst) { - rational k; - if (!m_simplifier.is_numeral(rhs, k)) - return false; - bool _is_int = m_simplifier.is_int(lhs); - ptr_buffer monomials; - ptr_buffer todo; - bool already_found = false; - rational c; - todo.push_back(lhs); - while (!todo.empty()) { - expr * curr = todo.back(); - todo.pop_back(); - rational coeff; - if (m_simplifier.is_add(curr)) { - SASSERT(to_app(curr)->get_num_args() == 2); - todo.push_back(to_app(curr)->get_arg(1)); - todo.push_back(to_app(curr)->get_arg(0)); - } - else { - if (!already_found) { - if (m_simplifier.is_mul(curr) && - m_simplifier.is_numeral(to_app(curr)->get_arg(0), coeff) && !coeff.is_zero() && (!_is_int || coeff.is_minus_one()) && - is_uninterp_const(to_app(curr)->get_arg(1)) && - !forbidden.is_marked(to_app(curr)->get_arg(1))) { - c = coeff; - var = to_app(to_app(curr)->get_arg(1)); - already_found = true; - } - else if (is_uninterp_const(curr) && !forbidden.is_marked(curr)) { - c = rational::one(); - var = to_app(curr); - already_found = true; - } - else { - monomials.push_back(curr); - } - } - else { - monomials.push_back(curr); - } - } - } - if (!already_found) - return false; - SASSERT(!c.is_zero()); - k /= c; - expr_ref_vector new_monomials(m_manager); - if (!k.is_zero()) - new_monomials.push_back(m_simplifier.mk_numeral(k, _is_int)); - c.neg(); - expr_ref inv_c(m_manager); - if (!c.is_one()) { - rational inv(1); - inv /= c; - inv_c = m_simplifier.mk_numeral(inv, _is_int); - } - // divide monomials by c - unsigned sz = monomials.size(); - for (unsigned i = 0; i < sz; i++) { - expr * m = monomials[i]; - expr_ref new_m(m_manager); - if (!c.is_one()) - m_simplifier.mk_mul(inv_c, m, new_m); - else - new_m = m; - new_monomials.push_back(new_m); - } - if (new_monomials.empty()) - subst = m_simplifier.mk_numeral(rational(0), _is_int); - else - m_simplifier.mk_add(new_monomials.size(), new_monomials.c_ptr(), subst); - TRACE("arith_solver", tout << "solving:\n" << mk_pp(lhs, m_manager) << "\n" << mk_pp(rhs, m_manager) - << "\nresult:\n" << mk_pp(var, m_manager) << "\n" << mk_pp(subst, m_manager) << "\n";); - return true; -} - - diff --git a/src/smt/arith_solver_plugin.h b/src/smt/arith_solver_plugin.h deleted file mode 100644 index bf64380b7..000000000 --- a/src/smt/arith_solver_plugin.h +++ /dev/null @@ -1,34 +0,0 @@ -/*++ -Copyright (c) 2006 Microsoft Corporation - -Module Name: - - arith_solver_plugin.h - -Abstract: - - - -Author: - - Leonardo de Moura (leonardo) 2008-06-30. - -Revision History: - ---*/ -#ifndef _ARITH_SOLVER_PLUGIN_H_ -#define _ARITH_SOLVER_PLUGIN_H_ - -#include"solver_plugin.h" -#include"arith_simplifier_plugin.h" - -class arith_solver_plugin : public solver_plugin { - arith_simplifier_plugin & m_simplifier; -public: - arith_solver_plugin(arith_simplifier_plugin & simp); - virtual ~arith_solver_plugin() {} - virtual bool solve(expr * lhs, expr * rhs, expr_mark const & forbidden, app_ref & var, expr_ref & subst); -}; - -#endif /* _ARITH_SOLVER_PLUGIN_H_ */ - diff --git a/src/smt/asserted_formulas.cpp b/src/smt/asserted_formulas.cpp index 6fdfc0488..f86da835c 100644 --- a/src/smt/asserted_formulas.cpp +++ b/src/smt/asserted_formulas.cpp @@ -19,13 +19,10 @@ Revision History: #include"asserted_formulas.h" #include"ast_ll_pp.h" #include"ast_pp.h" -#include"ast_smt2_pp.h" #include"arith_simplifier_plugin.h" #include"array_simplifier_plugin.h" #include"datatype_simplifier_plugin.h" #include"bv_simplifier_plugin.h" -#include"arith_solver_plugin.h" -#include"occurs.h" #include"for_each_expr.h" #include"well_sorted.h" #include"pull_ite_tree.h" @@ -34,7 +31,6 @@ Revision History: #include"pattern_inference.h" #include"nnf.h" #include"cnf.h" -#include"expr_context_simplifier.h" #include"bv_elim.h" #include"inj_axiom.h" #include"der.h" @@ -54,8 +50,6 @@ asserted_formulas::asserted_formulas(ast_manager & m, front_end_params & p): m_asserted_formulas(m), m_asserted_formula_prs(m), m_asserted_qhead(0), - m_subst(m), - m_vars_qhead(0), m_macro_manager(m, m_simplifier), m_bit2int(m), m_bv_sharing(m), @@ -68,7 +62,6 @@ asserted_formulas::asserted_formulas(ast_manager & m, front_end_params & p): setup_simplifier_plugins(m_simplifier, m_bsimp, arith_simp, m_bvsimp); SASSERT(m_bsimp != 0); SASSERT(arith_simp != 0); - m_simplifier.set_subst_map(&m_subst); m_macro_finder = alloc(macro_finder, m_manager, m_macro_manager); basic_simplifier_plugin * basic_simp = 0; @@ -171,7 +164,7 @@ void asserted_formulas::assert_expr(expr * e, proof * _in_pr) { expr_ref r2(m_manager); proof_ref pr2(m_manager); TRACE("assert_expr_before_simp", tout << mk_ll_pp(e, m_manager) << "\n";); - TRACE("assert_expr_bug", tout << mk_ismt2_pp(e, m_manager) << "\n";); + TRACE("assert_expr_bug", tout << mk_pp(e, m_manager) << "\n";); if (m_params.m_pre_simplifier) { m_pre_simplifier(e, r1, pr1); } @@ -181,7 +174,7 @@ void asserted_formulas::assert_expr(expr * e, proof * _in_pr) { } set_eliminate_and(false); // do not eliminate and before nnf. m_simplifier(r1, r2, pr2); - TRACE("assert_expr_bug", tout << "after...\n" << mk_ismt2_pp(r1, m_manager) << "\n";); + TRACE("assert_expr_bug", tout << "after...\n" << mk_pp(r1, m_manager) << "\n";); if (m_manager.proofs_enabled()) { if (e == r2) pr2 = in_pr; @@ -211,8 +204,6 @@ void asserted_formulas::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); - s.m_vars_lim = m_vars.size(); - s.m_forbidden_vars_lim = m_forbidden_vars.size(); s.m_inconsistent_old = m_inconsistent; m_defined_names.push_scope(); m_bv_sharing.push_scope(); @@ -226,54 +217,21 @@ void asserted_formulas::pop_scope(unsigned num_scopes) { unsigned new_lvl = m_scopes.size() - num_scopes; scope & s = m_scopes[new_lvl]; m_inconsistent = s.m_inconsistent_old; - restore_subst(s.m_vars_lim); - restore_forbidden_vars(s.m_forbidden_vars_lim); m_defined_names.pop_scope(num_scopes); m_asserted_formulas.shrink(s.m_asserted_formulas_lim); if (m_manager.proofs_enabled()) m_asserted_formula_prs.shrink(s.m_asserted_formulas_lim); m_asserted_qhead = s.m_asserted_formulas_lim; - m_vars_qhead = m_vars.size(); m_scopes.shrink(new_lvl); flush_cache(); TRACE("asserted_formulas_scopes", tout << "after pop " << num_scopes << "\n"; display(tout);); } -void asserted_formulas::restore_subst(unsigned old_size) { - unsigned sz = m_vars.size(); - SASSERT(sz >= old_size); - TRACE("asserted_formulas_bug", tout << "restore_subst, old_size: " << old_size << ", curr_size: " << sz << "\n";); - for (unsigned i = old_size; i < sz; i++) { - SASSERT(is_app(m_vars[i])); - TRACE("asserted_formulas_bug", tout << "removing subst: " << mk_pp(m_vars[i], m_manager) << "\n";); - m_subst.erase(m_vars[i]); - SASSERT(!m_subst.contains(m_vars[i])); - } - if (old_size != sz) - flush_cache(); - m_vars.shrink(old_size); -} - -void asserted_formulas::restore_forbidden_vars(unsigned old_size) { - unsigned sz = m_forbidden_vars.size(); - SASSERT(sz >= old_size); - for (unsigned i = old_size; i < sz; i++) { - TRACE("solver_bug", tout << "unmarking: " << m_forbidden_vars[i]->get_decl()->get_name() << "\n";); - m_forbidden.mark(m_forbidden_vars[i], false); - } - m_forbidden_vars.shrink(old_size); -} - void asserted_formulas::reset() { m_defined_names.reset(); m_asserted_qhead = 0; m_asserted_formulas.reset(); m_asserted_formula_prs.reset(); - m_subst.reset(); - m_vars.reset(); - m_vars_qhead = 0; - m_forbidden.reset(); - m_forbidden_vars.reset(); m_macro_manager.reset(); m_bv_sharing.reset(); m_inconsistent = false; @@ -315,33 +273,22 @@ void asserted_formulas::reduce() { 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_quant_elim && has_quantifiers()), quant_elim()); INVOKE(m_params.m_nnf_cnf, nnf_cnf()); - INVOKE(m_params.m_context_simplifier, context_simplifier()); - INVOKE(m_params.m_strong_context_simplifier, strong_context_simplifier()); INVOKE(m_params.m_eliminate_and, 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_solver, solve()); 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()); - TRACE("der_bug", tout << "before DER:\n"; display(tout);); - INVOKE(m_params.m_der && has_quantifiers(), apply_der()); - TRACE("der_bug", tout << "after DER:\n"; display(tout);); 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()); - TRACE("qbv_bug", tout << "before demod:\n"; display(tout);); - INVOKE(m_params.m_pre_demod && has_quantifiers(), apply_demodulators()); - TRACE("qbv_bug", tout << "after demod:\n"; display(tout);); 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_max_bv_sharing && has_bv(), max_bv_sharing()); INVOKE(m_params.m_bb_quantifiers, elim_bvs_from_quantifiers()); - INVOKE(m_params.m_bb_quantifiers && m_params.m_der && has_quantifiers(), apply_der()); // bit-vector elimination + bit-blasting creates new opportunities for der. // temporary HACK: make sure that arith & bv are list-assoc // this may destroy some simplification steps such as max_bv_sharing reduce_asserted_formulas(); @@ -362,46 +309,6 @@ void asserted_formulas::eliminate_and() { TRACE("after_elim_and", display(tout);); } -bool asserted_formulas::trivial_solve(expr * lhs, expr * rhs, app_ref & var, expr_ref & subst, proof_ref& pr) { - if (is_uninterp_const(lhs) && !m_forbidden.is_marked(lhs)) { - var = to_app(lhs); - subst = rhs; - if (m_manager.proofs_enabled()) { - app* n = m_manager.mk_eq(lhs,rhs); - pr = m_manager.mk_reflexivity(m_manager.mk_iff(n,n)); - } - TRACE("solve_bug", - tout << "trivial solve " << - mk_pp(var, m_manager) << " |-> " << - mk_pp(subst, m_manager) << "\n";); - return true; - } - else if (is_uninterp_const(rhs) && !m_forbidden.is_marked(rhs)) { - var = to_app(rhs); - subst = lhs; - if (m_manager.proofs_enabled()) { - app* m = m_manager.mk_eq(lhs,rhs); - pr = m_manager.mk_commutativity(m); - } - TRACE("solve_bug", - tout << "trivial solve " << - mk_pp(var, m_manager) << " |-> " << - mk_pp(subst, m_manager) << "\n";); - return true; - } - return false; -} - -bool asserted_formulas::is_pos_literal(expr * n) { - return is_app(n) && to_app(n)->get_num_args() == 0 && to_app(n)->get_family_id() == null_family_id; -} - -bool asserted_formulas::is_neg_literal(expr * n) { - if (m_manager.is_not(n)) - return is_pos_literal(to_app(n)->get_arg(0)); - return false; -} - unsigned asserted_formulas::get_formulas_last_level() const { if (m_scopes.empty()) { return 0; @@ -411,121 +318,6 @@ unsigned asserted_formulas::get_formulas_last_level() const { } } - -/** - \brief (ite x (= c1 y) (= c2 y)) where y is a constant. -> (= y (ite x c1 c2)) -*/ -bool asserted_formulas::solve_ite_definition_core(expr * lhs1, expr * rhs1, expr * lhs2, expr * rhs2, expr * cond, app_ref & var, expr_ref & subst) { - if (rhs1 == rhs2 && is_uninterp_const(rhs1) && !occurs(rhs1, cond) && !occurs(rhs1, lhs1) && !occurs(rhs1, lhs2)) { - var = to_app(rhs1); - m_bsimp->mk_ite(cond, lhs1, lhs2, subst); - return true; - } - return false; -} - -bool asserted_formulas::solve_ite_definition(expr * arg1, expr * arg2, expr * arg3, app_ref & var, expr_ref & subst) { - - if (!m_manager.is_eq(arg2) || !m_manager.is_eq(arg3)) - return false; - - app * app2 = to_app(arg2); - app * app3 = to_app(arg3); - expr * lhs1 = app2->get_arg(0); - expr * rhs1 = app2->get_arg(1); - expr * lhs2 = app3->get_arg(0); - expr * rhs2 = app3->get_arg(1); - - if (solve_ite_definition_core(lhs1, rhs1, lhs2, rhs2, arg1, var, subst)) - return true; - if (solve_ite_definition_core(rhs1, lhs1, lhs2, rhs2, arg1, var, subst)) - return true; - if (solve_ite_definition_core(lhs1, rhs1, rhs2, lhs2, arg1, var, subst)) - return true; - if (solve_ite_definition_core(rhs1, lhs1, rhs2, lhs2, arg1, var, subst)) - return true; - return false; -} - -bool asserted_formulas::solve_core(expr * n, app_ref & var, expr_ref & subst, proof_ref& pr) { - if (m_manager.is_eq(n)) { - // equality case - app * eq = to_app(n); - expr * lhs = eq->get_arg(0); - expr * rhs = eq->get_arg(1); - TRACE("solve_bug", tout << mk_bounded_pp(n, m_manager) << "\n" << mk_bounded_pp(lhs, m_manager) << "\n" << mk_bounded_pp(rhs, m_manager) << "\n";); - if (trivial_solve(lhs, rhs, var, subst, pr)) { - return true; - } - else { - sort * s = m_manager.get_sort(lhs); - family_id fid = s->get_family_id(); - solver_plugin * p = m_solver_plugins.get_plugin(fid); - if (p != 0 && p->solve(lhs, rhs, m_forbidden, var, subst)) { - if (m_manager.proofs_enabled()) { - app* new_eq = m_manager.mk_eq(var,subst); - pr = m_manager.mk_th_lemma(p->get_family_id(), m_manager.mk_iff(n,new_eq),0,0); - } - TRACE("solve_bug", tout << "theory solve\n";); - return true; - } - } - return false; - } - else if (m_manager.is_iff(n)) { - // <=> case - app * iff = to_app(n); - expr * lhs = iff->get_arg(0); - expr * rhs = iff->get_arg(1); - if (trivial_solve(lhs, rhs, var, subst, pr)) { - return true; - } - return false; - } - else { - if (m_manager.is_ite(n)) { - // - // (ite x (= c1 y) (= c2 y)) where y is a constant. -> (= y (ite x c1 c2)) - // - app * ite = to_app(n); - if (solve_ite_definition(ite->get_arg(0), ite->get_arg(1), ite->get_arg(2), var, subst)) { - if (m_manager.proofs_enabled()) { - pr = m_manager.mk_rewrite(n, m_manager.mk_eq(var, subst)); - } - return true; - } - } - - // check if literal - expr * lit = n; - if (is_pos_literal(lit)) { - var = to_app(lit); - subst = m_manager.mk_true(); - if (m_manager.proofs_enabled()) { - // [rewrite]: (iff (iff l true) l) - // [symmetry T1]: (iff l (iff l true)) - pr = m_manager.mk_rewrite(m_manager.mk_eq(var, subst), n); - pr = m_manager.mk_symmetry(pr); - } - - return true; - } - else if (is_neg_literal(lit)) { - var = to_app(to_app(lit)->get_arg(0)); - subst = m_manager.mk_false(); - if (m_manager.proofs_enabled()) { - // [rewrite]: (iff (iff l false) ~l) - // [symmetry T1]: (iff ~l (iff l false)) - pr = m_manager.mk_rewrite(m_manager.mk_eq(var, subst), n); - pr = m_manager.mk_symmetry(pr); - } - - return true; - } - } - return false; -} - void asserted_formulas::collect_static_features() { if (m_params.m_display_features) { unsigned sz = m_asserted_formulas.size(); @@ -545,7 +337,7 @@ void asserted_formulas::display(std::ostream & out) const { for (unsigned i = 0; i < m_asserted_formulas.size(); i++) { if (i == m_asserted_qhead) out << "[HEAD] ==>\n"; - out << mk_ismt2_pp(m_asserted_formulas.get(i), m_manager) << "\n"; + out << mk_pp(m_asserted_formulas.get(i), m_manager) << "\n"; } out << "inconsistent: " << inconsistent() << "\n"; } @@ -563,316 +355,6 @@ void asserted_formulas::display_ll(std::ostream & out, ast_mark & pp_visited) co } void asserted_formulas::collect_statistics(statistics & st) const { - // m_quant_elim.collect_statistics(st); -} - -/** - \brief Functor used to order solved equations x = t, in a way they can be solved - efficiently. -*/ -class top_sort { - enum color { White, Grey, Black }; - ast_manager & m_manager; - family_id m_bfid; - - expr_map * m_candidate_map; // Set of candidate substitutions var -> ast - obj_map m_var2idx; // var -> index in vars; - ptr_vector * m_ordered_vars; // Result1: set of variables ordered for applying substitution efficiently. - unsigned_vector * m_failed_idxs; // Result2: indices of substitutions that cannot be applied. - - svector m_colors; - ptr_vector m_todo; - - expr * get_candidate_def(expr * n) const { - if (is_app(n) && to_app(n)->get_num_args() == 0 && m_candidate_map->contains(n)) { - expr * d = 0; - proof * p = 0; - m_candidate_map->get(n, d, p); - SASSERT(d); - return d; - } - return 0; - } - - bool is_candidate(expr * n) const { - return get_candidate_def(n) != 0; - } - - void remove_candidate(app * n) { - TRACE("solve", tout << "removing candidate #" << n->get_id() << " " << mk_bounded_pp(n, m_manager) << "\n";); - unsigned idx = UINT_MAX; - m_var2idx.find(n, idx); - SASSERT(idx != UINT_MAX); - m_candidate_map->erase(n); - m_failed_idxs->push_back(idx); - } - - color get_color(expr * n) const { - return m_colors.get(n->get_id(), White); - } - - void set_color(expr * n, color c) { - unsigned id = n->get_id(); - m_colors.reserve(id+1, White); - m_colors[id] = c; - if (c == Black && is_candidate(n)) - m_ordered_vars->push_back(to_app(n)); - } - - void main_loop(app * n) { - m_todo.push_back(n); - expr * def; - while (!m_todo.empty()) { - expr * n = m_todo.back(); - switch (get_color(n)) { - case Black: - m_todo.pop_back(); - break; - case White: - set_color(n, Grey); - if (visit_children(n)) { - set_color(n, Black); - } - break; - case Grey: - if (all_black_children(n)) { - set_color(n, Black); - } - else { - def = get_candidate_def(n); - if (def) { - // Break loop - remove_candidate(to_app(n)); - set_color(n, Black); - } - // there is another occurrence of n on the stack - SASSERT(std::find(m_todo.begin(), m_todo.end() - 1, n) != m_todo.end()); - } - m_todo.pop_back(); - } - } - } - - void visit(expr * n, bool & visited) { - if (get_color(n) != Black) { - m_todo.push_back(n); - visited = false; - } - } - - bool visit_children(expr * n) { - bool visited = true; - unsigned j; - expr * def; - switch (n->get_kind()) { - case AST_VAR: - break; - case AST_APP: - j = to_app(n)->get_num_args(); - if (j == 0) { - def = get_candidate_def(n); - if (def) - visit(def, visited); - } - else { - while (j > 0) { - --j; - visit(to_app(n)->get_arg(j), visited); - } - } - break; - case AST_QUANTIFIER: - visit(to_quantifier(n)->get_expr(), visited); - break; - default: - UNREACHABLE(); - } - return visited; - } - - bool is_black(expr * n) const { - return get_color(n) == Black; - } - - bool all_black_children(expr * n) const { - expr * def; - unsigned j; - switch (n->get_kind()) { - case AST_VAR: - return true; - case AST_APP: - j = to_app(n)->get_num_args(); - if (j == 0) { - def = get_candidate_def(n); - if (def) - return is_black(def); - return true; - } - else { - while (j > 0) { - --j; - if (!is_black(to_app(n)->get_arg(j))) { - return false; - } - } - } - return true; - case AST_QUANTIFIER: - return is_black(to_quantifier(n)->get_expr()); - default: - UNREACHABLE(); - return true; - } - } - -public: - top_sort(ast_manager & m):m_manager(m), m_bfid(m.get_basic_family_id()) {} - - void operator()(ptr_vector const & vars, - expr_map & candidates, - ptr_vector & ordered_vars, - unsigned_vector & failed_idxs) { - m_var2idx.reset(); - ptr_vector::const_iterator it = vars.begin(); - ptr_vector::const_iterator end = vars.end(); - for (unsigned idx = 0; it != end; ++it, ++idx) - m_var2idx.insert(*it, idx); - m_candidate_map = &candidates; - m_ordered_vars = &ordered_vars; - m_failed_idxs = &failed_idxs; - m_colors.reset(); - it = vars.begin(); - end = vars.end(); - for (; it != end; ++it) { - TRACE("top_sort", tout << "processing: " << (*it)->get_decl()->get_name() << "\n";); - main_loop(*it); - } - } -}; - -void asserted_formulas::get_ordered_subst_vars(ptr_vector & ordered_vars) { - top_sort sort(m_manager); - unsigned_vector failed_idxs; - sort(m_vars, m_subst, ordered_vars, failed_idxs); - SASSERT(failed_idxs.empty()); -} - -bool asserted_formulas::solve_core() { - flush_cache(); - - expr_map tmp_subst(m_manager); - ptr_vector tmp_vars; // domain of m_tmp_subst - expr_ref_vector candidates(m_manager); - proof_ref_vector candidate_prs(m_manager); - - IF_IVERBOSE(10, verbose_stream() << "solving...\n";); - bool has_subst = false; - app_ref var(m_manager); - expr_ref subst(m_manager); - proof_ref pr1(m_manager); - unsigned i = m_asserted_qhead; - unsigned j = i; - 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); - TRACE("solve", tout << "processing... #" << n->get_id() << "\n";); - TRACE("solve", tout << mk_bounded_pp(n, m_manager, 3) << "\n"; - if (pr) tout << mk_bounded_pp(pr, m_manager, 3) << "\n";); - - if (solve_core(n, var, subst, pr1) && !m_forbidden.is_marked(var)) { - if (m_manager.proofs_enabled()) { - // TODO: refine potentially useless rewrite step - if (m_manager.is_eq(n) && to_app(n)->get_arg(0) == var && - to_app(n)->get_arg(1) == subst) { - // skip useless rewrite step. - } - else { - TRACE("solve", tout << mk_bounded_pp(n, m_manager, 3) << "\n"; - tout << mk_bounded_pp(pr1.get(), m_manager, 5) << "\n";); - pr = m_manager.mk_modus_ponens(pr, pr1.get()); - } - candidate_prs.push_back(pr); - } - - tmp_subst.insert(var, subst, pr); - SASSERT(!m_forbidden.is_marked(var)); - TRACE("solve_subst", tout << mk_pp(var, m_manager) << "\n" << mk_pp(subst, m_manager) << "\n";); - TRACE("solver_bug", tout << mk_pp(var, m_manager) << "\n" << mk_pp(subst, m_manager) << "\n";); - tmp_vars.push_back(var); - m_forbidden.mark(var, true); - candidates.push_back(n); - has_subst = true; - continue; - } - if (j < i) { - m_asserted_formulas.set(j, n); - if (m_manager.proofs_enabled()) - m_asserted_formula_prs.set(j, pr); - } - j++; - } - m_asserted_formulas.shrink(j); - if (m_manager.proofs_enabled()) - m_asserted_formula_prs.shrink(j); - - if (!has_subst) - return false; - - ptr_vector ordered_vars; - unsigned_vector failed_idxs; - top_sort sort(m_manager); - sort(tmp_vars, tmp_subst, ordered_vars, failed_idxs); - // restore substitutions that cannot be applied due to loops. - unsigned_vector::iterator it = failed_idxs.begin(); - unsigned_vector::iterator end = failed_idxs.end(); - for (; it != end; ++it) { - unsigned idx = *it; - m_asserted_formulas.push_back(candidates.get(idx)); - if (m_manager.proofs_enabled()) - m_asserted_formula_prs.push_back(candidate_prs.get(idx)); - app * var = tmp_vars[idx]; - m_forbidden.mark(var, false); - } - IF_IVERBOSE(10, verbose_stream() << "num. eliminated vars: " << ordered_vars.size() << "\n";); - ptr_vector::iterator it2 = ordered_vars.begin(); - ptr_vector::iterator end2 = ordered_vars.end(); - for (; it2 != end2; ++it2) { - app * var = *it2; - TRACE("solve_res", tout << "var: " << mk_pp(var, m_manager) << "\n";); - expr * def = 0; - proof * pr = 0; - tmp_subst.get(var, def, pr); - SASSERT(def != 0); - SASSERT(m_forbidden.is_marked(var)); - m_forbidden.mark(var, false); - expr_ref new_def(m_manager); - proof_ref def_eq_new_def_pr(m_manager); - proof_ref new_pr(m_manager); - TRACE("solve_res", tout << "reducing:\n" << mk_ll_pp(def, m_manager);); - m_simplifier(def, new_def, def_eq_new_def_pr); - TRACE("solve_res", tout << "reducing:\n" << mk_ll_pp(new_def, m_manager);); - new_pr = m_manager.mk_transitivity(pr, def_eq_new_def_pr); - m_subst.insert(var, new_def, new_pr); - m_vars.push_back(var); - TRACE("solve_res", tout << "new substitution:\n" << mk_ll_pp(var, m_manager) << "======>\n" << mk_ll_pp(new_def, m_manager);); - } - return !ordered_vars.empty(); -} - -void asserted_formulas::solve() { - // This method is buggy when unsatisfiable cores are enabled. - // It may eliminate answer literals. - // Since I will remove asserted_formulas.cpp in the future, I just disabled it. - // Note: asserted_formulas.cpp is based on the obsolete preprocessing stack. - // Users should the solve-eqs tactic if they want to eliminate variables. -#if 0 - while (solve_core()) { - IF_IVERBOSE(10, verbose_stream() << "reducing...\n";); - flush_cache(); // collect garbage - reduce_asserted_formulas(); - } -#endif } void asserted_formulas::reduce_asserted_formulas() { @@ -937,24 +419,6 @@ void asserted_formulas::expand_macros() { find_macros_core(); } -void asserted_formulas::apply_demodulators() { -#if 0 - IF_IVERBOSE(10, verbose_stream() << "applying demodulators...\n";); - TRACE("before_apply_demodulators", display(tout);); - expr_ref_vector new_exprs(m_manager); - proof_ref_vector new_prs(m_manager); - unsigned sz = m_asserted_formulas.size(); - ufbv_rewriter proc(m_manager, *m_bsimp); - proc(sz - m_asserted_qhead, - m_asserted_formulas.c_ptr() + m_asserted_qhead, - m_asserted_formula_prs.c_ptr() + m_asserted_qhead, - new_exprs, new_prs); - swap_asserted_formulas(new_exprs, new_prs); - TRACE("after_apply_demodulators", display(tout);); - reduce_and_solve(); -#endif -} - void asserted_formulas::apply_quasi_macros() { IF_IVERBOSE(10, verbose_stream() << "finding quasi macros...\n";); TRACE("before_quasi_macros", display(tout);); @@ -1090,8 +554,6 @@ void asserted_formulas::reduce_and_solve() { IF_IVERBOSE(10, verbose_stream() << "reducing...\n";); flush_cache(); // collect garbage reduce_asserted_formulas(); - if (m_params.m_solver) - solve(); } void asserted_formulas::infer_patterns() { @@ -1123,41 +585,8 @@ void asserted_formulas::infer_patterns() { TRACE("after_pattern_inference", display(tout);); } -struct mark_forbidden_proc { - expr_mark & m_forbidden; - ptr_vector & m_forbidden_vars; - mark_forbidden_proc(expr_mark & f, ptr_vector & v):m_forbidden(f), m_forbidden_vars(v) {} - void operator()(var * n) {} - void operator()(quantifier * n) {} - void operator()(app * n) { - if (is_uninterp(n) && !m_forbidden.is_marked(n)) { - TRACE("solver_bug", tout << "marking: " << n->get_decl()->get_name() << "\n";); - m_forbidden.mark(n, true); - m_forbidden_vars.push_back(n); - SASSERT(m_forbidden.is_marked(n)); - } - } -}; - void asserted_formulas::commit() { - expr_fast_mark1 uf_visited; // marks used for update_forbidden - mark_forbidden_proc p(m_forbidden, m_forbidden_vars); - unsigned sz = m_asserted_formulas.size(); - for (unsigned i = m_asserted_qhead; i < sz; i++) - quick_for_each_expr(p, uf_visited, m_asserted_formulas.get(i)); - - m_macro_manager.mark_forbidden(sz - m_asserted_qhead, m_asserted_formulas.c_ptr() + m_asserted_qhead); - - ptr_vector::const_iterator it2 = m_vars.begin() + m_vars_qhead; - ptr_vector::const_iterator end2 = m_vars.end(); - for (; it2 != end2; ++it2) { - app * var = *it2; - expr * def = get_subst(var); - m_forbidden.mark(var, true); - m_forbidden_vars.push_back(var); - quick_for_each_expr(p, uf_visited, def); - } - m_vars_qhead = m_vars.size(); + m_macro_manager.mark_forbidden(m_asserted_formulas.size() - m_asserted_qhead, m_asserted_formulas.c_ptr() + m_asserted_qhead); m_asserted_qhead = m_asserted_formulas.size(); } @@ -1376,11 +805,6 @@ proof * asserted_formulas::get_inconsistency_proof() const { return 0; } -MK_SIMPLE_SIMPLIFIER(context_simplifier, expr_context_simplifier functor(m_manager), "context_simplifier", "context simplifier"); - -MK_SIMPLE_SIMPLIFIER(strong_context_simplifier, expr_strong_context_simplifier functor(m_params, m_manager), "strong_context_simplifier", "strong context simplifier"); - - void asserted_formulas::refine_inj_axiom() { IF_IVERBOSE(10, verbose_stream() << "refining injectivity...\n";); TRACE("inj_axiom", display(tout);); @@ -1406,19 +830,6 @@ void asserted_formulas::refine_inj_axiom() { MK_SIMPLIFIER(apply_bit2int, bit2int& functor = m_bit2int, "bit2int", "propagate bit-vector over integers", true); -MK_SIMPLIFIER(apply_der_core, der_star functor(m_manager), "der", "destructive equality resolution", true); - -void asserted_formulas::apply_der() { - // Keep applying DER until it cannot be applied anymore. - // The simplifications applied by REDUCE may create new opportunities for applying DER. - while(!inconsistent() && apply_der_core()) { - } - - TRACE("a_der", for (unsigned i = 0; i m_vars; // domain of m_subst - unsigned m_vars_qhead; - - expr_mark m_forbidden; - ptr_vector m_forbidden_vars; - macro_manager m_macro_manager; scoped_ptr m_macro_finder; - typedef plugin_manager solver_plugins; - solver_plugins m_solver_plugins; - bit2int m_bit2int; maximise_bv_sharing m_bv_sharing; @@ -70,50 +59,33 @@ class asserted_formulas { struct scope { unsigned m_asserted_formulas_lim; - unsigned m_vars_lim; - unsigned m_forbidden_vars_lim; bool m_inconsistent_old; }; svector m_scopes; volatile bool m_cancel_flag; void setup_simplifier_plugins(simplifier & s, basic_simplifier_plugin * & bsimp, arith_simplifier_plugin * & asimp, bv_simplifier_plugin * & bvsimp); - bool trivial_solve(expr * lhs, expr * rhs, app_ref & var, expr_ref & subst, proof_ref& pr); - bool is_pos_literal(expr * n); - bool is_neg_literal(expr * n); - bool solve_ite_definition_core(expr * lhs1, expr * rhs1, expr * lhs2, expr * rhs2, expr * cond, app_ref & var, expr_ref & subst); - bool solve_ite_definition(expr * arg1, expr * arg2, expr * arg3, app_ref & var, expr_ref & subst); - bool solve_core(expr * n, app_ref & var, expr_ref & subst, proof_ref& pr); - bool solve_core(); - void solve(); 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_demodulators(); 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 restore_subst(unsigned old_size); - void restore_forbidden_vars(unsigned old_size); 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 context_simplifier(); - void strong_context_simplifier(); void eliminate_and(); void refine_inj_axiom(); bool cheap_quant_fourier_motzkin(); bool quant_elim(); - bool apply_der_core(); - void apply_der(); void apply_distribute_forall(); bool apply_bit2int(); void lift_ite(); @@ -174,20 +146,6 @@ public: // auxiliary function used to create a logic context based on a model. void insert_macro(func_decl * f, quantifier * m, proof * pr) { m_macro_manager.insert(f, m, pr); } - // ----------------------------------- - // - // Eliminated vars - // - // ----------------------------------- - ptr_vector::const_iterator begin_subst_vars() const { return m_vars.begin(); } - ptr_vector::const_iterator end_subst_vars() const { return m_vars.end(); } - ptr_vector::const_iterator begin_subst_vars_last_level() const { - unsigned sidx = m_scopes.empty() ? 0 : m_scopes.back().m_vars_lim; - return m_vars.begin() + sidx; - } - expr * get_subst(app * var) { expr * def = 0; proof * pr; m_subst.get(var, def, pr); return def; } - bool is_subst(app * var) const { return m_subst.contains(var); } - void get_ordered_subst_vars(ptr_vector & ordered_vars); }; #endif /* _ASSERTED_FORMULAS_H_ */ diff --git a/src/smt/expr_context_simplifier.cpp b/src/smt/expr_context_simplifier.cpp index b39e3fb9c..8fd5b41bb 100644 --- a/src/smt/expr_context_simplifier.cpp +++ b/src/smt/expr_context_simplifier.cpp @@ -329,7 +329,6 @@ void expr_strong_context_simplifier::simplify_basic(expr* fml, expr_ref& result) result = fml; return; } - flet fl1(m_params.m_strong_context_simplifier, false); ptr_vector todo; ptr_vector names; @@ -480,7 +479,6 @@ void expr_strong_context_simplifier::simplify_model_based(expr* fml, expr_ref& r result = fml; return; } - flet fl1(m_params.m_strong_context_simplifier, false); ptr_vector todo; ptr_vector names; diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h index 6137917f0..b44d42fc8 100644 --- a/src/smt/smt_context.h +++ b/src/smt/smt_context.h @@ -1431,19 +1431,6 @@ namespace smt { func_decl * get_macro_interpretation(unsigned i, expr_ref & interp) const { return m_asserted_formulas.get_macro_interpretation(i, interp); } quantifier * get_macro_quantifier(func_decl * f) const { return m_asserted_formulas.get_macro_quantifier(f); } void insert_macro(func_decl * f, quantifier * m, proof * pr) { m_asserted_formulas.insert_macro(f, m, pr); } - - // ----------------------------------- - // - // Eliminated vars - // - // ----------------------------------- - public: - ptr_vector::const_iterator begin_subst_vars() const { return m_asserted_formulas.begin_subst_vars(); } - ptr_vector::const_iterator end_subst_vars() const { return m_asserted_formulas.end_subst_vars(); } - ptr_vector::const_iterator begin_subst_vars_last_level() const { return m_asserted_formulas.begin_subst_vars_last_level(); } - expr * get_subst(app * var) { return m_asserted_formulas.get_subst(var); } - bool is_subst(app * var) const { return m_asserted_formulas.is_subst(var); } - void get_ordered_subst_vars(ptr_vector & ordered_vars) { return m_asserted_formulas.get_ordered_subst_vars(ordered_vars); } }; }; diff --git a/src/smt/smt_model_generator.cpp b/src/smt/smt_model_generator.cpp index 60c12b76d..1c441ad11 100644 --- a/src/smt/smt_model_generator.cpp +++ b/src/smt/smt_model_generator.cpp @@ -526,8 +526,6 @@ namespace smt { func_decl * d = n->get_decl(); if (m_model.has_interpretation(d)) return; // declaration already has an interpretation. - if (n->get_num_args() == 0 && m_context.is_subst(n) != 0) - return; // an interpretation will be generated for this variable using the evaluator. if (n->get_num_args() == 0) { sort * r = d->get_range(); expr * v = m_model.get_some_value(r); @@ -544,61 +542,6 @@ namespace smt { }; - /** - \brief Generate an interpretation for variables that were eliminated indirectly. - When a variable is eliminated by substitution and it does not occur anywhere, then - its definition may contain declarations that do not occur anywhere else. - This method will assign an arbitrary interpretation for these declarations. - - Example: consider the formula - - (= x (f y)) - - This formula is satisfiable. If the solver is used during preprocessing step, - this formula is reduced to "true", and the substitution set contains the entry (x -> (f y)). - The declarations f and y will not have an interpretation. This method will traverse the - definition of each eliminated variable, and generate an arbitrary interpretations for - declarations that do not have one yet. - */ - void model_generator::register_indirect_elim_decls() { - expr_mark visited; - mk_interp_proc proc(*m_context, *m_model); - ptr_vector::const_iterator it = m_context->begin_subst_vars(); - ptr_vector::const_iterator end = m_context->end_subst_vars(); - for (; it != end; ++it) { - app * var = *it; - if (var->get_num_args() > 0) - continue; - expr * subst = m_context->get_subst(var); - for_each_expr(proc, visited, subst); - } - } - - void model_generator::register_subst_vars() { - ptr_vector ordered_subst_vars; - m_context->get_ordered_subst_vars(ordered_subst_vars); - ptr_vector::const_iterator it = ordered_subst_vars.begin(); - ptr_vector::const_iterator end = ordered_subst_vars.end(); - for (; it != end; ++it) { - app * var = *it; - TRACE("model_subst_vars", tout << "processing: " << mk_pp(var, m_manager) << "\n";); - if (var->get_num_args() > 0) { - TRACE("model_subst_vars", tout << "not a constant...\n";); - continue; - } - expr * subst = m_context->get_subst(var); - if (subst == 0) { - TRACE("model_subst_vars", tout << "no definition...\n";); - continue; - } - TRACE("model_subst_vars", tout << "definition: " << mk_pp(subst, m_manager) << "\n";); - expr_ref r(m_manager); - m_model->eval(subst, r); - TRACE("model_subst_vars", tout << "result: " << mk_pp(r, m_manager) << "\n";); - m_model->register_decl(var->get_decl(), r); - } - } - proto_model * model_generator::mk_model() { SASSERT(!m_model); TRACE("func_interp_bug", m_context->display(tout);); @@ -609,22 +552,6 @@ namespace smt { mk_func_interps(); finalize_theory_models(); register_macros(); - TRACE("model_subst_vars", - tout << "substitution vars:\n"; - ptr_vector::const_iterator it = m_context->begin_subst_vars(); - ptr_vector::const_iterator end = m_context->end_subst_vars(); - for (; it != end; ++it) { - app * var = *it; - tout << mk_pp(var, m_manager) << "\n"; - if (var->get_num_args() > 0) - continue; - expr * subst = m_context->get_subst(var); - if (subst == 0) - continue; - tout << "-> " << mk_bounded_pp(subst, m_manager, 10) << "\n"; - }); - register_indirect_elim_decls(); - register_subst_vars(); return m_model; } diff --git a/src/smt/smt_model_generator.h b/src/smt/smt_model_generator.h index 853fa4b07..fcccc7fbe 100644 --- a/src/smt/smt_model_generator.h +++ b/src/smt/smt_model_generator.h @@ -193,8 +193,6 @@ namespace smt { void display(std::ostream & out); void register_existing_model_values(); void register_macros(); - void register_indirect_elim_decls(); - void register_subst_vars(); bool visit_children(source const & src, ptr_vector const & roots, obj_map const & root2proc, source2color & colors, obj_hashtable & already_traversed, svector & todo); @@ -227,3 +225,4 @@ namespace smt { #endif /* _SMT_MODEL_GENERATOR_H_ */ + diff --git a/src/smt/smt_setup.cpp b/src/smt/smt_setup.cpp index 63fe1b7f3..bd9196056 100644 --- a/src/smt/smt_setup.cpp +++ b/src/smt/smt_setup.cpp @@ -188,7 +188,6 @@ namespace smt { void setup::setup_QF_UF() { m_params.m_relevancy_lvl = 0; - m_params.m_solver = true; m_params.m_nnf_cnf = false; } @@ -201,7 +200,6 @@ namespace smt { void setup::setup_QF_UF(static_features const & st) { check_no_arithmetic(st, "QF_UF"); m_params.m_relevancy_lvl = 0; - m_params.m_solver = true; m_params.m_nnf_cnf = false; m_params.m_restart_strategy = RS_LUBY; m_params.m_phase_selection = PS_CACHING_CONSERVATIVE2; @@ -215,7 +213,6 @@ namespace smt { m_params.m_relevancy_lvl = 0; m_params.m_arith_expand_eqs = true; m_params.m_arith_reflect = false; - m_params.m_solver = true; m_params.m_arith_propagate_eqs = false; m_params.m_nnf_cnf = false; setup_mi_arith(); @@ -256,7 +253,6 @@ namespace smt { m_params.m_relevancy_lvl = 0; m_params.m_arith_expand_eqs = true; m_params.m_arith_reflect = false; - m_params.m_solver = true; m_params.m_arith_propagate_eqs = false; m_params.m_nnf_cnf = false; if (is_dense(st)) { @@ -308,7 +304,6 @@ namespace smt { m_params.m_relevancy_lvl = 0; m_params.m_arith_expand_eqs = true; m_params.m_arith_reflect = false; - m_params.m_solver = true; m_params.m_arith_propagate_eqs = false; m_params.m_arith_small_lemma_size = 30; m_params.m_nnf_cnf = false; @@ -327,7 +322,6 @@ namespace smt { m_params.m_relevancy_lvl = 0; m_params.m_arith_expand_eqs = true; m_params.m_arith_reflect = false; - m_params.m_solver = true; m_params.m_arith_propagate_eqs = false; m_params.m_arith_small_lemma_size = 30; m_params.m_nnf_cnf = false; @@ -377,7 +371,6 @@ namespace smt { TRACE("setup", tout << "setup_QF_UFIDL()\n";); m_params.m_relevancy_lvl = 0; m_params.m_arith_reflect = false; - m_params.m_solver = true; m_params.m_nnf_cnf = false; m_params.m_arith_eq_bounds = true; m_params.m_phase_selection = PS_ALWAYS_FALSE; @@ -393,7 +386,6 @@ namespace smt { throw default_exception("Benchmark has real variables but it is marked as QF_UFIDL (uninterpreted functions and difference logic)."); m_params.m_relevancy_lvl = 0; m_params.m_arith_reflect = false; - m_params.m_solver = true; m_params.m_nnf_cnf = false; if (st.m_num_uninterpreted_functions == 0) { m_params.m_arith_expand_eqs = true; @@ -434,7 +426,6 @@ namespace smt { m_params.m_arith_reflect = false; m_params.m_arith_propagate_eqs = false; m_params.m_eliminate_term_ite = true; - m_params.m_solver = true; m_params.m_nnf_cnf = false; setup_mi_arith(); } @@ -446,7 +437,6 @@ namespace smt { m_params.m_arith_reflect = false; m_params.m_arith_propagate_eqs = false; m_params.m_eliminate_term_ite = true; - m_params.m_solver = true; m_params.m_nnf_cnf = false; if (numerator(st.m_arith_k_sum) > rational(2000000) && denominator(st.m_arith_k_sum) > rational(500)) { m_params.m_relevancy_lvl = 2; @@ -519,7 +509,6 @@ namespace smt { void setup::setup_QF_UFLIA() { m_params.m_relevancy_lvl = 0; m_params.m_arith_reflect = false; - m_params.m_solver = true; m_params.m_nnf_cnf = false; m_params.m_arith_propagation_threshold = 1000; setup_i_arith(); @@ -534,7 +523,6 @@ namespace smt { void setup::setup_QF_UFLRA() { m_params.m_relevancy_lvl = 0; m_params.m_arith_reflect = false; - m_params.m_solver = true; m_params.m_nnf_cnf = false; setup_mi_arith(); } @@ -542,7 +530,6 @@ namespace smt { void setup::setup_QF_BV() { m_params.m_relevancy_lvl = 0; m_params.m_arith_reflect = false; - m_params.m_solver = true; m_params.m_bv_cc = false; m_params.m_bb_ext_gates = true; m_params.m_nnf_cnf = false; @@ -552,7 +539,6 @@ namespace smt { void setup::setup_QF_AUFBV() { m_params.m_array_mode = AR_SIMPLE; m_params.m_relevancy_lvl = 0; - m_params.m_solver = true; m_params.m_bv_cc = false; m_params.m_bb_ext_gates = true; m_params.m_nnf_cnf = false; @@ -575,7 +561,6 @@ namespace smt { } else { m_params.m_relevancy_lvl = 2; - m_params.m_solver = true; } m_context.register_plugin(alloc(smt::theory_array, m_manager, m_params)); } @@ -609,7 +594,6 @@ namespace smt { m_params.m_phase_selection = PS_CACHING_CONSERVATIVE2; m_params.m_random_initial_activity = IA_ZERO; } - // m_params.m_solver = true; // if (st.m_num_arith_ineqs == st.m_num_diff_ineqs && st.m_num_arith_eqs == st.m_num_diff_eqs && st.m_arith_k_sum < rational(INT_MAX / 8)) // m_context.register_plugin(new smt::theory_si_arith(m_manager, m_params)); // else @@ -688,14 +672,10 @@ namespace smt { } void setup::setup_LRA() { - m_params.m_quant_elim = true; - // after quantifier elimination, the result is a QF_LRA benchmark m_params.m_relevancy_lvl = 0; - // m_params.m_arith_expand_eqs = true; << may affect quant_elim m_params.m_arith_reflect = false; m_params.m_arith_propagate_eqs = false; m_params.m_eliminate_term_ite = true; - m_params.m_solver = true; setup_mi_arith(); } diff --git a/src/smt/solver_plugin.h b/src/smt/solver_plugin.h deleted file mode 100644 index ba682a639..000000000 --- a/src/smt/solver_plugin.h +++ /dev/null @@ -1,51 +0,0 @@ -/*++ -Copyright (c) 2006 Microsoft Corporation - -Module Name: - - solver_plugin.h - -Abstract: - - - -Author: - - Leonardo de Moura (leonardo) 2008-06-30. - -Revision History: - ---*/ -#ifndef _SOLVER_PLUGIN_H_ -#define _SOLVER_PLUGIN_H_ - -#include"ast.h" - -/** - \brief Abstract solver used during preprocessing step. -*/ -class solver_plugin { -protected: - ast_manager & m_manager; - family_id m_fid; -public: - solver_plugin(symbol const & fname, ast_manager & m):m_manager(m), m_fid(m.get_family_id(fname)) {} - - virtual ~solver_plugin() {} - - /** - \brief Return true if it is possible to solve lhs = rhs. The - arg. forbidden contains the set of variables that cannot be - used. Store the result (var = subst) in var and subst. - - \remark Only simple solvers are supported. That is, the solution set has only one entry. - */ - virtual bool solve(expr * lhs, expr * rhs, expr_mark const & forbidden, app_ref & var, expr_ref & subst) = 0; - - family_id get_family_id() const { return m_fid; } - - ast_manager & get_manager() { return m_manager; } -}; - -#endif /* _SOLVER_PLUGIN_H_ */ - diff --git a/src/smt/tactic/smt_tactic.cpp b/src/smt/tactic/smt_tactic.cpp index fd942d05c..84587b6c9 100644 --- a/src/smt/tactic/smt_tactic.cpp +++ b/src/smt/tactic/smt_tactic.cpp @@ -151,7 +151,7 @@ public: SASSERT(in->is_well_sorted()); ast_manager & m = in->m(); TRACE("smt_tactic", tout << this << "\nAUTO_CONFIG: " << fparams().m_auto_config << " HIDIV0: " << fparams().m_hi_div0 << " " - << " PREPROCESS: " << fparams().m_preprocess << ", SOLVER:" << fparams().m_solver << "\n"; + << " PREPROCESS: " << fparams().m_preprocess << "\n"; tout << "fail-if-inconclusive: " << m_fail_if_inconclusive << "\n"; tout << "params_ref: " << m_params_ref << "\n";); TRACE("smt_tactic_detail", in->display(tout);); diff --git a/src/test/quant_elim.cpp b/src/test/quant_elim.cpp index 859672f8d..0f1ddfabd 100644 --- a/src/test/quant_elim.cpp +++ b/src/test/quant_elim.cpp @@ -34,7 +34,7 @@ static void test_qe(ast_manager& m, lbool expected_outcome, expr* fml, char cons simplifier simp(m); front_end_params params; - params.m_quant_elim = true; + // params.m_quant_elim = true; std::cout << mk_pp(fml, m) << "\n"; qe::expr_quant_elim qe(m, params);