Lev2 (Z3Prover#42)

* local Signed-off-by: Nikolaj Bjorner <[email protected]> * cleanup Signed-off-by: Nikolaj Bjorner <[email protected]> * got the legacy build going for release mode Signed-off-by: Nikolaj Bjorner <[email protected]> * microtune Signed-off-by: Nikolaj Bjorner <[email protected]> * optimize Signed-off-by: Nikolaj Bjorner <[email protected]>
NikolajBjorner · Apr 17, 2017 · 7bf8c66 · 7bf8c66
1 parent 0777af7
commit 7bf8c66
Show file tree

Hide file tree

Showing 15 changed files with 55 additions and 44 deletions.
diff --git a/scripts/mk_project.py b/scripts/mk_project.py
@@ -11,8 +11,7 @@
 def init_project_def():
     set_version(4, 4, 2, 1)
     add_lib('util', [])
-    add_lib('lean', ['util'], 'util/lp/lean')
-    add_lib('lp', ['lean','util'], 'util/lp')
+    add_lib('lp', ['util'], 'util/lp')
     add_lib('polynomial', ['util'], 'math/polynomial')
     add_lib('sat', ['util'])
     add_lib('nlsat', ['polynomial', 'sat'])
@@ -54,7 +53,7 @@ def init_project_def():
     add_lib('smt_params', ['ast', 'simplifier', 'pattern', 'bit_blaster'], 'smt/params')
     add_lib('proto_model', ['model', 'simplifier', 'smt_params'], 'smt/proto_model')
     add_lib('smt', ['bit_blaster', 'macros', 'normal_forms', 'cmd_context', 'proto_model',
-                    'substitution', 'grobner', 'euclid', 'simplex', 'proof_checker', 'pattern', 'parser_util', 'fpa'])
+                    'substitution', 'grobner', 'euclid', 'simplex', 'proof_checker', 'pattern', 'parser_util', 'fpa', 'lp'])
     add_lib('bv_tactics', ['tactic', 'bit_blaster', 'core_tactics'], 'tactic/bv')
     add_lib('fuzzing', ['ast'], 'test/fuzzing')
     add_lib('smt_tactic', ['smt'], 'smt/tactic')

diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
@@ -1134,7 +1134,6 @@ namespace smt {
         }
 
         final_check_status final_check_eh() {
-            //     std::cout << "final check\n";
             lbool is_sat = l_true;
             if (m_delay_constraints) {
                 init_solver();
@@ -1333,19 +1332,24 @@ namespace smt {
             return false;
         }
 
-        struct local_bound_propagator: lean::bound_propagator {
+        struct local_bound_propagator: public lean::bound_propagator {
             imp & m_imp;
             local_bound_propagator(imp& i) : bound_propagator(*i.m_solver), m_imp(i) {}
 
             bool bound_is_interesting(unsigned j, lean::lconstraint_kind kind, const rational & v) {
                 return m_imp.bound_is_interesting(j, kind, v);
             }
+
+            virtual void consume(rational const& v, unsigned j) {
+                m_imp.set_evidence(j);
+            }
         };
+
 
         void propagate_lp_solver_bound(lean::implied_bound& be) {
+
             theory_var v;
             lean::var_index vi = be.m_j;
-            std::vector<std::pair<lean::mpq, unsigned>> explanation;
             if (m_solver->is_term(vi)) {
                 v = m_term_index2theory_var.get(m_solver->adjust_term_index(vi), null_theory_var);
             }
@@ -1361,6 +1365,7 @@ namespace smt {
                 return;
             }
             lp_bounds const& bounds = m_bounds[v];
+            bool first = true;
             for (unsigned i = 0; i < bounds.size(); ++i) {
                 lp::bound* b = bounds[i];
                 if (ctx().get_assignment(b->get_bv()) != l_undef) {
@@ -1372,22 +1377,21 @@ namespace smt {
                 }
 
                 m_solver->settings().st().m_num_of_implied_bounds ++;
-                m_core.reset();
-                m_eqs.reset();
-                m_params.reset();
-                if (explanation.size() == 0)
-                    m_solver->explain_implied_bound(be, explanation);
-                for (size_t j = 0; j < explanation.size(); ++j) {
-                    // be.m_evidence[j].first; // TBD coefficient. used for Farkas justification.
-                    set_evidence(explanation[j].second);
+                if (first) {
+                    first = false;
+                    m_core.reset();
+                    m_eqs.reset();
+                    m_params.reset();
+                    local_bound_propagator bp(*this);
+                    m_solver->explain_implied_bound(be, bp);
                 }
                 updt_unassigned_bounds(v, -1);
                 TRACE("arith",
                       ctx().display_literals_verbose(tout, m_core);
                       tout << "\n --> ";
                       ctx().display_literal_verbose(tout, lit);
                       tout << "\n";
-                      display_evidence(tout, explanation);
+                      // display_evidence(tout, m_explanation);
                       m_solver->print_implied_bound(be, tout);
                       );
                 DEBUG_CODE(
@@ -1400,19 +1404,22 @@ namespace smt {
             }
         }
 
+        literal_vector m_core2;
+
         void assign(literal lit) {
             SASSERT(validate_assign(lit));
             if (m_core.size() < small_lemma_size() && m_eqs.empty()) {
+                m_core2.reset();
                 for (unsigned i = 0; i < m_core.size(); ++i) {
-                    m_core[i].neg();
+                    m_core2.push_back(~m_core[i]);
                 }
-                m_core.push_back(lit);
+                m_core2.push_back(lit);
                 justification * js = 0;
                 if (proofs_enabled()) {
-                    js = alloc(theory_lemma_justification, get_id(), ctx(), m_core.size(), m_core.c_ptr(),
+                    js = alloc(theory_lemma_justification, get_id(), ctx(), m_core2.size(), m_core2.c_ptr(),
                                m_params.size(), m_params.c_ptr());
                 }
-                ctx().mk_clause(m_core.size(), m_core.c_ptr(), js, CLS_AUX_LEMMA, 0);
+                ctx().mk_clause(m_core2.size(), m_core2.c_ptr(), js, CLS_AUX_LEMMA, 0);
             }
             else {
                 ctx().assign(
@@ -2101,8 +2108,6 @@ namespace smt {
         }
 
         lbool make_feasible() {
-            //static unsigned m_count = 0;
-            //std::cout << "check feasible " << m_count++ << "\n";
             reset_variable_values();
             ++m_stats.m_make_feasible;
             if (m_solver->A_r().column_count() > m_stats.m_max_cols)
@@ -2123,9 +2128,8 @@ namespace smt {
             m_stats.m_num_iterations = m_solver->settings().st().m_total_iterations;
             m_stats.m_num_factorizations = m_solver->settings().st().m_num_factorizations;
             m_stats.m_need_to_solve_inf = m_solver->settings().st().m_need_to_solve_inf;
-
             if (print) {
-                std::cout << status << " " << sw.get_seconds() << " " << m_stats.m_num_iterations << " " << m_print_counter << "\n";
+                IF_VERBOSE(0, verbose_stream() << status << " " << sw.get_seconds() << " " << m_stats.m_num_iterations << " " << m_print_counter << "\n";);
             }
             //m_stats.m_num_iterations_with_no_progress += m_solver->settings().st().m_iters_with_no_cost_growing;
 
@@ -2145,7 +2149,7 @@ namespace smt {
                 return l_undef;
             }
         }
-
+ 
         std::vector<std::pair<rational, lean::constraint_index>> m_explanation;
         literal_vector      m_core;
         svector<enode_pair> m_eqs;

diff --git a/src/test/lp.cpp b/src/test/lp.cpp
@@ -44,6 +44,7 @@ struct simple_column_namer:public column_namer
     }
 };
 
+
 template <typename T, typename X>
 void test_matrix(sparse_matrix<T, X> & a) {
     auto m = a.dimension();

diff --git a/src/util/debug.h b/src/util/debug.h
@@ -66,6 +66,7 @@ bool is_debug_enabled(const char * tag);
 
 #ifdef Z3DEBUG
 # define UNREACHABLE() DEBUG_CODE(notify_assertion_violation(__FILE__, __LINE__, "UNREACHABLE CODE WAS REACHED."); INVOKE_DEBUGGER();)
+# define LEAN_DEBUG 1
 #else
 #if (defined(__GNUC__) && ((__GNUC__ * 100 + __GNUC_MINOR__) >= 405)) || __has_builtin(__builtin_unreachable)
 // only available in gcc >= 4.5 and in newer versions of clang

diff --git a/src/util/lp/bound_analyzer_on_row.h b/src/util/lp/bound_analyzer_on_row.h
@@ -44,6 +44,7 @@ public :
 
     unsigned j;
     void analyze() {
+
         mpq a; unsigned j;
         while (((m_column_of_l != -2) || (m_column_of_u != -2)) && m_it.next(a, j))
             analyze_bound_on_var_on_coeff(j, a);

diff --git a/src/util/lp/bound_propagator.h b/src/util/lp/bound_propagator.h
@@ -24,5 +24,6 @@ class bound_propagator {
                                       lean::lconstraint_kind kind,
                                       const rational & bval) {return true;}
     unsigned number_of_found_bounds() const { return m_ibounds.size(); }
+    virtual void consume(mpq const& v, unsigned j) { std::cout << "doh\n"; }
 };
 }
diff --git a/src/util/lp/dense_matrix_instances.cpp b/src/util/lp/dense_matrix_instances.cpp
@@ -22,4 +22,5 @@ template lean::dense_matrix<lean::mpq, lean::numeric_pair<lean::mpq> > lean::ope
 template void lean::dense_matrix<lean::mpq, lean::numeric_pair< lean::mpq> >::apply_from_right( std::vector< lean::mpq, std::allocator< lean::mpq> > &);
 template void lean::dense_matrix<double,double>::apply_from_right(class std::vector<double,class std::allocator<double> > &);
 template void lean::dense_matrix<lean::mpq, lean::mpq>::apply_from_left(std::vector<lean::mpq, std::allocator<lean::mpq> >&);
+template lean::dense_matrix<lean::mpq, lean::mpq> lean::get_B<lean::mpq, lean::mpq>(lean::lu<lean::mpq, lean::mpq>&, std::vector<unsigned int, std::allocator<unsigned int> > const&);
 #endif
diff --git a/src/util/lp/lar_solver.h b/src/util/lp/lar_solver.h
@@ -494,35 +494,30 @@ class lar_solver : public column_namer {
         lean_assert(false); // not implemented
     }
 
-    void explain_implied_bound(implied_bound & ib, std::vector<std::pair<mpq, unsigned>> & explanation) {
-        unsigned i = ib.m_row_or_term_index;
-        linear_combination_iterator<mpq> *it =
-            is_term(i)? 
-             create_new_iter_from_term(i) : new iterator_on_row<mpq>(A_r().m_rows[i]);
 
-        mpq a; unsigned j;
+    void explain_implied_bound(implied_bound & ib, bound_propagator & bp) {
+        unsigned i = ib.m_row_or_term_index;
         int bound_sign = ib.m_is_low_bound? 1: -1;
         int j_sign = (ib.m_coeff_before_j_is_pos ? 1 :-1) * bound_sign;
         unsigned m_j = ib.m_j;
         if (is_term(m_j)) {
             m_j = m_ext_vars_to_columns[m_j];
         }
-        while (it->next(a, j)) { // this iterator will bring real column indices
+        for (auto const& r : A_r().m_rows[i]) {
+            unsigned j = r.m_j;
+            mpq const& a = r.get_val();
             if (j == m_j) continue;
             if (is_term(j)) {
                 j = m_ext_vars_to_columns[j];
             } 
-
             int a_sign = is_pos(a)? 1: -1;
             int sign = j_sign * a_sign;
             const ul_pair & ul =  m_vars_to_ul_pairs[j];
             auto witness = sign > 0? ul.upper_bound_witness(): ul.low_bound_witness();
             lean_assert(is_valid(witness));
-            explanation.emplace_back(a, witness);
+            bp.consume(a, witness);
         }
-
-        delete it;
-        lean_assert(implied_bound_is_correctly_explained(ib, explanation));
+        // lean_assert(implied_bound_is_correctly_explained(ib, explanation));
     }
 
 

diff --git a/src/util/lp/lp_utils.h b/src/util/lp/lp_utils.h
@@ -24,6 +24,11 @@ bool contains(const std::unordered_map<A, B> & map, const A& key) {
 }
 
 #ifdef lp_for_z3
+
+#ifdef Z3DEBUG
+#define LEAN_DEBUG 1
+#endif
+
 namespace lean {
     inline void throw_exception(const std::string & str) {
         throw default_exception(str);
@@ -78,9 +83,9 @@ struct hash<lean::numeric_pair<lean::mpq>> {
 #else // else  of #if  lp_for_z3
 #include <utility>
 #include <functional>
-#include "util/numerics/mpq.h"
-#include "util/numerics/numeric_traits.h"
-#include "util/numerics/double.h"
+//include "util/numerics/mpq.h"
+//include "util/numerics/numeric_traits.h"
+//include "util/numerics/double.h"
 
 #ifdef __CLANG__
 #pragma clang diagnostic push

diff --git a/src/util/lp/lu.cpp b/src/util/lp/lu.cpp
@@ -9,6 +9,7 @@
 #include <set>
 #include <vector>
 #include <utility>
+#include "util/debug.h"
 #include "util/lp/lu.h"
 namespace lean {
 #ifdef LEAN_DEBUG

diff --git a/src/util/lp/lu_instances.cpp b/src/util/lp/lu_instances.cpp
@@ -8,6 +8,7 @@
 #include <memory>
 #include <string>
 #include <vector>
+#include "util/debug.h"
 #include "util/lp/lu.cpp"
 template double lean::dot_product<double, double>(std::vector<double, std::allocator<double> > const&, std::vector<double, std::allocator<double> > const&);
 template lean::lu<double, double>::lu(lean::static_matrix<double, double> const&, std::vector<unsigned int, std::allocator<unsigned int> >&, lean::lp_settings&);

diff --git a/src/util/lp/matrix.cpp b/src/util/lp/matrix.cpp
@@ -4,7 +4,8 @@
 
   Author: Lev Nachmanson
 */
-#ifdef LEAN_DEBUG
+
+#ifdef Z3DEBUG
 #include <cmath>
 #include <vector>
 #include <string>

diff --git a/src/util/lp/matrix.h b/src/util/lp/matrix.h
@@ -4,10 +4,9 @@
 
   Author: Lev Nachmanson
 */
-#ifdef LEAN_DEBUG
+#ifdef Z3DEBUG
 #pragma once
 #include "util/lp/numeric_pair.h"
-// #include "util/numerics/double.h"
 #include <vector>
 #include <string>
 #include "util/lp/lp_settings.h"

diff --git a/src/util/lp/numeric_pair.h b/src/util/lp/numeric_pair.h
@@ -16,8 +16,8 @@
 #include "../z3_exception.h"
 
 #else
-#include "util/numerics/mpq.h"
-#include "util/numerics/numeric_traits.h"
+ // include "util/numerics/mpq.h"
+ // include "util/numerics/numeric_traits.h"
 #endif
 namespace lean {
 #ifdef lp_for_z3 // rename rationals

diff --git a/src/util/numerics/double.h b/src/util/numerics/double.h
@@ -0,0 +1 @@
+// empty
-Original file line number
+Diff line change
@@ Expand Up / @@ -44,6 +44,7 @@ struct simple_column_namer:public column_namer @@
         }
     };
     template <typename T, typename X>
     void test_matrix(sparse_matrix<T, X> & a) {
         auto m = a.dimension();
@@ Expand Down @@