Add commands for forcing preferences during search

Add commands:

(prefer <formula>)
- will instruct case split queue to assign formula to true.
- prefer commands added within a scope are forgotten after leaving the scope.

(reset-preferences)
- resets asserted preferences. Has to be invoked at base level.

This provides functionality related to MathSAT and based on an ask by Tomáš Kolárik who is integrating the functionality with OpenSMT2

src/cmd_context/basic_cmds.cpp

@@ -334,6 +334,52 @@ public:
     }    
 };
 
+class prefer_cmd : public cmd {
+    expr *m_formula = nullptr;
+
+public:
+    prefer_cmd() : cmd("prefer") {}
+    char const *get_usage() const override {
+        return "<formula>";
+    }
+    char const *get_descr(cmd_context &ctx) const override {
+        return "set a preferred formula for the solver";
+    }
+    unsigned get_arity() const override {
+        return 1;
+    }
+    void prepare(cmd_context &ctx) override {
+        m_formula = nullptr;
+    }
+    cmd_arg_kind next_arg_kind(cmd_context &ctx) const override {
+        return CPK_EXPR;
+    }
+    void set_next_arg(cmd_context &ctx, expr *e) override {
+        m_formula = e;
+    }
+    void execute(cmd_context &ctx) override {
+        SASSERT(m_formula);
+        ctx.set_preferred(m_formula);
+    }
+};
+
+class reset_preferences_cmd : public cmd {
+    public:
+    reset_preferences_cmd() : cmd("reset-preferences") {}
+    char const *get_usage() const override {
+        return "";
+    }
+    char const *get_descr(cmd_context &ctx) const override {
+        return "reset all preferred formulas";
+    }
+    unsigned get_arity() const override {
+        return 0;
+    }
+    void execute(cmd_context &ctx) override {
+        ctx.reset_preferred();
+    }
+};
+
 class set_get_option_cmd : public cmd {
 protected:
     symbol      m_true;
@@ -926,6 +972,8 @@ void install_basic_cmds(cmd_context & ctx) {
     ctx.insert(alloc(get_info_cmd));
     ctx.insert(alloc(set_info_cmd));
     ctx.insert(alloc(set_initial_value_cmd));
+    ctx.insert(alloc(prefer_cmd));
+    ctx.insert(alloc(reset_preferences_cmd));
     ctx.insert(alloc(get_consequences_cmd));
     ctx.insert(alloc(builtin_cmd, "assert", "<term>", "assert term."));
     ctx.insert(alloc(builtin_cmd, "check-sat", "<boolean-constants>*", "check if the current context is satisfiable. If a list of boolean constants B is provided, then check if the current context is consistent with assigning every constant in B to true."));

src/cmd_context/cmd_context.cpp

@@ -628,6 +628,7 @@ cmd_context::~cmd_context() {
     finalize_tactic_manager();
     m_proof_cmds = nullptr;
     m_var2values.reset();
+    m_preferred = nullptr;
     reset(true);
     m_mcs.reset();
     m_solver = nullptr;
@@ -1518,6 +1519,8 @@ void cmd_context::reset(bool finalize) {
     m_dt_eh  = nullptr;
     m_std_subst = nullptr;
     m_rev_subst = nullptr;
+    m_preferred = nullptr;
+    m_var2values.reset();
     if (m_manager) {
         dealloc(m_pmanager);
         m_pmanager = nullptr;
@@ -1884,6 +1887,29 @@ void cmd_context::set_initial_value(expr* var, expr* value) {
     m_var2values.push_back({expr_ref(var, m()), expr_ref(value, m())});    
 }
 
+void cmd_context::set_preferred(expr* fmla) {
+    if (!m_preferred) {
+        auto p = alloc(preferred_value_propagator, m());
+        m_preferred = p;
+        if (get_solver()) {
+            get_solver()->user_propagate_init(p, p->push_eh, p->pop_eh, p->fresh_eh);
+            get_solver()->user_propagate_register_decide(p->decide_eh);
+        }
+    }
+    m_preferred->set_preferred(fmla);
+    if (get_opt()) {
+        throw default_exception("setting preferred on optimization context is not supported yet");
+        return;
+    }
+}
+
+void cmd_context::reset_preferred() {
+    if (!m_scopes.empty())
+        throw default_exception("reset-preferred can only be invoked at base level");
+    if (m_preferred) 
+        m_preferred->reset_preferred();   
+}
+
 
 void cmd_context::display_model(model_ref& mdl) {
     if (mdl) {
@@ -2261,8 +2287,13 @@ void cmd_context::mk_solver() {
     m_params.get_solver_params(p, proofs_enabled, models_enabled, unsat_core_enabled);
     m_solver = (*m_solver_factory)(m(), p, proofs_enabled, models_enabled, unsat_core_enabled, m_logic);
     m_solver = mk_slice_solver(m_solver.get());
-    if (m_simplifier_factory) 
+    if (m_simplifier_factory)
         m_solver = mk_simplifier_solver(m_solver.get(), &m_simplifier_factory);
+    if (m_preferred) {
+        auto p = m_preferred.get();
+        m_solver->user_propagate_init(p, p->push_eh, p->pop_eh, p->fresh_eh);
+        m_solver->user_propagate_register_decide(p->decide_eh);
+    }
 }
 
 

src/cmd_context/cmd_context.h

@@ -39,6 +39,7 @@ Notes:
 #include "solver/check_logic.h"
 #include "solver/progress_callback.h"
 #include "solver/simplifier_solver.h"
+#include "solver/preferred_value_propagator.h"
 #include "cmd_context/pdecl.h"
 #include "cmd_context/tactic_manager.h"
 #include "params/context_params.h"
@@ -265,6 +266,7 @@ protected:
     dictionary<object_ref*>      m_object_refs; // anything that can be named.
     dictionary<sexpr*>           m_user_tactic_decls;
     vector<std::pair<expr_ref, expr_ref>> m_var2values;
+    scoped_ptr<preferred_value_propagator> m_preferred;
 
     dictionary<func_decls>       m_func_decls;
     obj_map<func_decl, symbol>   m_func_decl2alias;
@@ -429,6 +431,8 @@ public:
     void set_solver(solver* s) { m_solver = s; }
     void set_proof_cmds(proof_cmds* pc) { m_proof_cmds = pc; }
     void set_initial_value(expr* var, expr* value);
+    void set_preferred(expr *fmla);
+    void reset_preferred();
 
     void set_solver_factory(solver_factory * s);
     void set_simplifier_factory(simplifier_factory& sf) { m_simplifier_factory = sf; }

src/smt/theory_bv.cpp

@@ -1890,6 +1890,8 @@ namespace smt {
 
     theory_bv::var_enode_pos theory_bv::get_bv_with_theory(bool_var v, theory_id id) const {
         atom* a      = get_bv2a(v);
+        if (!a)
+            return var_enode_pos(nullptr, UINT32_MAX);
         svector<var_enode_pos> vec;
         if (!a->is_bit())
             return var_enode_pos(nullptr, UINT32_MAX);

src/smt/theory_user_propagator.cpp

@@ -209,61 +209,36 @@ void theory_user_propagator::decide(bool_var& var, bool& is_pos) {
     if (!m_decide_eh)
         return;
 
-    const bool_var_data& d = ctx.get_bdata(var);
+    expr *e = ctx.bool_var2expr(var);
+    if (!e)
+        e = m.mk_true(); // use a dummy case split atom.
 
-    if (!d.is_enode() && !d.is_theory_atom())
-        return;
-
-    enode* original_enode = nullptr;
-    unsigned original_bit = 0;
-    bv_util bv(m);
-    theory* th = nullptr;
-    theory_var v = null_theory_var;
-
-    // get the associated theory
-    if (!d.is_enode()) {
-        // it might be a value that does not have an enode
-        th = ctx.get_theory(d.get_theory());
-    }
-    else {
-        original_enode = ctx.bool_var2enode(var);
-        v = original_enode->get_th_var(get_family_id());
-        if (v == null_theory_var) {
-            // it is not a registered boolean expression
-            th = ctx.get_theory(d.get_theory());
+    unsigned bit = 0;
+    // determine if case split is a bit-position in a bit-vector
+    {
+        bv_util bv(m);
+        auto th = ctx.get_theory(bv.get_fid());
+        if (th) {
+            // it is then n'th bit of a bit-vector n.
+            auto [n, nbit] = static_cast<theory_bv *>(th)->get_bv_with_theory(var, get_family_id());
+            if (n) {
+                e = n->get_expr();
+                bit = nbit;
+            }
         }
     }
 
-    if (v == null_theory_var && !th)
-        return;
-
-    if (v == null_theory_var && th->get_family_id() != bv.get_fid())
-        return;
-
-    if (v == null_theory_var) {
-        // it is not a registered boolean value but it is a bitvector
-        auto registered_bv = ((theory_bv*) th)->get_bv_with_theory(var, get_family_id());
-        if (!registered_bv.first)
-            // there is no registered bv associated with the bit
-            return;
-        original_enode = registered_bv.first;
-        original_bit = registered_bv.second;
-        v = original_enode->get_th_var(get_family_id());
-    }
-
-    // call the registered callback
-    unsigned new_bit = original_bit;
-
     force_push();
-    expr *e = var2expr(v);
-    m_decide_eh(m_user_context, this, e, new_bit, is_pos);
+    m_decide_eh(m_user_context, this, e, bit, is_pos);
 
     bool_var new_var;
     if (!get_case_split(new_var, is_pos) || new_var == var)
         // The user did not interfere
         return;
+    TRACE(user_propagate,
+          tout << "decide: " << ctx.bool_var2expr(var) << " -> " << ctx.bool_var2expr(new_var) << "\n");
     var = new_var;
-
+                    
     // check if the new variable is unassigned
     if (ctx.get_assignment(var) != l_undef)
         throw default_exception("expression in \"decide\" is already assigned");

src/solver/preferred_value_propagator.h

@@ -0,0 +1,85 @@
+/*++
+Copyright (c) 2025 Microsoft Corporation
+
+Module Name:
+
+    preferred_value_propagator.h
+
+Abstract:
+
+    Specialized propagator for preferred values
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 10-2-2025
+
+Notes:
+
+--*/
+#pragma once
+
+#include "tactic/user_propagator_base.h"
+#include "util/trail.h"
+
+
+class preferred_value_propagator {
+    ast_manager &m;
+    expr_ref_vector m_preferred;
+    unsigned m_qhead = 0;
+    trail_stack m_trail;
+
+    bool decide(user_propagator::callback& cb) {
+        if (m_qhead >= m_preferred.size())
+            return false;
+        m_trail.push(value_trail(m_qhead));
+        while (m_qhead < m_preferred.size()) {
+            expr *e = m_preferred.get(m_qhead);
+            bool is_not = m.is_not(e, e);
+            m_qhead++;
+            if (cb.next_split_cb(e, 0, is_not ? l_false : l_true))
+                return true;
+        }
+        return false;
+    }
+
+public:
+    preferred_value_propagator(ast_manager &m) : m(m), m_preferred(m) {
+         push_eh = [](void * ctx, user_propagator::callback* cb) {
+            auto &p = *static_cast<preferred_value_propagator *>(ctx);
+            p.m_trail.push_scope(); 
+         };
+        pop_eh = [](void * ctx, user_propagator::callback* cb, unsigned n) -> void {
+            auto &p = *static_cast<preferred_value_propagator *>(ctx);
+            p.m_trail.pop_scope(n);
+        };
+        fresh_eh = [](void* ctx, ast_manager& dst, user_propagator::context_obj*& co) -> void* {
+            auto &p = *static_cast<preferred_value_propagator *>(ctx);
+            ast_translation tr(p.m, dst);
+            auto r = alloc(preferred_value_propagator, dst);
+            for (auto e : p.m_preferred)
+                r->set_preferred(tr(e));
+            return r;
+        };
+
+        decide_eh = [](void * ctx, user_propagator::callback * cb, expr *, unsigned, bool) -> bool {
+            auto &p = *static_cast<preferred_value_propagator *>(ctx);
+            return p.decide(*cb);
+        };
+    }
+    ~preferred_value_propagator() = default;
+    void set_preferred(expr *e) {
+        m_preferred.push_back(e);
+        if (m_trail.get_num_scopes() > 0)
+            m_trail.push(push_back_vector(m_preferred));
+    }
+    void reset_preferred() {
+        if (m_trail.get_num_scopes() != 0)
+            throw default_exception("cannot reset preferred values in scoped context");
+        m_preferred.reset();
+        SASSERT(m_qhead == 0);
+    }
+    user_propagator::push_eh_t push_eh;
+    user_propagator::pop_eh_t pop_eh;
+    user_propagator::fresh_eh_t fresh_eh;
+    user_propagator::decide_eh_t decide_eh;
+};