From 4de58a42fe3fc6a975133947bf1f1ee7e2f334d0 Mon Sep 17 00:00:00 2001
From: Arie Gurfinkel <arie.gurfinkel@uwaterloo.ca>
Date: Mon, 21 May 2018 09:46:15 -0700
Subject: [PATCH] Update initialization order

---
 src/muz/spacer/spacer_context.cpp | 39 ++++++++++++++++++++++---------
 src/muz/spacer/spacer_context.h   | 10 +++++---
 2 files changed, 35 insertions(+), 14 deletions(-)

diff --git a/src/muz/spacer/spacer_context.cpp b/src/muz/spacer/spacer_context.cpp
index 9f54ac0d8..2baa70f46 100644
--- a/src/muz/spacer/spacer_context.cpp
+++ b/src/muz/spacer/spacer_context.cpp
@@ -1720,7 +1720,7 @@ void pred_transformer::add_premises(decl2rel const& pts, unsigned lvl, datalog::
     }
 }
 
-void pred_transformer::inherit_properties(pred_transformer& other)
+void pred_transformer::inherit_lemmas(pred_transformer& other)
 {m_frames.inherit_frames (other.m_frames);}
 
 app* pred_transformer::extend_initial (expr *e)
@@ -2091,24 +2091,37 @@ void context::init_rules(datalog::rule_set& rules, decl2rel& rels)
     for (auto &entry : rels) {entry.m_value->init_reach_facts();}
 }
 
-void context::inherit_properties(const decl2rel &rels) {
+void context::inherit_lemmas(const decl2rel &rels) {
     for (auto &entry : rels) {
         pred_transformer *pt = nullptr;
         if (m_rels.find(entry.m_key, pt)) {
-            entry.m_value->inherit_properties(*pt);
+            entry.m_value->inherit_lemmas(*pt);
         }
     }
 }
+
 void context::update_rules(datalog::rule_set& rules)
 {
     decl2rel rels;
-    init_lemma_generalizers(rules);
+    // SMT params must be set before any expression is asserted to any
+    // solver
+    init_global_smt_params();
+    // constructs new pred transformers and asserts trans and init
     init_rules(rules, rels);
-    inherit_properties(rels);
+    // inherits lemmas from m_rels into rels
+    inherit_lemmas(rels);
+    // switch context to new rels
+    init(rels);
+    // re-initialize lemma generalizers
+    init_lemma_generalizers();
+}
+
+void context::init(const decl2rel &rels) {
+    // reset context. Current state is all stored in rels
     reset();
-    for (auto &entry : rels) {
-        m_rels.insert(entry.m_key, entry.m_value);
-    }
+    // re-initialize context
+    for (auto &entry : rels)
+    {m_rels.insert(entry.m_key, entry.m_value);}
 }
 
 unsigned context::get_num_levels(func_decl* p)
@@ -2250,9 +2263,8 @@ void context::reset_lemma_generalizers()
     m_lemma_generalizers.reset();
 }
 
-void context::init_lemma_generalizers(datalog::rule_set& rules)
-{
-    reset_lemma_generalizers();
+// initialize global SMT parameters shared by all solvers
+void context::init_global_smt_params() {
     m.toggle_proof_mode(PGM_ENABLED);
     smt_params &fparams = m_pm.fparams ();
     if (!m_params.spacer_eq_prop ()) {
@@ -2282,6 +2294,11 @@ void context::init_lemma_generalizers(datalog::rule_set& rules)
         fparams.m_ng_lift_ite = LI_FULL;
     }
 
+}
+void context::init_lemma_generalizers()
+{
+    reset_lemma_generalizers();
+
     if (m_params.spacer_q3_use_qgen()) {
         m_lemma_generalizers.push_back(alloc(lemma_bool_inductive_generalizer,
                                              *this, 0, true));
diff --git a/src/muz/spacer/spacer_context.h b/src/muz/spacer/spacer_context.h
index db05df638..62d90e4c0 100644
--- a/src/muz/spacer/spacer_context.h
+++ b/src/muz/spacer/spacer_context.h
@@ -428,7 +428,7 @@ public:
 
     void add_premises(decl2rel const& pts, unsigned lvl, expr_ref_vector& r);
 
-    void inherit_properties(pred_transformer& other);
+    void inherit_lemmas(pred_transformer& other);
 
     void ground_free_vars(expr* e, app_ref_vector& vars, ptr_vector<app>& aux_vars,
                           bool is_init);
@@ -811,8 +811,9 @@ class context {
 
 
     // Initialization
-    void init_lemma_generalizers(datalog::rule_set& rules);
-    void inherit_properties(const decl2rel& rels);
+    void init_lemma_generalizers();
+    void inherit_lemmas(const decl2rel& rels);
+    void init_global_smt_params();
 
     bool check_invariant(unsigned lvl);
     bool check_invariant(unsigned lvl, func_decl* fn);
@@ -821,6 +822,9 @@ class context {
 
     void init_rules(datalog::rule_set& rules, decl2rel& transformers);
 
+    // (re)initialize context with new relations
+    void init(const decl2rel &rels);
+
     void simplify_formulas();
 
     void reset_lemma_generalizers();