snapshot adding simplex

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

scripts/mk_project.py

@@ -49,7 +49,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', 'proof_checker', 'pattern', 'parser_util'])
+                    'substitution', 'grobner', 'euclid', 'simplex', 'proof_checker', 'pattern', 'parser_util'])
     add_lib('user_plugin', ['smt'], 'smt/user_plugin')
     add_lib('bv_tactics', ['tactic', 'bit_blaster'], 'tactic/bv')
     add_lib('fuzzing', ['ast'], 'test/fuzzing')

src/smt/params/smt_params_helper.pyg

@@ -46,6 +46,7 @@ def_module_params(module_name='smt',
                           ('pb.conflict_frequency', UINT, 0, 'conflict frequency for Pseudo-Boolean theory'),
                           ('pb.learn_complements', BOOL, True, 'learn complement literals for Pseudo-Boolean theory'),
                           ('pb.enable_compilation', BOOL, True, 'enable compilation into sorting circuits for Pseudo-Boolean'),
+                          ('pb.enable_simplex', BOOL, False, 'enable simplex to check rational feasibility'),
                           ('array.weak', BOOL, False, 'weak array theory'),
                           ('array.extensional', BOOL, True, 'extensional array theory')
                           ))

src/smt/params/theory_pb_params.cpp

@@ -24,4 +24,5 @@ void theory_pb_params::updt_params(params_ref const & _p) {
     m_pb_conflict_frequency = p.pb_conflict_frequency();
     m_pb_learn_complements = p.pb_learn_complements();
     m_pb_enable_compilation = p.pb_enable_compilation();
+    m_pb_enable_simplex = p.pb_enable_simplex();
 }

src/smt/params/theory_pb_params.h

@@ -26,10 +26,12 @@ struct theory_pb_params {
     unsigned m_pb_conflict_frequency;
     bool     m_pb_learn_complements;
     bool     m_pb_enable_compilation;
+    bool     m_pb_enable_simplex;
     theory_pb_params(params_ref const & p = params_ref()):
         m_pb_conflict_frequency(0),
         m_pb_learn_complements(true),
-        m_pb_enable_compilation(true)
+        m_pb_enable_compilation(true),
+        m_pb_enable_simplex(false)    
     {}
     
     void updt_params(params_ref const & p);

src/smt/theory_pb.cpp

@@ -61,6 +61,20 @@ namespace smt {
         };
     };
 
