From 5820b16800d91794a4ff3921986cb86585e5f7ba Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 18 Jul 2019 08:25:42 -0700
Subject: [PATCH] mark assumption literals to be skolem to hide them from
 models #2406

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/ast/ast.h                   | 10 ++++++++++
 src/cmd_context/cmd_context.cpp |  2 +-
 src/opt/opt_solver.cpp          |  5 +++++
 src/smt/theory_diff_logic_def.h |  9 +++++----
 4 files changed, 21 insertions(+), 5 deletions(-)

diff --git a/src/ast/ast.h b/src/ast/ast.h
index a551b8928..0a7d5aa6a 100644
--- a/src/ast/ast.h
+++ b/src/ast/ast.h
@@ -1820,6 +1820,12 @@ public:
                             arity, domain);
     }
 
+    func_decl * mk_skolem_const_decl(symbol const& name, sort* s) {
+        func_decl_info info;
+        info.set_skolem(true);
+        return mk_func_decl(name, static_cast<unsigned>(0), nullptr, s, info);
+    }
+
     func_decl * mk_const_decl(const char* name, sort * s) {
         return mk_func_decl(symbol(name), static_cast<unsigned>(0), nullptr, s);
     }
@@ -1898,6 +1904,10 @@ public:
         return mk_app(decl, static_cast<unsigned>(0), static_cast<expr**>(nullptr));
     }
 
+    app * mk_skolem_const(symbol const & name, sort * s) {
+        return mk_const(mk_skolem_const_decl(name, s));
+    }
+
     app * mk_const(symbol const & name, sort * s) {
         return mk_const(mk_const_decl(name, s));
     }
diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp
index 671f64df0..22c82c0c9 100644
--- a/src/cmd_context/cmd_context.cpp
+++ b/src/cmd_context/cmd_context.cpp
@@ -1364,7 +1364,7 @@ void cmd_context::assert_expr(symbol const & name, expr * t) {
     m_check_sat_result = nullptr;
     m().inc_ref(t);
     m_assertions.push_back(t);
-    expr * ans  = m().mk_const(name, m().mk_bool_sort());
+    app * ans  = m().mk_skolem_const(name, m().mk_bool_sort());
     m().inc_ref(ans);
     m_assertion_names.push_back(ans);
     if (m_solver)
diff --git a/src/opt/opt_solver.cpp b/src/opt/opt_solver.cpp
index eb766a1ba..e69ced63f 100644
--- a/src/opt/opt_solver.cpp
+++ b/src/opt/opt_solver.cpp
@@ -406,6 +406,11 @@ namespace opt {
             smt::theory_rdl& th = dynamic_cast<smt::theory_rdl&>(opt);
             return th.mk_ge(m_fm, v, val);
         }
+
+        if (typeid(smt::theory_rdl) == typeid(opt)) {
+            smt::theory_rdl& th = dynamic_cast<smt::theory_rdl&>(opt);
+            return th.mk_ge(m_fm, v, val);
+        }
         
         if (typeid(smt::theory_dense_i) == typeid(opt) &&
             val.get_infinitesimal().is_zero()) {
diff --git a/src/smt/theory_diff_logic_def.h b/src/smt/theory_diff_logic_def.h
index bcfb3e845..8808cb316 100644
--- a/src/smt/theory_diff_logic_def.h
+++ b/src/smt/theory_diff_logic_def.h
@@ -1118,8 +1118,8 @@ unsigned theory_diff_logic<Ext>::simplex2edge(unsigned e) {
 
 template<typename Ext> 
 void theory_diff_logic<Ext>::update_simplex(Simplex& S) {
-    unsynch_mpq_manager mgr;
     unsynch_mpq_inf_manager inf_mgr;
+    unsynch_mpq_manager& mgr = inf_mgr.get_mpq_manager();
     unsigned num_nodes = m_graph.get_num_nodes();
     vector<dl_edge<GExt> > const& es = m_graph.get_all_edges();
     S.ensure_var(num_simplex_vars());
@@ -1127,7 +1127,8 @@ void theory_diff_logic<Ext>::update_simplex(Simplex& S) {
         numeral const& a = m_graph.get_assignment(i);
         rational fin = a.get_rational().to_rational();
         rational inf = a.get_infinitesimal().to_rational();
-        mpq_inf q(mgr.dup(fin.to_mpq()), mgr.dup(inf.to_mpq()));
+        mpq_inf q;
+        inf_mgr.set(q, fin.to_mpq(), inf.to_mpq());
         S.set_value(node2simplex(i), q);
         inf_mgr.del(q);
     }
@@ -1158,7 +1159,8 @@ void theory_diff_logic<Ext>::update_simplex(Simplex& S) {
             numeral const& w = e.get_weight();
             rational fin = w.get_rational().to_rational();
             rational inf = w.get_infinitesimal().to_rational();
-            mpq_inf q(mgr.dup(fin.to_mpq()), mgr.dup(inf.to_mpq()));
+            mpq_inf q;
+            inf_mgr.set(q, fin.to_mpq(), inf.to_mpq());
             S.set_upper(base_var, q);
             inf_mgr.del(q);
         }
@@ -1314,7 +1316,6 @@ expr_ref theory_diff_logic<Ext>::mk_ineq(theory_var v, inf_eps const& val, bool
         if (is_strict) {
             f = m.mk_not(f);
         }
-        TRACE("arith", tout << "block: " << f << "\n";);
         return f;
     }