add tracking for reason unknown

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

src/sat/sat_simplifier.cpp

@@ -233,11 +233,6 @@ namespace sat {
         CASSERT("sat_solver", s.check_invariant());
         TRACE("after_simplifier", s.display(tout); tout << "model_converter:\n"; s.m_mc.display(tout););
 
-        if (!learned) {
-            // perform lookahead simplification
-            lookahead(s).simplify();
-        }
-
         finalize();
 
     }

src/sat/sat_solver.cpp

@@ -57,6 +57,7 @@ namespace sat {
         m_scope_lvl(0),
         m_search_lvl(0),
         m_params(p) {
+        init_reason_unknown();
         updt_params(p);
         m_conflicts_since_gc      = 0;
         m_conflicts               = 0;
@@ -826,6 +827,7 @@ namespace sat {
     //
     // -----------------------
     lbool solver::check(unsigned num_lits, literal const* lits) {
+        init_reason_unknown();
         pop_to_base_level();
         IF_VERBOSE(2, verbose_stream() << "(sat.sat-solver)\n";);
         SASSERT(at_base_lvl());
@@ -872,6 +874,7 @@ namespace sat {
             if (check_inconsistent()) return l_false;
 
             if (m_config.m_max_conflicts == 0) {
+                m_reason_unknown = "sat.max.conflicts";
                 IF_VERBOSE(SAT_VB_LVL, verbose_stream() << "(sat \"abort: max-conflicts = 0\")\n";);
                 return l_undef;
             }
@@ -884,6 +887,7 @@ namespace sat {
                     return r;
 
                 if (m_conflicts > m_config.m_max_conflicts) {
+                    m_reason_unknown = "sat.max.conflicts";
                     IF_VERBOSE(SAT_VB_LVL, verbose_stream() << "(sat \"abort: max-conflicts = " << m_conflicts << "\")\n";);
                     return l_undef;
                 }
@@ -894,6 +898,7 @@ namespace sat {
                 gc();
 
                 if (m_config.m_restart_max <= m_restarts) {
+                    m_reason_unknown = "sat.max.restarts";
                     IF_VERBOSE(SAT_VB_LVL, verbose_stream() << "(sat \"abort: max-restarts\")\n";);
                     return l_undef;
                 }
@@ -901,6 +906,7 @@ namespace sat {
             }
         }
         catch (abort_solver) {
+            m_reason_unknown = "sat.giveup";
             return l_undef;
         }
     }

src/sat/sat_solver.h

@@ -132,6 +132,8 @@ namespace sat {
         unsigned                m_search_lvl;
         literal_vector          m_trail;
         clause_wrapper_vector   m_clauses_to_reinit;
+        std::string             m_reason_unknown;
+
         struct scope {
             unsigned m_trail_lim;
             unsigned m_clauses_to_reinit_lim;
@@ -351,6 +353,7 @@ namespace sat {
         literal_vector const& get_core() const { return m_core; }
         model_converter const & get_model_converter() const { return m_mc; }
         void set_model(model const& mdl);
+        char const* get_reason_unknown() const { return m_reason_unknown.c_str(); }
 
         literal select_lookahead(bool_var_vector const& vars);
 
@@ -374,6 +377,7 @@ namespace sat {
         
         literal_vector m_min_core;
         bool           m_min_core_valid;
+        void init_reason_unknown() { m_reason_unknown = "no reason given"; }
         void init_assumptions(unsigned num_lits, literal const* lits);
         void reassert_min_core();
         void update_min_core();

src/sat/sat_solver/inc_sat_solver.cpp

@@ -151,6 +151,7 @@ public:
         m_internalized = true;
         m_internalized_converted = false;
 
+        init_reason_unknown();
         r = m_solver.check(m_asms.size(), m_asms.c_ptr());
         
         switch (r) {
@@ -166,6 +167,7 @@ public:
             }
             break;
         default:
+            set_reason_unknown(m_solver.get_reason_unknown());
             break;
         }
         return r;
@@ -345,7 +347,9 @@ public:
         return l_true;
     }
 
-
+    void init_reason_unknown() {
+        m_unknown = "no reason given";
+    }
     virtual std::string reason_unknown() const {
         return m_unknown;
     }