mirror of
https://github.com/Z3Prover/z3
synced 2025-04-07 18:05:21 +00:00
Style, formatting
This commit is contained in:
parent
e0ff9d8fd9
commit
8b6d7c0251
|
@ -3,13 +3,13 @@ Copyright (c) 2015 Microsoft Corporation
|
|||
|
||||
Module Name:
|
||||
|
||||
ackr_model_converter.cpp
|
||||
ackr_model_converter.cpp
|
||||
|
||||
Abstract:
|
||||
|
||||
Author:
|
||||
|
||||
Mikolas Janota
|
||||
Mikolas Janota
|
||||
|
||||
Revision History:
|
||||
--*/
|
||||
|
@ -22,8 +22,8 @@ Revision History:
|
|||
class ackr_model_converter : public model_converter {
|
||||
public:
|
||||
ackr_model_converter(ast_manager & m,
|
||||
const ackr_info_ref& info,
|
||||
model_ref& abstr_model)
|
||||
const ackr_info_ref& info,
|
||||
model_ref& abstr_model)
|
||||
: m(m)
|
||||
, info(info)
|
||||
, abstr_model(abstr_model)
|
||||
|
@ -31,7 +31,7 @@ public:
|
|||
{ }
|
||||
|
||||
ackr_model_converter(ast_manager & m,
|
||||
const ackr_info_ref& info)
|
||||
const ackr_info_ref& info)
|
||||
: m(m)
|
||||
, info(info)
|
||||
, fixed_model(false)
|
||||
|
@ -51,8 +51,6 @@ public:
|
|||
|
||||
virtual void operator()(model_ref & md) { operator()(md, 0); }
|
||||
|
||||
//void display(std::ostream & out);
|
||||
|
||||
virtual model_converter * translate(ast_translation & translator) {
|
||||
ackr_info_ref retv_info = info->translate(translator);
|
||||
if (fixed_model) {
|
||||
|
@ -63,22 +61,23 @@ public:
|
|||
return alloc(ackr_model_converter, translator.to(), retv_info);
|
||||
}
|
||||
}
|
||||
|
||||
protected:
|
||||
ast_manager& m;
|
||||
ast_manager & m;
|
||||
const ackr_info_ref info;
|
||||
model_ref abstr_model;
|
||||
bool fixed_model;
|
||||
void convert(model * source, model * destination);
|
||||
void add_entry(model_evaluator & evaluator,
|
||||
app* term, expr* value,
|
||||
obj_map<func_decl, func_interp*>& interpretations);
|
||||
app* term, expr* value,
|
||||
obj_map<func_decl, func_interp*>& interpretations);
|
||||
void convert_constants(model * source, model * destination);
|
||||
};
|
||||
|
||||
void ackr_model_converter::convert(model * source, model * destination) {
|
||||
destination->copy_func_interps(*source);
|
||||
destination->copy_usort_interps(*source);
|
||||
convert_constants(source,destination);
|
||||
convert_constants(source, destination);
|
||||
}
|
||||
|
||||
void ackr_model_converter::convert_constants(model * source, model * destination) {
|
||||
|
@ -89,16 +88,17 @@ void ackr_model_converter::convert_constants(model * source, model * destination
|
|||
func_decl * const c = source->get_constant(i);
|
||||
app * const term = info->find_term(c);
|
||||
expr * value = source->get_const_interp(c);
|
||||
if(!term) {
|
||||
if (!term) {
|
||||
destination->register_decl(c, value);
|
||||
} else {
|
||||
}
|
||||
else {
|
||||
add_entry(evaluator, term, value, interpretations);
|
||||
}
|
||||
}
|
||||
|
||||
obj_map<func_decl, func_interp*>::iterator e = interpretations.end();
|
||||
for (obj_map<func_decl, func_interp*>::iterator i = interpretations.begin();
|
||||
i!=e; ++i) {
|
||||
i != e; ++i) {
|
||||
func_decl* const fd = i->m_key;
|
||||
func_interp* const fi = i->get_value();
|
||||
fi->set_else(m.get_some_value(fd->get_range()));
|
||||
|
@ -107,34 +107,35 @@ void ackr_model_converter::convert_constants(model * source, model * destination
|
|||
}
|
||||
|
||||
void ackr_model_converter::add_entry(model_evaluator & evaluator,
|
||||
app* term, expr* value,
|
||||
obj_map<func_decl, func_interp*>& interpretations) {
|
||||
app* term, expr* value,
|
||||
obj_map<func_decl, func_interp*>& interpretations) {
|
||||
TRACE("ackr_model", tout << "add_entry"
|
||||
<< mk_ismt2_pp(term, m, 2)
|
||||
<< "->"
|
||||
<< mk_ismt2_pp(value, m, 2) << "\n";
|
||||
<< mk_ismt2_pp(term, m, 2)
|
||||
<< "->"
|
||||
<< mk_ismt2_pp(value, m, 2) << "\n";
|
||||
);
|
||||
|
||||
func_interp* fi = 0;
|
||||
func_interp * fi = 0;
|
||||
func_decl * const declaration = term->get_decl();
|
||||
const unsigned sz = declaration->get_arity();
|
||||
SASSERT(sz == term->get_num_args());
|
||||
if (!interpretations.find(declaration, fi)) {
|
||||
fi = alloc(func_interp,m,sz);
|
||||
interpretations.insert(declaration, fi);
|
||||
if (!interpretations.find(declaration, fi)) {
|
||||
fi = alloc(func_interp, m, sz);
|
||||
interpretations.insert(declaration, fi);
|
||||
}
|
||||
expr_ref_vector args(m);
|
||||
for (unsigned gi = 0; gi < sz; ++gi) {
|
||||
expr * const arg = term->get_arg(gi);
|
||||
expr_ref aarg(m);
|
||||
info->abstract(arg, aarg);
|
||||
expr_ref arg_value(m);
|
||||
evaluator(aarg,arg_value);
|
||||
args.push_back(arg_value);
|
||||
expr * const arg = term->get_arg(gi);
|
||||
expr_ref aarg(m);
|
||||
info->abstract(arg, aarg);
|
||||
expr_ref arg_value(m);
|
||||
evaluator(aarg, arg_value);
|
||||
args.push_back(arg_value);
|
||||
}
|
||||
if (fi->get_entry(args.c_ptr()) == 0) {
|
||||
fi->insert_new_entry(args.c_ptr(), value);
|
||||
} else {
|
||||
}
|
||||
else {
|
||||
TRACE("ackr_model", tout << "entry already present\n";);
|
||||
}
|
||||
}
|
||||
|
|
|
@ -3,13 +3,13 @@ Copyright (c) 2015 Microsoft Corporation
|
|||
|
||||
Module Name:
|
||||
|
||||
ackr_model_converter.h
|
||||
ackr_model_converter.h
|
||||
|
||||
Abstract:
|
||||
|
||||
Author:
|
||||
|
||||
Mikolas Janota
|
||||
Mikolas Janota
|
||||
|
||||
Revision History:
|
||||
--*/
|
||||
|
@ -19,7 +19,7 @@ Revision History:
|
|||
#include "tactic/model_converter.h"
|
||||
#include "ackermannization/ackr_info.h"
|
||||
|
||||
model_converter * mk_ackr_model_converter(ast_manager & m, const ackr_info_ref& info, model_ref& abstr_model);
|
||||
model_converter * mk_ackr_model_converter(ast_manager & m, const ackr_info_ref& info);
|
||||
model_converter * mk_ackr_model_converter(ast_manager & m, const ackr_info_ref & info, model_ref & abstr_model);
|
||||
model_converter * mk_ackr_model_converter(ast_manager & m, const ackr_info_ref & info);
|
||||
|
||||
#endif /* LACKR_MODEL_CONVERTER_H_ */
|
||||
|
|
Loading…
Reference in a new issue