lookeahead updates

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

src/api/c++/z3++.h

@@ -2175,6 +2175,42 @@ namespace z3 {
     };
     inline std::ostream & operator<<(std::ostream & out, optimize const & s) { out << Z3_optimize_to_string(s.ctx(), s.m_opt); return out; }
 
+    class fixedpoint : public object {
+        Z3_fixedpoint m_fp;
+    public:
+        fixedpoint(context& c):object(c) { mfp = Z3_mk_fixedpoint(c); Z3_fixedpoint_inc_ref(c, m_fp); }
+        ~fixedpoint() { Z3_fixedpoint_dec_ref(ctx(), m_fp); }
+        operator Z3_fixedpoint() const { return m_fp; }        
+        void from_string(char const* s) { Z3_fixedpoint_from_string(ctx(), m_fp, s); check_error(); }
+        void from_file(char const* s) { Z3_fixedpoint_from_file(ctx(), m_fp, s); check_error(); }
+        void add_rule(expr& rule, symbol const& name) { Z3_fixedpoint_add_rule(ctx(), m_fp, rule, name); check_error(); }
+        void add_fact(func_decl& f, unsigned const* args) { Z3_fixedpoint_add_fact(ctx(), m_fp, f, f.num_args(), args); check_error(); }
+        check_result query(expr& q) { Z3_lbool r = Z3_fixedpoint_query(ctx(), m_fp, q); check_error(); to_check_result(r); }
+        check_result query(func_decl_vector& relations) { 
+            array<Z3_func_decl> rs(relations);
+            Z3_lbool r = Z3_fixedpoint_query_relations(ctx(), m_fp, rs.size(), rs.ptr()); 
+            check_error(); 
+            return to_check_result(r); 
+        }
+        expr get_answer() { Z3_ast r = Z3_fixedpoint_get_answer(ctx(), m_fp); check_error(); return expr(ctx(), r); }
+        std::string reason_unknown() { return Z3_fixedpoint_get_reason_unknown(ctx(), m_fp); }
+        void update_rule(expr& rule, synbol const& name) { Z3_fixedpoint_update_rule(ctx(), m_fp, rule, name); check_error(); }
+        unsigned get_num_levels(func_decl& p) { unsigned r = Z3_fixedpoint_get_num_levels(ctx(), m_fp, p); check_error(); return r; }
+        expr get_cover_delta(int level, func_decl& p) { return Z3_fixedpoint_get_cover_delta(ctx(), m_fp, level, p); check_error();  }
+        void add_cover(int level, func_decl& p, expr& property) { Z3_fixedpoint_add_cover(ctx(), m_fp, level, p, property); check_error();  }
+        stats statistics() const { Z3_stats r = Z3_fixedpoint_get_statistics(ctx(), m_fp); check_error(); return stats(ctx(), r); }
+        void register_relation(func_decl& p) { Z3_fixedpoint_register_relation(ctx(), m_fp, p); }
+        expr_vector assertions() const { Z3_ast_vector r = Z3_fixedpoint_get_assertions(ctx(), m_fp); check_error(); return expr_vector(ctx(), r); }
+        expr_vector rules() const { Z3_ast_vector r = Z3_fixedpoint_get_rules(ctx(), m_fp); check_error(); return expr_vector(ctx(), r); }
+        void set(params const & p) { Z3_fixedpoint_set_params(ctx(), m_fp, p); check_error(); }
+        std::string help() const { return Z3_fixedpoint_get_help(ctx(), m_fp); }
+        param_descrs get_param_descrs() { return param_descrs(ctx(), Z3_fixedpoint_get_param_descrs(ctx(), m_fp)); }
+        std::string to_string() { return Z3_fixedpoint_to_string(ctx(), m_fp); }
+        void push() { Z3_fixedpoint_push(ctx(), m_fp); check_error(); }
+        void pop() { Z3_fixedpoint_pop(ctx(), m_fp); check_error(); }
+    };
+    inline std::ostream & operator<<(std::ostream & out, fixedpoint const & f) { return out << Z3_fixedpoint_to_string(f.ctx(), f); }
+
     inline tactic fail_if(probe const & p) {
         Z3_tactic r = Z3_tactic_fail_if(p.ctx(), p);
         p.check_error();

src/sat/sat_lookahead.h

@@ -290,7 +290,7 @@ namespace sat {
                 get_scc();
                 find_heights();
                 construct_lookahead_table();
-            }
+            }            
         }
 
         struct candidate {
@@ -314,7 +314,10 @@ namespace sat {
                 if (!m_candidates.empty()) break;
                 if (is_sat()) {
                     return false;
-                }            
+                }         
+                if (newbies) {
+                    TRACE("sat", tout << sum << "\n";);
+                }
             }
             SASSERT(!m_candidates.empty());
             // cut number of candidates down to max_num_cand.
@@ -398,16 +401,27 @@ namespace sat {
                 literal l(*it, false);
                 literal_vector const& lits1 = m_binary[l.index()];
                 for (unsigned i = 0; i < lits1.size(); ++i) {
-                    if (!is_true(lits1[i])) return false;
+                    if (!is_true(lits1[i])) {
+                        TRACE("sat", tout << l << " " << lits1[i] << "\n";);
+                        return false;
+                    }
                 }
-                literal_vector const& lits2 = m_binary[(~l).index()];
+                l.neg();
+                literal_vector const& lits2 = m_binary[l.index()];
                 for (unsigned i = 0; i < lits2.size(); ++i) {
-                    if (!is_true(lits2[i])) return false;
+                    if (!is_true(lits2[i])) {
+                        TRACE("sat", tout << l << " " << lits2[i] << "\n";);
+                        return false;
+                    }
                 }
             }
             for (unsigned i = 0; i < m_clauses.size(); ++i) {
                 clause& c = *m_clauses[i];
-                if (!is_true(c[0]) && !is_true(c[1])) return false;
+                unsigned j = 0;
+                for (; j < c.size() && !is_true(c[j]); ++j) {}
+                if (j == c.size()) {
+                    return false;
+                }
             }
             return true;
         }
@@ -645,8 +659,8 @@ namespace sat {
             literal best = v;
             float best_rating = get_rating(v);
             set_rank(v, UINT_MAX);
-            m_settled.push_back(t);
             while (t != v) {
+                m_settled.push_back(t);
                 SASSERT(t != ~v);
                 set_rank(t, UINT_MAX);
                 set_parent(t, v);
@@ -657,6 +671,7 @@ namespace sat {
                 }
                 t = get_link(t);
             }
+            m_settled.push_back(v);
             set_parent(v, v);
             set_vcomp(v, best);
             if (get_rank(~v) == UINT_MAX) {
@@ -705,6 +720,7 @@ namespace sat {
         }
 
         void find_heights() {
+            TRACE("sat", tout << m_settled << "\n";);
             literal pp = null_literal;
             set_child(pp, null_literal);
             unsigned h = 0;

src/sat/sat_simplifier.cpp

@@ -283,7 +283,11 @@ namespace sat {
             unsigned sz = c.size();
             if (sz == 0) {
                 s.set_conflict(justification());
-                return;
+                for (; it != end; ++it) {
+                    *it2 = *it;
+                    ++it2;
+                }
+                break;
             }
             if (sz == 1) {
                 s.assign(c[0], justification());