From 5379130c8cb5bfd9fb3e6b9919e8e9fe401a74f5 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 5 Dec 2012 08:35:03 -0800 Subject: [PATCH] eliminated m_proof_mode from smt_params, ast_manager has this information Signed-off-by: Leonardo de Moura --- src/muz_qe/dl_cmds.cpp | 1 - src/muz_qe/pdr_context.cpp | 1 - src/muz_qe/pdr_farkas_learner.cpp | 1 - src/muz_qe/pdr_quantifiers.cpp | 2 +- src/muz_qe/unit_subsumption_tactic.cpp | 1 - src/muz_qe/vsubst_tactic.cpp | 3 +- src/smt/params/params2smt_params.cpp | 79 -------------------------- src/smt/params/params2smt_params.h | 31 ---------- src/smt/params/smt_params.cpp | 1 - src/smt/params/smt_params.h | 2 - src/smt/smt_kernel.cpp | 4 +- src/smt/tactic/smt_tactic.cpp | 4 +- 12 files changed, 6 insertions(+), 124 deletions(-) delete mode 100644 src/smt/params/params2smt_params.cpp delete mode 100644 src/smt/params/params2smt_params.h diff --git a/src/muz_qe/dl_cmds.cpp b/src/muz_qe/dl_cmds.cpp index 8c4e26db7..bf9c24203 100644 --- a/src/muz_qe/dl_cmds.cpp +++ b/src/muz_qe/dl_cmds.cpp @@ -28,7 +28,6 @@ Notes: #include"cancel_eh.h" #include"scoped_ctrl_c.h" #include"scoped_timer.h" -#include"params2smt_params.h" #include"trail.h" #include diff --git a/src/muz_qe/pdr_context.cpp b/src/muz_qe/pdr_context.cpp index 9faee3ab0..c8c1e3b2a 100644 --- a/src/muz_qe/pdr_context.cpp +++ b/src/muz_qe/pdr_context.cpp @@ -1456,7 +1456,6 @@ namespace pdr { } if (m_params.use_farkas() && !classify.is_bool()) { m.toggle_proof_mode(PGM_FINE); - m_fparams.m_proof_mode = PGM_FINE; m_fparams.m_arith_bound_prop = BP_NONE; m_fparams.m_arith_auto_config_simplex = true; m_fparams.m_arith_propagate_eqs = false; diff --git a/src/muz_qe/pdr_farkas_learner.cpp b/src/muz_qe/pdr_farkas_learner.cpp index b3d0b4fd0..06b8f5eeb 100644 --- a/src/muz_qe/pdr_farkas_learner.cpp +++ b/src/muz_qe/pdr_farkas_learner.cpp @@ -255,7 +255,6 @@ namespace pdr { smt_params farkas_learner::get_proof_params(smt_params& orig_params) { smt_params res(orig_params); - res.m_proof_mode = PROOF_MODE; res.m_arith_bound_prop = BP_NONE; // temp hack to fix the build // res.m_conflict_resolution_strategy = CR_ALL_DECIDED; diff --git a/src/muz_qe/pdr_quantifiers.cpp b/src/muz_qe/pdr_quantifiers.cpp index 51a86e38c..2816a58d4 100644 --- a/src/muz_qe/pdr_quantifiers.cpp +++ b/src/muz_qe/pdr_quantifiers.cpp @@ -214,7 +214,7 @@ namespace pdr { expr_ref_vector fmls(m); smt_params fparams; - fparams.m_proof_mode = PGM_FINE; + SASSERT(m.proofs_enabled()); fparams.m_mbqi = true; fmls.push_back(m_A.get()); diff --git a/src/muz_qe/unit_subsumption_tactic.cpp b/src/muz_qe/unit_subsumption_tactic.cpp index 1fb71490d..afc81723a 100644 --- a/src/muz_qe/unit_subsumption_tactic.cpp +++ b/src/muz_qe/unit_subsumption_tactic.cpp @@ -37,7 +37,6 @@ struct unit_subsumption_tactic : public tactic { m_cancel(false), m_context(m, m_fparams, p), m_clauses(m) { - m_fparams.m_proof_mode = m.proof_mode(); } void set_cancel(bool f) { diff --git a/src/muz_qe/vsubst_tactic.cpp b/src/muz_qe/vsubst_tactic.cpp index b84202ee9..c389d9a66 100644 --- a/src/muz_qe/vsubst_tactic.cpp +++ b/src/muz_qe/vsubst_tactic.cpp @@ -45,7 +45,6 @@ Notes: #include"arith_decl_plugin.h" #include"for_each_expr.h" #include"extension_model_converter.h" -#include"params2smt_params.h" #include"ast_smt2_pp.h" class vsubst_tactic : public tactic { @@ -94,7 +93,7 @@ class vsubst_tactic : public tactic { } smt_params params; - params2smt_params(p, params); + params.updt_params(p); params.m_model = false; flet fl1(params.m_nlquant_elim, true); flet fl2(params.m_nl_arith_gb, false); diff --git a/src/smt/params/params2smt_params.cpp b/src/smt/params/params2smt_params.cpp deleted file mode 100644 index b01d9478a..000000000 --- a/src/smt/params/params2smt_params.cpp +++ /dev/null @@ -1,79 +0,0 @@ -/*++ -Copyright (c) 2011 Microsoft Corporation - -Module Name: - - params2smt_params.h - -Abstract: - - Backward compatibility utilities for parameter setting - -Author: - - Leonardo de Moura (leonardo) 2011-05-19. - -Revision History: - ---*/ -#include"smt_params.h" -#include"params.h" - -/** - Update smt_params using s. - Only the most frequently used options are updated. - - This function is mainly used to allow smt::context to be used in - the new strategy framework. -*/ -void params2smt_params(params_ref const & s, smt_params & t) { - 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()); - t.m_mbqi = s.get_bool("mbqi", t.m_mbqi); - t.m_mbqi_max_iterations = s.get_uint("mbqi_max_iterations", t.m_mbqi_max_iterations); - t.m_random_seed = s.get_uint("random_seed", t.m_random_seed); - t.m_model = s.get_bool("produce_models", t.m_model); - if (s.get_bool("produce_proofs", false)) - t.m_proof_mode = PGM_FINE; - 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_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); - t.m_array_simplify = s.get_bool("array_old_simplifier", t.m_array_simplify); - t.m_arith_branch_cut_ratio = s.get_uint("arith_branch_cut_ratio", t.m_arith_branch_cut_ratio); - t.m_arith_expand_eqs = s.get_bool("arith_expand_eqs", t.m_arith_expand_eqs); - - if (s.get_bool("arith_greatest_error_pivot", false)) - t.m_arith_pivot_strategy = ARITH_PIVOT_GREATEST_ERROR; - else if (s.get_bool("arith_least_error_pivot", false)) - t.m_arith_pivot_strategy = ARITH_PIVOT_LEAST_ERROR; -} - -/** - \brief Copy parameters (from s) that affect the semantics of Z3 (e.g., HI_DIV0). - It also copies the model construction parameter. Thus, model construction - can be enabled at the command line. -*/ -void smt_params2params(smt_params const & s, params_ref & t) { - if (s.m_model) - t.set_bool("produce_models", true); - if (!s.m_hi_div0) - t.set_bool("hi_div0", false); -} - -/** - \brief Bridge for using params_ref with smt::context. -*/ -void solver_smt_params_descrs(param_descrs & r) { - r.insert("hi_div0", CPK_BOOL, "(default: true) if true, then Z3 uses the usual hardware interpretation for division (rem, mod) by zero. Otherwise, these operations are considered uninterpreted"); - r.insert("relevancy", CPK_UINT, "relevancy propagation heuristic: 0 - disabled, 1 - relevancy is tracked by only affects quantifier instantiation, 2 - relevancy is tracked, and an atom is only asserted if it is relevant"); - r.insert("mbqi", CPK_BOOL, "model based quantifier instantiation (MBQI)"); - r.insert("mbqi_max_iterations", CPK_UINT, "maximum number of rounds of MBQI"); - r.insert("random_seed", CPK_UINT, "random seed for smt solver"); - r.insert("qi_eager_threshold", CPK_DOUBLE, "threshold for eager quantifier instantiation"); - r.insert("qi_lazy_threshold", CPK_DOUBLE, "threshold for lazy quantifier instantiation"); - r.insert("auto_config", CPK_BOOL, "use heuristics to automatically configure smt solver"); - r.insert("arith_branch_cut_ratio", CPK_UINT, "branch&bound / gomory cut ratio"); -} diff --git a/src/smt/params/params2smt_params.h b/src/smt/params/params2smt_params.h deleted file mode 100644 index d4f60cb64..000000000 --- a/src/smt/params/params2smt_params.h +++ /dev/null @@ -1,31 +0,0 @@ -/*++ -Copyright (c) 2011 Microsoft Corporation - -Module Name: - - params2smt_params.h - -Abstract: - - Backward compatibility utilities for parameter setting - -Author: - - Leonardo de Moura (leonardo) 2011-05-19. - -Revision History: - ---*/ -#ifndef _PARAMS2SMT_PARAMS_H_ -#define _PARAMS2SMT_PARAMS_H_ - -class params_ref; -struct smt_params; - -void params2smt_params(params_ref const & s, smt_params & t); - -void smt_params2params(smt_params const & s, params_ref & t); - -void solver_smt_params_descrs(param_descrs & r); - -#endif diff --git a/src/smt/params/smt_params.cpp b/src/smt/params/smt_params.cpp index 113a2bead..22122cd83 100644 --- a/src/smt/params/smt_params.cpp +++ b/src/smt/params/smt_params.cpp @@ -51,6 +51,5 @@ void smt_params::updt_params(context_params const & p) { m_soft_timeout = p.m_timeout; m_model = p.m_model; m_model_validate = p.m_model_validate; - m_proof_mode = p.m_proof ? PGM_FINE : PGM_DISABLED; } diff --git a/src/smt/params/smt_params.h b/src/smt/params/smt_params.h index ec057239a..3d823cb51 100644 --- a/src/smt/params/smt_params.h +++ b/src/smt/params/smt_params.h @@ -207,7 +207,6 @@ struct smt_params : public preprocessor_params, bool m_at_labels_cex; // only use labels which contains the @ symbol when building multiple counterexamples. bool m_check_at_labels; // check that @ labels are inserted to generate unique counter-examples. bool m_dump_goal_as_smt; - proof_gen_mode m_proof_mode; bool m_auto_config; smt_params(params_ref const & p = params_ref()): @@ -277,7 +276,6 @@ struct smt_params : public preprocessor_params, m_at_labels_cex(false), m_check_at_labels(false), m_dump_goal_as_smt(false), - m_proof_mode(PGM_DISABLED), m_auto_config(true) { updt_local_params(p); } diff --git a/src/smt/smt_kernel.cpp b/src/smt/smt_kernel.cpp index 23687af8c..779c68625 100644 --- a/src/smt/smt_kernel.cpp +++ b/src/smt/smt_kernel.cpp @@ -19,7 +19,7 @@ Revision History: #include"smt_kernel.h" #include"smt_context.h" #include"ast_smt2_pp.h" -#include"params2smt_params.h" +#include"smt_params_helper.hpp" namespace smt { @@ -345,7 +345,7 @@ namespace smt { } void kernel::collect_param_descrs(param_descrs & d) { - solver_smt_params_descrs(d); + smt_params_helper::collect_param_descrs(d); } context & kernel::get_context() { diff --git a/src/smt/tactic/smt_tactic.cpp b/src/smt/tactic/smt_tactic.cpp index 20b6585e1..2c7d58b1a 100644 --- a/src/smt/tactic/smt_tactic.cpp +++ b/src/smt/tactic/smt_tactic.cpp @@ -20,7 +20,7 @@ Notes: #include"tactical.h" #include"smt_kernel.h" #include"smt_params.h" -#include"params2smt_params.h" +#include"smt_params_helper.hpp" #include"rewriter_types.h" class smt_tactic : public tactic { @@ -70,7 +70,7 @@ public: virtual void collect_param_descrs(param_descrs & r) { r.insert("candidate_models", CPK_BOOL, "(default: false) create candidate models even when quantifier or theory reasoning is incomplete."); r.insert("fail_if_inconclusive", CPK_BOOL, "(default: true) fail if found unsat (sat) for under (over) approximated goal."); - solver_smt_params_descrs(r); + smt_params_helper::collect_param_descrs(r); } virtual void set_cancel(bool f) {