From 56ab7a74953609c787f6f0e946a39efb7fa87008 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 21 Oct 2012 18:12:34 -0700 Subject: [PATCH] checkpoint Signed-off-by: Leonardo de Moura --- scripts/mk_make.py | 3 +- .../der_tactic.cpp | 0 src/{framework => core_tactics}/der_tactic.h | 0 src/framework/cmd_context.h | 8 +- src/{framework => model}/model_smt2_pp.cpp | 74 ++++--------------- src/{framework => model}/model_smt2_pp.h | 5 +- src/{framework => tactic}/converter.h | 0 .../extension_model_converter.cpp | 0 .../extension_model_converter.h | 0 .../filter_model_converter.cpp | 0 .../filter_model_converter.h | 0 src/{framework => tactic}/goal.cpp | 0 src/{framework => tactic}/goal.h | 0 .../goal_shared_occs.cpp | 0 src/{framework => tactic}/goal_shared_occs.h | 0 src/{framework => tactic}/goal_util.cpp | 0 src/{framework => tactic}/goal_util.h | 0 src/{framework => tactic}/model_converter.cpp | 0 src/{framework => tactic}/model_converter.h | 0 src/{framework => tactic}/num_occurs_goal.cpp | 0 src/{framework => tactic}/num_occurs_goal.h | 0 src/{framework => tactic}/probe.cpp | 0 src/{framework => tactic}/probe.h | 0 src/{framework => tactic}/proof_converter.cpp | 0 src/{framework => tactic}/proof_converter.h | 0 src/{framework => tactic}/tactic.cpp | 1 - src/{framework => tactic}/tactic.h | 0 src/{framework => tactic}/tactical.cpp | 0 src/{framework => tactic}/tactical.h | 0 29 files changed, 25 insertions(+), 66 deletions(-) rename src/{framework => core_tactics}/der_tactic.cpp (100%) rename src/{framework => core_tactics}/der_tactic.h (100%) rename src/{framework => model}/model_smt2_pp.cpp (77%) rename src/{framework => model}/model_smt2_pp.h (70%) rename src/{framework => tactic}/converter.h (100%) rename src/{framework => tactic}/extension_model_converter.cpp (100%) rename src/{framework => tactic}/extension_model_converter.h (100%) rename src/{framework => tactic}/filter_model_converter.cpp (100%) rename src/{framework => tactic}/filter_model_converter.h (100%) rename src/{framework => tactic}/goal.cpp (100%) rename src/{framework => tactic}/goal.h (100%) rename src/{framework => tactic}/goal_shared_occs.cpp (100%) rename src/{framework => tactic}/goal_shared_occs.h (100%) rename src/{framework => tactic}/goal_util.cpp (100%) rename src/{framework => tactic}/goal_util.h (100%) rename src/{framework => tactic}/model_converter.cpp (100%) rename src/{framework => tactic}/model_converter.h (100%) rename src/{framework => tactic}/num_occurs_goal.cpp (100%) rename src/{framework => tactic}/num_occurs_goal.h (100%) rename src/{framework => tactic}/probe.cpp (100%) rename src/{framework => tactic}/probe.h (100%) rename src/{framework => tactic}/proof_converter.cpp (100%) rename src/{framework => tactic}/proof_converter.h (100%) rename src/{framework => tactic}/tactic.cpp (99%) rename src/{framework => tactic}/tactic.h (100%) rename src/{framework => tactic}/tactical.cpp (100%) rename src/{framework => tactic}/tactical.h (100%) diff --git a/scripts/mk_make.py b/scripts/mk_make.py index 6d00b5761..22ad87dea 100644 --- a/scripts/mk_make.py +++ b/scripts/mk_make.py @@ -31,10 +31,11 @@ add_lib('simplifier', ['rewriter']) # Model module should not depend on simplifier module. # We must replace all occurrences of simplifier with rewriter. add_lib('model', ['rewriter', 'simplifier']) +add_lib('tactic', ['ast', 'model']) # Old (non-modular) parameter framework. It has been subsumed by util\params.h. # However, it is still used by many old components. add_lib('old_params', ['model', 'simplifier']) -add_lib('framework', ['rewriter', 'model', 'old_params', 'simplifier']) +add_lib('framework', ['tactic', 'rewriter', 'model', 'old_params', 'simplifier']) # Assertion set is the old tactic framework used in Z3 3.x. It will be deleted as soon as we finish the porting old # code to the new tactic framework. add_lib('assertion_set', ['framework']) diff --git a/src/framework/der_tactic.cpp b/src/core_tactics/der_tactic.cpp similarity index 100% rename from src/framework/der_tactic.cpp rename to src/core_tactics/der_tactic.cpp diff --git a/src/framework/der_tactic.h b/src/core_tactics/der_tactic.h similarity index 100% rename from src/framework/der_tactic.h rename to src/core_tactics/der_tactic.h diff --git a/src/framework/cmd_context.h b/src/framework/cmd_context.h index 08122f7d2..d730ba002 100644 --- a/src/framework/cmd_context.h +++ b/src/framework/cmd_context.h @@ -280,6 +280,7 @@ public: bool has_manager() const { return m_manager != 0; } ast_manager & m() const { if (!m_manager) const_cast(this)->init_manager(); return *m_manager; } + virtual ast_manager & get_ast_manager() { return m(); } pdecl_manager & pm() const { if (!m_pmanager) const_cast(this)->init_manager(); return *m_pmanager; } sexpr_manager & sm() const { if (!m_sexpr_manager) const_cast(this)->m_sexpr_manager = alloc(sexpr_manager); return *m_sexpr_manager; } front_end_params & params() const { return m_params; } @@ -383,9 +384,10 @@ public: } format_ns::format * pp(sort * s) const; - void pp(func_decl * f, format_ns::format_ref & r) const; - void pp(expr * n, unsigned num_vars, char const * var_prefix, format_ns::format_ref & r, sbuffer & var_names) const; - void pp(expr * n, format_ns::format_ref & r) const; + virtual void pp(sort * s, format_ns::format_ref & r) const { r = pp(s); } + virtual void pp(func_decl * f, format_ns::format_ref & r) const; + virtual void pp(expr * n, unsigned num_vars, char const * var_prefix, format_ns::format_ref & r, sbuffer & var_names) const; + virtual void pp(expr * n, format_ns::format_ref & r) const; virtual void display(std::ostream & out, sort * s, unsigned indent = 0) const; virtual void display(std::ostream & out, expr * n, unsigned indent, unsigned num_vars, char const * var_prefix, sbuffer & var_names) const; virtual void display(std::ostream & out, expr * n, unsigned indent = 0) const; diff --git a/src/framework/model_smt2_pp.cpp b/src/model/model_smt2_pp.cpp similarity index 77% rename from src/framework/model_smt2_pp.cpp rename to src/model/model_smt2_pp.cpp index 031c5d151..1a639b5f1 100644 --- a/src/framework/model_smt2_pp.cpp +++ b/src/model/model_smt2_pp.cpp @@ -17,6 +17,7 @@ Revision History: --*/ +#include #include"model_smt2_pp.h" #include"ast_smt2_pp.h" #include"func_decl_dependencies.h" @@ -47,53 +48,8 @@ static unsigned pp_symbol(std::ostream & out, symbol const & s) { #define TAB_SZ 2 -class model_smt2_pp_ctx { -public: - virtual ast_manager & m() const = 0; - virtual void display(std::ostream & out, sort * s, unsigned indent = 0) = 0; - virtual void display(std::ostream & out, expr * n, unsigned indent = 0) = 0; - virtual void pp(sort * s, format_ns::format_ref & r) = 0; - virtual void pp(func_decl * f, format_ns::format_ref & r) = 0; - virtual void pp(expr * n, format_ns::format_ref & r) = 0; - virtual void pp(expr * n, unsigned num_vars, char const * var_prefix, format_ns::format_ref & r, sbuffer & var_names) = 0; -}; - -class model_smt2_pp_cmd_ctx : public model_smt2_pp_ctx { - cmd_context & m_ctx; -public: - model_smt2_pp_cmd_ctx(cmd_context & ctx):m_ctx(ctx) {} - virtual ast_manager & m() const { return m_ctx.m(); } - virtual void display(std::ostream & out, sort * s, unsigned indent = 0) { m_ctx.display(out, s, indent); } - virtual void display(std::ostream & out, expr * n, unsigned indent = 0) { m_ctx.display(out, n, indent); } - virtual void pp(sort * s, format_ns::format_ref & r) { r = m_ctx.pp(s); } - virtual void pp(func_decl * f, format_ns::format_ref & r) { return m_ctx.pp(f, r); } - virtual void pp(expr * n, format_ns::format_ref & r) { return m_ctx.pp(n, r); } - virtual void pp(expr * n, unsigned num_vars, char const * var_prefix, format_ns::format_ref & r, sbuffer & var_names) { - return m_ctx.pp(n, num_vars, var_prefix, r, var_names); - } -}; - -class model_smt2_pp_simple_ctx : public model_smt2_pp_ctx { - ast_manager & m_manager; - smt2_pp_environment_dbg m_env; -public: - model_smt2_pp_simple_ctx(ast_manager & m):m_manager(m), m_env(m) {} - virtual ast_manager & m() const { return m_manager; } - virtual void display(std::ostream & out, sort * s, unsigned indent = 0) { out << mk_ismt2_pp(s, m(), indent); } - virtual void display(std::ostream & out, expr * n, unsigned indent = 0) { out << mk_ismt2_pp(n, m(), indent); } - virtual void pp(sort * s, format_ns::format_ref & r) { mk_smt2_format(s, m_env, get_pp_default_params(), r); } - virtual void pp(func_decl * f, format_ns::format_ref & r) { mk_smt2_format(f, m_env, get_pp_default_params(), r); } - virtual void pp(expr * n, format_ns::format_ref & r) { - sbuffer buf; - mk_smt2_format(n, m_env, get_pp_default_params(), 0, 0, r, buf); - } - virtual void pp(expr * n, unsigned num_vars, char const * var_prefix, format_ns::format_ref & r, sbuffer & var_names) { - mk_smt2_format(n, m_env, get_pp_default_params(), num_vars, var_prefix, r, var_names); - } -}; - -static void pp_uninterp_sorts(std::ostream & out, model_smt2_pp_ctx & ctx, model_core const & md, unsigned indent) { - ast_manager & m = ctx.m(); +static void pp_uninterp_sorts(std::ostream & out, ast_printer_context & ctx, model_core const & md, unsigned indent) { + ast_manager & m = ctx.get_ast_manager(); ptr_buffer f_conds; unsigned num = md.get_num_uninterpreted_sorts(); for (unsigned i = 0; i < num; i++) { @@ -179,7 +135,7 @@ static void pp_uninterp_sorts(std::ostream & out, model_smt2_pp_ctx & ctx, model } } -static void pp_consts(std::ostream & out, model_smt2_pp_ctx & ctx, model_core const & md, unsigned indent) { +static void pp_consts(std::ostream & out, ast_printer_context & ctx, model_core const & md, unsigned indent) { unsigned num = md.get_num_constants(); for (unsigned i = 0; i < num; i++) { func_decl * c = md.get_constant(i); @@ -233,8 +189,8 @@ void sort_fun_decls(ast_manager & m, model_core const & md, ptr_buffer var_names; ptr_buffer f_var_names; ptr_buffer f_arg_decls; @@ -333,16 +289,16 @@ static void pp_funs(std::ostream & out, model_smt2_pp_ctx & ctx, model_core cons } } -void model_smt2_pp(std::ostream & out, cmd_context & ctx, model_core const & m, unsigned indent) { - model_smt2_pp_cmd_ctx _ctx(ctx); - pp_uninterp_sorts(out, _ctx, m, indent); - pp_consts(out, _ctx, m, indent); - pp_funs(out, _ctx, m, indent); +void model_smt2_pp(std::ostream & out, ast_printer_context & ctx, model_core const & m, unsigned indent) { + pp_uninterp_sorts(out, ctx, m, indent); + pp_consts(out, ctx, m, indent); + pp_funs(out, ctx, m, indent); } void model_smt2_pp(std::ostream & out, ast_manager & m, model_core const & md, unsigned indent) { - model_smt2_pp_simple_ctx _ctx(m); - pp_uninterp_sorts(out, _ctx, md, indent); - pp_consts(out, _ctx, md, indent); - pp_funs(out, _ctx, md, indent); + scoped_ptr ctx; + ctx = mk_simple_ast_printer_context(m); + pp_uninterp_sorts(out, *(ctx.get()), md, indent); + pp_consts(out, *(ctx.get()), md, indent); + pp_funs(out, *(ctx.get()), md, indent); } diff --git a/src/framework/model_smt2_pp.h b/src/model/model_smt2_pp.h similarity index 70% rename from src/framework/model_smt2_pp.h rename to src/model/model_smt2_pp.h index 29a7cddf2..0b76a8bed 100644 --- a/src/framework/model_smt2_pp.h +++ b/src/model/model_smt2_pp.h @@ -20,9 +20,10 @@ Revision History: #ifndef _MODEL_SMT2_PP_H_ #define _MODEL_SMT2_PP_H_ -#include"cmd_context.h" +#include"ast_printer.h" +#include"model_core.h" -void model_smt2_pp(std::ostream & out, cmd_context & ctx, model_core const & m, unsigned indent); +void model_smt2_pp(std::ostream & out, ast_printer_context & ctx, model_core const & m, unsigned indent); void model_smt2_pp(std::ostream & out, ast_manager & m, model_core const & md, unsigned indent); #endif diff --git a/src/framework/converter.h b/src/tactic/converter.h similarity index 100% rename from src/framework/converter.h rename to src/tactic/converter.h diff --git a/src/framework/extension_model_converter.cpp b/src/tactic/extension_model_converter.cpp similarity index 100% rename from src/framework/extension_model_converter.cpp rename to src/tactic/extension_model_converter.cpp diff --git a/src/framework/extension_model_converter.h b/src/tactic/extension_model_converter.h similarity index 100% rename from src/framework/extension_model_converter.h rename to src/tactic/extension_model_converter.h diff --git a/src/framework/filter_model_converter.cpp b/src/tactic/filter_model_converter.cpp similarity index 100% rename from src/framework/filter_model_converter.cpp rename to src/tactic/filter_model_converter.cpp diff --git a/src/framework/filter_model_converter.h b/src/tactic/filter_model_converter.h similarity index 100% rename from src/framework/filter_model_converter.h rename to src/tactic/filter_model_converter.h diff --git a/src/framework/goal.cpp b/src/tactic/goal.cpp similarity index 100% rename from src/framework/goal.cpp rename to src/tactic/goal.cpp diff --git a/src/framework/goal.h b/src/tactic/goal.h similarity index 100% rename from src/framework/goal.h rename to src/tactic/goal.h diff --git a/src/framework/goal_shared_occs.cpp b/src/tactic/goal_shared_occs.cpp similarity index 100% rename from src/framework/goal_shared_occs.cpp rename to src/tactic/goal_shared_occs.cpp diff --git a/src/framework/goal_shared_occs.h b/src/tactic/goal_shared_occs.h similarity index 100% rename from src/framework/goal_shared_occs.h rename to src/tactic/goal_shared_occs.h diff --git a/src/framework/goal_util.cpp b/src/tactic/goal_util.cpp similarity index 100% rename from src/framework/goal_util.cpp rename to src/tactic/goal_util.cpp diff --git a/src/framework/goal_util.h b/src/tactic/goal_util.h similarity index 100% rename from src/framework/goal_util.h rename to src/tactic/goal_util.h diff --git a/src/framework/model_converter.cpp b/src/tactic/model_converter.cpp similarity index 100% rename from src/framework/model_converter.cpp rename to src/tactic/model_converter.cpp diff --git a/src/framework/model_converter.h b/src/tactic/model_converter.h similarity index 100% rename from src/framework/model_converter.h rename to src/tactic/model_converter.h diff --git a/src/framework/num_occurs_goal.cpp b/src/tactic/num_occurs_goal.cpp similarity index 100% rename from src/framework/num_occurs_goal.cpp rename to src/tactic/num_occurs_goal.cpp diff --git a/src/framework/num_occurs_goal.h b/src/tactic/num_occurs_goal.h similarity index 100% rename from src/framework/num_occurs_goal.h rename to src/tactic/num_occurs_goal.h diff --git a/src/framework/probe.cpp b/src/tactic/probe.cpp similarity index 100% rename from src/framework/probe.cpp rename to src/tactic/probe.cpp diff --git a/src/framework/probe.h b/src/tactic/probe.h similarity index 100% rename from src/framework/probe.h rename to src/tactic/probe.h diff --git a/src/framework/proof_converter.cpp b/src/tactic/proof_converter.cpp similarity index 100% rename from src/framework/proof_converter.cpp rename to src/tactic/proof_converter.cpp diff --git a/src/framework/proof_converter.h b/src/tactic/proof_converter.h similarity index 100% rename from src/framework/proof_converter.h rename to src/tactic/proof_converter.h diff --git a/src/framework/tactic.cpp b/src/tactic/tactic.cpp similarity index 99% rename from src/framework/tactic.cpp rename to src/tactic/tactic.cpp index d5ef15499..4bf9e48f4 100644 --- a/src/framework/tactic.cpp +++ b/src/tactic/tactic.cpp @@ -21,7 +21,6 @@ Notes: #include"probe.h" #include"stopwatch.h" #include"model_v2_pp.h" -#include"cmd_context.h" void tactic::cancel() { #pragma omp critical (tactic_cancel) diff --git a/src/framework/tactic.h b/src/tactic/tactic.h similarity index 100% rename from src/framework/tactic.h rename to src/tactic/tactic.h diff --git a/src/framework/tactical.cpp b/src/tactic/tactical.cpp similarity index 100% rename from src/framework/tactical.cpp rename to src/tactic/tactical.cpp diff --git a/src/framework/tactical.h b/src/tactic/tactical.h similarity index 100% rename from src/framework/tactical.h rename to src/tactic/tactical.h