From 973a32a015f9075657aabb649c37bf9c2aa57804 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 16 May 2021 13:50:41 -0700
Subject: [PATCH] na

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/math/polysat/linear_solver.cpp | 41 +++++++++++++++++++++++++-----
 src/math/polysat/linear_solver.h   | 41 ++++++++++++++++++++++++++++--
 2 files changed, 74 insertions(+), 8 deletions(-)

diff --git a/src/math/polysat/linear_solver.cpp b/src/math/polysat/linear_solver.cpp
index b7963e414..3e06e2019 100644
--- a/src/math/polysat/linear_solver.cpp
+++ b/src/math/polysat/linear_solver.cpp
@@ -13,6 +13,7 @@ Author:
 --*/
 
 #include "math/polysat/linear_solver.h"
+#include "math/polysat/fixplex_def.h"
 #include "math/polysat/solver.h"
 
 namespace polysat {
@@ -33,6 +34,13 @@ namespace polysat {
                 m_rows.pop_back();
                 break;
             }
+            case trail_i::add_mono_i: {
+                auto m = m_monomials.back();
+                m_mono2var.erase(m);
+                m_alloc.deallocate(m.num_vars*sizeof(unsigned), m.vars);
+                m_monomials.pop_back();
+                break;
+            }
             case trail_i::set_bound_i: {
                 auto [v, sz] = m_rows.back();
                 sz2fixplex(sz).restore_bound();
@@ -105,11 +113,12 @@ namespace polysat {
         auto& fp = sz2fixplex(sz);            
         m_trail.push_back(trail_i::set_bound_i);
         m_rows.push_back(std::make_pair(v, sz));
+        rational z(0), o(1);
         if (c.is_positive()) 
-            fp.set_bounds(v, rational::zero(), rational::zero());
+            fp.set_bounds(v, z, z);
         else 
-            fp.set_bounds(v, rational::one(), rational::power_of_two(sz) - 1);
-    }
+            fp.set_bounds(v, o, z);
+}
 
     void linear_solver::new_le(ule_constraint& c) {
         var_t v = internalize_pdd(c.lhs());
@@ -186,8 +195,17 @@ namespace polysat {
     }
 
     var_t linear_solver::mono2var(unsigned sz, unsigned_vector const& var) {
-        NOT_IMPLEMENTED_YET();
-        return 0;
+        mono_info m(sz, var.size(), var.data()), m1;
+        if (m_mono2var.find(m, m1))
+            return m1.var;
+        m.vars = static_cast<unsigned*>(m_alloc.allocate(var.size()*sizeof(unsigned)));
+        for (unsigned i = 0; i < var.size(); var.data()) 
+            m.vars[i] = var[i];
+        m.var = fresh_var(sz);
+        m_mono2var.insert(m);
+        m_monomials.push_back(m);
+        m_trail.push_back(trail_i::add_mono_i);
+        return m.var;
     }
 
     var_t linear_solver::pvar2var(unsigned sz, pvar v) {
@@ -222,9 +240,20 @@ namespace polysat {
     }
     
     // check integer modular feasibility under current bounds.
+    // and inequalities
     lbool linear_solver::check() { 
         lbool res = l_true;
-        // loop over fp solvers that have been touched and use make_feasible.        
+        for (auto* f : m_fix) {
+            if (!f)
+                continue;
+            lbool r = f->make_feasible();
+            if (r == l_false) {
+                // m_unsat_f = f;
+                return r;
+            }
+            if (r == l_undef)
+                res = l_undef;
+        }
         return res; 
     }
 
diff --git a/src/math/polysat/linear_solver.h b/src/math/polysat/linear_solver.h
index 9677a6f89..bd05dc6d1 100644
--- a/src/math/polysat/linear_solver.h
+++ b/src/math/polysat/linear_solver.h
@@ -25,6 +25,8 @@ Author:
 
 #pragma once
 
+#include "util/hashtable.h"
+#include "util/small_object_allocator.h"
 #include "math/polysat/fixplex.h"
 #include "math/polysat/constraint.h"
 #include "math/polysat/eq_constraint.h"
@@ -38,10 +40,40 @@ namespace polysat {
         enum trail_i {
             inc_level_i,
             add_var_i,
+            add_mono_i,
             set_bound_i,
             add_row_i
         };
 
+        struct mono_info {
+            unsigned  sz { 0 };
+            unsigned  num_vars { 0 }; 
+            unsigned* vars { nullptr };
+            unsigned  var { 0 };            
+            mono_info(unsigned sz, unsigned num_vars, unsigned* vars):
+                sz(sz),
+                num_vars(num_vars),
+                vars(vars)
+            {}
+            mono_info() {}
+            struct hash {
+                unsigned operator()(mono_info const& i) const {
+                    // TODO
+                    return 0;
+                }
+            };
+            struct eq {
+                 bool operator()(mono_info const& a, mono_info const& b) const {
+                     if (a.num_vars != b.num_vars)
+                         return false;
+                     for (unsigned i = 0; i < a.num_vars; ++i)
+                         if (a.vars[i] != b.vars[i])
+                             return false;
+                     return a.sz == b.sz;
+                }
+            };
+        };
+
         solver&                  s;
         scoped_ptr_vector<fixplex_base> m_fix;
         svector<trail_i>         m_trail;
@@ -51,8 +83,12 @@ namespace polysat {
 
         svector<var_t>           m_vars;
         vector<rational>         m_coeffs;
-        svector<std::pair<var_t, var_t>>           m_bool_var2row;
+        svector<std::pair<var_t, var_t>> m_bool_var2row;
+
+        hashtable<mono_info, mono_info::hash, mono_info::eq> m_mono2var;
         unsigned_vector          m_sz2num_vars;
+        small_object_allocator   m_alloc;
+        svector<mono_info>       m_monomials;
 
         fixplex_base& sz2fixplex(unsigned sz);
 
@@ -80,7 +116,8 @@ namespace polysat {
         //
     public:
         linear_solver(solver& s):
-            s(s) 
+            s(s),
+            m_alloc("mononials")
         {}
 
         void push();