experimenting with inc-sat

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

src/opt/weighted_maxsat.cpp

@@ -27,6 +27,7 @@ Notes:
 #include "pb_decl_plugin.h"
 #include "uint_set.h"
 #include "pb_preprocess_tactic.h"
+#include "aig_tactic.h"
 #include "simplify_tactic.h"
 #include "tactical.h"
 #include "tactic.h"
@@ -34,6 +35,7 @@ Notes:
 #include "pb_sls.h"
 #include "qfbv_tactic.h"
 #include "card2bv_tactic.h"
+#include "bit_blaster_tactic.h"
 #include "tactic2solver.h"
 #include "nnf_tactic.h"
 #include "opt_sls_solver.h"
@@ -54,13 +56,19 @@ namespace opt {
         model_converter_ref m_mc;   
         tactic_ref      m_preprocess;
         statistics      m_stats;
+        app_ref         m_soft;
     public:
-        inc_sat_solver(ast_manager& m, params_ref const& p):
+        inc_sat_solver(ast_manager& m, params_ref const& p, expr_ref_vector const& soft):
             m(m), m_solver(p,0), m_params(p),
-            m_fmls(m), m_map(m) {
+            m_fmls(m), m_map(m), m_soft(m) {
             tactic_ref pb2bv = mk_card2bv_tactic(m, m_params);
-            tactic_ref bv2sat = mk_qfbv_tactic(m, p, mk_skip_tactic(), mk_fail_tactic());
+            tactic_ref preamble_st = mk_qfbv_preamble(m, m_params);
-            m_preprocess = and_then(pb2bv.get(), bv2sat.get());
+            m_preprocess = and_then(pb2bv.get(), preamble_st.get(), mk_bit_blaster_tactic(m), mk_aig_tactic());
+            
+            ptr_vector<sort> sorts;
+            sorts.resize(soft.size(), m.mk_bool_sort());
+            func_decl_ref fn(m.mk_func_decl(symbol("Soft"), sorts.size(), sorts.c_ptr(), m.mk_bool_sort()), m);
+            m_soft = m.mk_app(fn, soft.size(), soft.c_ptr());
         }
 
         virtual ~inc_sat_solver() {}
@@ -81,12 +89,15 @@ namespace opt {
                 for (unsigned i = 0; i < m_fmls.size(); ++i) {
                     g->assert_expr(m_fmls[i].get());
                 }
+                g->assert_expr(m_soft);
+                TRACE("opt", g->display(tout););
                 m_fmls.reset();
-                try {
+                try {                   
                     (*m_preprocess)(g, result, mc, pc, core);
+                    TRACE("opt", result[0]->display(tout););
                 }
-                catch (tactic_exception &) {
+                catch (tactic_exception & ex) {
-                    IF_VERBOSE(0, verbose_stream() << "exception in tactic\n";);
+                    IF_VERBOSE(0, verbose_stream() << "exception in tactic " << ex.msg() << "\n";);
                     m_preprocess->collect_statistics(m_stats);
                     return l_undef;                    
                 }
@@ -96,7 +107,15 @@ namespace opt {
                     IF_VERBOSE(0, verbose_stream() << "size of result is not 1, it is: " << result.size() << "\n";);
                     return l_undef;
                 }
-                m_goal2sat(*result[0], m_params, m_solver, m_map);
+                g = result[0];
+                for (unsigned i = 0; i < g->size(); ++i) {
+                    expr* f = g->form(i);
+                    if (is_app_of(f, m_soft->get_decl())) {
+                        g->update(i, m.mk_true());
+                    }
+                }
+                TRACE("opt", g->display(tout););
+                m_goal2sat(*g, m_params, m_solver, m_map);
             }
             
             lbool r = m_solver.check();
@@ -312,7 +331,7 @@ namespace opt {
                 tactic_ref tac = and_then(pb2bv.get(), bv2sat.get());
                 solver* sat_solver = mk_tactic2solver(m, tac.get(), m_params);
 #else
-                solver* sat_solver = alloc(inc_sat_solver, m, m_params);
+                solver* sat_solver = alloc(inc_sat_solver, m, m_params, m_soft);
 #endif
                 unsigned sz = s().get_num_assertions();
                 for (unsigned i = 0; i < sz; ++i) {

src/tactic/smtlogics/qfbv_tactic.cpp

@@ -31,7 +31,7 @@ Notes:
 
 #define MEMLIMIT 300
 
-static tactic * mk_qfbv_preamble(ast_manager& m, params_ref const& p) {
+tactic * mk_qfbv_preamble(ast_manager& m, params_ref const& p) {
 
     params_ref solve_eq_p;
     // conservative guassian elimination. 
@@ -53,16 +53,18 @@ static tactic * mk_qfbv_preamble(ast_manager& m, params_ref const& p) {
 
     return
         and_then(
-            and_then(mk_simplify_tactic(m),
+            mk_simplify_tactic(m),
-                     mk_propagate_values_tactic(m),
+            mk_propagate_values_tactic(m),
-                     using_params(mk_solve_eqs_tactic(m), solve_eq_p),
+            using_params(mk_solve_eqs_tactic(m), solve_eq_p),
-                     mk_elim_uncnstr_tactic(m),
+            mk_elim_uncnstr_tactic(m),
-                     if_no_proofs(if_no_unsat_cores(mk_bv_size_reduction_tactic(m))),
+            if_no_proofs(if_no_unsat_cores(mk_bv_size_reduction_tactic(m))),
-                     using_params(mk_simplify_tactic(m), simp2_p)),
+            using_params(mk_simplify_tactic(m), simp2_p),
+            //
             // Z3 can solve a couple of extra benchmarks by using hoist_mul
             // but the timeout in SMT-COMP is too small. 
             // Moreover, it impacted negatively some easy benchmarks.
             // We should decide later, if we keep it or not.
+            //
             using_params(mk_simplify_tactic(m), hoist_p),
             mk_max_bv_sharing_tactic(m));
 }

src/tactic/smtlogics/qfbv_tactic.h

@@ -29,6 +29,8 @@ tactic * mk_qfbv_tactic(ast_manager & m, params_ref const & p = params_ref());
   ADD_TACTIC("qfbv",  "builtin strategy for solving QF_BV problems.", "mk_qfbv_tactic(m, p)")
 */
 
+tactic * mk_qfbv_preamble(ast_manager& m, params_ref const& p);
+
 tactic * mk_qfbv_tactic(ast_manager & m, params_ref const & p, tactic* sat, tactic* smt);
 
 #endif