From 9f6a733ff6a9be7668d0177be9be50d34444cc06 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 29 Apr 2020 12:06:53 -0700
Subject: [PATCH] add hook for induction

---
 src/smt/smt_context.cpp   | 24 +++++++++++++++---------
 src/smt/smt_context.h     |  6 +++++-
 src/smt/smt_induction.cpp |  1 -
 3 files changed, 20 insertions(+), 11 deletions(-)

diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp
index 9d8a81a8442..ee4d9e6da8f 100644
--- a/src/smt/smt_context.cpp
+++ b/src/smt/smt_context.cpp
@@ -270,18 +270,14 @@ namespace smt {
         }
         d.m_phase_available        = true;
         d.m_phase                  = !l.sign();
-        CTRACE("assign_core", l.var() == 13, tout << (decision?"decision: ":"propagating: ") << l << " ";
-               /*display_literal(tout, l);*/
-               tout << "relevant: " << is_relevant_core(l) << " level: " << m_scope_lvl << " is atom " << d.is_atom() << "\n";
-               /*display(tout, j);*/
-               );
+        TRACE("assign_core", tout << (decision?"decision: ":"propagating: ") << l << " ";
+              display_literal_smt2(tout, l) << "\n";
+              tout << "relevant: " << is_relevant_core(l) << " level: " << m_scope_lvl << " is atom " << d.is_atom() << "\n";
+              /*display(tout, j);*/
+              );
         TRACE("phase_selection", tout << "saving phase, is_pos: " << d.m_phase << " l: " << l << "\n";);
 
-        CTRACE("relevancy", l.var() == 13,
-              tout << "is_atom: " << d.is_atom() << " is relevant: " 
-              << is_relevant_core(l) << " relevancy-lvl: " << relevancy_lvl() << "\n";);
         if (d.is_atom() && (relevancy_lvl() == 0 || (relevancy_lvl() == 1 && !d.is_quantifier()) || is_relevant_core(l))) {
-            CTRACE("assign_core", l.var() == 13, tout << "propagation queue\n";);
             m_atom_propagation_queue.push_back(l);
         }
 
@@ -1655,6 +1651,16 @@ namespace smt {
             !m_th_diseq_propagation_queue.empty();
     }
 
+    /**
+       \brief retrieve facilities for creating induction lemmas.
+     */
+    induction& context::get_induction() {
+        if (!m_induction) {
+            m_induction = alloc(induction, *this, get_manager());
+        }
+        return *m_induction;
+    }
+
     /**
        \brief unit propagation.
        Cancelation is not safe during propagation at base level because
diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h
index 625ed92ac61..13439e883a8 100644
--- a/src/smt/smt_context.h
+++ b/src/smt/smt_context.h
@@ -34,6 +34,7 @@ Revision History:
 #include "smt/smt_statistics.h"
 #include "smt/smt_conflict_resolution.h"
 #include "smt/smt_relevancy.h"
+#include "smt/smt_induction.h"
 #include "smt/smt_case_split_queue.h"
 #include "smt/smt_almost_cg_table.h"
 #include "smt/smt_failure.h"
@@ -185,6 +186,7 @@ namespace smt {
         unsigned                    m_simp_qhead;
         int                         m_simp_counter; //!< can become negative
         scoped_ptr<case_split_queue> m_case_split_queue;
+        scoped_ptr<induction>       m_induction;
         double                      m_bvar_inc;
         bool                        m_phase_cache_on;
         unsigned                    m_phase_counter; //!< auxiliary variable used to decide when to turn on/off phase caching
@@ -848,7 +850,7 @@ namespace smt {
         void remove_lit_occs(clause const& cls, unsigned num_bool_vars);
 
         void add_lit_occs(clause const& cls);
-    public:
+    public:        
 
         void ensure_internalized(expr* e);
 
@@ -1267,6 +1269,8 @@ namespace smt {
     public:
         bool can_propagate() const;
 
+        induction& get_induction(); 
+
         // Retrieve arithmetic values. 
         bool get_arith_lo(expr* e, rational& lo, bool& strict);
         bool get_arith_up(expr* e, rational& up, bool& strict);
diff --git a/src/smt/smt_induction.cpp b/src/smt/smt_induction.cpp
index 5bbc0094894..3793f4d9f4a 100644
--- a/src/smt/smt_induction.cpp
+++ b/src/smt/smt_induction.cpp
@@ -240,7 +240,6 @@ void create_induction_lemmas::create_lemmas(expr* t, expr* sk, abstraction& a, l
     sort* s = m.get_sort(sk);
     if (!m_dt.is_datatype(s))
         return;
-    family_id fid = s->get_family_id();
     expr_ref alpha = a.m_term;
     auto const& eqs = a.m_eqs;
     literal_vector common_literals;