From 552cbd840fdd76e7cfa4323438eb5e942c63b8aa Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 23 Jan 2015 13:06:11 -0800
Subject: [PATCH] adding soft-assertions

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/opt/maxsmt.cpp      |  4 ++++
 src/opt/maxsmt.h        |  1 +
 src/opt/opt_context.cpp |  7 +++++++
 src/opt/opt_context.h   |  1 +
 src/sat/sat_config.cpp  |  1 +
 src/sat/sat_config.h    |  1 +
 src/sat/sat_params.pyg  |  1 +
 src/sat/sat_solver.cpp  | 19 ++++++++++++++-----
 8 files changed, 30 insertions(+), 5 deletions(-)

diff --git a/src/opt/maxsmt.cpp b/src/opt/maxsmt.cpp
index b1bf015f9..48d7e48bd 100644
--- a/src/opt/maxsmt.cpp
+++ b/src/opt/maxsmt.cpp
@@ -105,6 +105,10 @@ namespace opt {
         m_c.set_enable_sls(f);
     }
 
+    void maxsmt_solver_base::set_soft_assumptions() {
+        m_c.set_soft_assumptions()
+    }
+
     app* maxsmt_solver_base::mk_fresh_bool(char const* name) {
         app* result = m.mk_fresh_const(name, m.mk_bool_sort());
         m_c.fm().insert(result->get_decl());
diff --git a/src/opt/maxsmt.h b/src/opt/maxsmt.h
index 6a19a223b..356a2d50b 100644
--- a/src/opt/maxsmt.h
+++ b/src/opt/maxsmt.h
@@ -102,6 +102,7 @@ namespace opt {
     protected:
         void enable_sls(expr_ref_vector const& soft, weights_t& ws);
         void set_enable_sls(bool f);
+        void set_soft_assumptions();
         void trace_bounds(char const* solver);
 
     };
diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp
index 5cd2e1c1e..028cb4414 100644
--- a/src/opt/opt_context.cpp
+++ b/src/opt/opt_context.cpp
@@ -493,6 +493,13 @@ namespace opt {
         }
     }
 
+    void context::set_soft_assumptions() {
+        if (m_sat_solver.get()) {
+            m_params.set_bool("soft_assumptions", true);
+            m_sat_solver->updt_params(m_params);
+        }
+    }
+
     void context::enable_sls(expr_ref_vector const& soft, vector<rational> const& weights) {
         SASSERT(soft.size() == weights.size());
         if (m_sat_solver.get()) {
diff --git a/src/opt/opt_context.h b/src/opt/opt_context.h
index 3d29c8fee..ee4ce467a 100644
--- a/src/opt/opt_context.h
+++ b/src/opt/opt_context.h
@@ -184,6 +184,7 @@ namespace opt {
         params_ref& params() { return m_params; }
         void enable_sls(expr_ref_vector const& soft, weights_t& weights);
         void set_enable_sls(bool f) { m_enable_sls = f; }
+        void set_soft_assumptions();
         symbol const& maxsat_engine() const { return m_maxsat_engine; }
         void get_base_model(model_ref& m);
 
diff --git a/src/sat/sat_config.cpp b/src/sat/sat_config.cpp
index aff023b22..0c100aff2 100644
--- a/src/sat/sat_config.cpp
+++ b/src/sat/sat_config.cpp
@@ -110,6 +110,7 @@ namespace sat {
         m_minimize_core   = p.minimize_core();
         m_minimize_core_partial   = p.minimize_core_partial();
         m_optimize_model  = p.optimize_model();
+        m_soft_assumptions = p.soft_assumptions();
         m_bcd             = p.bcd();
         m_dyn_sub_res     = p.dyn_sub_res();
     }
diff --git a/src/sat/sat_config.h b/src/sat/sat_config.h
index 61ab71605..29ef25f03 100644
--- a/src/sat/sat_config.h
+++ b/src/sat/sat_config.h
@@ -72,6 +72,7 @@ namespace sat {
         bool               m_minimize_core;
         bool               m_minimize_core_partial;
         bool               m_optimize_model;
+        bool               m_soft_assumptions;
         bool               m_bcd;
 
 
diff --git a/src/sat/sat_params.pyg b/src/sat/sat_params.pyg
index c5ac97b4e..ed4f4910a 100644
--- a/src/sat/sat_params.pyg
+++ b/src/sat/sat_params.pyg
@@ -22,5 +22,6 @@ def_module_params('sat',
                           ('minimize_core', BOOL, False, 'minimize computed core'),
                           ('minimize_core_partial', BOOL, False, 'apply partial (cheap) core minimization'),
                           ('optimize_model', BOOL, False, 'enable optimization of soft constraints'),
+                          ('soft_assumptions', BOOL, False, 'disable assumptions that are forced during unit propagation'),
                           ('bcd', BOOL, False, 'enable blocked clause decomposition for equality extraction'),
                           ('dimacs.core', BOOL, False, 'extract core from DIMACS benchmarks')))
diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp
index 817fb2c23..1915f363f 100644
--- a/src/sat/sat_solver.cpp
+++ b/src/sat/sat_solver.cpp
@@ -914,17 +914,26 @@ namespace sat {
 
         for (unsigned i = 0; !inconsistent() && i < m_user_scope_literals.size(); ++i) {
             literal nlit = ~m_user_scope_literals[i];
-            assign(nlit, justification());       
-            //        propagate(false);         
+            assign(nlit, justification());                   
         }
 
         for (unsigned i = 0; !inconsistent() && i < num_lits; ++i) {
             literal lit = lits[i];
             SASSERT(is_external((lit).var()));  
             m_assumption_set.insert(lit);       
-            m_assumptions.push_back(lit);       
-            assign(lit, justification());       
-            //        propagate(false);         
+
+            if (m_config.soft_assumptions) {
+                if (value(lit) == l_undef) {
+                    m_assumptions.push_back(lit);       
+                    assign(lit, justification());
+                }
+                propagate(false);         
+            }
+            else {
+                m_assumptions.push_back(lit);       
+                assign(lit, justification());       
+                //        propagate(false);         
+            }
         }
     }