#include "ast/ast_pp.h"
#include "ast/ast_ll_pp.h"
#include "ast/for_each_expr.h"
#include "ast/ast_util.h"
#include "ast/occurs.h"
#include "ast/bv_decl_plugin.h"
#include "ast/rewriter/expr_safe_replace.h"
#include "ast/rewriter/th_rewriter.h"
#include "ast/converters/generic_model_converter.h"
#include "model/model_v2_pp.h"
#include "model/model_evaluator.h"
void generic_model_converter::add(func_decl * d, expr* e) {
VERIFY(e);
VERIFY(d->get_range() == e->get_sort());
m_entries.push_back(entry(d, e, m, instruction::ADD));
}
void generic_model_converter::operator()(model_ref & md) {
TRACE(model_converter, tout << "before generic_model_converter\n"; model_v2_pp(tout, *md); display(tout););
model_evaluator ev(*(md.get()));
ev.set_model_completion(m_completion);
ev.set_expand_array_equalities(false);
expr_ref val(m);
unsigned arity;
bool reset_ev = false;
obj_map<sort, ptr_vector<expr>> uninterpreted;
for (unsigned i = m_entries.size(); i-- > 0; ) {
entry const& e = m_entries[i];
switch (e.m_instruction) {
case instruction::HIDE:
md->unregister_decl(e.m_f);
break;
case instruction::ADD:
ev(e.m_def, val);
TRACE(model_converter, tout << e.m_f->get_name() << " ->\n" << e.m_def << "\n==>\n" << val << "\n";);
arity = e.m_f->get_arity();
reset_ev = false;
if (arity == 0) {
expr* old_val = md->get_const_interp(e.m_f);
if (old_val && old_val == val) {
}
else {
reset_ev = old_val != nullptr;
md->register_decl(e.m_f, val);
}
sort* s = e.m_f->get_range();
if (m.is_uninterp(s) && !md->has_uninterpreted_sort(s)) {
uninterpreted.insert_if_not_there(s, {});
if (!uninterpreted[s].contains(val))
uninterpreted[s].push_back(val);
}
}
else {
func_interp * old_val = md->get_func_interp(e.m_f);
if (old_val && old_val->get_else() == val) {
}
else {
reset_ev = old_val != nullptr;
func_interp * new_fi = alloc(func_interp, m, arity);
new_fi->set_else(val);
md->register_decl(e.m_f, new_fi);
}
}
if (reset_ev) {
ev.reset();
ev.set_model_completion(m_completion);
ev.set_expand_array_equalities(false);
}
break;
}
}
for (auto const& [s, u] : uninterpreted) {
md->register_usort(s, u.size(), u.data());
}
TRACE(model_converter, tout << "after generic_model_converter\n"; model_v2_pp(tout, *md););
}
void generic_model_converter::display(std::ostream & out) {
for (entry const& e : m_entries) {
switch (e.m_instruction) {
case instruction::HIDE:
display_del(out, e.m_f);
break;
case instruction::ADD:
display_add(out, m, e.m_f, e.m_def);
break;
}
}
}
generic_model_converter * generic_model_converter::copy(ast_translation & translator) {
ast_manager& to = translator.to();
generic_model_converter * res = alloc(generic_model_converter, to, m_orig.c_str());
for (entry const& e : m_entries) {
func_decl_ref d(translator(e.m_f.get()), to);
switch (e.m_instruction) {
case instruction::HIDE:
res->hide(d);
break;
case instruction::ADD: {
expr_ref def(translator(e.m_def.get()), to);
res->add(d, def);
break;
}
}
}
return res;
}
void generic_model_converter::convert_initialize_value(vector<std::pair<expr_ref, expr_ref>> & var2value) {
if (var2value.empty() || m_entries.empty())
return;
for (unsigned i = 0; i < var2value.size(); ++i) {
auto& [var, value] = var2value[i];
for (auto const& e : m_entries) {
switch (e.m_instruction) {
case instruction::HIDE:
break;
case instruction::ADD:
if (is_uninterp_const(var) && e.m_f == to_app(var)->get_decl())
convert_initialize_value(e.m_def, i, var2value);
break;
}
}
}
}
void generic_model_converter::convert_initialize_value(expr* def, unsigned i, vector<std::pair<expr_ref, expr_ref>>& var2value) {
expr* c = nullptr, *th = nullptr, *el = nullptr;
auto& [var, value] = var2value[i];
if (m.is_ite(def, c, th, el)) {
if (value == th) {
var = c;
value = m.mk_true();
return;
}
if (value == el) {
var = c;
value = m.mk_false();
return;
}
}
if (is_uninterp(def)) {
var = def;
return;
}
}
void generic_model_converter::set_env(ast_pp_util* visitor) {
if (!visitor) {
m_env = nullptr;
}
else {
m_env = &visitor->env();
for (entry const& e : m_entries) {
visitor->coll.visit_func(e.m_f);
if (e.m_def) visitor->coll.visit(e.m_def);
}
}
}
void generic_model_converter::get_units(obj_map<expr, bool>& units) {
th_rewriter rw(m);
expr_safe_replace rep(m);
expr_ref tmp(m);
for (auto const& kv : units) {
rep.insert(kv.m_key, kv.m_value ? m.mk_true() : m.mk_false());
}
for (unsigned i = m_entries.size(); i-- > 0;) {
entry const& e = m_entries[i];
switch (e.m_instruction) {
case instruction::HIDE:
tmp = m.mk_const(e.m_f);
if (units.contains(tmp)) {
m.dec_ref(tmp);
units.remove(tmp);
}
break;
case instruction::ADD:
if (e.m_f->get_arity() == 0 && m.is_bool(e.m_f->get_range())) {
tmp = m.mk_const(e.m_f);
if (units.contains(tmp)) {
break;
}
tmp = e.m_def;
rep(tmp);
rw(tmp);
if (m.is_true(tmp)) {
tmp = m.mk_const(e.m_f);
m.inc_ref(tmp);
units.insert(tmp, true);
rep.insert(tmp, m.mk_true());
}
else if (m.is_false(tmp)) {
tmp = m.mk_const(e.m_f);
m.inc_ref(tmp);
units.insert(tmp, false);
rep.insert(tmp, m.mk_false());
}
}
break;
}
}
}
expr_ref generic_model_converter::simplify_def(entry const& e) {
expr_ref c(m.mk_const(e.m_f), m);
if (m.is_bool(c) && occurs(c, e.m_def)) {
expr_safe_replace rep(m);
expr_ref result1 = e.m_def;
expr_ref result2 = e.m_def;
rep.apply_substitution(c, m.mk_true(), result1);
rep.apply_substitution(c, m.mk_false(), result2);
th_rewriter rw(m);
expr_ref lhs(m.mk_implies(result2, c), m);
expr_ref rhs(m.mk_implies(c, result1), m);
expr_ref result(m.mk_and(lhs, rhs), m);
rw(result);
return result;
}
else {
return expr_ref(m.mk_eq(c, e.m_def), m);
}
}