eliminated m_proof_mode from smt_params, ast_manager has this information

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

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<iomanip>
 

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;

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;

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());

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) {

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<bool> fl1(params.m_nlquant_elim, true);
         flet<bool> fl2(params.m_nl_arith_gb, false);

src/smt/params/params2smt_params.cpp

@@ -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");
-}

src/smt/params/params2smt_params.h

@@ -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

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;
 }
 

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);
     }

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() {

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) {