fix #3733 persist uninterpreted atoms across calls to incremental sat solver

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

src/math/lp/factorization.h

@@ -11,8 +11,8 @@
   <abstract>
 
   Author:
-  Nikolaj Bjorner (nbjorner)
   Lev Nachmanson (levnach)
+  Nikolaj Bjorner (nbjorner)
 
   Revision History:
 

src/math/lp/lar_constraints.h

@@ -25,11 +25,11 @@ Revision History:
 
 #include "util/vector.h"
 #include "util/region.h"
+#include "util/stacked_value.h"
 #include "math/lp/lp_utils.h"
 #include "math/lp/ul_pair.h"
 #include "math/lp/lar_term.h"
 #include "math/lp/column_namer.h"
-#include "math/lp/stacked_value.h"
 namespace lp {
 inline lconstraint_kind flip_kind(lconstraint_kind t) {
     return static_cast<lconstraint_kind>( - static_cast<int>(t));

src/math/lp/lar_core_solver.h

@@ -29,7 +29,7 @@ Revision History:
 #include "math/lp/lp_primal_core_solver.h"
 #include "math/lp/stacked_vector.h"
 #include "math/lp/lar_solution_signature.h"
-#include "math/lp/stacked_value.h"
+#include "util/stacked_value.h"
 namespace lp {
 
 class lar_core_solver  {

src/math/lp/lar_solver.h

@@ -34,7 +34,7 @@ Revision History:
 #include "math/lp/scaler.h"
 #include "math/lp/lp_primal_core_solver.h"
 #include "math/lp/random_updater.h"
-#include "math/lp/stacked_value.h"
+#include "util/stacked_value.h"
 #include "math/lp/stacked_vector.h"
 #include "math/lp/implied_bound.h"
 #include "math/lp/bound_analyzer_on_row.h"

src/sat/sat_solver/inc_sat_solver.cpp

@@ -19,6 +19,7 @@ Notes:
 
 
 #include "util/gparams.h"
+#include "util/stacked_value.h"
 #include "ast/ast_pp.h"
 #include "ast/ast_translation.h"
 #include "ast/ast_util.h"
@@ -47,6 +48,7 @@ Notes:
 class inc_sat_solver : public solver {
     ast_manager&    m;
     mutable sat::solver     m_solver;
+    stacked_value<bool> m_has_uninterpreted;
     goal2sat        m_goal2sat;
     params_ref      m_params;
     expr_ref_vector m_fmls;
@@ -83,6 +85,7 @@ public:
     inc_sat_solver(ast_manager& m, params_ref const& p, bool incremental_mode):
         m(m), 
         m_solver(p, m.limit()),
+        m_has_uninterpreted(false),
         m_fmls(m),
         m_asmsf(m),
         m_fmls_head(0),
@@ -128,6 +131,7 @@ public:
         for (expr* f : m_internalized_fmls) result->m_internalized_fmls.push_back(tr(f));
         if (m_mcs.back()) result->m_mcs.push_back(m_mcs.back()->translate(tr));
         if (m_sat_mc) result->m_sat_mc = dynamic_cast<sat2goal::mc*>(m_sat_mc->translate(tr));
+        result->m_has_uninterpreted = m_has_uninterpreted;
         // copy m_bb_rewriter?
         result->m_internalized_converted = m_internalized_converted;
         return result;
@@ -208,7 +212,11 @@ public:
         }
         switch (r) {
         case l_true:
-            if (sz > 0) {
+            if (m_has_uninterpreted()) {
+                set_reason_unknown("(sat.giveup has-uninterpreted)");
+                r = l_undef;
+            }
+            else if (sz > 0) {
                 check_assumptions(dep2asm);
             }
             break;
@@ -247,6 +255,7 @@ public:
         m_fmls_head_lim.push_back(m_fmls_head);
         if (m_bb_rewriter) m_bb_rewriter->push();
         m_map.push();
+        m_has_uninterpreted.push();
     }
 
     void pop(unsigned n) override {
@@ -260,6 +269,7 @@ public:
         m_solver.user_pop(n);
         m_num_scopes -= n;
         // ? m_internalized_converted = false;
+        m_has_uninterpreted.pop(n);
         while (n > 0) {
             m_mcs.pop_back();
             m_fmls_head = m_fmls_head_lim.back();
@@ -640,8 +650,9 @@ private:
         if (!m_sat_mc) m_sat_mc = alloc(sat2goal::mc, m);
         m_sat_mc->flush_smc(m_solver, m_map);
         if (!atoms.empty()) {
+            m_has_uninterpreted = true;
             std::stringstream strm;
-            strm << "interpreted atoms sent to SAT solver " << atoms;
+            strm << "(sat.giveup interpreted atoms sent to SAT solver " << atoms <<")";
             TRACE("sat", tout << strm.str() << "\n";);
             IF_VERBOSE(1, verbose_stream() << strm.str() << "\n";);
             set_reason_unknown(strm.str().c_str());

src/util/stacked_value.h

@@ -21,11 +21,12 @@ Revision History:
 #pragma once
 // add to value the stack semantics
 #include <stack>
-namespace lp {
 template <typename T> class stacked_value {
     T m_value;    
     std::stack<T> m_stack;
 public:
+
+
     void push() {
         m_stack.push(m_value);
     }
@@ -63,6 +64,12 @@ public:
         return m_value;
     }
 
+    stacked_value& operator=(stacked_value const& other) {
+        m_value = other.m_value;
+        m_stack = other.m_stack;
+        return *this;
+    }
+
     operator T&() {
         return m_value;
     }
@@ -81,4 +88,3 @@ public:
 
 
 };
-}