working on DL opt

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

src/smt/smt_setup.cpp

@@ -352,10 +352,14 @@ namespace smt {
         else if (!m_params.m_arith_auto_config_simplex && is_dense(st)) {
             TRACE("setup", tout << "using dense diff logic...\n";);
             m_params.m_phase_selection = PS_CACHING_CONSERVATIVE;
+            //m_context.register_plugin(alloc(smt::theory_idl, m_manager, m_params));
+#if 1
             if (st.m_arith_k_sum < rational(INT_MAX / 8))
                 m_context.register_plugin(alloc(smt::theory_dense_si, m_manager, m_params));
             else
                 m_context.register_plugin(alloc(smt::theory_dense_i, m_manager, m_params));
+#endif
+
         }
         else {
             // if (st.m_arith_k_sum < rational(INT_MAX / 8)) {

src/smt/theory_dense_diff_logic.h

@@ -229,6 +229,8 @@ namespace smt {
         virtual void flush_eh();
         virtual void reset_eh();
         
+        bool dump_lemmas() const { return m_params.m_arith_dump_lemmas; }
+
         virtual bool validate_eq_in_model(theory_var v1, theory_var v2, bool is_true) const;
 
         virtual void display(std::ostream & out) const;

src/smt/theory_dense_diff_logic_def.h

@@ -120,6 +120,7 @@ namespace smt {
         if (!m_non_diff_logic_exprs) {
             TRACE("non_diff_logic", tout << "found non diff logic expression:\n" << mk_pp(n, get_manager()) << "\n";);
             get_context().push_trail(value_trail<context, bool>(m_non_diff_logic_exprs));
+        IF_VERBOSE(0, verbose_stream() << "(smt.diff_logic: non-diff logic expression " << mk_pp(n, get_manager()) << ")\n";); 
             m_non_diff_logic_exprs = true;
         }
     }
@@ -587,6 +588,11 @@ namespace smt {
             context & ctx = get_context();
             region & r    = ctx.get_region();
             ctx.set_conflict(ctx.mk_justification(theory_conflict_justification(get_id(), r, antecedents.size(), antecedents.c_ptr())));
+
+            if (dump_lemmas()) {
+                ctx.display_lemma_as_smt_problem(antecedents.size(), antecedents.c_ptr(), false_literal, "");
+            }
+
             return;
         }
         

src/smt/theory_diff_logic.h

@@ -170,6 +170,9 @@ namespace smt {
         eq_prop_info_set               m_eq_prop_info_set;        // set of existing equality prop infos
         ptr_vector<eq_prop_info>       m_eq_prop_infos;
 
+        app_ref_vector                 m_terms;
+        svector<bool>                  m_signs;
+
         ptr_vector<atom>               m_atoms;
         ptr_vector<atom>               m_asserted_atoms;   // set of asserted atoms
         unsigned                       m_asserted_qhead;   
@@ -217,6 +220,7 @@ namespace smt {
             m_util(m),
             m_arith_eq_adapter(*this, params, m_util),
             m_zero(null_theory_var),
+            m_terms(m),
             m_asserted_qhead(0),
             m_num_core_conflicts(0),
             m_num_propagation_calls(0),
@@ -323,6 +327,10 @@ namespace smt {
 
         virtual void new_diseq_eh(theory_var v1, theory_var v2, justification& j);
 
+        bool decompose_linear(app_ref_vector& args, svector<bool>& signs);
+
+        bool is_sign(expr* n, bool& sign);
+
         bool is_negative(app* n, app*& m);
 
         void del_atoms(unsigned old_size);

src/smt/theory_diff_logic_def.h

@@ -177,7 +177,6 @@ bool theory_diff_logic<Ext>::internalize_atom(app * n, bool gate_ctx) {
     bool is_ge = m_util.is_ge(n);
     bool_var bv;
     rational kr;
-    app * x, *y, *z;
     theory_var source, target; // target - source <= k
     app * lhs = to_app(n->get_arg(0));
     app * rhs = to_app(n->get_arg(1));
@@ -191,25 +190,26 @@ bool theory_diff_logic<Ext>::internalize_atom(app * n, bool gate_ctx) {
     }
     numeral k(kr);
 
-    bool is_add = m_util.is_add(lhs) && lhs->get_num_args() == 2;
+    m_terms.reset();
-
+    m_signs.reset();
-    if (is_add) {
+    m_terms.push_back(lhs);
-        x = to_app(lhs->get_arg(0));
+    m_signs.push_back(true);
-        y = to_app(lhs->get_arg(1));
+    if (!decompose_linear(m_terms, m_signs)) {
+        found_non_diff_logic_expr(n);        
+        return false;
     }
-
+    if (m_terms.size() == 2 && m_signs[0] != m_signs[1]) {
-    if (is_add && is_negative(x, z)) {  
+        target = mk_var(m_terms[0].get());
-        target = mk_var(y);
+        source = mk_var(m_terms[1].get());
-        source = mk_var(z);
+        if (!m_signs[0]) {
-    }
+            std::swap(target, source);
-    else if (is_add && is_negative(y, z)) {
+        }
-        target = mk_var(x);
-        source = mk_var(z);
     }
     else {
         target = mk_var(lhs);
         source = get_zero();
     }
+
     if (is_ge) {
         std::swap(target, source);
         k.neg();
@@ -378,6 +378,70 @@ void theory_diff_logic<Ext>::del_atoms(unsigned old_size) {
 }
 
 
+template<typename Ext>
+bool theory_diff_logic<Ext>::decompose_linear(app_ref_vector& terms, svector<bool>& signs) {
+    for (unsigned i = 0; i < terms.size(); ++i) {
+        app* n = terms[i].get();
+        if (m_util.is_add(n)) {
+            expr* arg = n->get_arg(0);
+            if (!is_app(arg)) return false;
+            terms[i] = to_app(arg);
+            for (unsigned j = 1; j < n->get_num_args(); ++j) {
+                arg = n->get_arg(j);
+                if (!is_app(arg)) return false;
+                terms.push_back(to_app(arg));
+                signs.push_back(signs[i]);
+            }
+            --i;
+            continue;
+        }
+        expr* x, *y;
+        bool sign;
+        if (m_util.is_mul(n, x, y)) {
+            if (is_sign(x, sign) && is_app(y)) {
+                terms[i] = to_app(y);
+                signs[i] = (signs[i] == sign);
+                --i;
+            }
+            else if (is_sign(y, sign) && is_app(x)) {
+                terms[i] = to_app(x);
+                signs[i] = (signs[i] == sign);
+                --i;
+            }
+            continue;
+        }
+        if (m_util.is_uminus(n, x) && is_app(x)) {
+            terms[i] = to_app(x);
+            signs[i] = !signs[i];
+            --i;
+            continue;
+        }
+    }
+    return true;
+}
+
+template<typename Ext>
+bool theory_diff_logic<Ext>::is_sign(expr* n, bool& sign) {
+    rational r;
+    expr* x;
+    if (m_util.is_numeral(n, r)) {
+        if (r.is_one()) {
+            sign = true;
+            return true;
+        }
+        if (r.is_minus_one()) {
+            sign = false;
+            return true;
+        }
+    }
+    else if (m_util.is_uminus(n, x)) {
+        if (is_sign(x, sign)) {
+            sign = !sign;
+            return true;
+        }
+    }
+    return false;
+}
 
 template<typename Ext>
 bool theory_diff_logic<Ext>::is_negative(app* n, app*& m) {