mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-07 09:55:19 +00:00
Code Activity

whitespace

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2016-04-01 13:22:16 +01:00
parent 405650c183
commit 852dc6d190
3 changed files with 48 additions and 48 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

22
src/model/model.cpp
View file

@ -25,7 +25,7 @@ Revision History:
#include"used_symbols.h" #include"used_symbols.h"
#include"model_evaluator.h" #include"model_evaluator.h"
model::model(ast_manager & m): model::model(ast_manager & m):
model_core(m) { model_core(m) {
} }
@ -56,7 +56,7 @@ void model::copy_func_interps(model const & source) {
register_decl(it2->m_key, it2->m_value->copy()); register_decl(it2->m_key, it2->m_value->copy());
} }
} }
void model::copy_usort_interps(model const & source) { void model::copy_usort_interps(model const & source) {
sort2universe::iterator it3 = source.m_usort2universe.begin(); sort2universe::iterator it3 = source.m_usort2universe.begin();
sort2universe::iterator end3 = source.m_usort2universe.end(); sort2universe::iterator end3 = source.m_usort2universe.end();
@ -67,7 +67,7 @@ void model::copy_usort_interps(model const & source) {
model * model::copy() const { model * model::copy() const {
model * m = alloc(model, m_manager); model * m = alloc(model, m_manager);
m->copy_const_interps(*this); m->copy_const_interps(*this);
m->copy_func_interps(*this); m->copy_func_interps(*this);
m->copy_usort_interps(*this); m->copy_usort_interps(*this);
@ -121,12 +121,12 @@ bool model::has_uninterpreted_sort(sort * s) const {
return u != 0; return u != 0;
} }
unsigned model::get_num_uninterpreted_sorts() const { unsigned model::get_num_uninterpreted_sorts() const {
return m_usorts.size(); return m_usorts.size();
} }
sort * model::get_uninterpreted_sort(unsigned idx) const { sort * model::get_uninterpreted_sort(unsigned idx) const {
return m_usorts[idx]; return m_usorts[idx];
} }
void model::register_usort(sort * s, unsigned usize, expr * const * universe) { void model::register_usort(sort * s, unsigned usize, expr * const * universe) {
@ -151,7 +151,7 @@ void model::register_usort(sort * s, unsigned usize, expr * const * universe) {
} }
model * model::translate(ast_translation & translator) const { model * model::translate(ast_translation & translator) const {
model * res = alloc(model, translator.to()); model * res = alloc(model, translator.to());
// Translate const interps // Translate const interps
decl2expr::iterator it1 = m_interp.begin(); decl2expr::iterator it1 = m_interp.begin();
@ -167,7 +167,7 @@ model * model::translate(ast_translation & translator) const {
func_interp * fi = it2->m_value; func_interp * fi = it2->m_value;
res->register_decl(translator(it2->m_key), fi->translate(translator)); res->register_decl(translator(it2->m_key), fi->translate(translator));
} }
// Translate usort interps // Translate usort interps
sort2universe::iterator it3 = m_usort2universe.begin(); sort2universe::iterator it3 = m_usort2universe.begin();
sort2universe::iterator end3 = m_usort2universe.end(); sort2universe::iterator end3 = m_usort2universe.end();
@ -175,8 +175,8 @@ model * model::translate(ast_translation & translator) const {
ptr_vector<expr> new_universe; ptr_vector<expr> new_universe;
for (unsigned i=0; i<it3->m_value->size(); i++) for (unsigned i=0; i<it3->m_value->size(); i++)
new_universe.push_back(translator(it3->m_value->get(i))); new_universe.push_back(translator(it3->m_value->get(i)));
res->register_usort(translator(it3->m_key), res->register_usort(translator(it3->m_key),
new_universe.size(), new_universe.size(),
new_universe.c_ptr()); new_universe.c_ptr());
} }

2
src/model/model_core.cpp
View file

@ -31,7 +31,7 @@ model_core::~model_core() {
for (; it2 != end2; ++it2) { for (; it2 != end2; ++it2) {
m_manager.dec_ref(it2->m_key); m_manager.dec_ref(it2->m_key);
dealloc(it2->m_value); dealloc(it2->m_value);
} }
} }
bool model_core::eval(func_decl* f, expr_ref & r) const { bool model_core::eval(func_decl* f, expr_ref & r) const {

72
src/smt/proto_model/proto_model.cpp
View file

@ -34,7 +34,7 @@ proto_model::proto_model(ast_manager & m, params_ref const & p):
register_factory(alloc(basic_factory, m)); register_factory(alloc(basic_factory, m));
m_user_sort_factory = alloc(user_sort_factory, m); m_user_sort_factory = alloc(user_sort_factory, m);
register_factory(m_user_sort_factory); register_factory(m_user_sort_factory);
m_model_partial = model_params(p).partial(); m_model_partial = model_params(p).partial();
} }
@ -85,8 +85,8 @@ expr * proto_model::mk_some_interp_for(func_decl * d) {
bool proto_model::is_select_of_model_value(expr* e) const { bool proto_model::is_select_of_model_value(expr* e) const {
return return
is_app_of(e, m_afid, OP_SELECT) && is_app_of(e, m_afid, OP_SELECT) &&
is_as_array(to_app(e)->get_arg(0)) && is_as_array(to_app(e)->get_arg(0)) &&
has_interpretation(array_util(m_manager).get_as_array_func_decl(to_app(to_app(e)->get_arg(0)))); has_interpretation(array_util(m_manager).get_as_array_func_decl(to_app(to_app(e)->get_arg(0))));
} }
@ -115,7 +115,7 @@ bool proto_model::eval(expr * e, expr_ref & result, bool model_completion) {
It returns \c true if succeeded, and false otherwise. If the evaluation fails, It returns \c true if succeeded, and false otherwise. If the evaluation fails,
then r contains a term that is simplified as much as possible using the interpretations then r contains a term that is simplified as much as possible using the interpretations
available in the model. available in the model.
When model_completion == true, if the model does not assign an interpretation to a When model_completion == true, if the model does not assign an interpretation to a
declaration it will build one for it. Moreover, partial functions will also be completed. declaration it will build one for it. Moreover, partial functions will also be completed.
So, if model_completion == true, the evaluator never fails if it doesn't contain quantifiers. So, if model_completion == true, the evaluator never fails if it doesn't contain quantifiers.
@ -194,7 +194,7 @@ void proto_model::cleanup_func_interp(func_interp * fi, func_decl_set & found_au
if (!cache.find(fi_else, a)) { if (!cache.find(fi_else, a)) {
UNREACHABLE(); UNREACHABLE();
} }
fi->set_else(a); fi->set_else(a);
} }
@ -225,12 +225,12 @@ void proto_model::cleanup() {
func_interp * fi = (*it).m_value; func_interp * fi = (*it).m_value;
cleanup_func_interp(fi, found_aux_fs); cleanup_func_interp(fi, found_aux_fs);
} }
// remove auxiliary declarations that are not used. // remove auxiliary declarations that are not used.
if (found_aux_fs.size() != m_aux_decls.size()) { if (found_aux_fs.size() != m_aux_decls.size()) {
remove_aux_decls_not_in_set(m_decls, found_aux_fs); remove_aux_decls_not_in_set(m_decls, found_aux_fs);
remove_aux_decls_not_in_set(m_func_decls, found_aux_fs); remove_aux_decls_not_in_set(m_func_decls, found_aux_fs);
func_decl_set::iterator it2 = m_aux_decls.begin(); func_decl_set::iterator it2 = m_aux_decls.begin();
func_decl_set::iterator end2 = m_aux_decls.end(); func_decl_set::iterator end2 = m_aux_decls.end();
for (; it2 != end2; ++it2) { for (; it2 != end2; ++it2) {
@ -277,13 +277,13 @@ ptr_vector<expr> const & proto_model::get_universe(sort * s) const {
return tmp; return tmp;
} }
unsigned proto_model::get_num_uninterpreted_sorts() const { unsigned proto_model::get_num_uninterpreted_sorts() const {
return m_user_sort_factory->get_num_sorts(); return m_user_sort_factory->get_num_sorts();
} }
sort * proto_model::get_uninterpreted_sort(unsigned idx) const { sort * proto_model::get_uninterpreted_sort(unsigned idx) const {
SASSERT(idx < get_num_uninterpreted_sorts()); SASSERT(idx < get_num_uninterpreted_sorts());
return m_user_sort_factory->get_sort(idx); return m_user_sort_factory->get_sort(idx);
} }
/** /**
@ -301,7 +301,7 @@ expr * proto_model::get_some_value(sort * s) {
else { else {
family_id fid = s->get_family_id(); family_id fid = s->get_family_id();
value_factory * f = get_factory(fid); value_factory * f = get_factory(fid);
if (f) if (f)
return f->get_some_value(s); return f->get_some_value(s);
// there is no factory for the family id, then assume s is uninterpreted. // there is no factory for the family id, then assume s is uninterpreted.
return m_user_sort_factory->get_some_value(s); return m_user_sort_factory->get_some_value(s);
@ -315,7 +315,7 @@ bool proto_model::get_some_values(sort * s, expr_ref & v1, expr_ref & v2) {
else { else {
family_id fid = s->get_family_id(); family_id fid = s->get_family_id();
value_factory * f = get_factory(fid); value_factory * f = get_factory(fid);
if (f) if (f)
return f->get_some_values(s, v1, v2); return f->get_some_values(s, v1, v2);
else else
return false; return false;
@ -327,9 +327,9 @@ expr * proto_model::get_fresh_value(sort * s) {
return m_user_sort_factory->get_fresh_value(s); return m_user_sort_factory->get_fresh_value(s);
} }
else { else {
family_id fid = s->get_family_id(); family_id fid = s->get_family_id();
value_factory * f = get_factory(fid); value_factory * f = get_factory(fid);
if (f) if (f)
return f->get_fresh_value(s); return f->get_fresh_value(s);
else else
// Use user_sort_factory if the theory has no support for model construnction. // Use user_sort_factory if the theory has no support for model construnction.
@ -374,7 +374,7 @@ void proto_model::complete_partial_func(func_decl * f) {
func_interp * fi = get_func_interp(f); func_interp * fi = get_func_interp(f);
if (fi && fi->is_partial()) { if (fi && fi->is_partial()) {
expr * else_value = 0; expr * else_value = 0;
#if 0 #if 0
// For UFBV benchmarks, setting the "else" to false is not a good idea. // For UFBV benchmarks, setting the "else" to false is not a good idea.
// TODO: find a permanent solution. A possibility is to add another option. // TODO: find a permanent solution. A possibility is to add another option.
if (m_manager.is_bool(f->get_range())) { if (m_manager.is_bool(f->get_range())) {
@ -395,7 +395,7 @@ void proto_model::complete_partial_func(func_decl * f) {
} }
/** /**
\brief Set the (else) field of function interpretations... \brief Set the (else) field of function interpretations...
*/ */
void proto_model::complete_partial_funcs() { void proto_model::complete_partial_funcs() {
if (m_model_partial) if (m_model_partial)
@ -424,7 +424,7 @@ model * proto_model::mk_model() {
m->register_decl(it2->m_key, it2->m_value); m->register_decl(it2->m_key, it2->m_value);
m_manager.dec_ref(it2->m_key); m_manager.dec_ref(it2->m_key);
} }
m_finterp.reset(); // m took the ownership of the func_interp's m_finterp.reset(); // m took the ownership of the func_interp's
unsigned sz = get_num_uninterpreted_sorts(); unsigned sz = get_num_uninterpreted_sorts();
@ -450,7 +450,7 @@ model * proto_model::mk_model() {
// It uses the simplifier s during the computation. // It uses the simplifier s during the computation.
bool eval(func_interp & fi, simplifier & s, expr * const * args, expr_ref & result) { bool eval(func_interp & fi, simplifier & s, expr * const * args, expr_ref & result) {
bool actuals_are_values = true; bool actuals_are_values = true;
if (fi.num_entries() != 0) { if (fi.num_entries() != 0) {
for (unsigned i = 0; actuals_are_values && i < fi.get_arity(); i++) { for (unsigned i = 0; actuals_are_values && i < fi.get_arity(); i++) {
actuals_are_values = fi.m().is_value(args[i]); actuals_are_values = fi.m().is_value(args[i]);
@ -462,16 +462,16 @@ bool eval(func_interp & fi, simplifier & s, expr * const * args, expr_ref & resu
result = entry->get_result(); result = entry->get_result();
return true; return true;
} }
TRACE("func_interp", tout << "failed to find entry for: "; TRACE("func_interp", tout << "failed to find entry for: ";
for(unsigned i = 0; i < fi.get_arity(); i++) for(unsigned i = 0; i < fi.get_arity(); i++)
tout << mk_pp(args[i], fi.m()) << " "; tout << mk_pp(args[i], fi.m()) << " ";
tout << "\nis partial: " << fi.is_partial() << "\n";); tout << "\nis partial: " << fi.is_partial() << "\n";);
if (!fi.eval_else(args, result)) { if (!fi.eval_else(args, result)) {
return false; return false;
} }
if (actuals_are_values && fi.args_are_values()) { if (actuals_are_values && fi.args_are_values()) {
// cheap case... we are done // cheap case... we are done
return true; return true;
@ -506,14 +506,14 @@ bool proto_model::eval(expr * e, expr_ref & result, bool model_completion) {
SASSERT(is_well_sorted(m_manager, e)); SASSERT(is_well_sorted(m_manager, e));
TRACE("model_eval", tout << mk_pp(e, m_manager) << "\n"; TRACE("model_eval", tout << mk_pp(e, m_manager) << "\n";
tout << "sort: " << mk_pp(m_manager.get_sort(e), m_manager) << "\n";); tout << "sort: " << mk_pp(m_manager.get_sort(e), m_manager) << "\n";);
obj_map<expr, expr*> eval_cache; obj_map<expr, expr*> eval_cache;
expr_ref_vector trail(m_manager); expr_ref_vector trail(m_manager);
sbuffer<std::pair<expr*, expr*>, 128> todo; sbuffer<std::pair<expr*, expr*>, 128> todo;
ptr_buffer<expr> args; ptr_buffer<expr> args;
expr * null = static_cast<expr*>(0); expr * null = static_cast<expr*>(0);
todo.push_back(std::make_pair(e, null)); todo.push_back(std::make_pair(e, null));
simplifier m_simplifier(m_manager); simplifier m_simplifier(m_manager);
expr * a; expr * a;
@ -528,7 +528,7 @@ bool proto_model::eval(expr * e, expr_ref & result, bool model_completion) {
SASSERT(r != 0); SASSERT(r != 0);
todo.pop_back(); todo.pop_back();
eval_cache.insert(a, r); eval_cache.insert(a, r);
TRACE("model_eval", TRACE("model_eval",
tout << "orig:\n" << mk_pp(a, m_manager) << "\n"; tout << "orig:\n" << mk_pp(a, m_manager) << "\n";
tout << "after beta reduction:\n" << mk_pp(expanded_a, m_manager) << "\n"; tout << "after beta reduction:\n" << mk_pp(expanded_a, m_manager) << "\n";
tout << "new:\n" << mk_pp(r, m_manager) << "\n";); tout << "new:\n" << mk_pp(r, m_manager) << "\n";);
@ -556,7 +556,7 @@ bool proto_model::eval(expr * e, expr_ref & result, bool model_completion) {
SASSERT(args.size() == t->get_num_args()); SASSERT(args.size() == t->get_num_args());
expr_ref new_t(m_manager); expr_ref new_t(m_manager);
func_decl * f = t->get_decl(); func_decl * f = t->get_decl();
if (!has_interpretation(f)) { if (!has_interpretation(f)) {
// the model does not assign an interpretation to f. // the model does not assign an interpretation to f.
SASSERT(new_t.get() == 0); SASSERT(new_t.get() == 0);
@ -606,7 +606,7 @@ bool proto_model::eval(expr * e, expr_ref & result, bool model_completion) {
if (!::eval(*fi, m_simplifier, args.c_ptr(), r1)) { if (!::eval(*fi, m_simplifier, args.c_ptr(), r1)) {
SASSERT(fi->is_partial()); // fi->eval only fails when fi is partial. SASSERT(fi->is_partial()); // fi->eval only fails when fi is partial.
if (model_completion) { if (model_completion) {
expr * r = get_some_value(f->get_range()); expr * r = get_some_value(f->get_range());
fi->set_else(r); fi->set_else(r);
SASSERT(!fi->is_partial()); SASSERT(!fi->is_partial());
new_t = r; new_t = r;
@ -635,7 +635,7 @@ bool proto_model::eval(expr * e, expr_ref & result, bool model_completion) {
} }
} }
} }
TRACE("model_eval", TRACE("model_eval",
tout << "orig:\n" << mk_pp(t, m_manager) << "\n"; tout << "orig:\n" << mk_pp(t, m_manager) << "\n";
tout << "new:\n" << mk_pp(new_t, m_manager) << "\n";); tout << "new:\n" << mk_pp(new_t, m_manager) << "\n";);
todo.pop_back(); todo.pop_back();
@ -643,12 +643,12 @@ bool proto_model::eval(expr * e, expr_ref & result, bool model_completion) {
eval_cache.insert(t, new_t); eval_cache.insert(t, new_t);
break; break;
} }
case AST_VAR: case AST_VAR:
SASSERT(a != 0); SASSERT(a != 0);
eval_cache.insert(a, a); eval_cache.insert(a, a);
todo.pop_back(); todo.pop_back();
break; break;
case AST_QUANTIFIER: case AST_QUANTIFIER:
TRACE("model_eval", tout << "found quantifier\n" << mk_pp(a, m_manager) << "\n";); TRACE("model_eval", tout << "found quantifier\n" << mk_pp(a, m_manager) << "\n";);
is_ok = false; // evaluator does not handle quantifiers. is_ok = false; // evaluator does not handle quantifiers.
SASSERT(a != 0); SASSERT(a != 0);
@ -669,12 +669,12 @@ bool proto_model::eval(expr * e, expr_ref & result, bool model_completion) {
result = a; result = a;
std::cout << mk_pp(e, m_manager) << "\n===>\n" << result << "\n"; std::cout << mk_pp(e, m_manager) << "\n===>\n" << result << "\n";
TRACE("model_eval", TRACE("model_eval",
ast_ll_pp(tout << "original: ", m_manager, e); ast_ll_pp(tout << "original: ", m_manager, e);
ast_ll_pp(tout << "evaluated: ", m_manager, a); ast_ll_pp(tout << "evaluated: ", m_manager, a);
ast_ll_pp(tout << "reduced: ", m_manager, result.get()); ast_ll_pp(tout << "reduced: ", m_manager, result.get());
tout << "sort: " << mk_pp(m_manager.get_sort(e), m_manager) << "\n"; tout << "sort: " << mk_pp(m_manager.get_sort(e), m_manager) << "\n";
); );
SASSERT(is_well_sorted(m_manager, result.get())); SASSERT(is_well_sorted(m_manager, result.get()));
return is_ok; return is_ok;
} }