+    unsigned theory_pb::ineq::get_hash() const {
+        return get_composite_hash<arg_t, ineq::kind_hash, ineq::child_hash>(m_args, m_args.size());
+    }
+
+    bool theory_pb::ineq::operator==(ineq const& other) const {
+        if (size() != other.size()) return false;
+        for (unsigned i = 0; i < size(); ++i) {
+            if (lit(i) != other.lit(i)) return false;
+            if (coeff(i) != other.coeff(i)) return false;
+        }
+        return true;
+    }
+
+
     void theory_pb::ineq::negate() {
         SASSERT(!m_is_eq);
         m_lit.neg();
@@ -101,6 +115,16 @@ namespace smt {
         util.prune(m_args, m_k, m_is_eq);        
     }
 
+    void theory_pb::ineq::remove_negations() {
+        for (unsigned i = 0; i < size(); ++i) {
+            if (lit(i).sign()) {
+                m_args[i].first.neg();
+                m_args[i].second.neg();
+                m_k += coeff(i);
+            }
+        }
+    }
+
     lbool theory_pb::ineq::normalize() {
         pb_lit_rewriter_util pbu;
         pb_rewriter_util<pb_lit_rewriter_util> util(pbu);
@@ -152,9 +176,10 @@ namespace smt {
         m_lemma(null_literal, false),
         m_max_compiled_coeff(rational(8))
     {        
-        m_learn_complements = p.m_pb_learn_complements;
+        m_learn_complements  = p.m_pb_learn_complements;
         m_conflict_frequency = p.m_pb_conflict_frequency;
         m_enable_compilation = p.m_pb_enable_compilation;
+        m_enable_simplex     = p.m_pb_enable_simplex;
     }
 
     theory_pb::~theory_pb() {
@@ -273,6 +298,47 @@ namespace smt {
         m_ineqs.insert(abv, c);
         m_ineqs_trail.push_back(abv);
 
+        if (m_enable_simplex) {
+            //
+            // TBD: using abv as slack identity doesn't quite 
+            // work if psuedo-Booleans are used 
+            // in a nested way. So assume 
+            //
+
+            //
+            // TBD: track and delete rows.
+            // 
+            ineq rep(*c);
+            rep.remove_negations();  // normalize representative
+            numeral k = rep.k();
+            theory_var slack;
+            bool_var abv2;
+            row r;
+            if (m_ineq_rep.find(rep, abv2)) {
+                slack = abv2; 
+                r = m_ineq_row_info.find(abv2).m_row;
+                TRACE("pb", tout << "Found: " << abv << " |-> " << slack << " " << m_ineq_row_info.find(abv2).m_bound << " vs. " << k << "\n";);
+            }
+            else {
+                m_ineq_rep.insert(rep, abv);
+                svector<unsigned> vars;
+                unsynch_mpz_manager mgr;
+                scoped_mpz_vector coeffs(mgr);
+                for (unsigned i = 0; i < rep.size(); ++i) {
+                    unsigned v = rep.lit(i).var();
+                    std::cout << v << "\n";
+                    m_simplex.ensure_var(v);
+                    vars.push_back(v);
+                    coeffs.push_back(rep.coeff(i).to_mpq().numerator());
+                }
+                slack = abv;
+                m_simplex.ensure_var(abv);
+                r = m_simplex.add_row(vars.size(), slack, vars.c_ptr(), coeffs.c_ptr());
+                TRACE("pb", tout << "New row: " << abv << " " << k << "\n";);
+            }
+            m_ineq_row_info.insert(abv, row_info(slack, k, rep, r));
+        }
+
         TRACE("pb", display(tout, *c););
 
         return true;

src/smt/theory_pb.h

@@ -24,6 +24,7 @@ Notes:
 #include "pb_decl_plugin.h"
 #include "smt_clause.h"
 #include "theory_pb_params.h"
+#include "simplex.h"
 
 namespace smt {
     class theory_pb : public theory {
@@ -37,6 +38,8 @@ namespace smt {
         class  negate_ineq;
         typedef rational numeral;
         typedef vector<std::pair<literal, numeral> > arg_t;
+        typedef simplex::simplex<simplex::mpz_ext> simplex;
+        typedef simplex::row row;
 
         struct stats {
             unsigned m_num_conflicts;
@@ -69,6 +72,8 @@ namespace smt {
             unsigned        m_compilation_threshold;
             lbool           m_compiled;
 
+            ineq(): m_lit(null_literal), m_is_eq(false) {}
+
             ineq(literal l, bool is_eq) : m_lit(l), m_is_eq(is_eq) {
                 reset();
             }
@@ -111,12 +116,46 @@ namespace smt {
 
             void prune();
 
+            void remove_negations();
+
             bool well_formed() const;
 
             app_ref to_expr(context& ctx, ast_manager& m);
 
             bool is_eq() const { return m_is_eq; }
             bool is_ge() const { return !m_is_eq; }
+
+            unsigned get_hash() const;
+            bool operator==(ineq const& other) const;
+
+            struct hash {
+                unsigned operator()(ineq const& i) const { return i.get_hash(); }
+            };
+            struct eq {
+                bool operator()(ineq const& a, ineq const& b) const { 
+                    return a == b;
+                }
+            };
+            struct child_hash {
+                unsigned operator()(arg_t const& args, unsigned idx) const {
+                    return args[idx].first.hash() ^ args[idx].second.hash();
+                }
+            };
+            struct kind_hash {
+                unsigned operator()(arg_t const& args) const {
+                    return args.size();
+                }
+            };
+        };
+
+        struct row_info {
+            unsigned     m_slack;   // slack variable in simplex tableau
+            numeral      m_bound;   // bound
+            ineq         m_rep;     // representative
+            row          m_row;
+            row_info(theory_var slack, numeral const& b, ineq const& r, row const& ro):
+                m_slack(slack), m_bound(b), m_rep(r), m_row(ro) {}
+            row_info(): m_slack(0) {}
         };
 
         typedef ptr_vector<ineq> watch_list;
@@ -125,6 +164,9 @@ namespace smt {
         u_map<watch_list*>       m_lwatch;      // per literal.
         u_map<watch_list*>       m_vwatch;      // per variable.
         u_map<ineq*>             m_ineqs;       // per inequality.
+        map<ineq, bool_var, ineq::hash, ineq::eq>      m_ineq_rep;       // Simplex: representative inequality
+        u_map<row_info>          m_ineq_row_info;  // Simplex: row information per variable.
+        simplex                  m_simplex;        // Simplex
         unsigned_vector          m_ineqs_trail;
         unsigned_vector          m_ineqs_lim;
         literal_vector           m_literals;    // temporary vector
@@ -134,6 +176,7 @@ namespace smt {
         unsigned                 m_conflict_frequency;
         bool                     m_learn_complements;
         bool                     m_enable_compilation;
+        bool                     m_enable_simplex;
         rational                 m_max_compiled_coeff;
 
         // internalize_atom:

src/tactic/arith/elim01_tactic.cpp

@@ -127,7 +127,7 @@ public:
     elim01_tactic(ast_manager & _m, params_ref const & p):
         m(_m),
         a(m),
-        m_max_hi_default(1),
+        m_max_hi_default(8),
         m_max_hi(rational(m_max_hi_default)) {
     }