diff --git a/src/model/model.cpp b/src/model/model.cpp index f4f9af873..0e6e17c8e 100644 --- a/src/model/model.cpp +++ b/src/model/model.cpp @@ -25,7 +25,7 @@ Revision History: #include"used_symbols.h" #include"model_evaluator.h" -model::model(ast_manager & m): +model::model(ast_manager & 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()); } } - + void model::copy_usort_interps(model const & source) { sort2universe::iterator it3 = source.m_usort2universe.begin(); sort2universe::iterator end3 = source.m_usort2universe.end(); @@ -67,7 +67,7 @@ void model::copy_usort_interps(model const & source) { model * model::copy() const { model * m = alloc(model, m_manager); - + m->copy_const_interps(*this); m->copy_func_interps(*this); m->copy_usort_interps(*this); @@ -121,12 +121,12 @@ bool model::has_uninterpreted_sort(sort * s) const { return u != 0; } -unsigned model::get_num_uninterpreted_sorts() const { - return m_usorts.size(); +unsigned model::get_num_uninterpreted_sorts() const { + return m_usorts.size(); } -sort * model::get_uninterpreted_sort(unsigned idx) const { - return m_usorts[idx]; +sort * model::get_uninterpreted_sort(unsigned idx) const { + return m_usorts[idx]; } 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 * res = alloc(model, translator.to()); + model * res = alloc(model, translator.to()); // Translate const interps decl2expr::iterator it1 = m_interp.begin(); @@ -167,7 +167,7 @@ model * model::translate(ast_translation & translator) const { func_interp * fi = it2->m_value; res->register_decl(translator(it2->m_key), fi->translate(translator)); } - + // Translate usort interps sort2universe::iterator it3 = m_usort2universe.begin(); sort2universe::iterator end3 = m_usort2universe.end(); @@ -175,8 +175,8 @@ model * model::translate(ast_translation & translator) const { ptr_vector new_universe; for (unsigned i=0; im_value->size(); i++) new_universe.push_back(translator(it3->m_value->get(i))); - res->register_usort(translator(it3->m_key), - new_universe.size(), + res->register_usort(translator(it3->m_key), + new_universe.size(), new_universe.c_ptr()); } diff --git a/src/model/model_core.cpp b/src/model/model_core.cpp index 3a3a8a93a..3c10f8704 100644 --- a/src/model/model_core.cpp +++ b/src/model/model_core.cpp @@ -31,7 +31,7 @@ model_core::~model_core() { for (; it2 != end2; ++it2) { m_manager.dec_ref(it2->m_key); dealloc(it2->m_value); - } + } } bool model_core::eval(func_decl* f, expr_ref & r) const { diff --git a/src/smt/proto_model/proto_model.cpp b/src/smt/proto_model/proto_model.cpp index 036a09bb6..8fc262bac 100644 --- a/src/smt/proto_model/proto_model.cpp +++ b/src/smt/proto_model/proto_model.cpp @@ -34,7 +34,7 @@ proto_model::proto_model(ast_manager & m, params_ref const & p): register_factory(alloc(basic_factory, m)); m_user_sort_factory = alloc(user_sort_factory, m); register_factory(m_user_sort_factory); - + 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 { - return - is_app_of(e, m_afid, OP_SELECT) && + return + is_app_of(e, m_afid, OP_SELECT) && 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)))); } @@ -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, then r contains a term that is simplified as much as possible using the interpretations available in the model. - + 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. 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)) { UNREACHABLE(); } - + fi->set_else(a); } @@ -225,12 +225,12 @@ void proto_model::cleanup() { func_interp * fi = (*it).m_value; cleanup_func_interp(fi, found_aux_fs); } - + // remove auxiliary declarations that are not used. 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_func_decls, found_aux_fs); - + func_decl_set::iterator it2 = m_aux_decls.begin(); func_decl_set::iterator end2 = m_aux_decls.end(); for (; it2 != end2; ++it2) { @@ -277,13 +277,13 @@ ptr_vector const & proto_model::get_universe(sort * s) const { return tmp; } -unsigned proto_model::get_num_uninterpreted_sorts() const { - return m_user_sort_factory->get_num_sorts(); +unsigned proto_model::get_num_uninterpreted_sorts() const { + return m_user_sort_factory->get_num_sorts(); } -sort * proto_model::get_uninterpreted_sort(unsigned idx) const { - SASSERT(idx < get_num_uninterpreted_sorts()); - return m_user_sort_factory->get_sort(idx); +sort * proto_model::get_uninterpreted_sort(unsigned idx) const { + SASSERT(idx < get_num_uninterpreted_sorts()); + return m_user_sort_factory->get_sort(idx); } /** @@ -301,7 +301,7 @@ expr * proto_model::get_some_value(sort * s) { else { family_id fid = s->get_family_id(); value_factory * f = get_factory(fid); - if (f) + if (f) return f->get_some_value(s); // there is no factory for the family id, then assume s is uninterpreted. 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 { family_id fid = s->get_family_id(); value_factory * f = get_factory(fid); - if (f) + if (f) return f->get_some_values(s, v1, v2); else return false; @@ -327,9 +327,9 @@ expr * proto_model::get_fresh_value(sort * s) { return m_user_sort_factory->get_fresh_value(s); } else { - family_id fid = s->get_family_id(); + family_id fid = s->get_family_id(); value_factory * f = get_factory(fid); - if (f) + if (f) return f->get_fresh_value(s); else // 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); if (fi && fi->is_partial()) { expr * else_value = 0; -#if 0 +#if 0 // 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. 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() { if (m_model_partial) @@ -424,7 +424,7 @@ model * proto_model::mk_model() { m->register_decl(it2->m_key, it2->m_value); m_manager.dec_ref(it2->m_key); } - + m_finterp.reset(); // m took the ownership of the func_interp's unsigned sz = get_num_uninterpreted_sorts(); @@ -450,7 +450,7 @@ model * proto_model::mk_model() { // It uses the simplifier s during the computation. bool eval(func_interp & fi, simplifier & s, expr * const * args, expr_ref & result) { bool actuals_are_values = true; - + if (fi.num_entries() != 0) { for (unsigned i = 0; actuals_are_values && i < fi.get_arity(); 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(); return true; } - - TRACE("func_interp", tout << "failed to find entry for: "; - for(unsigned i = 0; i < fi.get_arity(); i++) - tout << mk_pp(args[i], fi.m()) << " "; + + TRACE("func_interp", tout << "failed to find entry for: "; + for(unsigned i = 0; i < fi.get_arity(); i++) + tout << mk_pp(args[i], fi.m()) << " "; tout << "\nis partial: " << fi.is_partial() << "\n";); - + if (!fi.eval_else(args, result)) { return false; } - + if (actuals_are_values && fi.args_are_values()) { // cheap case... we are done 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)); TRACE("model_eval", tout << mk_pp(e, m_manager) << "\n"; tout << "sort: " << mk_pp(m_manager.get_sort(e), m_manager) << "\n";); - + obj_map eval_cache; expr_ref_vector trail(m_manager); sbuffer, 128> todo; ptr_buffer args; expr * null = static_cast(0); todo.push_back(std::make_pair(e, null)); - + simplifier m_simplifier(m_manager); expr * a; @@ -528,7 +528,7 @@ bool proto_model::eval(expr * e, expr_ref & result, bool model_completion) { SASSERT(r != 0); todo.pop_back(); eval_cache.insert(a, r); - TRACE("model_eval", + TRACE("model_eval", tout << "orig:\n" << mk_pp(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";); @@ -556,7 +556,7 @@ bool proto_model::eval(expr * e, expr_ref & result, bool model_completion) { SASSERT(args.size() == t->get_num_args()); expr_ref new_t(m_manager); func_decl * f = t->get_decl(); - + if (!has_interpretation(f)) { // the model does not assign an interpretation to f. 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)) { SASSERT(fi->is_partial()); // fi->eval only fails when fi is partial. if (model_completion) { - expr * r = get_some_value(f->get_range()); + expr * r = get_some_value(f->get_range()); fi->set_else(r); SASSERT(!fi->is_partial()); 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 << "new:\n" << mk_pp(new_t, m_manager) << "\n";); 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); break; } - case AST_VAR: + case AST_VAR: SASSERT(a != 0); eval_cache.insert(a, a); todo.pop_back(); break; - case AST_QUANTIFIER: + case AST_QUANTIFIER: TRACE("model_eval", tout << "found quantifier\n" << mk_pp(a, m_manager) << "\n";); is_ok = false; // evaluator does not handle quantifiers. SASSERT(a != 0); @@ -669,12 +669,12 @@ bool proto_model::eval(expr * e, expr_ref & result, bool model_completion) { result = a; 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 << "evaluated: ", m_manager, a); ast_ll_pp(tout << "reduced: ", m_manager, result.get()); tout << "sort: " << mk_pp(m_manager.get_sort(e), m_manager) << "\n"; - ); + ); SASSERT(is_well_sorted(m_manager, result.get())); return is_ok; }