merge while skyping

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

src/opt/maxres.cpp

@@ -383,8 +383,8 @@ public:
         }
         TRACE("opt", 
               tout << "num cores: " << cores.size() << "\n";
-              for (unsigned i = 0; i < cores.size(); ++i) {
-                  display_vec(tout, cores[i]);
+              for (auto const& c : cores) {
+                  display_vec(tout, c);
               }
               tout << "num satisfying: " << asms.size() << "\n";);
         
@@ -476,8 +476,8 @@ public:
     }
 
     void process_unsat(vector<exprs> const& cores) {
-        for (unsigned i = 0; i < cores.size(); ++i) {
-            process_unsat(cores[i]);
+        for (auto const & c : cores) {
+            process_unsat(c);
         }
     }
 
@@ -602,8 +602,7 @@ public:
     }
 
     void display(std::ostream& out) {
-        for (unsigned i = 0; i < m_asms.size(); ++i) {
-            expr* a = m_asms[i].get();
+        for (expr * a : m_asms) {
             out << mk_pp(a, m) << " : " << get_weight(a) << "\n";
         }
     }
@@ -710,8 +709,8 @@ public:
 
     void update_assignment(model* mdl) {
         unsigned correction_set_size = 0;
-        for (unsigned i = 0; i < m_asms.size(); ++i) {
-            if (is_false(mdl, m_asms[i].get())) {
+        for (expr* a : m_asms) {
+            if (is_false(mdl, a)) {
                 ++correction_set_size;
             }
         }
@@ -722,10 +721,12 @@ public:
 
         rational upper(0);
         expr_ref tmp(m);
-        for (unsigned i = 0; i < m_soft.size(); ++i) {
-            if (!is_true(mdl, m_soft[i])) {
+        unsigned i = 0;
+        for (expr* s : m_soft) {
+            if (!is_true(mdl, s)) {
                 upper += m_weights[i];
             }
+            ++i;
         }
 
         if (upper > m_upper) {
@@ -741,8 +742,9 @@ public:
 
         TRACE("opt", model_smt2_pp(tout << "updated model\n", m, *m_model, 0););
 
-        for (unsigned i = 0; i < m_soft.size(); ++i) {
-            m_assignment[i] = is_true(m_soft[i]);
+        i = 0;
+        for (expr* s : m_soft) {
+            m_assignment[i++] = is_true(s);
         }
        
         // DEBUG_CODE(verify_assignment(););
@@ -759,8 +761,8 @@ public:
         pb_util u(m);
         expr_ref_vector nsoft(m);
         expr_ref fml(m);
-        for (unsigned i = 0; i < m_soft.size(); ++i) {
-            nsoft.push_back(mk_not(m, m_soft[i]));
+        for (expr* s : m_soft) {
+            nsoft.push_back(mk_not(m, s));
         }            
         fml = u.mk_lt(nsoft.size(), m_weights.c_ptr(), nsoft.c_ptr(), m_upper);
         TRACE("opt", tout << "block upper bound " << fml << "\n";);;

src/qe/qe_mbi.cpp

@@ -16,6 +16,62 @@ Author:
 Revision History:
 
 
+Notes:
+
+  Reduction into:
+   T_EUF
+   T_LIRA
+
+  Other theories: DT, ARR reduced to EUF
+  BV is EUF/Boolean.
+
+  Purify EUF1 & LIRA1 & EUF2 & LIRA2
+
+  Then EUF1 & EUF2   |- false
+       LIRA1 & LIRA2 |- false
+
+  Sketch of approach by example:
+
+       A: s <= 2a <= t     & f(a) = q
+       
+       B: t <= 2b <= s + 1 & f(b) != q
+
+  1. Extract arithmetic consequences of A over shared vocabulary.
+
+       A -> s <= t & (even(t) | s < t) 
+ 
+  2a. Send to B, have B solve shared variables with EUF_B.
+        epsilon b . B & A_pure
+        epsilon b . t <= 2b <= s + 1 & s <= t & (even(t) | s < t) 
+        = t <= s + 1 & (even(t) | t <= s) & s <= t & (even(t) | s < t) 
+        = even(t) & t = s 
+        b := t div 2
+
+      B & A_pure -> B[b/t div 2] = f(t div 2) != q & t <= s + 1
+
+  3a. Send purified result to A
+      A & B_pure -> false
+
+      Invoke the ping-pong principle to extract interpolant.
+      
+  2b. Solve for shared variables with EUF.
+
+    epsilon a . A 
+  = a := (s + 1) div 2 & s < t & f((s + 1) div 2) = q
+
+  3b. Send to B. Produces core 
+          s < t & f((s + 1) div 2) = q
+
+  4b Solve again in arithmetic for shared variables with EUF.
+
+    epsion a . A & (s >= t | f((s + 1) div 2) != q)
+
+         a := t div 2 | s = t & f(t div 2) = q & even(t)
+
+    Send to B, produces core (s != t | f(t div 2) != q)
+
+  5b. There is no longer a solution for A. A is unsat.
+      
 --*/
 
 #include "ast/ast_util.h"
@@ -129,7 +185,6 @@ namespace qe {
             // optionally minimize core using superposition.
             return mbi_unsat;
         case l_true: {
-            expr_ref_vector fmls(m);
             m_solver->get_model(mdl);
             model_evaluator mev(*mdl.get());
             lits.reset();
@@ -263,3 +318,4 @@ namespace qe {
         }
     }
 };
+

src/smt/smt_context.cpp

@@ -3438,7 +3438,6 @@ namespace smt {
             th->init_search_eh();
         }
         m_qmanager->init_search_eh();
-        m_assumption_core.reset();
         m_incomplete_theories.reset();
         m_num_conflicts                = 0;
         m_num_conflicts_since_restart  = 0;

src/smt/smt_context.h

@@ -894,7 +894,6 @@ namespace smt {
         failure            m_last_search_failure;
         ptr_vector<theory> m_incomplete_theories; //!< theories that failed to produce a model
         bool               m_searching;
-        ptr_vector<expr>   m_assumption_core;
         unsigned           m_num_conflicts;
         unsigned           m_num_conflicts_since_restart;
         unsigned           m_num_conflicts_since_lemma_gc;