From c1a6163bda4fc7c84d5579eb2b0a3c8415784272 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 20 Nov 2015 14:34:31 -0800
Subject: [PATCH] disable aig tactic in inc_sat_solver (it can blow up the size
 of formulas significantly without sharing) and fix configuration update bug
 for optimization context exposed in example by Corina

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/cmd_context/cmd_context.cpp       | 3 +++
 src/cmd_context/cmd_context.h         | 1 +
 src/opt/opt_context.h                 | 2 +-
 src/sat/sat_solver/inc_sat_solver.cpp | 4 +++-
 4 files changed, 8 insertions(+), 2 deletions(-)

diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp
index 6e443d476..4fa7b88bf 100644
--- a/src/cmd_context/cmd_context.cpp
+++ b/src/cmd_context/cmd_context.cpp
@@ -383,6 +383,9 @@ void cmd_context::global_params_updated() {
             p.set_bool("auto_config", false);
         m_solver->updt_params(p);
     }
+    if (m_opt) {
+        get_opt()->updt_params(gparams::get_module("opt"));
+    }
 }
 
 void cmd_context::set_produce_models(bool f) {
diff --git a/src/cmd_context/cmd_context.h b/src/cmd_context/cmd_context.h
index 516b47e3c..f3fe5078e 100644
--- a/src/cmd_context/cmd_context.h
+++ b/src/cmd_context/cmd_context.h
@@ -125,6 +125,7 @@ public:
     virtual bool is_pareto() = 0;
     virtual void set_logic(symbol const& s) = 0;
     virtual bool print_model() const = 0;
+    virtual void updt_params(params_ref& p) = 0;
 };
 
 class cmd_context : public progress_callback, public tactic_manager, public ast_printer_context {
diff --git a/src/opt/opt_context.h b/src/opt/opt_context.h
index 946c2a5a3..ff3be1cd2 100644
--- a/src/opt/opt_context.h
+++ b/src/opt/opt_context.h
@@ -195,7 +195,7 @@ namespace opt {
 
         void display(std::ostream& out);
         static void collect_param_descrs(param_descrs & r);
-        void updt_params(params_ref& p);
+        virtual void updt_params(params_ref& p);
         params_ref& get_params() { return m_params; }
 
         expr_ref get_lower(unsigned idx);
diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp
index 43b2c2e3f..3f2700053 100644
--- a/src/sat/sat_solver/inc_sat_solver.cpp
+++ b/src/sat/sat_solver/inc_sat_solver.cpp
@@ -84,12 +84,14 @@ public:
         simp2_p.set_uint("local_ctx_limit", 10000000);
         simp2_p.set_bool("flat", true); // required by som
         simp2_p.set_bool("hoist_mul", false); // required by som
+        simp2_p.set_bool("elim_and", true);
+
         m_preprocess = 
             and_then(mk_card2bv_tactic(m, m_params),
                      using_params(mk_simplify_tactic(m), simp2_p),
                      mk_max_bv_sharing_tactic(m),
                      mk_bit_blaster_tactic(m, &m_bb_rewriter), 
-                     mk_aig_tactic(),
+                     //mk_aig_tactic(),
                      using_params(mk_simplify_tactic(m), simp2_p));               
     }