add smt lookahead

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

src/smt/CMakeLists.txt

@@ -32,6 +32,7 @@ z3_add_component(smt
     smt_justification.cpp
     smt_kernel.cpp
     smt_literal.cpp
+    smt_lookahead.cpp
     smt_model_checker.cpp
     smt_model_finder.cpp
     smt_model_generator.cpp

src/smt/smt_context.cpp

@@ -1784,15 +1784,6 @@ namespace smt {
         m_bvar_inc *= INV_ACTIVITY_LIMIT;
     }
 
-    expr* context::next_decision() {
-        bool_var var;
-        lbool phase;
-        m_case_split_queue->next_case_split(var, phase);
-        if (var == null_bool_var) return m_manager.mk_true();
-        m_case_split_queue->unassign_var_eh(var);
-        return bool_var2expr(var);
-    }
-
     /**
        \brief Execute next case split, return false if there are no
        more case splits to be performed.

src/smt/smt_context.h

@@ -67,6 +67,7 @@ namespace smt {
 
     class context {
         friend class model_generator;
+        friend class lookahead;
     public:
         statistics                  m_stats;
 
@@ -1074,8 +1075,6 @@ namespace smt {
 
         enode * get_enode_eq_to(func_decl * f, unsigned num_args, enode * const * args);
 
-        expr* next_decision();
-
     protected:
         bool decide();
 

src/smt/smt_internalizer.cpp

@@ -900,6 +900,7 @@ namespace smt {
         expr * n              = m_b_internalized_stack.back();
         unsigned n_id         = n->get_id();
         bool_var v            = get_bool_var_of_id(n_id);
+        m_bool_var2expr[v]    = nullptr;
         TRACE("undo_mk_bool_var", tout << "undo_bool: " << v << "\n" << mk_pp(n, m_manager) << "\n" << "m_bdata.size: " << m_bdata.size()
               << " m_assignment.size: " << m_assignment.size() << "\n";);
         TRACE("mk_var_bug", tout << "undo_mk_bool: " << v << "\n";);

src/smt/smt_kernel.cpp

@@ -18,6 +18,7 @@ Revision History:
 --*/
 #include "smt/smt_kernel.h"
 #include "smt/smt_context.h"
+#include "smt/smt_lookahead.h"
 #include "ast/ast_smt2_pp.h"
 #include "smt/params/smt_params_helper.hpp"
 
@@ -202,8 +203,9 @@ namespace smt {
             m_kernel.get_guessed_literals(result);
         }
 
-        expr* next_decision() {
+        expr_ref next_cube() {
-            return m_kernel.next_decision();
+            lookahead lh(m_kernel);
+            return lh.choose();
         }
                 
         void collect_statistics(::statistics & st) const {
@@ -379,8 +381,8 @@ namespace smt {
         m_imp->get_guessed_literals(result);
     }
 
-    expr* kernel::next_decision() {
+    expr_ref kernel::next_cube() {
-        return m_imp->next_decision();
+        return m_imp->next_cube();
     }        
 
     std::ostream& kernel::display(std::ostream & out) const {

src/smt/smt_kernel.h

@@ -217,7 +217,7 @@ namespace smt {
         /**
            \brief return the next case split literal.
         */
-        expr* next_decision();
+        expr_ref next_cube();
 
         /**
            \brief retrieve depth of variables from decision stack.

src/smt/smt_lookahead.cpp

@@ -0,0 +1,134 @@
+/*++
+Copyright (c) 2006 Microsoft Corporation
+
+Module Name:
+
+    smt_lookahead.cpp
+
+Abstract:
+
+    Lookahead cuber for SMT
+
+Author:
+
+    nbjorner 2019-05-27.
+
+Revision History:
+
+--*/
+
+#include "ast/ast_smt2_pp.h"
+#include "smt/smt_lookahead.h"
+#include "smt/smt_context.h"
+
+namespace smt {
+
+    lookahead::lookahead(context& ctx): 
+        ctx(ctx), m(ctx.get_manager()) {}
+
+    double lookahead::get_score() {
+        double score = 0;
+        for (clause* cp : ctx.m_aux_clauses) {
+            unsigned nf = 0, nu = 0;
+            bool is_taut = false;
+            for (literal lit : *cp) {
+                switch (ctx.get_assignment(lit)) {
+                case l_false:
+                    if (ctx.get_assign_level(lit) > 0) {
+                        ++nf;
+                    }
+                    break;
+                case l_true:
+                    is_taut = true;
+                    break;
+                default:
+                    ++nu;
+                    break;
+                }
+            }
+            if (!is_taut && nf > 0) {
+                score += pow(0.5, nu);
+            }
+        }
+        return score;
+    }
+
+    struct lookahead::compare {
+        context& ctx;
+        compare(context& ctx): ctx(ctx) {}
+
+        bool operator()(bool_var v1, bool_var v2) const {
+            return ctx.get_activity(v1) > ctx.get_activity(v2);
+        }
+    };
+    
+    expr_ref lookahead::choose() {
+        ctx.pop_to_base_lvl();
+        unsigned sz = ctx.m_bool_var2expr.size();
+        bool_var best_v = null_bool_var;
+        double best_score = -1;
+        svector<bool_var> vars;
+        for (bool_var v = 0; v < static_cast<bool_var>(sz); ++v) {
+            expr* b = ctx.bool_var2expr(v);
+            if (b && ctx.get_assignment(v) == l_undef) {
+                vars.push_back(v);
+            }
+        }
+        compare comp(ctx);
+        std::sort(vars.begin(), vars.end(), comp);
+        
+        unsigned nf = 0, nc = 0, ns = 0, bound = 2000;
+        for (bool_var v : vars) {
+            if (!ctx.bool_var2expr(v)) continue;
+            literal lit(v, false);			
+            ctx.push_scope();
+            ctx.assign(lit, b_justification::mk_axiom(), true);
+            ctx.propagate();
+            bool inconsistent = ctx.inconsistent();
+            double score1 = get_score();
+            ctx.pop_scope(1);
+            if (inconsistent) {
+                ctx.assign(~lit, b_justification::mk_axiom(), false);
+                ctx.propagate();           
+                ++nf;
+                continue;
+            }
+
+            ctx.push_scope();
+            ctx.assign(~lit, b_justification::mk_axiom(), true);
+            ctx.propagate();
+            inconsistent = ctx.inconsistent();
+            double score2 = get_score();
+            ctx.pop_scope(1);
+            if (inconsistent) {
+                ctx.assign(lit, b_justification::mk_axiom(), false);
+                ctx.propagate(); 
+                ++nf;
+                continue;
+            }
+            double score = score1 + score2 + 1024*score1*score2;
+            if (score > best_score) {
+                best_score = score;
+                best_v = v;
+                bound += ns;
+                ns = 0;
+            }
+            ++nc;
+            ++ns;
+            if (ns > bound) {
+                break;
+            }
+        }
+        expr_ref result(m);
+        if (ctx.inconsistent()) {
+            result = m.mk_false();
+        }
+        else if (best_v != null_bool_var) {
+            result = ctx.bool_var2expr(best_v);
+        }
+        else {
+            result = m.mk_true();
+        }
+        return result;
+    }
+}

src/smt/smt_lookahead.h

@@ -0,0 +1,40 @@
+/*++
+Copyright (c) 2006 Microsoft Corporation
+
+Module Name:
+
+    smt_lookahead.h
+
+Abstract:
+
+    Lookahead solver for SMT
+
+Author:
+
+    nbjorner 2019-05-27.
+
+Revision History:
+
+--*/
+
+#pragma once
+
+#include "ast/ast.h"
+
+namespace smt {
+    class context;
+
+    class lookahead {
+        context&     ctx;
+        ast_manager& m;
+
+        struct compare;
+
+        double get_score();
+
+    public:
+        lookahead(context& ctx);
+
+        expr_ref choose();
+    };
+}

src/smt/smt_solver.cpp

@@ -42,7 +42,7 @@ namespace smt {
             expr_ref cube() {
                 switch (m_round) {
                 case 0:
-                    m_result = m_solver.m_context.next_decision();
+                    m_result = m_solver.m_context.next_cube();
                     break;
                 case 1:
                     m_result = m_solver.get_manager().mk_not(m_result);

src/solver/parallel_params.pyg

@@ -10,6 +10,7 @@ def_module_params('parallel',
 	                  ('conquer.delay', UINT, 10, 'delay of cubes until applying conquer'),
 	                  ('conquer.backtrack_frequency', UINT, 10, 'frequency to apply core minimization during conquer'),
                           ('simplify.exp', DOUBLE, 1, 'restart and inprocess max is multiplied by simplify.exp ^ depth'),
+                          ('simplify.max_conflicts', UINT, UINT_MAX, 'maximal number of conflicts during simplifcation phase'),
 	                  ('simplify.restart.max', UINT, 5000, 'maximal number of restarts during simplification phase'),
                           ('simplify.inprocess.max', UINT, 2, 'maximal number of inprocessing steps during simplification'),
                           ))

src/solver/parallel_tactic.cpp

@@ -297,6 +297,7 @@ class parallel_tactic : public tactic {
             p.set_uint("restart.max", pp.simplify_restart_max() * mult);
             p.set_bool("lookahead_simplify", true);
             p.set_bool("retain_blocked_clauses", retain_blocked);
+            p.set_uint("max_conflicts", pp.simplify_max_conflicts());
             if (m_depth > 1) p.set_uint("bce_delay", 0);
             get_solver().updt_params(p);
         }