remove conflict on false disequality, introduced regression

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

src/sat/sat_solver.cpp

@@ -3168,7 +3168,8 @@ namespace sat {
             ++num_iterations;
             checkpoint();
             literal_set::iterator it = vars.begin(), end = vars.end();
-            for (; it != end; ++it) {
+            unsigned chunk_size = 100;
+            for (; it != end && chunk_size > 0; ++it) {
                 literal lit = *it;
                 if (value(lit) != l_undef) {
                     continue;
@@ -3182,6 +3183,7 @@ namespace sat {
                         return l_false;
                     }
                     propagate(false);
+                    --chunk_size;
                 }
             }
             lbool is_sat;

src/sat/sat_solver/inc_sat_solver.cpp

@@ -257,10 +257,12 @@ public:
             bool_var2conseq.insert(lconseq[i][0].var(), i);
         }
         
-        // extract original fixed variables 
+        // extract original fixed variables
+        u_map<expr*> asm2dep;
+        extract_asm2dep(dep2asm, asm2dep);
         for (unsigned i = 0; i < vars.size(); ++i) {
             expr_ref cons(m);
-            if (extract_fixed_variable(dep2asm, vars[i], bool_var2conseq, lconseq, cons)) {
+            if (extract_fixed_variable(dep2asm, asm2dep, vars[i], bool_var2conseq, lconseq, cons)) {
                 conseq.push_back(cons);
             }
         }
@@ -378,7 +380,7 @@ private:
         if (!atoms.empty()) {
             std::stringstream strm;
             strm << "interpreted atoms sent to SAT solver " << atoms;
-            TRACE("sat", std::cout << strm.str() << "\n";);
+            TRACE("sat", tout << strm.str() << "\n";);
             IF_VERBOSE(1, verbose_stream() << strm.str() << "\n";);
             set_reason_unknown(strm.str().c_str());
             return l_undef;
@@ -449,9 +451,7 @@ private:
         return internalized;
     }
 
-    bool extract_fixed_variable(dep2asm_t& dep2asm, expr* v, u_map<unsigned> const& bool_var2conseq, vector<sat::literal_vector> const& lconseq, expr_ref& conseq) {
+    bool extract_fixed_variable(dep2asm_t& dep2asm, u_map<expr*>& asm2dep, expr* v, u_map<unsigned> const& bool_var2conseq, vector<sat::literal_vector> const& lconseq, expr_ref& conseq) {
-        u_map<expr*> asm2dep;
-        extract_asm2dep(dep2asm, asm2dep);
 
         sat::bool_var_vector bvars;
         if (!internalize_var(v, bvars)) {
@@ -484,6 +484,7 @@ private:
         return true;
     }
 
+    vector<rational> m_exps;
     void internalize_value(sat::literal_vector const& value, expr* v, expr_ref& val) {
         bv_util bvutil(m);
         if (is_uninterp_const(v) && m.is_bool(v)) {
@@ -492,10 +493,16 @@ private:
         }
         else if (is_uninterp_const(v) && bvutil.is_bv_sort(m.get_sort(v))) {
             SASSERT(value.size() == bvutil.get_bv_size(v));
+            if (m_exps.empty()) {
+                m_exps.push_back(rational::one());
+            }
+            while (m_exps.size() < value.size()) {
+                m_exps.push_back(rational(2)*m_exps.back());
+            }
             rational r(0);
             for (unsigned i = 0; i < value.size(); ++i) {
                 if (!value[i].sign()) {
-                    r += rational(2).expt(i);
+                    r += m_exps[i];
                 }
             }
             val = m.mk_eq(v, bvutil.mk_numeral(r, value.size()));

src/smt/smt_context.cpp

@@ -1111,7 +1111,8 @@ namespace smt {
 
         if (r1 == r2) {
             TRACE("add_diseq_inconsistent", tout << "add_diseq #" << n1->get_owner_id() << " #" << n2->get_owner_id() << " inconsistency, scope_lvl: " << m_scope_lvl << "\n";);
-            return false; // context is inconsistent
+            return true;
+            // return false; // context is inconsistent
         }
 
         // Propagate disequalities to theories

src/solver/solver2tactic.cpp

@@ -160,9 +160,7 @@ public:
     }
     virtual void reset_statistics() {}
 
-    virtual void cleanup() {
+    virtual void cleanup() { }
-        m_solver = m_solver->translate(m, m_params);
-    }
     virtual void reset() { cleanup(); }
 
     virtual void set_logic(symbol const & l) {}

src/util/sorting_network.h

@@ -251,6 +251,15 @@ Notes:
             return result;
         }
 
+#if 0
+        literal mk_and(literal_vector const& lits) {
+            if (lits.size() == 1) {
+                return lits[0];
+            }
+            
+        }
+#endif
+
         void mk_implies_or(literal l, unsigned n, literal const* xs) {
             literal_vector lits(n, xs);
             lits.push_back(ctx.mk_not(l));
@@ -337,11 +346,28 @@ Notes:
             ors.push_back(ex);                
             
             // result => xs[0] + ... + xs[n-1] <= 1
+#if 1
             for (unsigned i = 0; i < n; ++i) {
                 for (unsigned j = i + 1; j < n; ++j) {
                     add_clause(ctx.mk_not(result), ctx.mk_not(xs[i]), ctx.mk_not(xs[j]));
                 }
             }            
+#else
+            literal_vector atm;
+            for (unsigned i = 0; i < n; ++i) {
+                // at => !xs[1] & .. & !xs[i-1] & !xs[i+1] & ... & !xs[n-1] 
+                literal at = fresh();
+                for (unsigned j = 0; j < n; ++j) {
+                    if (i != j) {
+                        add_clause(ctx.mk_not(at), ctx.mk_not(xs[j]));
+                    }
+                }
+                atm.push_back(at);
+            }            
+            atm.push_back(ctx.mk_not(result));
+            add_clause(atm);
+
+#endif
             // xs[0] + ... + xs[n-1] <= 1 => and_x
             if (full) {
                 literal and_i = fresh();