Merge pull request #999 from mtrberzi/theory-aware-branching

Theory-aware branching heuristic

src/smt/params/smt_params.h

@@ -66,7 +66,8 @@ enum case_split_strategy {
     CS_ACTIVITY_WITH_CACHE, // case split based on activity and cache the activity
     CS_RELEVANCY, // case split based on relevancy
     CS_RELEVANCY_ACTIVITY, // case split based on relevancy and activity
-    CS_RELEVANCY_GOAL // based on relevancy and the current goal
+    CS_RELEVANCY_GOAL, // based on relevancy and the current goal
+    CS_ACTIVITY_THEORY_AWARE_BRANCHING // activity-based case split, but theory solvers can manipulate activity
 };
 
 struct smt_params : public preprocessor_params, 

src/smt/params/smt_params_helper.pyg

@@ -11,7 +11,7 @@ def_module_params(module_name='smt',
                           ('phase_selection', UINT, 3, 'phase selection heuristic: 0 - always false, 1 - always true, 2 - phase caching, 3 - phase caching conservative, 4 - phase caching conservative 2, 5 - random, 6 - number of occurrences'),
                           ('restart_strategy', UINT, 1, '0 - geometric, 1 - inner-outer-geometric, 2 - luby, 3 - fixed, 4 - arithmetic'),
                           ('restart_factor', DOUBLE, 1.1, 'when using geometric (or inner-outer-geometric) progression of restarts, it specifies the constant used to multiply the currect restart threshold'),
-                          ('case_split', UINT, 1, '0 - case split based on variable activity, 1 - similar to 0, but delay case splits created during the search, 2 - similar to 0, but cache the relevancy, 3 - case split based on relevancy (structural splitting), 4 - case split on relevancy and activity, 5 - case split on relevancy and current goal'),
+                          ('case_split', UINT, 1, '0 - case split based on variable activity, 1 - similar to 0, but delay case splits created during the search, 2 - similar to 0, but cache the relevancy, 3 - case split based on relevancy (structural splitting), 4 - case split on relevancy and activity, 5 - case split on relevancy and current goal, 6 - activity-based case split with theory-aware branching activity'),
                           ('delay_units', BOOL, False, 'if true then z3 will not restart when a unit clause is learned'),
                           ('delay_units_threshold', UINT, 32, 'maximum number of learned unit clauses before restarting, ignored if delay_units is false'),
                           ('pull_nested_quantifiers', BOOL, False, 'pull nested quantifiers'),

src/smt/smt_case_split_queue.cpp

@@ -22,9 +22,13 @@ Revision History:
 #include"stopwatch.h"
 #include"for_each_expr.h"
 #include"ast_pp.h"
+#include"map.h"
+#include"hashtable.h"
 
 namespace smt {
 
+    typedef map<bool_var, double, int_hash, default_eq<bool_var> > theory_var_priority_map;
+
     struct bool_var_act_lt {
         svector<double> const & m_activity;
         bool_var_act_lt(svector<double> const & a):m_activity(a) {}
@@ -35,6 +39,27 @@ namespace smt {
 
     typedef heap<bool_var_act_lt> bool_var_act_queue;
 
+    struct theory_aware_act_lt {
+        svector<double> const & m_activity;
+        theory_var_priority_map const & m_theory_var_priority;
+        theory_aware_act_lt(svector<double> const & act, theory_var_priority_map const & a):m_activity(act),m_theory_var_priority(a) {}
+        bool operator()(bool_var v1, bool_var v2) const {
+            double p_v1, p_v2;
+            if (!m_theory_var_priority.find(v1, p_v1)) {
+                p_v1 = 0.0;
+            }
+            if (!m_theory_var_priority.find(v2, p_v2)) {
+                p_v2 = 0.0;
+            }
+	    // add clause activity
+	    p_v1 += m_activity[v1];
+	    p_v2 += m_activity[v2];
+            return p_v1 > p_v2;
+        }
+    };
+
+    typedef heap<theory_aware_act_lt> theory_aware_act_queue;
+
     /**
        \brief Case split queue based on activity and random splits.
     */
@@ -1086,16 +1111,130 @@ namespace smt {
                 m_params.m_qi_eager_threshold += start_gen;
         }
     };
-   
+
+    class theory_aware_branching_queue : public case_split_queue {
+    protected:
+        context &          m_context;
+        smt_params &       m_params;
+        theory_var_priority_map m_theory_var_priority;
+        theory_aware_act_queue m_queue;
+
+        int_hashtable<int_hash, default_eq<bool_var> > m_theory_vars;
+        map<bool_var, lbool, int_hash, default_eq<bool_var> > m_theory_var_phase;
+    public:
+        theory_aware_branching_queue(context & ctx, smt_params & p):
+            m_context(ctx),
+            m_params(p),
+            m_theory_var_priority(),
+            m_queue(1024, theory_aware_act_lt(ctx.get_activity_vector(), m_theory_var_priority)) {
+        }
+
+        virtual void activity_increased_eh(bool_var v) {
+            if (m_queue.contains(v))
+                m_queue.decreased(v);
+        }
+
+        virtual void mk_var_eh(bool_var v) {
+            m_queue.reserve(v+1);
+            m_queue.insert(v);
+        }
+
+        virtual void del_var_eh(bool_var v) {
+            if (m_queue.contains(v))
+                m_queue.erase(v);
+        }
+
+        virtual void unassign_var_eh(bool_var v) {
+            if (!m_queue.contains(v))
+                m_queue.insert(v);
+        }
+
+        virtual void relevant_eh(expr * n) {}
+
+        virtual void init_search_eh() {}
+
+        virtual void end_search_eh() {}
+
+        virtual void reset() {
+            m_queue.reset();
+        }
+
+        virtual void push_scope() {}
+
+        virtual void pop_scope(unsigned num_scopes) {}
+
+        virtual void next_case_split(bool_var & next, lbool & phase) {
+            int threshold = static_cast<int>(m_params.m_random_var_freq * random_gen::max_value());
+            SASSERT(threshold >= 0);
+            if (m_context.get_random_value() < threshold) {
+                SASSERT(m_context.get_num_b_internalized() > 0);
+                next = m_context.get_random_value() % m_context.get_num_b_internalized(); 
+                TRACE("random_split", tout << "next: " << next << " get_assignment(next): " << m_context.get_assignment(next) << "\n";);
+                if (m_context.get_assignment(next) == l_undef)
+                    return;
+            }
+
+            while (!m_queue.empty()) {
+                next = m_queue.erase_min();
+                if (m_context.get_assignment(next) == l_undef)
+                    return;
+            }
+
+            next = null_bool_var;
+            if (m_theory_vars.contains(next)) {
+                if (!m_theory_var_phase.find(next, phase)) {
+                    phase = l_undef;
+                }
+            }
+        }
+
+        virtual void add_theory_aware_branching_info(bool_var v, double priority, lbool phase) {
+            TRACE("theory_aware_branching", tout << "Add theory-aware branching information for l#" << v << ": priority=" << priority << std::endl;);
+            m_theory_vars.insert(v);
+            m_theory_var_phase.insert(v, phase);
+            m_theory_var_priority.insert(v, priority);
+            if (m_queue.contains(v)) {
+                if (priority > 0.0) {
+                    m_queue.decreased(v);
+                } else {
+                    m_queue.increased(v);
+                }
+            }
+            // m_theory_queue.reserve(v+1);
+            // m_theory_queue.insert(v);
+        }
+
+        virtual void display(std::ostream & out) {
+            bool first = true;
+            bool_var_act_queue::const_iterator it  = m_queue.begin();
+            bool_var_act_queue::const_iterator end = m_queue.end();
+            for (; it != end ; ++it) {
+                unsigned v = *it;
+                if (m_context.get_assignment(v) == l_undef) {
+                    if (first) {
+                        out << "remaining case-splits:\n";
+                        first = false;
+                    }
+                    out << "#" << m_context.bool_var2expr(v)->get_id() << " ";
+                }
+            }
+            if (!first)
+                out << "\n";
+
+        }
+
+        virtual ~theory_aware_branching_queue() {};
+    };
+
 
     case_split_queue * mk_case_split_queue(context & ctx, smt_params & p) {
         if (p.m_relevancy_lvl < 2 && (p.m_case_split_strategy == CS_RELEVANCY || p.m_case_split_strategy == CS_RELEVANCY_ACTIVITY || 
-                                      p.m_case_split_strategy == CS_RELEVANCY_GOAL)) {
+                p.m_case_split_strategy == CS_RELEVANCY_GOAL)) {
             warning_msg("relevancy must be enabled to use option CASE_SPLIT=3, 4 or 5");
             p.m_case_split_strategy = CS_ACTIVITY;
         }
         if (p.m_auto_config && (p.m_case_split_strategy == CS_RELEVANCY || p.m_case_split_strategy == CS_RELEVANCY_ACTIVITY || 
-                                p.m_case_split_strategy == CS_RELEVANCY_GOAL)) {
+                p.m_case_split_strategy == CS_RELEVANCY_GOAL)) {
             warning_msg("auto configuration (option AUTO_CONFIG) must be disabled to use option CASE_SPLIT=3, 4 or 5");
             p.m_case_split_strategy = CS_ACTIVITY;
         }
@@ -1110,6 +1249,8 @@ namespace smt {
             return alloc(rel_act_case_split_queue, ctx, p);
         case CS_RELEVANCY_GOAL:
             return alloc(rel_goal_case_split_queue, ctx, p);
+        case CS_ACTIVITY_THEORY_AWARE_BRANCHING:
+            return alloc(theory_aware_branching_queue, ctx, p);
         default:
             return alloc(act_case_split_queue, ctx, p);
         }

src/smt/smt_case_split_queue.h

@@ -46,6 +46,9 @@ namespace smt {
         virtual void next_case_split(bool_var & next, lbool & phase) = 0;
         virtual void display(std::ostream & out) = 0;
         virtual ~case_split_queue() {}
+
+        // theory-aware branching hint
+        virtual void add_theory_aware_branching_info(bool_var v, double priority, lbool phase) {}
     };
 
     case_split_queue * mk_case_split_queue(context & ctx, smt_params & p);

src/smt/smt_context.cpp

@@ -3022,6 +3022,10 @@ namespace smt {
         }
     }
 
+    void context::add_theory_aware_branching_info(bool_var v, double priority, lbool phase) {
+        m_case_split_queue->add_theory_aware_branching_info(v, priority, phase);
+    }
+
     bool context::propagate_th_case_split(unsigned qhead) {
         if (m_all_th_case_split_literals.empty())
             return true;

src/smt/smt_context.h

@@ -838,12 +838,20 @@ namespace smt {
          */
         void mk_th_case_split(unsigned num_lits, literal * lits);
 
+
+        /*
+         * Provide a hint to the branching heuristic about the priority of a "theory-aware literal".
+         * Literals marked in this way will always be branched on before unmarked literals,
+         * starting with the literal having the highest priority.
+         */
+        void add_theory_aware_branching_info(bool_var v, double priority, lbool phase);
+
     public:
 
         // helper function for trail
         void undo_th_case_split(literal l);
 
-	bool propagate_th_case_split(unsigned qhead);
+        bool propagate_th_case_split(unsigned qhead);
 
         bool_var mk_bool_var(expr * n);