fix bound bug #991

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

src/sat/sat_solver.cpp

@@ -3141,6 +3141,101 @@ namespace sat {
     //
     // -----------------------
 
+static void prune_unfixed(sat::literal_vector& lambda, sat::model const& m) {
+    for (unsigned i = 0; i < lambda.size(); ++i) {
+        if ((m[lambda[i].var()] == l_false) != lambda[i].sign()) {
+            lambda[i] = lambda.back();
+            lambda.pop_back();
+            --i;
+        }
+    }
+}
+
+// Algorithm 7: Corebased Algorithm with Chunking
+
+static void back_remove(sat::literal_vector& lits, sat::literal l) {
+    for (unsigned i = lits.size(); i > 0; ) {
+        --i;
+        if (lits[i] == l) {
+            lits[i] = lits.back();
+            lits.pop_back();
+            return;
+        }
+    }
+    std::cout << "UNREACHABLE\n";
+}
+
+    static void brute_force_consequences(sat::solver& s, sat::literal_vector const& asms, sat::literal_vector const& gamma, vector<sat::literal_vector>& conseq) {
+    for (unsigned i = 0; i < gamma.size(); ++i) {
+        sat::literal nlit = ~gamma[i];
+        sat::literal_vector asms1(asms);
+        asms1.push_back(nlit);
+        lbool r = s.check(asms1.size(), asms1.c_ptr());
+        if (r == l_false) {
+            conseq.push_back(s.get_core());
+        }
+    }
+}
+
+    static lbool core_chunking(sat::solver& s, model const& m, sat::bool_var_vector const& vars, sat::literal_vector const& asms, vector<sat::literal_vector>& conseq, unsigned K) {
+        sat::literal_vector lambda;
+        for (unsigned i = 0; i < vars.size(); i++) {
+            lambda.push_back(sat::literal(i, m[vars[i]] == l_false));
+        }
+        while (!lambda.empty()) {
+            IF_VERBOSE(1, verbose_stream() << "(sat-backbone-core " << lambda.size() << " " << conseq.size() << ")\n";);
+            unsigned k = std::min(K, lambda.size());
+            sat::literal_vector gamma, omegaN;
+            for (unsigned i = 0; i < k; ++i) {
+                sat::literal l = lambda[lambda.size() - i - 1];
+                gamma.push_back(l);
+                omegaN.push_back(~l);
+            }
+            while (true) {
+                sat::literal_vector asms1(asms);
+                asms1.append(omegaN);
+                lbool r = s.check(asms1.size(), asms1.c_ptr());
+                if (r == l_true) {
+                    IF_VERBOSE(1, verbose_stream() << "(sat) " << omegaN << "\n";);
+                    prune_unfixed(lambda, s.get_model());
+                    break;
+                }
+                sat::literal_vector const& core = s.get_core();
+                sat::literal_vector occurs;
+                IF_VERBOSE(1, verbose_stream() << "(core " << core.size() << ")\n";);
+                for (unsigned i = 0; i < omegaN.size(); ++i) {
+                    if (core.contains(omegaN[i])) {
+                        occurs.push_back(omegaN[i]);
+                    }
+                }
+                if (occurs.size() == 1) {
+                    sat::literal lit = occurs.back();
+                    sat::literal nlit = ~lit;
+                    conseq.push_back(core);
+                    back_remove(lambda, ~lit);
+                    back_remove(gamma, ~lit);
+                    s.mk_clause(1, &nlit);
+                }
+                for (unsigned i = 0; i < omegaN.size(); ++i) {
+                    if (occurs.contains(omegaN[i])) {
+                        omegaN[i] = omegaN.back();
+                        omegaN.pop_back();
+                        --i;
+                    }
+                }
+                if (omegaN.empty() && occurs.size() > 1) {
+                    brute_force_consequences(s, asms, gamma, conseq);
+                    for (unsigned i = 0; i < gamma.size(); ++i) {
+                        back_remove(lambda, gamma[i]);
+                    }
+                    break;
+                }
+            }
+        }
+        return l_true;
+    }
+
+
     lbool solver::get_consequences(literal_vector const& asms, bool_var_vector const& vars, vector<literal_vector>& conseq) {
         literal_vector lits;
         lbool is_sat = l_true;
@@ -3163,6 +3258,9 @@ namespace sat {
             default: break;
             }
         }
+
+        // is_sat = core_chunking(*this, mdl, vars, asms, conseq, 100);
+
         is_sat = get_consequences(asms, lits, conseq);
         set_model(mdl);
         return is_sat;
@@ -3307,7 +3405,7 @@ namespace sat {
                     propagate(false);
                     ++num_resolves;
                 }
-                if (scope_lvl() == 1) {
+                if (false && scope_lvl() == 1) {
                     break;
                 }
             }

src/smt/theory_arith.h

@@ -552,6 +552,7 @@ namespace smt {
         bool is_int(theory_var v) const { return m_data[v].m_is_int; }
         bool is_int_src(theory_var v) const { return m_util.is_int(var2expr(v)); }
         bool is_real(theory_var v) const { return !is_int(v); }
+        bool is_real_src(theory_var v) const { return !is_int_src(v); }
         bool get_implied_old_value(theory_var v, inf_numeral & r) const;
         inf_numeral const & get_implied_value(theory_var v) const;
         inf_numeral const & get_quasi_base_value(theory_var v) const { return get_implied_value(v); }

src/smt/theory_arith_nl.h

@@ -444,7 +444,7 @@ namespace smt {
         m_asserted_bounds.push_back(new_bound);
         // copy justification to new bound
         dependency2new_bound(dep, *new_bound);
-        TRACE("buggy_bound", new_bound->display(*this, tout); tout << "\n";);
+        TRACE("non_linear", new_bound->display(*this, tout); tout << "\n";);
     }
 
     /**
@@ -457,8 +457,19 @@ namespace smt {
         bool r = false;
         if (!i.minus_infinity()) {
             inf_numeral new_lower(i.get_lower_value());
-            if (i.is_lower_open())
+            if (i.is_lower_open()) {
-                new_lower += get_epsilon(v);
+                if (is_int(v)) {
+                    if (new_lower.is_int()) {
+                        new_lower += rational::one();
+                    }
+                    else {
+                        new_lower = ceil(new_lower.get_rational());
+                    }
+                }
+                else {
+                    new_lower += get_epsilon(v);
+                }
+            }
             bound * old_lower = lower(v);
             if (old_lower == 0 || new_lower > old_lower->get_value()) {
                 TRACE("non_linear", tout << "NEW lower bound for v" << v << " " << new_lower << "\n";
@@ -469,8 +480,19 @@ namespace smt {
         }
         if (!i.plus_infinity()) {
             inf_numeral new_upper(i.get_upper_value());
-            if (i.is_upper_open())
+            if (i.is_upper_open()) {
-                new_upper -= get_epsilon(v);
+                if (is_int(v)) {
+                    if (new_upper.is_int()) {
+                        new_upper -= rational::one();
+                    }
+                    else {
+                        new_upper = floor(new_upper.get_rational());
+                    }
+                }
+                else {
+                    new_upper -= get_epsilon(v);
+                }
+            }
             bound * old_upper = upper(v);
             if (old_upper == 0 || new_upper < old_upper->get_value()) {
                 TRACE("non_linear", tout << "NEW upper bound for v" << v << " " << new_upper << "\n";
@@ -819,6 +841,7 @@ namespace smt {
             if (is_fixed(_var))
                 r *= lower_bound(_var).get_rational();
         }
+        TRACE("arith", tout << mk_pp(m, get_manager()) << " " << r << "\n";);
         return r;
     }
 
@@ -896,7 +919,7 @@ namespace smt {
 
             // Assert the equality
             // (= (* x_1 ... x_n) k)
-            TRACE("non_linear", tout << "all variables are fixed.\n";);
+            TRACE("non_linear", tout << "all variables are fixed, and bound is: " << k << "\n";);
             new_lower    = alloc(derived_bound, v, inf_numeral(k), B_LOWER);
             new_upper    = alloc(derived_bound, v, inf_numeral(k), B_UPPER);
         }
@@ -953,7 +976,8 @@ namespace smt {
         new_upper->m_eqs.append(new_lower->m_eqs);
 
         TRACE("non_linear",
-              tout << "lower: " << new_lower << " upper: " << new_upper << "\n";
+              new_lower->display(*this, tout << "lower: "); tout << "\n";
+              new_upper->display(*this, tout << "upper: "); tout << "\n";
               for (unsigned j = 0; j < new_upper->m_lits.size(); ++j) {
                   ctx.display_detailed_literal(tout, new_upper->m_lits[j]);
                   tout << " ";

src/test/cnf_backbones.cpp

@@ -64,6 +64,56 @@ static void display_status(lbool r) {
     }
 }
 
+static void track_clause(sat::solver& dst,
+                         sat::literal_vector& lits,
+                         sat::literal_vector& assumptions,
+                         vector<sat::literal_vector>& tracking_clauses) {
+    sat::literal lit = sat::literal(dst.mk_var(true, false), false);
+    tracking_clauses.set(lit.var(), lits);
+    lits.push_back(~lit);
+    dst.mk_clause(lits.size(), lits.c_ptr());
+    assumptions.push_back(lit);            
+}
+
+
+static void track_clauses(sat::solver const& src, 
+                          sat::solver& dst, 
+                          sat::literal_vector& assumptions,
+                          vector<sat::literal_vector>& tracking_clauses) {
+    for (sat::bool_var v = 0; v < src.num_vars(); ++v) {
+        dst.mk_var(false, true);
+    }
+    sat::literal_vector lits;
+    sat::literal lit;
+    sat::clause * const * it  = src.begin_clauses();
+    sat::clause * const * end = src.end_clauses();
+    svector<sat::solver::bin_clause> bin_clauses;
+    src.collect_bin_clauses(bin_clauses, false);
+    tracking_clauses.reserve(2*src.num_vars() + static_cast<unsigned>(end - it) + bin_clauses.size());
+
+    for (sat::bool_var v = 1; v < src.num_vars(); ++v) {
+        if (src.value(v) != l_undef) {
+            bool sign = src.value(v) == l_false;
+            lits.reset();
+            lits.push_back(sat::literal(v, sign));
+            track_clause(dst, lits, assumptions, tracking_clauses);
+        }
+    }
+    for (; it != end; ++it) {
+        lits.reset();
+        sat::clause& cls = *(*it);
+        lits.append(static_cast<unsigned>(cls.end()-cls.begin()), cls.begin());
+        track_clause(dst, lits, assumptions, tracking_clauses);
+    }
+    for (unsigned i = 0; i < bin_clauses.size(); ++i) {
+        lits.reset();
+        lits.push_back(bin_clauses[i].first);
+        lits.push_back(bin_clauses[i].second);        
+        track_clause(dst, lits, assumptions, tracking_clauses);
+    }
+}
+
+
 static void prune_unfixed(sat::literal_vector& lambda, sat::model const& m) {
     for (unsigned i = 0; i < lambda.size(); ++i) {
         if ((m[lambda[i].var()] == l_false) != lambda[i].sign()) {
@@ -88,18 +138,20 @@ static void back_remove(sat::literal_vector& lits, sat::literal l) {
     std::cout << "UNREACHABLE\n";
 }
 
-static void brute_force_consequences(sat::solver& s, sat::literal_vector const& gamma, sat::literal_vector& backbones) {
+static void brute_force_consequences(sat::solver& s, sat::literal_vector const& asms, sat::literal_vector const& gamma, sat::literal_vector& backbones) {
     for (unsigned i = 0; i < gamma.size(); ++i) {
         sat::literal nlit = ~gamma[i];
-        lbool r = s.check(1, &nlit);
+        sat::literal_vector asms1(asms);
+        asms1.push_back(nlit);
+        lbool r = s.check(asms1.size(), asms1.c_ptr());
         if (r == l_false) {
             backbones.push_back(gamma[i]);
         }
     }
 }
 
-static lbool core_chunking(sat::solver& s, sat::bool_var_vector& vars, vector<sat::literal_vector>& conseq, unsigned K) {
+static lbool core_chunking(sat::solver& s, sat::bool_var_vector& vars, sat::literal_vector const& asms, vector<sat::literal_vector>& conseq, unsigned K) {
-    lbool r = s.check();
+    lbool r = s.check(asms.size(), asms.c_ptr());
     display_status(r);
     if (r != l_true) {
         return r;
@@ -119,7 +171,9 @@ static lbool core_chunking(sat::solver& s, sat::bool_var_vector& vars, vector<sa
             omegaN.push_back(~l);
         }
         while (true) {
-            r = s.check(omegaN.size(), omegaN.c_ptr());
+            sat::literal_vector asms1(asms);
+            asms1.append(omegaN);
+            r = s.check(asms1.size(), asms1.c_ptr());
             if (r == l_true) {
                 IF_VERBOSE(1, verbose_stream() << "(sat) " << omegaN << "\n";);
                 prune_unfixed(lambda, s.get_model());
@@ -149,7 +203,7 @@ static lbool core_chunking(sat::solver& s, sat::bool_var_vector& vars, vector<sa
                 }
             }
             if (omegaN.empty() && occurs.size() > 1) {
-                brute_force_consequences(s, gamma, backbones);
+                brute_force_consequences(s, asms, gamma, backbones);
                 for (unsigned i = 0; i < gamma.size(); ++i) {
                     back_remove(lambda, gamma[i]);
                 }
@@ -174,6 +228,7 @@ static void cnf_backbones(bool use_chunk, char const* file_name) {
     p.set_bool("produce_models", true);
     reslimit limit;
     sat::solver solver(p, limit, 0);
+    sat::solver solver2(p, limit, 0);
     g_solver = &solver;
 
     if (file_name) {
@@ -192,16 +247,22 @@ static void cnf_backbones(bool use_chunk, char const* file_name) {
     vector<sat::literal_vector> conseq;
     sat::bool_var_vector vars;
     sat::literal_vector assumptions;
-    for (unsigned i = 1; i < solver.num_vars(); ++i) {
+    if (p.get_bool("dimacs.core", false)) {
+        g_solver = &solver2;        
+        vector<sat::literal_vector> tracking_clauses;
+        track_clauses(solver, solver2, assumptions, tracking_clauses);
+    }
+
+    for (unsigned i = 1; i < g_solver->num_vars(); ++i) {
         vars.push_back(i);        
-        solver.set_external(i);
+        g_solver->set_external(i);
     }
     lbool r;
     if (use_chunk) {
-        r = core_chunking(solver, vars, conseq, 100);
+        r = core_chunking(*g_solver, vars, assumptions, conseq, 100);
     }
     else {
-        r = solver.get_consequences(assumptions, vars, conseq);
+        r = g_solver->get_consequences(assumptions, vars, conseq);
     }
     std::cout << vars.size() << " " << conseq.size() << "\n";
     display_status(r);

src/test/main.cpp

@@ -8,6 +8,7 @@
 #include"timeit.h"
 #include"warning.h"
 #include "memory_manager.h"
+#include"gparams.h"
 
 //
 // Unit tests fail by asserting.
@@ -75,7 +76,7 @@ void display_usage() {
 void parse_cmd_line_args(int argc, char ** argv, bool& do_display_usage, bool& test_all) {
     int i = 1;
     while (i < argc) {
-	char * arg = argv[i];    
+	char * arg = argv[i], *eq_pos = 0;
 
 	if (arg[0] == '-' || arg[0] == '/') {
 	    char * opt_name = arg + 1;
@@ -118,6 +119,17 @@ void parse_cmd_line_args(int argc, char ** argv, bool& do_display_usage, bool& t
 	    }
 #endif
 	}
+        else if (arg[0] != '"' && (eq_pos = strchr(arg, '='))) {
+            char * key   = arg;
+            *eq_pos      = 0;
+            char * value = eq_pos+1; 
+            try {
+                gparams::set(key, value);
+            }
+            catch (z3_exception& ex) {
+                std::cerr << ex.msg() << "\n";
+            }
+        }            
 	i++;
     }
 }