parameters, local search, arithmetic propagation

add get-info parameters to print current parameters in scope of solver
add interface to set values in int-blaster
settle on propagation for arithmetic assignments

src/cmd_context/basic_cmds.cpp

@@ -433,7 +433,7 @@ class set_option_cmd : public set_get_option_cmd {
     }
 
     void set_param(cmd_context & ctx, char const * value) {
-        try {
+        try {            
             gparams::set(m_option, value);
             env_params::updt_params();
             ctx.global_params_updated();
@@ -693,7 +693,7 @@ public:
         m_rlimit(":rlimit") {
     }
     char const * get_usage() const override { return "<keyword>"; }
-    char const * get_descr(cmd_context & ctx) const override { return "get information."; }
+    char const * get_descr(cmd_context & ctx) const override { return "(get-info :?) for options."; }
     unsigned get_arity() const override { return 1; }
     cmd_arg_kind next_arg_kind(cmd_context & ctx) const override { return CPK_KEYWORD; }
     void set_next_arg(cmd_context & ctx, symbol const & opt) override {
@@ -707,7 +707,7 @@ public:
             ctx.regular_stream() << "(:name \"Z3\")" << std::endl;
         }
         else if (opt == m_authors) {
-            ctx.regular_stream() << "(:authors \"Leonardo de Moura, Nikolaj Bjorner and Christoph Wintersteiger\")" << std::endl;
+            ctx.regular_stream() << "(:authors \"Leonardo de Moura, Nikolaj Bjorner, Lev Nachmanson and Christoph Wintersteiger\")" << std::endl;
         }
         else if (opt == m_version) {
             ctx.regular_stream() << "(:version \"" << Z3_MAJOR_VERSION << "." << Z3_MINOR_VERSION << "." << Z3_BUILD_NUMBER
@@ -731,8 +731,20 @@ public:
         else if (opt == m_assertion_stack_levels) {
             ctx.regular_stream() << "(:assertion-stack-levels " << ctx.num_scopes() << ")" << std::endl;
         }
+        else if (opt == symbol(":parameters")) {
+            ctx.display_parameters(ctx.regular_stream());
+        }
         else {
-            ctx.print_unsupported(opt, m_line, m_pos);
+            if (opt != symbol(":?"))
+               ctx.print_unsupported(opt, m_line, m_pos);
+            ctx.regular_stream() << "; (get-info :reason-unknown)\n";
+            ctx.regular_stream() << "; (get-info :status)\n";
+            ctx.regular_stream() << "; (get-info :version)\n";
+            ctx.regular_stream() << "; (get-info :authors)\n";
+            ctx.regular_stream() << "; (get-info :error-behavior)\n";
+            ctx.regular_stream() << "; (get-info :parameters)\n";
+            ctx.regular_stream() << "; (get-info :rlimit)\n";
+            ctx.regular_stream() << "; (get-info :assertion-stack-levels)\n";
         }
     }
 };

src/cmd_context/cmd_context.cpp

@@ -1902,6 +1902,11 @@ void cmd_context::display_model(model_ref& mdl) {
     }
 }
 
+void cmd_context::display_parameters(std::ostream& out) {
+    if (m_solver)
+        m_solver->display_parameters(out);
+}
+
 void cmd_context::add_declared_functions(model& mdl) {
     model_params p;
     if (!p.user_functions())

src/cmd_context/cmd_context.h

@@ -506,6 +506,7 @@ public:
     void display_assertions();
     void display_statistics(bool show_total_time = false, double total_time = 0.0);
     void display_dimacs();
+    void display_parameters(std::ostream& out);
     void reset(bool finalize = false);
     void assert_expr(expr * t);
     void assert_expr(symbol const & name, expr * t);

src/smt/smt_context.cpp

@@ -2927,6 +2927,22 @@ namespace smt {
         push_trail(push_back_vector(m_values));
     }
 
+    void context::set_sls_value(expr* var, expr* value) {
+        expr_ref _var(var, m);
+        expr_ref _valueu(value, m);
+        if (!e_internalized(var))
+            return;
+        enode* n = get_enode(var);
+        theory_var_list* l = n->get_th_var_list();
+        while (l) {
+            theory_id tid = l->get_id();
+            auto* p = m_theories.get_plugin(tid);
+            if (p)
+                p->initialize_value(var, value);
+            l = l->get_next();
+        }
+    }
+
     void context::initialize_value(expr* var, expr* value) {
         IF_VERBOSE(10, verbose_stream() << "initialize " << mk_pp(var, m) << " := " << mk_pp(value, m) << "\n");
         sort* s = var->get_sort();

src/smt/smt_context.h

@@ -1812,6 +1812,8 @@ namespace smt {
 
         void user_propagate_initialize_value(expr* var, expr* value);
 
+        void set_sls_value(expr* var, expr* value);
+
         bool watches_fixed(enode* n) const;
 
         bool has_split_candidate(bool_var& var, bool& is_pos);

src/smt/theory_intblast.cpp

@@ -187,5 +187,33 @@ namespace smt {
         return alloc(expr_wrapper_proc, m_factory->mk_num_value(r, bv.get_bv_size(e)));
     }
 
+    void theory_intblast::initialize_value(expr* var, expr* value) {
+        auto avar = expr_ref(m_translator.translated(var), m);
+        if (!avar)
+            return;
+        rational r;
+        if (!bv.is_numeral(value, r))
+            return;
+        auto aval = expr_ref(a.mk_numeral(r, true), m);
+        ctx.set_sls_value(avar, aval);
+    }
+
+    bool theory_intblast::get_value(enode* n, expr_ref& r) {
+        auto avar = expr_ref(m_translator.translated(n->get_expr()), m);
+        if (!avar)
+            return false;
+        if (!ctx.e_internalized(avar))
+            return false;
+        enode* n2 = ctx.get_enode(avar);
+        auto has_value = ctx.get_value(n2, r);
+        if (!has_value)
+            return false;
+        rational val;
+        if (!a.is_numeral(r, val))
+            return false;
+        r = bv.mk_numeral(val, bv.get_bv_size(n->get_expr()));
+        return true;
+    }
+
 
 }

src/smt/theory_intblast.h

@@ -66,6 +66,8 @@ namespace smt {
         model_value_proc* mk_value(enode* n, model_generator& m) override;
         void new_eq_eh(theory_var v1, theory_var v2) override {}
         void new_diseq_eh(theory_var v1, theory_var v2) override {}
+        void initialize_value(expr* var, expr* value) override;
+        bool get_value(enode* n, expr_ref& r) override;
 
     };
 

src/smt/theory_lra.cpp

@@ -2411,6 +2411,7 @@ public:
                            ps.size(), ps.data());
             }
             ctx().mk_clause(m_core2.size(), m_core2.data(), js, CLS_TH_LEMMA_RELEVANT, nullptr);
+            ctx().mk_clause(m_core2.size(), m_core2.data(), js, CLS_TH_LEMMA_LEARNED, nullptr);
         }
         else {
             ctx().assign(
@@ -2465,12 +2466,12 @@ public:
         bool is_int;
         VERIFY(a.is_band(n, sz, _x, _y) || a.is_shl(n, sz, _x, _y) || a.is_ashr(n, sz, _x, _y) || a.is_lshr(n, sz, _x, _y));
         if (!get_value(ctx().get_enode(_x), vx) || !get_value(ctx().get_enode(_y), vy) || !get_value(ctx().get_enode(n), vn)) {
-            IF_VERBOSE(2, verbose_stream() << "could not get value of " << mk_pp(n, m) << "\n");
+            IF_VERBOSE(4, verbose_stream() << "could not get value of " << mk_pp(n, m) << "\n");
             found_unsupported(n);
             return true;
         }
         if (!a.is_numeral(vn, valn, is_int) || !is_int || !a.is_numeral(vx, valx, is_int) || !is_int || !a.is_numeral(vy, valy, is_int) || !is_int) {
-            IF_VERBOSE(2, verbose_stream() << "could not get value of " << mk_pp(n, m) << "\n");
+            IF_VERBOSE(4, verbose_stream() << "could not get value of " << mk_pp(n, m) << "\n");
             found_unsupported(n);
             return true;
         }
@@ -2489,7 +2490,7 @@ public:
         };
 
         if (a.is_band(n)) {
-            IF_VERBOSE(2, verbose_stream() << "band: " << mk_bounded_pp(n, m) << " " << valn << " := " << valx << "&" << valy << "\n");
+            IF_VERBOSE(4, verbose_stream() << "band: " << mk_bounded_pp(n, m) << " " << valn << " := " << valx << "&" << valy << "\n");
             for (unsigned i = 0; i < sz; ++i) {
                 bool xb = valx.get_bit(i);
                 bool yb = valy.get_bit(i);
@@ -2514,7 +2515,7 @@ public:
             if (ctx().get_assignment(eq) == l_true)
                 return true;            
             ctx().mk_th_axiom(get_id(), ~th.mk_eq(y, a.mk_int(k), false), eq);
-            IF_VERBOSE(2, verbose_stream() << "shl: " << mk_bounded_pp(n, m) << " " << valn << " := " << valx << " << " << valy << "\n");
+            IF_VERBOSE(4, verbose_stream() << "shl: " << mk_bounded_pp(n, m) << " " << valn << " := " << valx << " << " << valy << "\n");
             return false;
         }
         if (a.is_lshr(n)) {
@@ -2526,7 +2527,7 @@ public:
             if (ctx().get_assignment(eq) == l_true)
                 return true;            
             ctx().mk_th_axiom(get_id(), ~th.mk_eq(y, a.mk_int(k), false), eq);
-            IF_VERBOSE(2, verbose_stream() << "lshr: " << mk_bounded_pp(n, m) << " " << valn << " := " << valx << " >>l " << valy << "\n");
+            IF_VERBOSE(4, verbose_stream() << "lshr: " << mk_bounded_pp(n, m) << " " << valn << " := " << valx << " >>l " << valy << "\n");
             return false;
         }
         if (a.is_ashr(n)) {
@@ -3555,28 +3556,19 @@ public:
     }
 
     bool get_value(enode* n, rational& val) {
-        theory_var v = n->get_th_var(get_id());            
-        if (!is_registered_var(v)) return false;
-        lpvar vi = get_lpvar(v);
-        if (lp().has_value(vi, val)) {
-            TRACE("arith", tout << expr_ref(n->get_expr(), m) << " := " << val << "\n";);
-            if (is_int(n) && !val.is_int()) return false;
-            return true;
-        }
-        else {
+        theory_var v = n->get_th_var(get_id());    
+        if (!is_registered_var(v)) 
             return false;
-        }
+        lpvar vi = get_lpvar(v);
+        return lp().has_value(vi, val) && (!is_int(n) || val.is_int());
     }    
 
     bool get_value(enode* n, expr_ref& r) {
         rational val;
-        if (get_value(n, val)) {
-            r = a.mk_numeral(val, is_int(n));
-            return true;
-        }
-        else {
+        if (!get_value(n, val))
             return false;
-        }
+        r = a.mk_numeral(val, is_int(n));
+        return true;
     }    
 
     bool include_func_interp(func_decl* f) {

src/smt/theory_sls.cpp

@@ -38,7 +38,7 @@ namespace smt {
     }
     
     void theory_sls::set_value(expr* t, expr* v) {
-        ctx.user_propagate_initialize_value(t, v);
+        ctx.set_sls_value(t, v);
     }
     
     void theory_sls::force_phase(sat::literal lit) {

src/solver/solver.cpp

@@ -225,6 +225,18 @@ void solver::collect_param_descrs(param_descrs & r) {
     insert_ctrl_c(r);
 }
 
+std::ostream& solver::display_parameters(std::ostream& out) {
+    //
+    // this is a partial patch. 
+    // The modules should be present in 'p'.
+    // if p has smt parameters that are updated, they may be visible.
+    // parameters within sub-solvers will / may not be visible at this level.
+    //
+    auto const& p = get_params();
+    gparams::display_updated_parameters(out, p);
+    return out;
+}
+
 void solver::reset_params(params_ref const & p) {
     m_params.append(p);
     solver_params sp(m_params);

src/solver/solver.h

@@ -81,6 +81,11 @@ public:
     */
     virtual void collect_param_descrs(param_descrs & r);
 
+    /**
+    * \brief display parameters
+    */
+    std::ostream& display_parameters(std::ostream& out);
+
     /**
        \brief Push a parameter state. It is restored upon pop.
        Only a single scope of push is supported.

src/util/gparams.cpp

@@ -412,7 +412,7 @@ public:
         }
     }
 
-    std::string get_value(params_ref const & ps, std::string const & p) {
+    std::string get_value(params_ref const& ps, std::string const& p) {
         symbol sp(p.c_str());
         std::ostringstream buffer;
         ps.display(buffer, sp);
@@ -430,6 +430,19 @@ public:
         return r;
     }
 
+    void display_updated_parameters(std::ostream& out, params_ref const& p) {
+        param_descrs* d = nullptr;
+        for (auto const& [k, v] : m_module_params) {
+            if (!get_module_param_descr(k, d))
+                continue;
+            params_ref* ps = nullptr;
+            if (!m_module_params.find(k, ps))
+                continue;
+            ps->display_smt2(out, k, *d);
+            p.display_smt2(out, k, *d);
+        }
+    }
+
     std::string get_value(char const * name) {
         std::string m, p;
         normalize(name, m, p);
@@ -691,3 +704,7 @@ std::string& gparams::g_buffer() {
     SASSERT(g_imp);
     return g_imp->m_buffer;
 }
+
+void gparams::display_updated_parameters(std::ostream& out, params_ref const& p) {
+    g_imp->display_updated_parameters(out, p);
+}

src/util/gparams.h

@@ -118,9 +118,11 @@ public:
     
     // Auxiliary APIs for better command line support
     static void display_modules(std::ostream & out);
+    static void display_updated_parameters(std::ostream& out, params_ref const& p);
     static void display_module(std::ostream & out, char const * module_name);
     static void display_module_markdown(std::ostream & out, char const * module_name);
     static void display_parameter(std::ostream & out, char const * name);
+
     static param_descrs const& get_global_param_descrs();
 
     /**

src/util/params.cpp

@@ -476,7 +476,8 @@ public:
 
     void display_smt2(std::ostream & out, char const* module, param_descrs& descrs) const {
         for (params::entry const& e : m_entries) {
-            if (!descrs.contains(e.first)) continue;
+            if (!descrs.contains(e.first)) 
+                continue;
             out << "(set-option :";
             out << module << ".";        
             out << e.first;
@@ -504,6 +505,7 @@ public:
                 break;
             }
             out << ")\n";
+            out << "; " << descrs.get_descr(e.first) << "\n";
         }
     }