mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
parent
a20d4fa362
commit
7d976e4f4d
|
@ -879,11 +879,11 @@ private:
|
|||
}
|
||||
TRACE("sat", m_solver.display_model(tout););
|
||||
sat::model ll_m = m_solver.get_model();
|
||||
mdl = alloc(model, m);
|
||||
if (m_sat_mc) {
|
||||
(*m_sat_mc)(ll_m);
|
||||
}
|
||||
mdl = alloc(model, m);
|
||||
for (sat::bool_var v = 0; v < ll_m.size(); ++v) {
|
||||
}
|
||||
for (sat::bool_var v = 0; m_sat_mc && v < m_sat_mc->num_vars(); ++v) {
|
||||
expr* n = m_sat_mc->var2expr(v);
|
||||
if (!n || !is_app(n) || to_app(n)->get_num_args() > 0) {
|
||||
continue;
|
||||
|
|
|
@ -96,6 +96,7 @@ public:
|
|||
void set_env(ast_pp_util* visitor) override;
|
||||
void display(std::ostream& out) override;
|
||||
void get_units(obj_map<expr, bool>& units) override;
|
||||
unsigned num_vars() const { return m_var2expr.size(); }
|
||||
app* var2expr(sat::bool_var v) const { return m_var2expr.get(v, nullptr); }
|
||||
expr_ref lit2expr(sat::literal l);
|
||||
void insert(sat::bool_var v, app * atom, bool aux);
|
||||
|
|
Loading…
Reference in a new issue