bug fixes to LUT extraction, bug fix for real value case of freedom intervals

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

src/math/lp/int_solver.cpp

@@ -513,12 +513,12 @@ bool int_solver::shift_var(unsigned j, unsigned range) {
     }
 
     SASSERT(!inf_l && !inf_u);
-    mpq r = floor((u.x - l.x) / m);
+    mpq r = floor((u - l) / m);
     if (r < mpq(range)) range = static_cast<unsigned>(r.get_uint64());
     // the interval contains at least range multiples of m.
     // the number of multiples to the left of the value of j is floor((get_value(j) - l.x)/m)
     // shift either left or right of the current value by available multiples.
-    impq shift = impq(random() % (range + 1)) - impq(floor((x.x - l.x) / m));
+    impq shift = impq(random() % (range + 1)) - impq(floor((x - l) / m));
     impq new_val = x + m * shift;
     SASSERT(l <= new_val && new_val <= u);
     set_value_for_nbasic_column_ignore_old_values(j, new_val);    return true;

src/sat/sat_aig_cuts.cpp

@@ -632,7 +632,7 @@ namespace sat {
             }
             unsigned num_comp = (1 << n.size());
             for (unsigned i = 0; i < num_comp; ++i) {
-                bool parity = false;
+                bool parity = n.size() % 2 == 1;
                 m_clause.reset();
                 for (unsigned j = 0; j < n.size(); ++j) {
                     literal lit = m_literals[n.offset() + j];
@@ -645,6 +645,7 @@ namespace sat {
                     m_clause.push_back(lit);
                 }
                 m_clause.push_back(parity ? r : ~r);
+                TRACE("aig_simplifier", tout << "validate: " << m_clause << "\n";);
                 on_clause(m_clause);
             }
             return;

src/sat/sat_aig_simplifier.cpp

@@ -226,11 +226,14 @@ namespace sat {
             m_lits.reset();
             m_stats.m_xxors++;            
         };
+#if 0
+        // 
         xor_finder xf(s);
         xf.set(on_xor);
         xf(clauses);
+#endif
 
-        if (m_config.m_enable_lut) {
+        if (s.m_config.m_aig_lut) {
             std::function<void(uint64_t, bool_var_vector const&, bool_var)> on_lut = 
                 [&,this](uint64_t lut, bool_var_vector const& vars, bool_var v) {
                 m_stats.m_xluts++;

src/sat/sat_aig_simplifier.h

@@ -36,7 +36,6 @@ namespace sat {
         struct config {
             bool m_enable_units;            // enable learning units
             bool m_enable_dont_cares;       // enable applying don't cares to LUTs
-            bool m_enable_lut;              // enable lut finding
             bool m_learn_implies;           // learn binary clauses
             bool m_learned2aig;             // add learned clauses to AIGs used by cut-set enumeration
             bool m_validate_cuts;           // enable direct validation of generated cuts
@@ -45,7 +44,6 @@ namespace sat {
             config():
                 m_enable_units(true),
                 m_enable_dont_cares(true),
-                m_enable_lut(false),
                 m_learn_implies(false),
                 m_learned2aig(true),
                 m_validate_cuts(false), 

src/sat/sat_config.cpp

@@ -105,6 +105,7 @@ namespace sat {
         m_anf_exlin         = p.anf_exlin();
         m_aig_simplify      = p.aig();
         m_aig_delay         = p.aig_delay();
+        m_aig_lut           = p.aig_lut();
         m_lookahead_simplify = p.lookahead_simplify();
         m_lookahead_double = p.lookahead_double();
         m_lookahead_simplify_bca = p.lookahead_simplify_bca();

src/sat/sat_config.h

@@ -122,6 +122,7 @@ namespace sat {
         bool               m_binspr;
         bool               m_aig_simplify;
         unsigned           m_aig_delay;
+        bool               m_aig_lut;
         bool               m_anf_simplify;
         unsigned           m_anf_delay;
         bool               m_anf_exlin;

src/sat/sat_lut_finder.cpp

@@ -113,6 +113,12 @@ namespace sat {
         m_removed_clauses.append(m_clauses_to_remove);
         bool_var v;
         uint64_t lut = convert_combination(m_vars, v);
+        IF_VERBOSE(12, 
+                   for (clause* cp : m_clauses_to_remove) {
+                       verbose_stream() << *cp << "\n";
+                       verbose_stream() << v << ": " << m_vars << "\n";
+                   }
+                   display_mask(verbose_stream(), lut, 1u << m_vars.size()) << "\n";);
         m_on_lut(lut, m_vars, v);
     }
 
@@ -166,6 +172,13 @@ namespace sat {
         return update_combinations(mask);
     }
 
+    void lut_finder::set_combination(unsigned mask) {
+        if (!get_combination(mask)) { 
+            m_combination |= (1ull << mask); 
+            m_num_combinations++;
+        }
+    }
+
     bool lut_finder::update_combinations(unsigned mask) {
         unsigned num_missing = m_missing.size();
         for (unsigned k = 0; k < (1ul << num_missing); ++k) {
@@ -183,7 +196,7 @@ namespace sat {
     bool lut_finder::lut_is_defined(unsigned sz) {
         if (m_num_combinations < (1ull << (sz/2))) 
             return false;
-        for (unsigned i = 0; i < sz; ++i) {
+        for (unsigned i = sz; i-- > 0; ) {
             if (lut_is_defined(i, sz)) 
                 return true;
         }
@@ -221,7 +234,7 @@ namespace sat {
     bool lut_finder::lut_is_defined(unsigned i, unsigned sz) {
         uint64_t c = m_combination | (m_combination >> (1ull << (uint64_t)i));
         uint64_t m = m_masks[i];
-        if (sz < 6) m &= ((1ull << sz) - 1);
+        if (sz < 6) m &= ((1ull << (1ull << sz)) - 1);
         return (c & m) == m;
     }
 
@@ -235,16 +248,17 @@ namespace sat {
     uint64_t lut_finder::convert_combination(bool_var_vector& vars, bool_var& v) {
         SASSERT(lut_is_defined(vars.size()));
         unsigned i = 0;
-        for (; i < vars.size(); ++i) {
+        for (i = vars.size(); i-- > 0; ) {
             if (lut_is_defined(i, vars.size())) {
                 break;
             }
         }
+        unsigned nbits = 1u << vars.size();
         SASSERT(i < vars.size());
         v = vars[i];
         vars.erase(v);
         uint64_t r = 0;
-        uint64_t m = m_masks[vars.size()];
+        uint64_t m = m_masks[i];
         unsigned offset = 0;
         // example, if i = 2, then we are examining 
         // how m_combination evaluates at position xy0uv
@@ -253,7 +267,7 @@ namespace sat {
         // 
         for (unsigned j = 0; j < 64; ++j) {
             if (0 != (m & (1ull << j))) {
-                if (0 == (m_combination & (1ull << j))) {
+                if (0 != (m_combination & (1ull << j))) {
                     r |= 1ull << offset;
                 }
                 ++offset;
@@ -289,5 +303,11 @@ namespace sat {
         return filter;
     }
 
+    std::ostream& lut_finder::display_mask(std::ostream& out, uint64_t mask, unsigned sz) const {
+        for (unsigned i = 0; i < sz; ++i) {
+            out << ((0 != (((mask >> i)) & 0x1)) ? "1" : "0");
+        }
+        return out;
+    }
 
 }

src/sat/sat_lut_finder.h

@@ -51,12 +51,7 @@ namespace sat {
         clause_vector           m_removed_clauses;
         std::function<void (uint64_t, svector<bool_var> const& vars, bool_var v)> m_on_lut;
 
-        inline void set_combination(unsigned mask) { 
+        void set_combination(unsigned mask);
-            if (!get_combination(mask)) { 
-                m_combination |= (1ull << mask); 
-                m_num_combinations++;
-            }
-        }
         inline bool get_combination(unsigned mask) const { return (m_combination & (1ull << mask)) != 0; }
         bool lut_is_defined(unsigned sz);
         bool lut_is_defined(unsigned i, unsigned sz);
@@ -70,6 +65,7 @@ namespace sat {
         void init_clause_filter();
         void init_clause_filter(clause_vector& clauses);
         unsigned get_clause_filter(clause const& c);
+        std::ostream& display_mask(std::ostream& out, uint64_t mask, unsigned sz) const;
 
     public:
         lut_finder(solver& s) : s(s), m_max_lut_size(5) { }

src/sat/sat_params.pyg

@@ -75,6 +75,7 @@ def_module_params('sat',
                           ('anf.exlin', BOOL, False, 'enable extended linear simplification'), 
 		          ('aig', BOOL, False, 'enable AIG based simplification in-processing'),
 	                  ('aig.delay', UINT, 2, 'delay AIG simplification by in-processing round'),
+                          ('aig.lut',   BOOL, False, 'extract luts from clauses'),
                           ('lookahead.cube.cutoff', SYMBOL, 'depth', 'cutoff type used to create lookahead cubes: depth, freevars, psat, adaptive_freevars, adaptive_psat'),
                           # - depth: the maximal cutoff is fixed to the value of lookahead.cube.depth.
                           #          So if the value is 10, at most 1024 cubes will be generated of length 10.