From 9109968e5541d58159139773ffeda20e661781a5 Mon Sep 17 00:00:00 2001 From: Arie Gurfinkel Date: Wed, 13 Jun 2018 15:29:34 -0700 Subject: [PATCH] Cleanup fixedpoint options Replace pdr options with spacer Repace fixedpoint module with fp --- src/muz/base/CMakeLists.txt | 2 +- src/muz/base/dl_context.cpp | 103 +++++++------- src/muz/base/dl_context.h | 63 +++++---- .../{fixedpoint_params.pyg => fp_params.pyg} | 2 +- src/muz/bmc/dl_bmc_engine.cpp | 2 +- src/muz/fp/dl_cmds.cpp | 68 ++++----- src/muz/fp/horn_tactic.cpp | 59 ++++---- src/muz/spacer/spacer_context.cpp | 3 +- src/muz/spacer/spacer_context.h | 8 +- src/muz/spacer/spacer_iuc_solver.cpp | 40 +++--- src/muz/spacer/spacer_iuc_solver.h | 20 +-- src/muz/spacer/spacer_prop_solver.cpp | 7 +- src/muz/spacer/spacer_prop_solver.h | 4 +- src/muz/tab/tab_context.cpp | 2 +- src/muz/transforms/dl_mk_array_eq_rewrite.cpp | 2 +- .../transforms/dl_mk_array_instantiation.cpp | 2 +- src/muz/transforms/dl_mk_bit_blast.cpp | 52 +++---- .../dl_mk_interp_tail_simplifier.cpp | 31 ++--- .../dl_mk_quantifier_abstraction.cpp | 49 ++++--- src/muz/transforms/dl_mk_rule_inliner.cpp | 129 +++++++++--------- src/muz/transforms/dl_mk_scale.cpp | 20 +-- .../transforms/dl_mk_subsumption_checker.cpp | 25 ++-- src/muz/transforms/dl_transforms.cpp | 4 +- 23 files changed, 344 insertions(+), 353 deletions(-) rename src/muz/base/{fixedpoint_params.pyg => fp_params.pyg} (99%) diff --git a/src/muz/base/CMakeLists.txt b/src/muz/base/CMakeLists.txt index 6b0334664..8c21e1557 100644 --- a/src/muz/base/CMakeLists.txt +++ b/src/muz/base/CMakeLists.txt @@ -18,5 +18,5 @@ z3_add_component(muz smt smt2parser PYG_FILES - fixedpoint_params.pyg + fp_params.pyg ) diff --git a/src/muz/base/dl_context.cpp b/src/muz/base/dl_context.cpp index 2b0987be7..220b2516d 100644 --- a/src/muz/base/dl_context.cpp +++ b/src/muz/base/dl_context.cpp @@ -27,7 +27,7 @@ Revision History: #include "ast/ast_smt2_pp.h" #include "ast/datatype_decl_plugin.h" #include "ast/scoped_proof.h" -#include "muz/base/fixedpoint_params.hpp" +#include "muz/base/fp_params.hpp" #include "ast/ast_pp_util.h" @@ -152,15 +152,15 @@ namespace datalog { class context::restore_rules : public trail { rule_set* m_old_rules; - void reset() { - dealloc(m_old_rules); + void reset() { + dealloc(m_old_rules); m_old_rules = nullptr; } public: restore_rules(rule_set& r): m_old_rules(alloc(rule_set, r)) {} ~restore_rules() override {} - + void undo(context& ctx) override { ctx.replace_rules(*m_old_rules); reset(); @@ -189,7 +189,7 @@ namespace datalog { throw default_exception("there are no backtracking points to pop to"); } throw default_exception("pop operation is not supported"); - m_trail.pop_scope(1); + m_trail.pop_scope(1); } // ----------------------------------- @@ -203,7 +203,7 @@ namespace datalog { m_register_engine(re), m_fparams(fp), m_params_ref(pa), - m_params(alloc(fixedpoint_params, m_params_ref)), + m_params(alloc(fp_params, m_params_ref)), m_decl_util(m), m_rewriter(m), m_var_subst(m), @@ -235,7 +235,7 @@ namespace datalog { context::~context() { reset(); - dealloc(m_params); + dealloc(m_params); } void context::reset() { @@ -291,14 +291,14 @@ namespace datalog { bool context::similarity_compressor() const { return m_params->datalog_similarity_compressor(); } unsigned context::similarity_compressor_threshold() const { return m_params->datalog_similarity_compressor_threshold(); } unsigned context::soft_timeout() const { return m_fparams.m_timeout; } - unsigned context::initial_restart_timeout() const { return m_params->datalog_initial_restart_timeout(); } + unsigned context::initial_restart_timeout() const { return m_params->datalog_initial_restart_timeout(); } bool context::generate_explanations() const { return m_params->datalog_generate_explanations(); } bool context::explanations_on_relation_level() const { return m_params->datalog_explanations_on_relation_level(); } bool context::magic_sets_for_queries() const { return m_params->datalog_magic_sets_for_queries(); } symbol context::tab_selection() const { return m_params->tab_selection(); } bool context::xform_coi() const { return m_params->xform_coi(); } bool context::xform_slice() const { return m_params->xform_slice(); } - bool context::xform_bit_blast() const { return m_params->xform_bit_blast(); } + bool context::xform_bit_blast() const { return m_params->xform_bit_blast(); } bool context::karr() const { return m_params->xform_karr(); } bool context::scale() const { return m_params->xform_scale(); } bool context::magic() const { return m_params->xform_magic(); } @@ -428,7 +428,7 @@ namespace datalog { } - void context::set_predicate_representation(func_decl * pred, unsigned relation_name_cnt, + void context::set_predicate_representation(func_decl * pred, unsigned relation_name_cnt, symbol const * relation_names) { if (relation_name_cnt > 0) { ensure_engine(); @@ -438,9 +438,9 @@ namespace datalog { } } - func_decl * context::mk_fresh_head_predicate(symbol const & prefix, symbol const & suffix, + func_decl * context::mk_fresh_head_predicate(symbol const & prefix, symbol const & suffix, unsigned arity, sort * const * domain, func_decl* orig_pred) { - func_decl* new_pred = + func_decl* new_pred = m.mk_fresh_func_decl(prefix, suffix, arity, domain, m.mk_bool_sort()); register_predicate(new_pred, true); @@ -473,7 +473,7 @@ namespace datalog { // // Update a rule with a new. // It requires basic subsumption. - // + // void context::update_rule(expr* rl, symbol const& name) { datalog::rule_manager& rm = get_rule_manager(); proof* p = nullptr; @@ -494,13 +494,13 @@ namespace datalog { rule* old_rule = nullptr; for (unsigned i = 0; i < size_before; ++i) { if (rls[i]->name() == name) { - if (old_rule) { + if (old_rule) { std::stringstream strm; strm << "Rule " << name << " occurs twice. It cannot be modified"; m_rule_set.del_rule(r); throw default_exception(strm.str()); } - old_rule = rls[i]; + old_rule = rls[i]; } } if (old_rule) { @@ -556,7 +556,7 @@ namespace datalog { ensure_engine(); m_engine->add_cover(level, pred, property); } - + void context::add_invariant(func_decl* pred, expr *property) { ensure_engine(); @@ -566,11 +566,11 @@ namespace datalog { void context::check_rules(rule_set& r) { m_rule_properties.set_generate_proof(generate_proof_trace()); switch(get_engine()) { - case DATALOG_ENGINE: + case DATALOG_ENGINE: m_rule_properties.collect(r); m_rule_properties.check_quantifier_free(); m_rule_properties.check_uninterpreted_free(); - m_rule_properties.check_nested_free(); + m_rule_properties.check_nested_free(); m_rule_properties.check_infinite_sorts(); break; case SPACER_ENGINE: @@ -582,12 +582,12 @@ namespace datalog { case BMC_ENGINE: m_rule_properties.collect(r); m_rule_properties.check_for_negated_predicates(); - break; + break; case QBMC_ENGINE: m_rule_properties.collect(r); m_rule_properties.check_existential_tail(); m_rule_properties.check_for_negated_predicates(); - break; + break; case TAB_ENGINE: m_rule_properties.collect(r); m_rule_properties.check_existential_tail(); @@ -650,7 +650,7 @@ namespace datalog { add_fact(pred, rfact); } } - + void context::add_table_fact(func_decl * pred, unsigned num_args, unsigned args[]) { if (pred->get_arity() != num_args) { std::ostringstream out; @@ -682,7 +682,7 @@ namespace datalog { reopen(); } } - + void context::reopen() { SASSERT(m_closed); m_rule_set.reopen(); @@ -695,7 +695,7 @@ namespace datalog { transformer.register_plugin(plugin); transform_rules(transformer); } - + void context::transform_rules(rule_transformer& transf) { SASSERT(m_closed); //we must finish adding rules before we start transforming them TRACE("dl", display_rules(tout);); @@ -724,7 +724,7 @@ namespace datalog { } void context::collect_params(param_descrs& p) { - fixedpoint_params::collect_param_descrs(p); + fp_params::collect_param_descrs(p); insert_timeout(p); } @@ -732,8 +732,8 @@ namespace datalog { m_params_ref.copy(p); if (m_engine.get()) m_engine->updt_params(); m_generate_proof_trace = m_params->generate_proof_trace(); - m_unbound_compressor = m_params->datalog_unbound_compressor(); - m_default_relation = m_params->datalog_default_relation(); + m_unbound_compressor = m_params->datalog_unbound_compressor(); + m_default_relation = m_params->datalog_default_relation(); } expr_ref context::get_background_assertion() { @@ -748,7 +748,7 @@ namespace datalog { void context::assert_expr(expr* e) { TRACE("dl", tout << mk_ismt2_pp(e, m) << "\n";); - m_background.push_back(e); + m_background.push_back(e); } void context::cleanup() { @@ -785,7 +785,7 @@ namespace datalog { return; } symbol e = m_params->engine(); - + if (e == symbol("datalog")) { m_engine_type = DATALOG_ENGINE; } @@ -811,7 +811,7 @@ namespace datalog { if (m_engine_type == LAST_ENGINE) { expr_fast_mark1 mark; engine_type_proc proc(m); - m_engine_type = DATALOG_ENGINE; + m_engine_type = DATALOG_ENGINE; for (unsigned i = 0; m_engine_type == DATALOG_ENGINE && i < m_rule_set.get_num_rules(); ++i) { rule * r = m_rule_set.get_rule(i); quick_for_each_expr(proc, mark, r->get_head()); @@ -893,15 +893,15 @@ namespace datalog { m_rel = dynamic_cast(m_engine.get()); } - } + } } - lbool context::rel_query(unsigned num_rels, func_decl * const* rels) { + lbool context::rel_query(unsigned num_rels, func_decl * const* rels) { m_last_answer = nullptr; ensure_engine(); return m_engine->query(num_rels, rels); } - + expr* context::get_answer_as_formula() { if (m_last_answer) { return m_last_answer.get(); @@ -954,7 +954,7 @@ namespace datalog { void context::display(std::ostream & out) const { display_rules(out); - if (m_rel) m_rel->display_facts(out); + if (m_rel) m_rel->display_facts(out); } void context::display_profile(std::ostream& out) const { @@ -990,10 +990,10 @@ namespace datalog { bool context::result_contains_fact(relation_fact const& f) { return m_rel && m_rel->result_contains_fact(f); } - + // NB: algebraic data-types declarations will not be printed. - static void collect_free_funcs(unsigned sz, expr* const* exprs, + static void collect_free_funcs(unsigned sz, expr* const* exprs, ast_pp_util& v, mk_fresh_name& fresh_names) { v.collect(sz, exprs); @@ -1005,7 +1005,7 @@ namespace datalog { fresh_names.add(e); } } - + void context::get_raw_rule_formulas(expr_ref_vector& rules, svector& names, unsigned_vector &bounds) { for (unsigned i = 0; i < m_rule_fmls.size(); ++i) { expr_ref r = bind_vars(m_rule_fmls[i].get(), true); @@ -1018,7 +1018,7 @@ namespace datalog { void context::get_rules_as_formulas(expr_ref_vector& rules, expr_ref_vector& queries, svector& names) { expr_ref fml(m); rule_manager& rm = get_rule_manager(); - + // ensure that rules are all using bound variables. for (unsigned i = m_rule_fmls_head; i < m_rule_fmls.size(); ++i) { m_free_vars(m_rule_fmls[i].get()); @@ -1067,7 +1067,7 @@ namespace datalog { } for (unsigned i = m_rule_fmls_head; i < m_rule_fmls.size(); ++i) { rules.push_back(m_rule_fmls[i].get()); - names.push_back(m_rule_names[i]); + names.push_back(m_rule_names[i]); } } @@ -1080,7 +1080,7 @@ namespace datalog { } return out; } - + void context::display_smt2(unsigned num_queries, expr* const* qs, std::ostream& out) { ast_manager& m = get_manager(); ast_pp_util visitor(m); @@ -1109,7 +1109,7 @@ namespace datalog { for (unsigned i = 0; i < sz; ++i) { func_decl* f = visitor.coll.get_func_decls()[i]; if (f->get_family_id() != null_family_id) { - // + // } else if (is_predicate(f) && use_fixedpoint_extensions) { rels.insert(f); @@ -1122,12 +1122,12 @@ namespace datalog { if (!use_fixedpoint_extensions) { out << "(set-logic HORN)\n"; } - for (func_decl * f : rels) + for (func_decl * f : rels) visitor.remove_decl(f); visitor.display_decls(out); - for (func_decl * f : rels) + for (func_decl * f : rels) display_rel_decl(out, f); if (use_fixedpoint_extensions && do_declare_vars) { @@ -1143,7 +1143,7 @@ namespace datalog { PP(axioms[i]); out << ")\n"; } - for (unsigned i = 0; i < rules.size(); ++i) { + for (unsigned i = 0; i < rules.size(); ++i) { out << (use_fixedpoint_extensions?"(rule ":"(assert "); expr* r = rules[i].get(); symbol nm = names[i]; @@ -1156,7 +1156,7 @@ namespace datalog { while (fresh_names.contains(nm)) { std::ostringstream s; s << nm << "!"; - nm = symbol(s.str().c_str()); + nm = symbol(s.str().c_str()); } fresh_names.add(nm); display_symbol(out, nm) << ")"; @@ -1182,7 +1182,7 @@ namespace datalog { args.push_back(m.mk_var(j, m_free_vars[j])); } qfn = m.mk_implies(q, m.mk_app(fn, args.size(), args.c_ptr())); - + out << "(assert "; PP(qfn); out << ")\n"; @@ -1209,7 +1209,7 @@ namespace datalog { smt2_pp_environment_dbg env(m); out << "(declare-rel "; display_symbol(out, f->get_name()) << " ("; - for (unsigned i = 0; i < f->get_arity(); ++i) { + for (unsigned i = 0; i < f->get_arity(); ++i) { ast_smt2_pp(out, f->get_domain(i), env); if (i + 1 < f->get_arity()) { out << " "; @@ -1239,12 +1239,12 @@ namespace datalog { void context::declare_vars(expr_ref_vector& rules, mk_fresh_name& fresh_names, std::ostream& out) { // // replace bound variables in rules by 'var declarations' - // First remove quantifers, then replace bound variables + // First remove quantifers, then replace bound variables // by fresh constants. - // + // smt2_pp_environment_dbg env(m); var_subst vsubst(m, false); - + expr_ref_vector fresh_vars(m), subst(m); expr_ref res(m); obj_map var_idxs; @@ -1257,7 +1257,7 @@ namespace datalog { quantifier* q = to_quantifier(r); if (!q->is_forall()) { continue; - } + } if (has_quantifiers(q->get_expr())) { continue; } @@ -1287,7 +1287,7 @@ namespace datalog { fresh_vars.push_back(m.mk_const(name, s)); out << "(declare-var " << name << " "; ast_smt2_pp(out, s, env); - out << ")\n"; + out << ")\n"; } subst.push_back(fresh_vars[vars[max_var]].get()); } @@ -1299,4 +1299,3 @@ namespace datalog { }; - diff --git a/src/muz/base/dl_context.h b/src/muz/base/dl_context.h index b49c7e665..6e6bc80dc 100644 --- a/src/muz/base/dl_context.h +++ b/src/muz/base/dl_context.h @@ -44,7 +44,7 @@ Revision History: #include "muz/base/bind_variables.h" #include "muz/base/rule_properties.h" -struct fixedpoint_params; +struct fp_params; namespace datalog { @@ -98,7 +98,7 @@ namespace datalog { relation_fact(ast_manager & m) : app_ref_vector(m) {} relation_fact(ast_manager & m, unsigned sz) : app_ref_vector(m) { resize(sz); } relation_fact(context & ctx); - + iterator begin() const { return c_ptr(); } iterator end() const { return c_ptr()+size(); } @@ -126,7 +126,7 @@ namespace datalog { virtual bool has_facts(func_decl * pred) const = 0; virtual void store_relation(func_decl * pred, relation_base * rel) = 0; virtual void inherit_predicate_kind(func_decl* new_pred, func_decl* orig_pred) = 0; - virtual void set_predicate_representation(func_decl * pred, unsigned relation_name_cnt, + virtual void set_predicate_representation(func_decl * pred, unsigned relation_name_cnt, symbol const * relation_names) = 0; virtual bool output_profile() const = 0; virtual void collect_non_empty_predicates(func_decl_set& preds) = 0; @@ -147,7 +147,7 @@ namespace datalog { public: contains_pred(context& ctx): ctx(ctx) {} ~contains_pred() override {} - + bool operator()(expr* e) override { return ctx.is_predicate(e); } @@ -170,7 +170,7 @@ namespace datalog { register_engine_base& m_register_engine; smt_params & m_fparams; params_ref m_params_ref; - fixedpoint_params* m_params; + fp_params* m_params; bool m_generate_proof_trace; // cached configuration parameter bool m_unbound_compressor; // cached configuration parameter symbol m_default_relation; // cached configuration parameter @@ -227,7 +227,7 @@ namespace datalog { void push(); void pop(); - + bool saturation_was_run() const { return m_saturation_was_run; } void notify_saturation_was_run() { m_saturation_was_run = true; } @@ -236,7 +236,7 @@ namespace datalog { ast_manager & get_manager() const { return m; } rule_manager & get_rule_manager() { return m_rule_manager; } smt_params & get_fparams() const { return m_fparams; } - fixedpoint_params const& get_params() const { return *m_params; } + fp_params const& get_params() const { return *m_params; } DL_ENGINE get_engine() { configure_engine(); return m_engine_type; } register_engine_base& get_register_engine() { return m_register_engine; } th_rewriter& get_rewriter() { return m_rewriter; } @@ -251,7 +251,7 @@ namespace datalog { symbol default_table() const; symbol default_relation() const; void set_default_relation(symbol const& s); - symbol default_table_checker() const; + symbol default_table_checker() const; symbol check_relation() const; bool default_table_checked() const; bool dbg_fpr_nonempty_relation_signature() const; @@ -275,7 +275,7 @@ namespace datalog { bool compress_unbound() const; bool quantify_arrays() const; bool instantiate_quantifiers() const; - bool xform_bit_blast() const; + bool xform_bit_blast() const; bool xform_slice() const; bool xform_coi() const; bool array_blast() const; @@ -291,9 +291,9 @@ namespace datalog { void register_variable(func_decl* var); /* - Replace constants that have been registered as + Replace constants that have been registered as variables by de-Bruijn indices and corresponding - universal (if is_forall is true) or existential + universal (if is_forall is true) or existential quantifier. */ expr_ref bind_vars(expr* fml, bool is_forall); @@ -303,7 +303,7 @@ namespace datalog { /** Register datalog relation. - If named is true, we associate the predicate with its name, so that it can be + If named is true, we associate the predicate with its name, so that it can be retrieved by the try_get_predicate_decl() function. Auxiliary predicates introduced e.g. by rule transformations do not need to be named. */ @@ -326,7 +326,7 @@ namespace datalog { /** \brief If a predicate name has a \c func_decl object assigned, return pointer to it; otherwise return 0. - + Not all \c func_decl object used as relation identifiers need to be assigned to their names. Generally, the names coming from the parses are registered here. */ @@ -334,13 +334,13 @@ namespace datalog { func_decl * res = nullptr; m_preds_by_name.find(pred_name, res); return res; - } + } /** \brief Create a fresh head predicate declaration. */ - func_decl * mk_fresh_head_predicate(symbol const & prefix, symbol const & suffix, + func_decl * mk_fresh_head_predicate(symbol const & prefix, symbol const & suffix, unsigned arity, sort * const * domain, func_decl* orig_pred=nullptr); @@ -365,13 +365,13 @@ namespace datalog { /** \brief Assign names of variables used in the declaration of a predicate. - These names are used when printing out the relations to make the output conform + These names are used when printing out the relations to make the output conform to the one of bddbddb. */ void set_argument_names(const func_decl * pred, const svector & var_names); symbol get_argument_name(const func_decl * pred, unsigned arg_index); - void set_predicate_representation(func_decl * pred, unsigned relation_name_cnt, + void set_predicate_representation(func_decl * pred, unsigned relation_name_cnt, symbol const * relation_names); void set_output_predicate(func_decl * pred) { m_rule_set.set_output_predicate(pred); } @@ -385,9 +385,9 @@ namespace datalog { void add_fact(func_decl * pred, const relation_fact & fact); bool has_facts(func_decl * pred) const; - + void add_rule(rule_ref& r); - + void assert_expr(expr* e); expr_ref get_background_assertion(); unsigned get_num_assertions() { return m_background.size(); } @@ -397,7 +397,7 @@ namespace datalog { Method exposed from API for adding rules. */ void add_rule(expr* rl, symbol const& name, unsigned bound = UINT_MAX); - + /** Update a named rule. @@ -421,9 +421,9 @@ namespace datalog { at 'level+1', 'level+2' etc, and include level=-1. */ expr_ref get_cover_delta(int level, func_decl* pred); - + /** - Add a property of predicate 'pred' at 'level'. + Add a property of predicate 'pred' at 'level'. It gets pushed forward when possible. */ void add_cover(int level, func_decl* pred, expr* property); @@ -432,7 +432,7 @@ namespace datalog { Add an invariant of predicate 'pred'. */ void add_invariant (func_decl *pred, expr *property); - + /** \brief Check rule subsumption. */ @@ -471,15 +471,15 @@ namespace datalog { proof_converter_ref& get_proof_converter() { return m_pc; } void add_proof_converter(proof_converter* pc) { m_pc = concat(m_pc.get(), pc); } - void transform_rules(rule_transformer& transf); + void transform_rules(rule_transformer& transf); void transform_rules(rule_transformer::plugin* plugin); void replace_rules(rule_set const& rs); void record_transformed_rules(); - void apply_default_transformation(); + void apply_default_transformation(); void collect_params(param_descrs& r); - + void updt_params(params_ref const& p); void display_rules(std::ostream & out) const { @@ -507,7 +507,7 @@ namespace datalog { /** \brief check if query 'q' is satisfied under asserted rules and background. - If successful, return OK and into \c result assign a relation with all + If successful, return OK and into \c result assign a relation with all tuples matching the query. Otherwise return reason for failure and do not modify \c result. @@ -515,7 +515,7 @@ namespace datalog { starting from zero. The caller becomes an owner of the relation object returned in \c result. The - relation object, however, should not outlive the datalog context since it is + relation object, however, should not outlive the datalog context since it is linked to a relation plugin in the context. */ @@ -524,7 +524,7 @@ namespace datalog { lbool query_from_lvl (expr* q, unsigned lvl); /** \brief retrieve model from inductive invariant that shows query is unsat. - + \pre engine == 'pdr' || engine == 'duality' - this option is only supported for PDR mode and Duality mode. */ @@ -532,7 +532,7 @@ namespace datalog { /** \brief retrieve proof from derivation of the query. - + \pre engine == 'pdr' || engine == 'duality'- this option is only supported for PDR mode and Duality mode. */ @@ -606,7 +606,7 @@ namespace datalog { /** Just reset all tables. */ - void reset_tables(); + void reset_tables(); void flush_add_rules(); @@ -627,4 +627,3 @@ namespace datalog { }; #endif /* DL_CONTEXT_H_ */ - diff --git a/src/muz/base/fixedpoint_params.pyg b/src/muz/base/fp_params.pyg similarity index 99% rename from src/muz/base/fixedpoint_params.pyg rename to src/muz/base/fp_params.pyg index 7e92b0d2c..c96a12ca2 100644 --- a/src/muz/base/fixedpoint_params.pyg +++ b/src/muz/base/fp_params.pyg @@ -1,4 +1,4 @@ -def_module_params('fixedpoint', +def_module_params('fp', description='fixedpoint parameters', export=True, params=(('timeout', UINT, UINT_MAX, 'set timeout'), diff --git a/src/muz/bmc/dl_bmc_engine.cpp b/src/muz/bmc/dl_bmc_engine.cpp index 56b7e449d..c7657a0d7 100644 --- a/src/muz/bmc/dl_bmc_engine.cpp +++ b/src/muz/bmc/dl_bmc_engine.cpp @@ -33,7 +33,7 @@ Revision History: #include "muz/transforms/dl_mk_rule_inliner.h" #include "ast/scoped_proof.h" -#include "muz/base/fixedpoint_params.hpp" +#include "muz/base/fp_params.hpp" namespace datalog { diff --git a/src/muz/fp/dl_cmds.cpp b/src/muz/fp/dl_cmds.cpp index ba12c849c..4605826ba 100644 --- a/src/muz/fp/dl_cmds.cpp +++ b/src/muz/fp/dl_cmds.cpp @@ -30,23 +30,23 @@ Notes: #include "util/scoped_ctrl_c.h" #include "util/scoped_timer.h" #include "util/trail.h" -#include "muz/base/fixedpoint_params.hpp" +#include "muz/base/fp_params.hpp" #include struct dl_context { smt_params m_fparams; params_ref m_params_ref; - fixedpoint_params m_params; + fp_params m_params; cmd_context & m_cmd; datalog::register_engine m_register_engine; dl_collected_cmds* m_collected_cmds; unsigned m_ref_count; datalog::dl_decl_plugin* m_decl_plugin; - scoped_ptr m_context; + scoped_ptr m_context; trail_stack m_trail; - fixedpoint_params const& get_params() { + fp_params const& get_params() { init(); return m_context->get_params(); } @@ -58,18 +58,18 @@ struct dl_context { m_ref_count(0), m_decl_plugin(nullptr), m_trail(*this) {} - + void inc_ref() { ++m_ref_count; } - + void dec_ref() { --m_ref_count; if (0 == m_ref_count) { dealloc(this); } } - + void init() { ast_manager& m = m_cmd.m(); if (!m_context) { @@ -83,10 +83,10 @@ struct dl_context { else { m_decl_plugin = alloc(datalog::dl_decl_plugin); m.register_plugin(symbol("datalog_relation"), m_decl_plugin); - } + } } } - + void reset() { m_context = nullptr; } @@ -97,9 +97,9 @@ struct dl_context { m_trail.push(push_back_vector(m_collected_cmds->m_rels)); } dlctx().register_predicate(pred, false); - dlctx().set_predicate_representation(pred, num_kinds, kinds); + dlctx().set_predicate_representation(pred, num_kinds, kinds); } - + void add_rule(expr * rule, symbol const& name, unsigned bound) { init(); if (m_collected_cmds) { @@ -112,7 +112,7 @@ struct dl_context { else { m_context->add_rule(rule, name, bound); } - } + } bool collect_query(func_decl* q) { if (m_collected_cmds) { @@ -127,7 +127,7 @@ struct dl_context { m_collected_cmds->m_queries.push_back(qr); m_trail.push(push_back_vector(m_collected_cmds->m_queries)); return true; - } + } else { return false; } @@ -142,7 +142,7 @@ struct dl_context { m_trail.pop_scope(1); dlctx().pop(); } - + datalog::context & dlctx() { init(); return *m_context; @@ -162,7 +162,7 @@ class dl_rule_cmd : public cmd { public: dl_rule_cmd(dl_context * dl_ctx): cmd("rule"), - m_dl_ctx(dl_ctx), + m_dl_ctx(dl_ctx), m_arg_idx(0), m_t(nullptr), m_bound(UINT_MAX) {} @@ -210,7 +210,7 @@ public: } char const * get_usage() const override { return "predicate"; } char const * get_main_descr() const override { - return "pose a query to a predicate based on the Horn rules."; + return "pose a query to a predicate based on the Horn rules."; } cmd_arg_kind next_arg_kind(cmd_context & ctx) const override { @@ -243,9 +243,9 @@ public: return; } datalog::context& dlctx = m_dl_ctx->dlctx(); - set_background(ctx); + set_background(ctx); dlctx.updt_params(m_params); - unsigned timeout = m_dl_ctx->get_params().timeout(); + unsigned timeout = m_dl_ctx->get_params().timeout(); cancel_eh eh(ctx.m().limit()); bool query_exn = false; lbool status = l_undef; @@ -271,12 +271,12 @@ public: ctx.regular_stream() << "unsat\n"; print_certificate(ctx); break; - case l_true: + case l_true: ctx.regular_stream() << "sat\n"; print_answer(ctx); print_certificate(ctx); break; - case l_undef: + case l_undef: if (dlctx.get_status() == datalog::BOUNDED){ ctx.regular_stream() << "bounded\n"; print_certificate(ctx); @@ -287,7 +287,7 @@ public: case datalog::INPUT_ERROR: ctx.regular_stream() << "input error\n"; break; - + case datalog::MEMOUT: ctx.regular_stream() << "memory bounds exceeded\n"; break; @@ -295,12 +295,12 @@ public: case datalog::TIMEOUT: ctx.regular_stream() << "timeout\n"; break; - + case datalog::APPROX: ctx.regular_stream() << "approximated relations\n"; break; - case datalog::OK: + case datalog::OK: (void)query_exn; SASSERT(query_exn); break; @@ -324,7 +324,7 @@ public: void init_pdescrs(cmd_context & ctx, param_descrs & p) override { m_dl_ctx->dlctx().collect_params(p); } - + private: void set_background(cmd_context& ctx) { @@ -356,8 +356,8 @@ private: statistics st; datalog::context& dlctx = m_dl_ctx->dlctx(); dlctx.collect_statistics(st); - st.update("time", ctx.get_seconds()); - st.display_smt2(ctx.regular_stream()); + st.update("time", ctx.get_seconds()); + st.display_smt2(ctx.regular_stream()); } } @@ -391,8 +391,8 @@ public: void prepare(cmd_context & ctx) override { ctx.m(); // ensure manager is initialized. - m_arg_idx = 0; - m_query_arg_idx = 0; + m_arg_idx = 0; + m_query_arg_idx = 0; m_domain.reset(); m_kinds.reset(); } @@ -443,21 +443,21 @@ public: m_arg_idx(0), m_dl_ctx(dl_ctx) {} - + char const * get_usage() const override { return " "; } char const * get_descr(cmd_context & ctx) const override { return "declare constant as variable"; } unsigned get_arity() const override { return 2; } void prepare(cmd_context & ctx) override { ctx.m(); // ensure manager is initialized. - m_arg_idx = 0; + m_arg_idx = 0; } cmd_arg_kind next_arg_kind(cmd_context & ctx) const override { SASSERT(m_arg_idx <= 1); if (m_arg_idx == 0) { - return CPK_SYMBOL; + return CPK_SYMBOL; } - return CPK_SORT; + return CPK_SORT; } void set_next_arg(cmd_context & ctx, sort* s) override { @@ -466,7 +466,7 @@ public: } void set_next_arg(cmd_context & ctx, symbol const & s) override { - m_var_name = s; + m_var_name = s; ++m_arg_idx; } @@ -523,7 +523,7 @@ static void install_dl_cmds_aux(cmd_context& ctx, dl_collected_cmds* collected_c ctx.insert(alloc(dl_query_cmd, dl_ctx)); ctx.insert(alloc(dl_declare_rel_cmd, dl_ctx)); ctx.insert(alloc(dl_declare_var_cmd, dl_ctx)); - ctx.insert(alloc(dl_push_cmd, dl_ctx)); + ctx.insert(alloc(dl_push_cmd, dl_ctx)); ctx.insert(alloc(dl_pop_cmd, dl_ctx)); } diff --git a/src/muz/fp/horn_tactic.cpp b/src/muz/fp/horn_tactic.cpp index 4843a2623..eef95915d 100644 --- a/src/muz/fp/horn_tactic.cpp +++ b/src/muz/fp/horn_tactic.cpp @@ -27,7 +27,7 @@ Revision History: #include "muz/transforms/dl_mk_slice.h" #include "tactic/generic_model_converter.h" #include "muz/transforms/dl_transforms.h" -#include "muz/base/fixedpoint_params.hpp" +#include "muz/base/fp_params.hpp" #include "ast/ast_util.h" #include "ast/rewriter/var_subst.h" @@ -71,7 +71,7 @@ class horn_tactic : public tactic { f = to_quantifier(f)->get_expr(); } else if (is_exists(f) && !is_positive) { - f = to_quantifier(f)->get_expr(); + f = to_quantifier(f)->get_expr(); } else if (m.is_not(f, e)) { is_positive = !is_positive; @@ -84,7 +84,7 @@ class horn_tactic : public tactic { if (!is_positive) { f = m.mk_not(f); } - + } bool is_predicate(expr* a) { @@ -144,7 +144,7 @@ class horn_tactic : public tactic { expr* a = nullptr, *a1 = nullptr; flatten_or(tmp, args); for (unsigned i = 0; i < args.size(); ++i) { - a = args[i].get(); + a = args[i].get(); check_predicate(mark, a); if (m.is_not(a, a1)) { body.push_back(a1); @@ -176,13 +176,13 @@ class horn_tactic : public tactic { return expr_ref(m.mk_implies(body, head), m); } - void operator()(goal_ref const & g, + void operator()(goal_ref const & g, goal_ref_buffer & result) { SASSERT(g->is_well_sorted()); tactic_report report("horn", *g); bool produce_proofs = g->proofs_enabled(); - if (produce_proofs) { + if (produce_proofs) { if (!m_ctx.generate_proof_trace()) { params_ref params = m_ctx.get_params().p; params.set_bool("generate_proof_trace", true); @@ -208,7 +208,7 @@ class horn_tactic : public tactic { case IS_QUERY: queries.push_back(f); break; - default: + default: msg << "formula is not in Horn fragment: " << mk_pp(g->form(i), m) << "\n"; TRACE("horn", tout << msg.str();); throw tactic_exception(msg.str().c_str()); @@ -243,10 +243,10 @@ class horn_tactic : public tactic { g->set(mc.get()); } - void verify(expr* q, + void verify(expr* q, goal_ref const& g, - goal_ref_buffer & result, - model_converter_ref & mc, + goal_ref_buffer & result, + model_converter_ref & mc, proof_converter_ref & pc) { lbool is_reachable = l_undef; @@ -275,9 +275,9 @@ class horn_tactic : public tactic { else { g->assert_expr(m.mk_false()); } - break; + break; } - case l_false: { + case l_false: { // goal is sat g->reset(); if (produce_models) { @@ -290,11 +290,11 @@ class horn_tactic : public tactic { mc = mc2; } } - break; + break; } - case l_undef: + case l_undef: // subgoal is unchanged. - break; + break; } TRACE("horn", g->display(tout);); SASSERT(g->is_well_sorted()); @@ -314,20 +314,20 @@ class horn_tactic : public tactic { } } - void simplify(expr* q, + void simplify(expr* q, goal_ref const& g, - goal_ref_buffer & result, - model_converter_ref & mc, + goal_ref_buffer & result, + model_converter_ref & mc, proof_converter_ref & pc) { - expr_ref fml(m); + expr_ref fml(m); func_decl* query_pred = to_app(q)->get_decl(); m_ctx.set_output_predicate(query_pred); m_ctx.get_rules(); // flush adding rules. apply_default_transformation(m_ctx); - + if (m_ctx.xform_slice()) { datalog::rule_transformer transformer(m_ctx); datalog::mk_slice* slice = alloc(datalog::mk_slice, m_ctx); @@ -351,7 +351,7 @@ class horn_tactic : public tactic { g->assert_expr(fml); } } - + }; bool m_is_simplify; @@ -368,7 +368,7 @@ public: tactic * translate(ast_manager & m) override { return alloc(horn_tactic, m_is_simplify, m, m_params); } - + ~horn_tactic() override { dealloc(m_imp); } @@ -378,16 +378,16 @@ public: m_imp->updt_params(p); } - + void collect_param_descrs(param_descrs & r) override { m_imp->collect_param_descrs(r); } - - void operator()(goal_ref const & in, + + void operator()(goal_ref const & in, goal_ref_buffer & result) override { (*m_imp)(in, result); } - + void collect_statistics(statistics & st) const override { m_imp->collect_statistics(st); st.copy(m_stats); @@ -397,15 +397,15 @@ public: m_stats.reset(); m_imp->reset_statistics(); } - + void cleanup() override { ast_manager & m = m_imp->m; m_imp->collect_statistics(m_stats); dealloc(m_imp); m_imp = alloc(imp, m_is_simplify, m, m_params); - + } - + }; @@ -416,4 +416,3 @@ tactic * mk_horn_tactic(ast_manager & m, params_ref const & p) { tactic * mk_horn_simplify_tactic(ast_manager & m, params_ref const & p) { return clean(alloc(horn_tactic, true, m, p)); } - diff --git a/src/muz/spacer/spacer_context.cpp b/src/muz/spacer/spacer_context.cpp index 40c42015b..03093ab63 100644 --- a/src/muz/spacer/spacer_context.cpp +++ b/src/muz/spacer/spacer_context.cpp @@ -2175,8 +2175,7 @@ pob* pred_transformer::pobs::mk_pob(pob *parent, // ---------------- // context -context::context(fixedpoint_params const& params, - ast_manager& m) : +context::context(fp_params const& params, ast_manager& m) : m_params(params), m(m), m_context(nullptr), diff --git a/src/muz/spacer/spacer_context.h b/src/muz/spacer/spacer_context.h index f3d00a857..760f38f69 100644 --- a/src/muz/spacer/spacer_context.h +++ b/src/muz/spacer/spacer_context.h @@ -33,7 +33,7 @@ Notes: #include "muz/spacer/spacer_prop_solver.h" #include "muz/spacer/spacer_json.h" -#include "muz/base/fixedpoint_params.hpp" +#include "muz/base/fp_params.hpp" namespace datalog { class rule_set; @@ -877,7 +877,7 @@ class context { stopwatch m_create_children_watch; stopwatch m_init_rules_watch; - fixedpoint_params const& m_params; + fp_params const& m_params; ast_manager& m; datalog::context* m_context; manager m_pm; @@ -993,11 +993,11 @@ public: Initial values of predicates are stored in corresponding relations in dctx. We check whether there is some reachable state of the relation checked_relation. */ - context(fixedpoint_params const& params, ast_manager& m); + context(fp_params const& params, ast_manager& m); ~context(); - const fixedpoint_params &get_params() const { return m_params; } + const fp_params &get_params() const { return m_params; } bool use_native_mbp () {return m_use_native_mbp;} bool use_ground_pob () {return m_ground_pob;} bool use_instantiate () {return m_instantiate;} diff --git a/src/muz/spacer/spacer_iuc_solver.cpp b/src/muz/spacer/spacer_iuc_solver.cpp index 5a3a53f0b..a68db4c0a 100644 --- a/src/muz/spacer/spacer_iuc_solver.cpp +++ b/src/muz/spacer/spacer_iuc_solver.cpp @@ -99,8 +99,8 @@ void iuc_solver::pop_bg (unsigned n) { if (n == 0) { return; } - if (m_assumptions.size () > m_first_assumption) { - m_assumptions.shrink(m_first_assumption); + if (m_assumptions.size () > m_first_assumption) { + m_assumptions.shrink(m_first_assumption); } m_first_assumption = m_first_assumption > n ? m_first_assumption - n : 0; m_assumptions.shrink (m_first_assumption); @@ -111,8 +111,8 @@ unsigned iuc_solver::get_num_bg () {return m_first_assumption;} lbool iuc_solver::check_sat (unsigned num_assumptions, expr * const *assumptions) { // -- remove any old assumptions - m_assumptions.shrink(m_first_assumption); - + m_assumptions.shrink(m_first_assumption); + // -- replace theory literals in background assumptions with proxies mk_proxies (m_assumptions); // -- in case mk_proxies added new literals, they are all background @@ -126,12 +126,12 @@ lbool iuc_solver::check_sat (unsigned num_assumptions, expr * const *assumptions lbool iuc_solver::check_sat_cc(const expr_ref_vector &cube, vector const & clauses) { - if (clauses.empty()) + if (clauses.empty()) return check_sat(cube.size(), cube.c_ptr()); - + // -- remove any old assumptions - m_assumptions.shrink(m_first_assumption); - + m_assumptions.shrink(m_first_assumption); + // -- replace theory literals in background assumptions with proxies mk_proxies(m_assumptions); // -- in case mk_proxies added new literals, they are all background @@ -147,8 +147,8 @@ lbool iuc_solver::check_sat_cc(const expr_ref_vector &cube, app* iuc_solver::def_manager::mk_proxy (expr *v) { app* r; - if (m_expr2proxy.find(v, r)) - return r; + if (m_expr2proxy.find(v, r)) + return r; ast_manager &m = m_parent.m; app* proxy = m_parent.fresh_proxy (); @@ -184,14 +184,14 @@ bool iuc_solver::def_manager::is_proxy_def (expr *v) bool iuc_solver::is_proxy(expr *e, app_ref &def) { - if (!is_uninterp_const(e)) - return false; + if (!is_uninterp_const(e)) + return false; app* a = to_app (e); for (int i = m_defs.size (); i-- > 0; ) if (m_defs[i].is_proxy (a, def)) - return true; + return true; return m_base_defs.is_proxy (a, def); } @@ -263,9 +263,9 @@ void iuc_solver::elim_proxies (expr_ref_vector &v) expr_ref f = mk_and (v); scoped_ptr rep = mk_expr_simp_replacer (m); rep->set_substitution (&m_elim_proxies_sub); - (*rep) (f); - v.reset (); - flatten_and (f, v); + (*rep)(f); + v.reset(); + flatten_and(f, v); } void iuc_solver::get_iuc(expr_ref_vector &core) @@ -362,7 +362,7 @@ void iuc_solver::get_iuc(expr_ref_vector &core) // -- register iuc plugins switch (m_iuc_arith) { case 0: - case 1: + case 1: plugin = alloc(unsat_core_plugin_farkas_lemma, learner, m_split_literals, @@ -398,18 +398,18 @@ void iuc_solver::get_iuc(expr_ref_vector &core) UNREACHABLE(); break; } - + { scoped_watch _t_ (m_learn_core_sw); // compute interpolating unsat core learner.compute_unsat_core(core); } - + elim_proxies (core); // AG: this should be taken care of by minimizing the iuc cut simplify_bounds (core); } - + IF_VERBOSE(2, verbose_stream () << "IUC Core:\n" << core << "\n";); } diff --git a/src/muz/spacer/spacer_iuc_solver.h b/src/muz/spacer/spacer_iuc_solver.h index 3c6251be0..c0a0072ed 100644 --- a/src/muz/spacer/spacer_iuc_solver.h +++ b/src/muz/spacer/spacer_iuc_solver.h @@ -65,7 +65,7 @@ private: bool m_print_farkas_stats; bool m_old_hyp_reducer; bool is_proxy(expr *e, app_ref &def); - void undo_proxies_in_core(ptr_vector &v); + void undo_proxies_in_core(expr_ref_vector &v); app* mk_proxy(expr *v); app* fresh_proxy(); void elim_proxies(expr_ref_vector &v); @@ -101,16 +101,16 @@ public: void pop_bg(unsigned n); unsigned get_num_bg(); - void get_full_unsat_core(ptr_vector &core) { + void get_full_unsat_core(ptr_vector &core) { expr_ref_vector _core(m); - m_solver.get_unsat_core(_core); + m_solver.get_unsat_core(_core); core.append(_core.size(), _core.c_ptr()); } /* solver interface */ - solver* translate(ast_manager &m, params_ref const &p) override { - return m_solver.translate(m, p); + solver* translate(ast_manager &m, params_ref const &p) override { + return m_solver.translate(m, p); } void updt_params(params_ref const &p) override { m_solver.updt_params(p); } void reset_params(params_ref const &p) override { m_solver.reset_params(p); } @@ -136,8 +136,8 @@ public: expr * get_assertion(unsigned idx) const override { return m_solver.get_assertion(idx); } unsigned get_num_assumptions() const override { return m_solver.get_num_assumptions(); } expr * get_assumption(unsigned idx) const override { return m_solver.get_assumption(idx); } - std::ostream &display(std::ostream &out, unsigned n, expr* const* es) const override { - return m_solver.display(out, n, es); + std::ostream &display(std::ostream &out, unsigned n, expr* const* es) const override { + return m_solver.display(out, n, es); } /* check_sat_result interface */ @@ -159,7 +159,7 @@ public: iuc_solver &m_s; expr_ref_vector &m_v; public: - scoped_mk_proxy(iuc_solver &s, expr_ref_vector &v) : m_s(s), m_v(v) { + scoped_mk_proxy(iuc_solver &s, expr_ref_vector &v) : m_s(s), m_v(v) { m_s.mk_proxies(m_v); } ~scoped_mk_proxy() { m_s.undo_proxies(m_v); } @@ -171,8 +171,8 @@ public: public: scoped_bg(iuc_solver &s) : m_s(s), m_bg_sz(m_s.get_num_bg()) {} ~scoped_bg() { - if (m_s.get_num_bg() > m_bg_sz) { - m_s.pop_bg(m_s.get_num_bg() - m_bg_sz); + if (m_s.get_num_bg() > m_bg_sz) { + m_s.pop_bg(m_s.get_num_bg() - m_bg_sz); } } }; diff --git a/src/muz/spacer/spacer_prop_solver.cpp b/src/muz/spacer/spacer_prop_solver.cpp index 435f0af3a..7bd21a1b5 100644 --- a/src/muz/spacer/spacer_prop_solver.cpp +++ b/src/muz/spacer/spacer_prop_solver.cpp @@ -36,13 +36,13 @@ Revision History: #include "muz/spacer/spacer_prop_solver.h" #include "model/model_evaluator.h" -#include "muz/base/fixedpoint_params.hpp" +#include "muz/base/fp_params.hpp" namespace spacer { prop_solver::prop_solver(ast_manager &m, solver *solver0, solver *solver1, - fixedpoint_params const& p, symbol const& name) : + fp_params const& p, symbol const& name) : m(m), m_name(name), m_ctx(nullptr), @@ -329,13 +329,14 @@ lbool prop_solver::internal_check_assumptions(expr_ref_vector &hard_atoms, } if (result == l_false && m_core && m.proofs_enabled() && !m_subset_based_core) { - TRACE("spacer", tout << "theory core\n";); + TRACE("spacer", tout << "Using IUC core\n";); m_core->reset(); m_ctx->get_iuc(*m_core); } else if (result == l_false && m_core) { m_core->reset(); m_ctx->get_unsat_core(*m_core); // manually undo proxies because maxsmt() call above manually adds proxies + // AG: don't think this is needed. maxsmt() undoes the proxies already m_ctx->undo_proxies(*m_core); } diff --git a/src/muz/spacer/spacer_prop_solver.h b/src/muz/spacer/spacer_prop_solver.h index 042215eff..1db65dc3e 100644 --- a/src/muz/spacer/spacer_prop_solver.h +++ b/src/muz/spacer/spacer_prop_solver.h @@ -33,7 +33,7 @@ Revision History: #include "muz/spacer/spacer_iuc_solver.h" #include "muz/spacer/spacer_util.h" -struct fixedpoint_params; +struct fp_params; namespace spacer { typedef ptr_vector decl_vector; @@ -76,7 +76,7 @@ private: public: prop_solver(ast_manager &m, solver *solver0, solver* solver1, - fixedpoint_params const& p, symbol const& name); + fp_params const& p, symbol const& name); void set_core(expr_ref_vector* core) { m_core = core; } diff --git a/src/muz/tab/tab_context.cpp b/src/muz/tab/tab_context.cpp index 39b7af634..2fb329ff4 100644 --- a/src/muz/tab/tab_context.cpp +++ b/src/muz/tab/tab_context.cpp @@ -30,7 +30,7 @@ Revision History: #include "ast/for_each_expr.h" #include "ast/substitution/matcher.h" #include "ast/scoped_proof.h" -#include "muz/base/fixedpoint_params.hpp" +#include "muz/base/fp_params.hpp" #include "ast/ast_util.h" namespace tb { diff --git a/src/muz/transforms/dl_mk_array_eq_rewrite.cpp b/src/muz/transforms/dl_mk_array_eq_rewrite.cpp index c33cecda9..61eafae64 100644 --- a/src/muz/transforms/dl_mk_array_eq_rewrite.cpp +++ b/src/muz/transforms/dl_mk_array_eq_rewrite.cpp @@ -20,7 +20,7 @@ Revision History: #include "ast/expr_abstract.h" #include "muz/base/dl_context.h" #include "muz/base/dl_context.h" -#include "muz/base/fixedpoint_params.hpp" +#include "muz/base/fp_params.hpp" #include "muz/transforms/dl_mk_array_eq_rewrite.h" #include "ast/factor_equivs.h" diff --git a/src/muz/transforms/dl_mk_array_instantiation.cpp b/src/muz/transforms/dl_mk_array_instantiation.cpp index 362d83865..6a8f0ce81 100644 --- a/src/muz/transforms/dl_mk_array_instantiation.cpp +++ b/src/muz/transforms/dl_mk_array_instantiation.cpp @@ -23,7 +23,7 @@ Revision History: #include "muz/base/dl_context.h" #include "ast/rewriter/expr_safe_replace.h" #include "ast/expr_abstract.h" -#include "muz/base/fixedpoint_params.hpp" +#include "muz/base/fp_params.hpp" namespace datalog { diff --git a/src/muz/transforms/dl_mk_bit_blast.cpp b/src/muz/transforms/dl_mk_bit_blast.cpp index 8a21bc37c..992b8f51b 100644 --- a/src/muz/transforms/dl_mk_bit_blast.cpp +++ b/src/muz/transforms/dl_mk_bit_blast.cpp @@ -24,7 +24,7 @@ Revision History: #include "ast/rewriter/expr_safe_replace.h" #include "tactic/generic_model_converter.h" #include "muz/transforms/dl_mk_interp_tail_simplifier.h" -#include "muz/base/fixedpoint_params.hpp" +#include "muz/base/fp_params.hpp" #include "ast/scoped_proof.h" #include "model/model_v2_pp.h" @@ -32,9 +32,9 @@ namespace datalog { // // P(v) :- Q(extract[1:1]v ++ 0), R(1 ++ extract[0:0]v). - // -> + // -> // P(bv(x,y)) :- Q(bv(x,0)), R(bv(1,y)) . - // + // // Introduce P_bv: // P_bv(x,y) :- Q_bv(x,0), R_bv(1,y) // P(bv(x,y)) :- P_bv(x,y) @@ -51,7 +51,7 @@ namespace datalog { bit_blast_model_converter(ast_manager& m): m(m), m_bv(m), - m_old_funcs(m), + m_old_funcs(m), m_new_funcs(m) {} void insert(func_decl* old_f, func_decl* new_f) { @@ -73,7 +73,7 @@ namespace datalog { func_decl* q = m_old_funcs[i].get(); func_interp* f = model->get_func_interp(p); if (!f) continue; - expr_ref body(m); + expr_ref body(m); unsigned arity_q = q->get_arity(); TRACE("dl", model_v2_pp(tout, *model); @@ -87,10 +87,10 @@ namespace datalog { if (f) { body = f->get_interp(); SASSERT(!f->is_partial()); - SASSERT(body); + SASSERT(body); } else { - body = m.mk_false(); + body = m.mk_false(); } unsigned idx = 0; expr_ref arg(m), proj(m); @@ -104,18 +104,18 @@ namespace datalog { for (unsigned k = 0; k < sz; ++k) { parameter p(k); proj = m.mk_app(m_bv.get_family_id(), OP_BIT2BOOL, 1, &p, 1, &t); - sub.insert(m.mk_var(idx++, m.mk_bool_sort()), proj); + sub.insert(m.mk_var(idx++, m.mk_bool_sort()), proj); } } else { sub.insert(m.mk_var(idx++, s), arg); } } - sub(body); + sub(body); g->set_else(body); model->register_decl(q, g); - } - } + } + } }; class expand_mkbv_cfg : public default_rewriter_cfg { @@ -134,10 +134,10 @@ namespace datalog { public: expand_mkbv_cfg(context& ctx): - m_context(ctx), + m_context(ctx), m(ctx.get_manager()), m_util(m), - m_args(m), + m_args(m), m_f_vars(m), m_g_vars(m), m_old_funcs(m), @@ -152,8 +152,8 @@ namespace datalog { void set_dst(rule_set* dst) { m_dst = dst; } func_decl_ref_vector const& old_funcs() const { return m_old_funcs; } func_decl_ref_vector const& new_funcs() const { return m_new_funcs; } - - br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) { + + br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) { if (num == 0) { if (m_src->is_output_predicate(f)) m_dst->set_output_predicate(f); @@ -165,9 +165,9 @@ namespace datalog { return BR_FAILED; } - // + // // f(mk_bv(args),...) - // + // m_args.reset(); m_g_vars.reset(); m_f_vars.reset(); @@ -191,9 +191,9 @@ namespace datalog { } } func_decl* g = nullptr; - + if (!m_pred2blast.find(f, g)) { - + ptr_vector domain; for (unsigned i = 0; i < m_args.size(); ++i) { domain.push_back(m.get_sort(m_args[i].get())); @@ -262,7 +262,7 @@ namespace datalog { m_params.set_bool("blast_quant", true); m_blaster.updt_params(m_params); } - + rule_set * operator()(rule_set const & source) { // TODO pc if (!m_context.xform_bit_blast()) { @@ -270,8 +270,8 @@ namespace datalog { } rule_manager& rm = m_context.get_rule_manager(); unsigned sz = source.get_num_rules(); - expr_ref fml(m); - rule_set * result = alloc(rule_set, m_context); + expr_ref fml(m); + rule_set * result = alloc(rule_set, m_context); m_rewriter.m_cfg.set_src(&source); m_rewriter.m_cfg.set_dst(result); for (unsigned i = 0; !m_context.canceled() && i < sz; ++i) { @@ -299,8 +299,8 @@ namespace datalog { if (!source.contains(*I)) result->set_output_predicate(*I); } - - if (m_context.get_model_converter()) { + + if (m_context.get_model_converter()) { generic_model_converter* fmc = alloc(generic_model_converter, m, "dl_mk_bit_blast"); bit_blast_model_converter* bvmc = alloc(bit_blast_model_converter, m); func_decl_ref_vector const& old_funcs = m_rewriter.m_cfg.old_funcs(); @@ -311,7 +311,7 @@ namespace datalog { } m_context.add_model_converter(concat(bvmc, fmc)); } - + return result; } }; @@ -326,6 +326,6 @@ namespace datalog { rule_set * mk_bit_blast::operator()(rule_set const & source) { return (*m_impl)(source); - } + } }; diff --git a/src/muz/transforms/dl_mk_interp_tail_simplifier.cpp b/src/muz/transforms/dl_mk_interp_tail_simplifier.cpp index 38000c65a..c1abd7bef 100644 --- a/src/muz/transforms/dl_mk_interp_tail_simplifier.cpp +++ b/src/muz/transforms/dl_mk_interp_tail_simplifier.cpp @@ -27,7 +27,7 @@ Revision History: #include "muz/transforms/dl_mk_interp_tail_simplifier.h" #include "ast/ast_util.h" -#include "muz/base/fixedpoint_params.hpp" +#include "muz/base/fp_params.hpp" namespace datalog { // ----------------------------------- @@ -46,7 +46,7 @@ namespace datalog { bool mk_interp_tail_simplifier::rule_substitution::unify(expr * e1, expr * e2) { SASSERT(m_rule); - //we need to apply the current substitution in order to ensure the unifier + //we need to apply the current substitution in order to ensure the unifier //works in an incremental way expr_ref e1_s(m); expr_ref e2_s(m); @@ -268,7 +268,7 @@ namespace datalog { if (neq) { have_pair = false; v[prev_pair_idx] = neq; - + read_idx++; continue; } @@ -294,7 +294,7 @@ namespace datalog { //bool detect_same_variable_conj_pairs - br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, + br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) { if (m.is_not(f) && (m.is_and(args[0]) || m.is_or(args[0]))) { @@ -307,15 +307,15 @@ namespace datalog { m_app_args.push_back(tmp); } if (m.is_and(args[0])) { - result = mk_or(m_app_args); + result = mk_or(m_app_args); } else { - result = mk_and(m_app_args); + result = mk_and(m_app_args); } return BR_REWRITE2; } - if (!m.is_and(f) && !m.is_or(f)) { - return BR_FAILED; + if (!m.is_and(f) && !m.is_or(f)) { + return BR_FAILED; } if (num == 0) { if (m.is_and(f)) { @@ -375,7 +375,7 @@ namespace datalog { m_simp(ctx.get_rewriter()), a(m), m_rule_subst(ctx), - m_tail(m), + m_tail(m), m_itail_members(m), m_conj(m) { m_cfg = alloc(normalizer_cfg, m); @@ -386,7 +386,7 @@ namespace datalog { dealloc(m_rw); dealloc(m_cfg); } - + void mk_interp_tail_simplifier::simplify_expr(app * a, expr_ref& res) { @@ -537,7 +537,7 @@ namespace datalog { simplify_expr(itail.get(), simp_res); modified |= itail.get() != simp_res.get(); - + if (m.is_false(simp_res)) { TRACE("dl", r->display(m_context, tout << "rule is infeasible\n");); return false; @@ -568,7 +568,7 @@ namespace datalog { rule_ref pro_var_eq_result(m_context.get_rule_manager()); if (propagate_variable_equivalences(res, pro_var_eq_result)) { - SASSERT(rule_counter().get_max_rule_var(*r.get())==0 || + SASSERT(rule_counter().get_max_rule_var(*r.get())==0 || rule_counter().get_max_rule_var(*r.get()) > rule_counter().get_max_rule_var(*pro_var_eq_result.get())); r = pro_var_eq_result; goto start; @@ -607,8 +607,8 @@ namespace datalog { rule_set * res = alloc(rule_set, m_context); if (transform_rules(source, *res)) { res->inherit_predicates(source); - TRACE("dl", - source.display(tout); + TRACE("dl", + source.display(tout); res->display(tout);); } else { dealloc(res); @@ -616,6 +616,5 @@ namespace datalog { } return res; } - -}; +}; diff --git a/src/muz/transforms/dl_mk_quantifier_abstraction.cpp b/src/muz/transforms/dl_mk_quantifier_abstraction.cpp index e9a4f2f54..dafb0ddd5 100644 --- a/src/muz/transforms/dl_mk_quantifier_abstraction.cpp +++ b/src/muz/transforms/dl_mk_quantifier_abstraction.cpp @@ -11,7 +11,7 @@ Abstract: Author: - Ken McMillan + Ken McMillan Andrey Rybalchenko Nikolaj Bjorner (nbjorner) 2013-04-02 @@ -23,13 +23,12 @@ Revision History: #include "muz/base/dl_context.h" #include "ast/rewriter/expr_safe_replace.h" #include "ast/expr_abstract.h" -#include "muz/base/fixedpoint_params.hpp" namespace datalog { - // model converter: + // model converter: // Given model for P^(x, y, i, a[i]) // create model: P(x,y,a) == forall i . P^(x,y,i,a[i]) // requires substitution and list of bound variables. @@ -55,7 +54,7 @@ namespace datalog { void display(std::ostream& out) override { display_add(out, m); } - void get_units(obj_map& units) override { units.reset(); } + void get_units(obj_map& units) override { units.reset(); } void insert(func_decl* old_p, func_decl* new_p, expr_ref_vector& sub, sort_ref_vector& sorts, svector const& bound) { m_old_funcs.push_back(old_p); @@ -74,7 +73,7 @@ namespace datalog { sort_ref_vector const& sorts = m_sorts[i]; svector const& is_bound = m_bound[i]; func_interp* f = old_model->get_func_interp(p); - expr_ref body(m); + expr_ref body(m); unsigned arity_q = q->get_arity(); SASSERT(0 < p->get_arity()); func_interp* g = alloc(func_interp, m, arity_q); @@ -82,7 +81,7 @@ namespace datalog { if (f) { body = f->get_interp(); SASSERT(!f->is_partial()); - SASSERT(body); + SASSERT(body); } else { expr_ref_vector args(m); @@ -94,7 +93,7 @@ namespace datalog { // Create quantifier wrapper around body. TRACE("dl", tout << mk_pp(body, m) << "\n";); - // 1. replace variables by the compound terms from + // 1. replace variables by the compound terms from // the original predicate. expr_safe_replace rep(m); for (unsigned i = 0; i < sub.size(); ++i) { @@ -121,7 +120,7 @@ namespace datalog { _free.push_back(consts.back()); } } - rep(body); + rep(body); rep.reset(); TRACE("dl", tout << mk_pp(body, m) << "\n";); @@ -130,18 +129,18 @@ namespace datalog { body = m.mk_forall(names.size(), bound_sorts.c_ptr(), names.c_ptr(), body); TRACE("dl", tout << mk_pp(body, m) << "\n";); - // 4. replace remaining constants by variables. + // 4. replace remaining constants by variables. for (unsigned i = 0; i < _free.size(); ++i) { rep.insert(_free[i].get(), m.mk_var(i, m.get_sort(_free[i].get()))); } - rep(body); + rep(body); g->set_else(body); TRACE("dl", tout << mk_pp(body, m) << "\n";); new_model->register_decl(q, g); - } + } old_model = new_model; - } + } }; mk_quantifier_abstraction::mk_quantifier_abstraction( @@ -154,7 +153,7 @@ namespace datalog { m_mc(nullptr) { } - mk_quantifier_abstraction::~mk_quantifier_abstraction() { + mk_quantifier_abstraction::~mk_quantifier_abstraction() { } func_decl* mk_quantifier_abstraction::declare_pred(rule_set const& rules, rule_set& dst, func_decl* old_p) { @@ -178,7 +177,7 @@ namespace datalog { func_decl* new_p = nullptr; if (!m_old2new.find(old_p, new_p)) { expr_ref_vector sub(m), vars(m); - svector bound; + svector bound; sort_ref_vector domain(m), sorts(m); expr_ref arg(m); for (unsigned i = 0; i < sz; ++i) { @@ -208,7 +207,7 @@ namespace datalog { bound.push_back(false); sub.push_back(arg); sorts.push_back(s0); - } + } SASSERT(old_p->get_range() == m.mk_bool_sort()); new_p = m.mk_func_decl(old_p->get_name(), domain.size(), domain.c_ptr(), old_p->get_range()); m_refs.push_back(new_p); @@ -242,12 +241,12 @@ namespace datalog { } args.push_back(arg); } - TRACE("dl", + TRACE("dl", tout << mk_pp(new_p, m) << "\n"; for (unsigned i = 0; i < args.size(); ++i) { tout << mk_pp(args[i].get(), m) << "\n"; }); - return app_ref(m.mk_app(new_p, args.size(), args.c_ptr()), m); + return app_ref(m.mk_app(new_p, args.size(), args.c_ptr()), m); } app_ref mk_quantifier_abstraction::mk_tail(rule_set const& rules, rule_set& dst, app* p) { @@ -272,7 +271,7 @@ namespace datalog { for (unsigned i = 0; i < sz; ++i) { arg = ps->get_arg(i); sort* s = m.get_sort(arg); - bool is_pattern = false; + bool is_pattern = false; while (a.is_array(s)) { is_pattern = true; unsigned arity = get_array_arity(s); @@ -304,9 +303,9 @@ namespace datalog { ptr_vector args2; args2.push_back(arg); args2.append(num_args, args); - return a.mk_select(args2.size(), args2.c_ptr()); + return a.mk_select(args2.size(), args2.c_ptr()); } - + rule_set * mk_quantifier_abstraction::operator()(rule_set const & source) { if (!m_ctx.quantify_arrays()) { return nullptr; @@ -334,10 +333,10 @@ namespace datalog { } rule_set * result = alloc(rule_set, m_ctx); - for (unsigned i = 0; i < sz; ++i) { + for (unsigned i = 0; i < sz; ++i) { tail.reset(); rule & r = *source.get_rule(i); - TRACE("dl", r.display(m_ctx, tout); ); + TRACE("dl", r.display(m_ctx, tout); ); unsigned cnt = vc.get_max_rule_var(r)+1; unsigned utsz = r.get_uninterpreted_tail_size(); unsigned tsz = r.get_tail_size(); @@ -352,8 +351,8 @@ namespace datalog { proof_ref pr(m); rm.mk_rule(fml, pr, *result, r.name()); TRACE("dl", result->last()->display(m_ctx, tout);); - } - + } + // proof converter: proofs are not necessarily preserved using this transformation. if (m_old2new.empty()) { @@ -371,5 +370,3 @@ namespace datalog { }; - - diff --git a/src/muz/transforms/dl_mk_rule_inliner.cpp b/src/muz/transforms/dl_mk_rule_inliner.cpp index 584f44303..317f13ff8 100644 --- a/src/muz/transforms/dl_mk_rule_inliner.cpp +++ b/src/muz/transforms/dl_mk_rule_inliner.cpp @@ -18,7 +18,7 @@ Revision History: Added linear_inline 2012-9-10 (nbjorner) Disable inliner for quantified rules 2012-10-31 (nbjorner) - + Notes: Resolution transformation (resolve): @@ -27,7 +27,7 @@ Resolution transformation (resolve): -------------------------------------------------- P(x) :- R(z), phi(x,y), psi(y,z) - Proof converter: + Proof converter: replace assumption (*) by rule and upper assumptions. @@ -37,9 +37,9 @@ Subsumption transformation (remove rule): P(x) :- Q(y), phi(x,y) Rules --------------------------------- Rules - - - Model converter: + + + Model converter: P(x) := P(x) or (exists y . Q(y) & phi(x,y)) @@ -52,7 +52,7 @@ Subsumption transformation (remove rule): #include "ast/rewriter/rewriter.h" #include "ast/rewriter/rewriter_def.h" #include "muz/transforms/dl_mk_rule_inliner.h" -#include "muz/base/fixedpoint_params.hpp" +#include "muz/base/fp_params.hpp" namespace datalog { @@ -67,15 +67,15 @@ namespace datalog { unsigned var_cnt = std::max(vc.get_max_rule_var(tgt), vc.get_max_rule_var(src))+1; m_subst.reset(); m_subst.reserve(2, var_cnt); - + m_ready = m_unif(tgt.get_tail(tgt_idx), src.get_head(), m_subst); if (m_ready) { m_deltas[0] = 0; m_deltas[1] = var_cnt; - TRACE("dl", - output_predicate(m_context, src.get_head(), tout << "unify rules "); - output_predicate(m_context, tgt.get_head(), tout << "\n"); + TRACE("dl", + output_predicate(m_context, src.get_head(), tout << "unify rules "); + output_predicate(m_context, tgt.get_head(), tout << "\n"); tout << "\n";); } return m_ready; @@ -90,7 +90,7 @@ namespace datalog { } void rule_unifier::apply( - rule const& r, bool is_tgt, unsigned skipped_index, + rule const& r, bool is_tgt, unsigned skipped_index, app_ref_vector& res, svector& res_neg) { unsigned rule_len = r.get_tail_size(); for (unsigned i = 0; i < rule_len; i++) { @@ -127,7 +127,7 @@ namespace datalog { ); if (m_normalize) { - m_rm.fix_unbound_vars(res, true); + m_rm.fix_unbound_vars(res, true); if (m_interp_simplifier.transform_rule(res.get(), simpl_rule)) { res = simpl_rule; return true; @@ -150,8 +150,8 @@ namespace datalog { for (unsigned i = 0; i < sorts.size(); ++i) { v = m.mk_var(i, sorts[i]); m_subst.apply(2, m_deltas, expr_offset(v, is_tgt?0:1), w); - result.push_back(w); - } + result.push_back(w); + } return result; } @@ -184,7 +184,7 @@ namespace datalog { expr_ref_vector s2 = m_unifier.get_rule_subst(src, false); datalog::resolve_rule(m_rm, tgt, src, tail_index, s1, s2, *res.get()); } - return true; + return true; } else { TRACE("dl", res->display(m_context, tout << "interpreted tail is unsat\n");); @@ -240,12 +240,12 @@ namespace datalog { return false; } - // - // these conditions are optional, they avoid possible exponential increase + // + // these conditions are optional, they avoid possible exponential increase // in the size of the problem - // + // - return + return //m_head_pred_non_empty_tails_ctr.get(pred)<=1 m_head_pred_ctr.get(pred) <= 1 || (m_tail_pred_ctr.get(pred) <= 1 && m_head_pred_ctr.get(pred) <= 4) @@ -253,7 +253,7 @@ namespace datalog { } /** Caller has to dealloc the returned object */ - rule_set * mk_rule_inliner::create_allowed_rule_set(rule_set const & orig) + rule_set * mk_rule_inliner::create_allowed_rule_set(rule_set const & orig) { rule_set * res = alloc(rule_set, m_context); for (rule * r : orig) { @@ -268,7 +268,7 @@ namespace datalog { /** Try to make the set of inlined predicates acyclic by forbidding inlining of one - predicate from each strongly connected component. Return true if we did forbide some + predicate from each strongly connected component. Return true if we did forbide some predicate, and false if the set of rules is already acyclic. */ bool mk_rule_inliner::forbid_preds_from_cycles(rule_set const & r) @@ -276,7 +276,7 @@ namespace datalog { SASSERT(r.is_closed()); bool something_forbidden = false; - + const rule_stratifier::comp_vector& comps = r.get_stratifier().get_strats(); for (rule_stratifier::item_set * stratum : comps) { @@ -293,12 +293,12 @@ namespace datalog { return something_forbidden; } - bool mk_rule_inliner::forbid_multiple_multipliers(const rule_set & orig, + bool mk_rule_inliner::forbid_multiple_multipliers(const rule_set & orig, rule_set const & proposed_inlined_rules) { bool something_forbidden = false; - const rule_stratifier::comp_vector& comps = + const rule_stratifier::comp_vector& comps = proposed_inlined_rules.get_stratifier().get_strats(); for (rule_stratifier::item_set * stratum : comps) { @@ -332,7 +332,7 @@ namespace datalog { } else { is_multi_head_pred = true; - m_head_pred_ctr.get(head_pred) = + m_head_pred_ctr.get(head_pred) = m_head_pred_ctr.get(head_pred)*tail_pred_head_cnt; } } @@ -379,7 +379,7 @@ namespace datalog { void mk_rule_inliner::plan_inlining(rule_set const & orig) { count_pred_occurrences(orig); - + scoped_ptr candidate_inlined_set = create_allowed_rule_set(orig); while (forbid_preds_from_cycles(*candidate_inlined_set)) { candidate_inlined_set = create_allowed_rule_set(orig); @@ -458,8 +458,8 @@ namespace datalog { rule_ref r(rl, m_rm); func_decl * pred = r->get_decl(); - // if inlining is allowed, then we are eliminating - // this relation through inlining, + // if inlining is allowed, then we are eliminating + // this relation through inlining, // so we don't add its rules to the result something_done |= !inlining_allowed(orig, pred) && transform_rule(orig, r, tgt); @@ -472,14 +472,14 @@ namespace datalog { } } } - + return something_done; } /** Check whether rule r is oriented in a particular ordering. This is to avoid infinite cycle of inlining in the eager inliner. - + Out ordering is lexicographic, comparing atoms first on stratum they are in, then on arity and then on ast ID of their func_decl. */ @@ -488,7 +488,7 @@ namespace datalog { unsigned head_strat = strat.get_predicate_strat(head_pred); unsigned head_arity = head_pred->get_arity(); unsigned pt_len = r->get_positive_tail_size(); - for (unsigned ti=0; ti < pt_len; ++ti) { + for (unsigned ti=0; ti < pt_len; ++ti) { func_decl * pred = r->get_decl(ti); unsigned pred_strat = strat.get_predicate_strat(pred); SASSERT(pred_strat <= head_strat); @@ -516,7 +516,7 @@ namespace datalog { unsigned pt_len = r->get_positive_tail_size(); for (unsigned ti = 0; ti < pt_len; ++ti) { - + func_decl * pred = r->get_decl(ti); if (pred == head_pred || m_preds_with_facts.contains(pred)) { continue; } @@ -532,7 +532,7 @@ namespace datalog { } else { inlining_candidate = nullptr; - + for (unsigned ri = 0; ri < rule_cnt; ++ri) { rule * pred_rule = pred_rules[ri]; if (!m_unifier.unify_rules(*r, ti, *pred_rule)) { @@ -540,9 +540,9 @@ namespace datalog { continue; } if (inlining_candidate != nullptr) { - // We have two rules that can be inlined into the current + // We have two rules that can be inlined into the current // tail predicate. In this situation we don't do inlinning - // on this tail atom, as we don't want the overall number + // on this tail atom, as we don't want the overall number // of rules to increase. goto process_next_tail; } @@ -608,14 +608,14 @@ namespace datalog { P(1,x) :- P(1,z), phi(x,y), psi(y,z) - whenever P(0,x) is not unifiable with the + whenever P(0,x) is not unifiable with the body of the rule where it appears (P(1,z)) - and P(0,x) is unifiable with at most one (?) + and P(0,x) is unifiable with at most one (?) other rule (and it does not occur negatively). */ bool mk_rule_inliner::visitor::operator()(expr* e) { m_unifiers.append(m_positions.find(e)); - TRACE("dl", + TRACE("dl", tout << "unifier: " << (m_unifiers.empty()?0:m_unifiers.back()); tout << " num unifiers: " << m_unifiers.size(); tout << " num positions: " << m_positions.find(e).size() << "\n"; @@ -640,7 +640,7 @@ namespace datalog { } unsigned_vector const& mk_rule_inliner::visitor::del_position(expr* e, unsigned j) { - obj_map::obj_map_entry * et = m_positions.find_core(e); + obj_map::obj_map_entry * et = m_positions.find_core(e); SASSERT(et && et->get_data().m_value.contains(j)); et->get_data().m_value.erase(j); return et->get_data().m_value; @@ -654,7 +654,7 @@ namespace datalog { m_head_visitor.add_position(head, i); m_head_index.insert(head); m_pinned.push_back(r); - + if (source.is_output_predicate(headd) || m_preds_with_facts.contains(headd)) { can_remove.set(i, false); @@ -667,10 +667,10 @@ namespace datalog { m_tail_visitor.add_position(tail, i); m_tail_index.insert(tail); } - bool can_exp = + bool can_exp = tl_sz == 1 - && r->get_positive_tail_size() == 1 - && !m_preds_with_facts.contains(r->get_decl(0)) + && r->get_positive_tail_size() == 1 + && !m_preds_with_facts.contains(r->get_decl(0)) && !source.is_output_predicate(r->get_decl(0)); can_expand.set(i, can_exp); } @@ -682,14 +682,14 @@ namespace datalog { for (unsigned j = 0; j < tl_sz; ++j) { app* tail = r->get_tail(j); m_tail_visitor.del_position(tail, i); - } + } } #define PRT(_x_) ((_x_)?"T":"F") bool mk_rule_inliner::inline_linear(scoped_ptr& rules) { - bool done_something = false; + bool done_something = false; unsigned sz = rules->get_num_rules(); m_head_visitor.reset(sz); @@ -704,7 +704,7 @@ namespace datalog { acc.push_back(rules->get_rule(i)); } - // set up unification index. + // set up unification index. svector& can_remove = m_head_visitor.can_remove(); svector& can_expand = m_head_visitor.can_expand(); @@ -729,7 +729,7 @@ namespace datalog { svector valid; valid.reset(); - valid.resize(sz, true); + valid.resize(sz, true); bool allow_branching = m_context.get_params().xform_inline_linear_branch(); @@ -738,9 +738,9 @@ namespace datalog { while (true) { rule_ref r(acc[i].get(), m_rm); - + TRACE("dl", r->display(m_context, tout << "processing: " << i << "\n");); - + if (!valid.get(i)) { TRACE("dl", tout << "invalid: " << i << "\n";); break; @@ -762,9 +762,9 @@ namespace datalog { TRACE("dl", tout << PRT(can_remove.get(j)) << " " << PRT(valid.get(j)) << " " << PRT(i != j) << "\n";); break; } - + rule* r2 = acc[j].get(); - + // check that the head of r2 only unifies with this single body position. TRACE("dl", output_predicate(m_context, r2->get_head(), tout << "unify head: "); tout << "\n";); m_tail_visitor.reset(); @@ -776,7 +776,7 @@ namespace datalog { TRACE("dl", tout << "too many tails " << num_tail_unifiers << "\n";); break; } - + rule_ref rl_res(m_rm); if (!try_to_inline_rule(*r.get(), *r2, 0, rl_res)) { TRACE("dl", r->display(m_context, tout << "inlining failed\n"); r2->display(m_context, tout); ); @@ -787,12 +787,12 @@ namespace datalog { del_rule(r, i); add_rule(*rules, rl_res.get(), i); - + r = rl_res; acc[i] = r.get(); can_expand.set(i, can_expand.get(j)); - + if (num_tail_unifiers == 1) { TRACE("dl", tout << "setting invalid: " << j << "\n";); valid.set(j, false); @@ -815,22 +815,22 @@ namespace datalog { res->inherit_predicates(*rules); TRACE("dl", res->display(tout);); rules = res.detach(); - } + } return done_something; } rule_set * mk_rule_inliner::operator()(rule_set const & source) { bool something_done = false; - ref hsmc; + ref hsmc; if (source.get_num_rules() == 0) { return nullptr; } - for (rule const* r : source) - if (has_quantifier(*r)) - return nullptr; + for (rule const* r : source) + if (has_quantifier(*r)) + return nullptr; if (m_context.get_model_converter()) { hsmc = alloc(horn_subsume_model_converter, m); @@ -841,15 +841,15 @@ namespace datalog { if (m_context.get_params().xform_inline_eager()) { TRACE("dl", source.display(tout << "before eager inlining\n");); - plan_inlining(source); - something_done = transform_rules(source, *res); + plan_inlining(source); + something_done = transform_rules(source, *res); VERIFY(res->close()); //this transformation doesn't break the negation stratification // try eager inlining if (do_eager_inlining(res)) { something_done = true; - } + } TRACE("dl", res->display(tout << "after eager inlining\n");); - } + } if (something_done) { res->inherit_predicates(source); } @@ -870,6 +870,5 @@ namespace datalog { return res.detach(); } - -}; +}; diff --git a/src/muz/transforms/dl_mk_scale.cpp b/src/muz/transforms/dl_mk_scale.cpp index 0144948bd..9ceaeeab3 100644 --- a/src/muz/transforms/dl_mk_scale.cpp +++ b/src/muz/transforms/dl_mk_scale.cpp @@ -18,7 +18,7 @@ Revision History: #include "muz/transforms/dl_mk_scale.h" #include "muz/base/dl_context.h" -#include "muz/base/fixedpoint_params.hpp" +#include "muz/base/fp_params.hpp" namespace datalog { @@ -37,7 +37,7 @@ namespace datalog { m_trail.push_back(new_f); m_new2old.insert(new_f, old_f); } - + void get_units(obj_map& units) override { units.reset(); } void operator()(model_ref& md) override { @@ -74,7 +74,7 @@ namespace datalog { old_model->register_decl(old_p, old_fi); } } - + // register values that have not been scaled. unsigned sz = md->get_num_constants(); for (unsigned i = 0; i < sz; ++i) { @@ -111,12 +111,12 @@ namespace datalog { m_ctx(ctx), a(m), m_trail(m), - m_eqs(m) { + m_eqs(m) { } - mk_scale::~mk_scale() { + mk_scale::~mk_scale() { } - + rule_set * mk_scale::operator()(rule_set const & source) { if (!m_ctx.scale()) { return nullptr; @@ -135,7 +135,7 @@ namespace datalog { } m_mc = smc.get(); - for (unsigned i = 0; i < sz; ++i) { + for (unsigned i = 0; i < sz; ++i) { rule & r = *source.get_rule(i); unsigned utsz = r.get_uninterpreted_tail_size(); unsigned tsz = r.get_tail_size(); @@ -157,10 +157,10 @@ namespace datalog { tail.push_back(a.mk_gt(m.mk_var(num_vars, a.mk_real()), a.mk_numeral(rational(0), false))); neg.resize(tail.size(), false); new_rule = rm.mk(new_pred, tail.size(), tail.c_ptr(), neg.c_ptr(), r.name(), true); - result->add_rule(new_rule); + result->add_rule(new_rule); if (source.is_output_predicate(r.get_decl())) { result->set_output_predicate(new_rule->get_decl()); - } + } } TRACE("dl", result->display(tout);); if (m_mc) { @@ -227,7 +227,7 @@ namespace datalog { a.is_lt(e) || a.is_gt(e)) { expr_ref_vector args(m); for (unsigned i = 0; i < ap->get_num_args(); ++i) { - args.push_back(linearize(sigma_idx, ap->get_arg(i))); + args.push_back(linearize(sigma_idx, ap->get_arg(i))); } result = m.mk_app(ap->get_decl(), args.size(), args.c_ptr()); } diff --git a/src/muz/transforms/dl_mk_subsumption_checker.cpp b/src/muz/transforms/dl_mk_subsumption_checker.cpp index 56883460a..da41b4ba4 100644 --- a/src/muz/transforms/dl_mk_subsumption_checker.cpp +++ b/src/muz/transforms/dl_mk_subsumption_checker.cpp @@ -24,7 +24,7 @@ Revision History: #include "ast/rewriter/rewriter.h" #include "ast/rewriter/rewriter_def.h" #include "muz/transforms/dl_mk_subsumption_checker.h" -#include "muz/base/fixedpoint_params.hpp" +#include "muz/base/fp_params.hpp" #include "tactic/generic_model_converter.h" @@ -39,8 +39,8 @@ namespace datalog { bool mk_subsumption_checker::is_total_rule(const rule * r) { - if (r->get_tail_size() != 0) { - return false; + if (r->get_tail_size() != 0) { + return false; } unsigned pt_len = r->get_positive_tail_size(); @@ -113,7 +113,7 @@ namespace datalog { } - bool mk_subsumption_checker::transform_rule(rule * r, + bool mk_subsumption_checker::transform_rule(rule * r, rule_subsumption_index& subs_index, rule_ref & res) { unsigned u_len = r->get_uninterpreted_tail_size(); @@ -133,7 +133,7 @@ namespace datalog { if(m_total_relations.contains(tail_atom->get_decl()) || subs_index.is_subsumed(tail_atom)) { if(neg) { - //rule contains negated total relation, this means that it is unsatisfiable + //rule contains negated total relation, this means that it is unsatisfiable //and can be removed return false; } @@ -143,8 +143,8 @@ namespace datalog { } } if(!neg && head.get()==tail_atom) { - //rule contains its head positively in the tail, therefore - //it will never add any new facts to the relation, so it + //rule contains its head positively in the tail, therefore + //it will never add any new facts to the relation, so it //can be removed return false; } @@ -197,9 +197,9 @@ namespace datalog { if (m_total_relations.contains(head_pred)) { if (!orig.is_output_predicate(head_pred) || total_relations_with_included_rules.contains(head_pred)) { - //We just skip definitions of total non-output relations as + //We just skip definitions of total non-output relations as //we'll eliminate them from the problem. - //We also skip rules of total output relations for which we have + //We also skip rules of total output relations for which we have //already output the rule which implies their totality. modified = true; continue; @@ -286,7 +286,7 @@ namespace datalog { obj_hashtable * head_store; if(m_ground_unconditional_rule_heads.find(pred, head_store)) { //Some relations may receive facts by ground unconditioned rules. - //We scanned for those earlier, so now we check whether we cannot get a + //We scanned for those earlier, so now we check whether we cannot get a //better estimate of relation size from these. unsigned gnd_rule_cnt = head_store->size(); @@ -334,7 +334,7 @@ namespace datalog { rule_set * mk_subsumption_checker::operator()(rule_set const & source) { // TODO mc - if (!m_context.get_params ().xform_subsumption_checker()) + if (!m_context.get_params ().xform_subsumption_checker()) return nullptr; m_have_new_total_rule = false; @@ -366,6 +366,5 @@ namespace datalog { return res; } - -}; +}; diff --git a/src/muz/transforms/dl_transforms.cpp b/src/muz/transforms/dl_transforms.cpp index d456d95f9..d4b9506e8 100644 --- a/src/muz/transforms/dl_transforms.cpp +++ b/src/muz/transforms/dl_transforms.cpp @@ -35,7 +35,7 @@ Revision History: #include "muz/transforms/dl_mk_scale.h" #include "muz/transforms/dl_mk_array_eq_rewrite.h" #include "muz/transforms/dl_mk_array_instantiation.h" -#include "muz/base/fixedpoint_params.hpp" +#include "muz/base/fp_params.hpp" namespace datalog { @@ -72,7 +72,7 @@ namespace datalog { transf.register_plugin(alloc(datalog::mk_rule_inliner, ctx, 34970)); transf.register_plugin(alloc(datalog::mk_coi_filter, ctx, 34960)); transf.register_plugin(alloc(datalog::mk_interp_tail_simplifier, ctx, 34950)); - + if (ctx.get_params().datalog_subsumption()) { transf.register_plugin(alloc(datalog::mk_subsumption_checker, ctx, 34940)); transf.register_plugin(alloc(datalog::mk_rule_inliner, ctx, 34930));