avoid going creating hnf_cuts if all involved vars have integral values

Signed-off-by: Lev Nachmanson <levnach@hotmail.com> add explanations to hnf cuts Signed-off-by: Lev Nachmanson <levnach@hotmail.com> nits and virtual methods (Z3Prover#68) * local Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * virtual method in bound propagator Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> cleanup from std::cout Signed-off-by: Lev Nachmanson <levnach@hotmail.com> handle the case when the number of terms is greater than the number of variables in hnf Signed-off-by: Lev Nachmanson <levnach@hotmail.com> method name's fix Signed-off-by: Lev Nachmanson <levnach@hotmail.com> restore hnf_cutter to work with m_row_count <= m_column_count Signed-off-by: Lev Nachmanson <levnach@hotmail.com> tune addition of rational numbers (Z3Prover#70) * log quantifiers only if present Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * merge and fix some warnings Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * set new arith as default for LIA Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * local Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * virtual method in bound propagator Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * prepare for mixed integer-real Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * fix default tactic usage Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> give shorter explanations, call hnf only when have a not integral var Signed-off-by: Lev Nachmanson <levnach@hotmail.com> overhaul of mpq (Z3Prover#71) * log quantifiers only if present Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * merge and fix some warnings Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * set new arith as default for LIA Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * local Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * virtual method in bound propagator Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * prepare for mixed integer-real Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * fix default tactic usage Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * overhaul of mpz/mpq Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * disabled temporary setting Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * remove prints Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> fix for 32 bit build (Z3Prover#72) * log quantifiers only if present Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * merge and fix some warnings Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * set new arith as default for LIA Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * local Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * virtual method in bound propagator Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * prepare for mixed integer-real Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * fix default tactic usage Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * overhaul of mpz/mpq Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * disabled temporary setting Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * remove prints Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * customize for 64 bit Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> yes (Z3Prover#74) * log quantifiers only if present Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * merge and fix some warnings Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * set new arith as default for LIA Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * local Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * virtual method in bound propagator Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * prepare for mixed integer-real Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * fix default tactic usage Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * overhaul of mpz/mpq Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * disabled temporary setting Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * remove prints Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * customize for 64 bit Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * customize for 64 bit Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * more refactor Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> fix the merge Signed-off-by: Lev Nachmanson <levnach@hotmail.com> fixes in maximize_term untested Signed-off-by: Lev Nachmanson <levnach@hotmail.com> fix compilation (Z3Prover#75) * log quantifiers only if present Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * merge and fix some warnings Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * set new arith as default for LIA Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * local Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * virtual method in bound propagator Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * prepare for mixed integer-real Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * fix default tactic usage Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * overhaul of mpz/mpq Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * disabled temporary setting Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * remove prints Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * customize for 64 bit Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * customize for 64 bit Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * more refactor Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * merge Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * relax check Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * change for gcc Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * merge Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
NikolajBjorner · Jun 27, 2018 · 9ba4026 · 9ba4026
1 parent 9be49ff
commit 9ba4026
Show file tree

Hide file tree

Showing 41 changed files with 933 additions and 1,271 deletions.
diff --git a/src/smt/params/smt_params_helper.pyg b/src/smt/params/smt_params_helper.pyg
@@ -40,7 +40,7 @@ def_module_params(module_name='smt',
                           ('bv.reflect', BOOL, True, 'create enode for every bit-vector term'),
                           ('bv.enable_int2bv', BOOL, True, 'enable support for int2bv and bv2int operators'),
                           ('arith.random_initial_value', BOOL, False, 'use random initial values in the simplex-based procedure for linear arithmetic'),
-                          ('arith.solver', UINT, 2, 'arithmetic solver: 0 - no solver, 1 - bellman-ford based solver (diff. logic only), 2 - simplex based solver, 3 - floyd-warshall based solver (diff. logic only) and no theory combination 4 - utvpi, 5 - infinitary lra, 6 - lra solver'),
+                          ('arith.solver', UINT, 6, 'arithmetic solver: 0 - no solver, 1 - bellman-ford based solver (diff. logic only), 2 - simplex based solver, 3 - floyd-warshall based solver (diff. logic only) and no theory combination 4 - utvpi, 5 - infinitary lra, 6 - lra solver'),
                           ('arith.nl', BOOL, True, '(incomplete) nonlinear arithmetic support based on Groebner basis and interval propagation'),
                           ('arith.nl.gb', BOOL, True, 'groebner Basis computation, this option is ignored when arith.nl=false'),
                           ('arith.nl.branching', BOOL, True, 'branching on integer variables in non linear clusters'),

diff --git a/src/smt/smt_setup.cpp b/src/smt/smt_setup.cpp
@@ -818,10 +818,7 @@ namespace smt {
                 m_context.register_plugin(alloc(smt::theory_mi_arith, m_manager, m_params));
             break;
         default:
-            if (m_params.m_arith_int_only && int_only)
-                setup_i_arith();
-            else
-                m_context.register_plugin(alloc(smt::theory_mi_arith, m_manager, m_params));
+            setup_i_arith();
             break;
         }
     }

diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
@@ -751,12 +751,14 @@ class theory_lra::imp {
         init_solver();
     }
 
-    bool internalize_atom(app * atom, bool gate_ctx) {
-        return internalize_atom_strict(atom, gate_ctx);
-
+    void internalize_is_int(app * n) {
+        SASSERT(a.is_is_int(n));
+        (void) mk_enode(n);
+        if (!ctx().relevancy())
+            mk_is_int_axiom(n);        
     }
 
-    bool internalize_atom_strict(app * atom, bool gate_ctx) {
+    bool internalize_atom(app * atom, bool gate_ctx) {
         SASSERT(!ctx().b_internalized(atom));
         bool_var bv = ctx().mk_bool_var(atom);
         ctx().set_var_theory(bv, get_id());
@@ -772,6 +774,10 @@ class theory_lra::imp {
             v = internalize_def(to_app(n1));
             k = lp_api::lower_t;
         }    
+        else if (a.is_is_int(atom)) {
+            internalize_is_int(atom);
+            return true;
+        }
         else {
             TRACE("arith", tout << "Could not internalize " << mk_pp(atom, m) << "\n";);
             found_not_handled(atom);
@@ -1527,7 +1533,7 @@ class theory_lra::imp {
             return m_imp.bound_is_interesting(j, kind, v);
         }
 
-        virtual void consume(rational const& v, unsigned j) {
+        void consume(rational const& v, lp::constraint_index j) override {
             m_imp.set_evidence(j);
             m_imp.m_explanation.push_back(std::make_pair(v, j));
         }
@@ -2619,12 +2625,17 @@ class theory_lra::imp {
             coeff = rational::zero();
         }
         lp::impq term_max;
-        if (m_solver->maximize_term(coeffs, term_max)) {
+        lp::lp_status st = m_solver->maximize_term(coeffs, term_max);
+        if (st == lp::lp_status::OPTIMAL) {
             blocker = mk_gt(v);
             inf_rational val(term_max.x + coeff, term_max.y);
             return inf_eps(rational::zero(), val);
+        } if (st == lp::lp_status::FEASIBLE) {
+            lp_assert(false); // not implemented
+            // todo: what to return?
         }
         else {
+            SASSERT(st == lp::lp_status::UNBOUNDED);
             TRACE("arith", tout << "Unbounded " << v << "\n";);
             has_shared = false;
             blocker = m.mk_false();

diff --git a/src/tactic/smtlogics/qflia_tactic.cpp b/src/tactic/smtlogics/qflia_tactic.cpp
@@ -228,18 +228,6 @@ tactic * mk_qflia_tactic(ast_manager & m, params_ref const & p) {
 #endif
                                main_p);
 
-    //
-
-
-    // tactic * st = using_params(and_then(preamble_st,
-    //                                     or_else(mk_ilp_model_finder_tactic(m),
-    //                                             mk_pb_tactic(m),
-    //                                             and_then(fail_if_not(mk_is_quasi_pb_probe()), 
-    //                                                      using_params(mk_lia2sat_tactic(m), quasi_pb_p),
-    //                                                      mk_fail_if_undecided_tactic()),
-    //                                             mk_bounded_tactic(m),
-    //                                             mk_smt_tactic())),
-    //                            main_p);
 
     st->updt_params(p);
     return st;

diff --git a/src/test/lp/lp.cpp b/src/test/lp/lp.cpp
@@ -44,20 +44,25 @@
 #include "util/lp/numeric_pair.h"
 #include "util/lp/binary_heap_upair_queue.h"
 #include "util/lp/stacked_value.h"
-#include "util/lp/stacked_unordered_set.h"
 #include "util/lp/int_set.h"
 #include "util/stopwatch.h"
-#include "util/lp/stacked_map.h"
 #include <cstdlib>
 #include "test/lp/gomory_test.h"
 #include "util/lp/matrix.h"
 #include "util/lp/hnf.h"
 #include "util/lp/square_sparse_matrix_def.h"
 #include "util/lp/lu_def.h"
 #include "util/lp/general_matrix.h"
+#include "util/lp/bound_propagator.h"
 namespace lp {
 unsigned seed = 1;
 
+    class my_bound_propagator : public bound_propagator {
+    public:
+        my_bound_propagator(lar_solver & ls): bound_propagator(ls) {}
+        void consume(mpq const& v, lp::constraint_index j) override {}
+    };
+
 random_gen g_rand;
 static unsigned my_random() {
     return g_rand();
@@ -1942,44 +1947,6 @@ void setup_args_parser(argument_parser & parser) {
 
 struct fff { int a; int b;};
 
-void test_stacked_map_itself() {
-    vector<int> v(3,0);
-    for(auto u : v)
-        std::cout << u << std::endl;    
-
-    std::unordered_map<int, fff> foo;
-    fff l;
-    l.a = 0;
-    l.b =1;
-    foo[1] = l;
-    int r = 1;
-    int k = foo[r].a;
-    std::cout << k << std::endl;
-
-    stacked_map<int, double> m;
-    m[0] = 3;
-    m[1] = 4;
-    m.push();
-    m[1] = 5;
-    m[2] = 2;
-    m.pop();
-    m.erase(2);
-    m[2] = 3;
-    m.erase(1);
-    m.push();
-    m[3] = 100;
-    m[4] = 200;
-    m.erase(1);
-    m.push();
-    m[5] = 300;
-    m[6] = 400;
-    m[5] = 301;
-    m.erase(5);
-    m[3] = 122;
-
-    m.pop(2);
-    m.pop();
-}
 
 void test_stacked_unsigned() {
     std::cout << "test stacked unsigned" << std::endl;
@@ -2038,36 +2005,10 @@ void test_stacked_vector() {
 
 }
 
-void test_stacked_set() {
-#ifdef Z3DEBUG
-    std::cout << "test_stacked_set" << std::endl;
-    stacked_unordered_set<int> s;
-    s.insert(1);
-    s.insert(2);
-    s.insert(3);
-    std::unordered_set<int> scopy = s();
-    s.push();
-    s.insert(4);
-    s.pop();
-    lp_assert(s() == scopy);
-    s.push();
-    s.push();
-    s.insert(4);
-    s.insert(5);
-    s.push();
-    s.insert(4);
-    s.pop(3);
-    lp_assert(s() == scopy);
-#endif
-}
 
 void test_stacked() {
-    std::cout << "test_stacked_map()" << std::endl;
-    test_stacked_map_itself();
     test_stacked_value();
     test_stacked_vector();
-    test_stacked_set();
-
 }
 
 char * find_home_dir() {
@@ -2815,7 +2756,7 @@ void test_bound_propagation_one_small_sample1() {
     vector<implied_bound> ev;
     ls.add_var_bound(a, LE, mpq(1));
     ls.solve();
-    bound_propagator bp(ls);
+    my_bound_propagator bp(ls);
     ls.propagate_bounds_for_touched_rows(bp);
     std::cout << " bound ev from test_bound_propagation_one_small_sample1" << std::endl;
     for (auto & be : bp.m_ibounds)  {
@@ -2868,7 +2809,7 @@ void test_bound_propagation_one_row() {
     vector<implied_bound> ev;
     ls.add_var_bound(x0, LE, mpq(1));
     ls.solve();
-    bound_propagator bp(ls);
+    my_bound_propagator bp(ls);
     ls.propagate_bounds_for_touched_rows(bp);
 } 
 void test_bound_propagation_one_row_with_bounded_vars() {
@@ -2884,7 +2825,7 @@ void test_bound_propagation_one_row_with_bounded_vars() {
     ls.add_var_bound(x0, LE, mpq(3));
     ls.add_var_bound(x0, LE, mpq(1));
     ls.solve();
-    bound_propagator bp(ls);
+    my_bound_propagator bp(ls);
     ls.propagate_bounds_for_touched_rows(bp);
 }
 void test_bound_propagation_one_row_mixed() {
@@ -2898,7 +2839,7 @@ void test_bound_propagation_one_row_mixed() {
     vector<implied_bound> ev;
     ls.add_var_bound(x1, LE, mpq(1));
     ls.solve();
-    bound_propagator bp(ls);
+    my_bound_propagator bp(ls);
     ls.propagate_bounds_for_touched_rows(bp);
 } 
 
@@ -2921,7 +2862,7 @@ void test_bound_propagation_two_rows() {
     vector<implied_bound> ev;
     ls.add_var_bound(y, LE, mpq(1));
     ls.solve();
-    bound_propagator bp(ls);
+    my_bound_propagator bp(ls);
     ls.propagate_bounds_for_touched_rows(bp);
 } 
 
@@ -2941,7 +2882,7 @@ void test_total_case_u() {
     vector<implied_bound> ev;
     ls.add_var_bound(z, GE, zero_of_type<mpq>());
     ls.solve();
-    bound_propagator bp(ls);
+    my_bound_propagator bp(ls);
     ls.propagate_bounds_for_touched_rows(bp);
 }
 bool contains_j_kind(unsigned j, lconstraint_kind kind, const mpq & rs, const vector<implied_bound> & ev) {
@@ -2968,7 +2909,7 @@ void test_total_case_l(){
     vector<implied_bound> ev;
     ls.add_var_bound(z, LE, zero_of_type<mpq>());
     ls.solve();
-    bound_propagator bp(ls);
+    my_bound_propagator bp(ls);
     ls.propagate_bounds_for_touched_rows(bp);
     lp_assert(ev.size() == 4);
     lp_assert(contains_j_kind(x, GE, - one_of_type<mpq>(), ev));

diff --git a/src/test/simplex.cpp b/src/test/simplex.cpp
@@ -4,7 +4,6 @@ Copyright (c) 2015 Microsoft Corporation
 
 --*/
 
-#include "util/lp/sparse_matrix.h"
 #include "math/simplex/sparse_matrix_def.h"
 #include "math/simplex/simplex.h"
 #include "math/simplex/simplex_def.h"

diff --git a/src/util/lp/bound_propagator.h b/src/util/lp/bound_propagator.h
@@ -22,6 +22,6 @@ class bound_propagator {
                                       lp::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"; }
+    virtual void consume(mpq const& v, lp::constraint_index j) = 0;
 };
 }
diff --git a/src/util/lp/explanation.h b/src/util/lp/explanation.h
@@ -20,6 +20,7 @@ Revision History:
 #pragma once
 namespace lp {
 struct explanation {
+    void clear() { m_explanation.clear(); }
     vector<std::pair<mpq, constraint_index>> m_explanation;
     void push_justification(constraint_index j, const mpq& v) {
         m_explanation.push_back(std::make_pair(v, j));