mirror of
https://github.com/Z3Prover/z3
synced 2025-08-13 14:40:55 +00:00
104 lines
2.9 KiB
C++
104 lines
2.9 KiB
C++
/*++
|
|
Copyright (c) 2012 Microsoft Corporation
|
|
|
|
Module Name:
|
|
|
|
pb2bv_model_converter.cpp
|
|
|
|
Abstract:
|
|
|
|
Model converter for the pb2bv tactic.
|
|
|
|
Author:
|
|
|
|
Christoph (cwinter) 2012-02-15
|
|
|
|
Notes:
|
|
|
|
--*/
|
|
#include "util/trace.h"
|
|
#include "ast/arith_decl_plugin.h"
|
|
#include "model/model_v2_pp.h"
|
|
#include "tactic/arith/pb2bv_model_converter.h"
|
|
|
|
pb2bv_model_converter::pb2bv_model_converter(ast_manager & _m) : m(_m) {
|
|
|
|
}
|
|
|
|
pb2bv_model_converter::pb2bv_model_converter(ast_manager & _m, obj_map<func_decl, expr*> const & c2bit, bound_manager const & bm):
|
|
m(_m) {
|
|
for (auto const& kv : c2bit) {
|
|
m_c2bit.push_back(func_decl_pair(kv.m_key, to_app(kv.m_value)->get_decl()));
|
|
m.inc_ref(kv.m_key);
|
|
m.inc_ref(to_app(kv.m_value)->get_decl());
|
|
}
|
|
for (expr* c : bm) {
|
|
SASSERT(is_uninterp_const(c));
|
|
func_decl * d = to_app(c)->get_decl();
|
|
if (!c2bit.contains(d)) {
|
|
SASSERT(d->get_arity() == 0);
|
|
m.inc_ref(d);
|
|
m_c2bit.push_back(func_decl_pair(d, static_cast<func_decl*>(nullptr)));
|
|
}
|
|
}
|
|
}
|
|
|
|
pb2bv_model_converter::~pb2bv_model_converter() {
|
|
for (auto const& kv : m_c2bit) {
|
|
m.dec_ref(kv.first);
|
|
m.dec_ref(kv.second);
|
|
}
|
|
}
|
|
|
|
void pb2bv_model_converter::get_units(obj_map<expr, bool>& units) {
|
|
if (!m_c2bit.empty()) units.reset();
|
|
}
|
|
|
|
|
|
void pb2bv_model_converter::operator()(model_ref & md) {
|
|
TRACE("pb2bv", tout << "converting model:\n"; model_v2_pp(tout, *md); display(tout););
|
|
arith_util a_util(m);
|
|
|
|
for (auto const& kv : m_c2bit) {
|
|
if (kv.second) {
|
|
expr * val = md->get_const_interp(kv.second);
|
|
if (val == nullptr || m.is_false(val)) {
|
|
/* false's and don't cares get the integer 0 solution*/
|
|
md->register_decl(kv.first, a_util.mk_numeral(rational(0), true));
|
|
}
|
|
else {
|
|
md->register_decl(kv.first, a_util.mk_numeral(rational(1), true));
|
|
}
|
|
}
|
|
else {
|
|
// kv.first is a don't care.
|
|
md->register_decl(kv.first, a_util.mk_numeral(rational(0), true));
|
|
}
|
|
}
|
|
}
|
|
|
|
void pb2bv_model_converter::display(std::ostream & out) {
|
|
out << "(pb2bv-model-converter";
|
|
for (auto const& kv : m_c2bit) {
|
|
out << "\n (" << kv.first->get_name() << " ";
|
|
if (kv.second == 0)
|
|
out << "0";
|
|
else
|
|
out << kv.second->get_name();
|
|
out << ")";
|
|
}
|
|
out << ")\n";
|
|
}
|
|
|
|
model_converter * pb2bv_model_converter::translate(ast_translation & translator) {
|
|
ast_manager & to = translator.to();
|
|
pb2bv_model_converter * res = alloc(pb2bv_model_converter, to);
|
|
for (auto const& kv : m_c2bit) {
|
|
func_decl * f1 = translator(kv.first);
|
|
func_decl * f2 = translator(kv.second);
|
|
res->m_c2bit.push_back(func_decl_pair(f1, f2));
|
|
to.inc_ref(f1);
|
|
to.inc_ref(f2);
|
|
}
|
|
return res;
|
|
}
|