From 5c11f394cd69f1502ffd496aa104c3b8d1dc1f6b Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 3 Dec 2012 11:01:33 -0800 Subject: [PATCH] port to new parameter infrastructure Signed-off-by: Nikolaj Bjorner --- src/muz_qe/datalog_parser.cpp | 6 +- src/muz_qe/dl_bmc_engine.cpp | 5 +- src/muz_qe/dl_bmc_engine.h | 3 +- src/muz_qe/dl_cmds.cpp | 24 +- src/muz_qe/dl_context.cpp | 72 +-- src/muz_qe/dl_context.h | 47 +- src/muz_qe/dl_mk_bit_blast.cpp | 4 +- src/muz_qe/dl_mk_rule_inliner.cpp | 8 +- src/muz_qe/dl_smt_relation.cpp | 766 ------------------------ src/muz_qe/dl_smt_relation.h | 141 ----- src/muz_qe/dl_util.h | 1 + src/muz_qe/fixedpoint_params.pyg | 62 ++ src/muz_qe/horn_tactic.cpp | 4 +- src/muz_qe/pdr_context.cpp | 52 +- src/muz_qe/pdr_context.h | 7 +- src/muz_qe/pdr_dl_interface.cpp | 41 +- src/muz_qe/pdr_dl_interface.h | 2 - src/muz_qe/pdr_farkas_learner.cpp | 1 - src/muz_qe/pdr_generalizers.cpp | 74 +-- src/muz_qe/pdr_generalizers.h | 7 - src/muz_qe/pdr_interpolant_provider.cpp | 381 ------------ src/muz_qe/pdr_interpolant_provider.h | 54 -- src/muz_qe/pdr_manager.cpp | 15 +- src/muz_qe/pdr_manager.h | 18 +- src/muz_qe/pdr_prop_solver.cpp | 2 +- src/muz_qe/pdr_reachable_cache.cpp | 4 +- src/muz_qe/pdr_reachable_cache.h | 11 +- src/muz_qe/pdr_smt_context_manager.cpp | 4 +- src/muz_qe/pdr_smt_context_manager.h | 3 +- src/shell/datalog_frontend.cpp | 8 +- src/test/dl_smt_relation.cpp | 234 -------- src/test/main.cpp | 1 - 32 files changed, 174 insertions(+), 1888 deletions(-) delete mode 100644 src/muz_qe/dl_smt_relation.cpp delete mode 100644 src/muz_qe/dl_smt_relation.h create mode 100644 src/muz_qe/fixedpoint_params.pyg delete mode 100644 src/muz_qe/pdr_interpolant_provider.cpp delete mode 100644 src/muz_qe/pdr_interpolant_provider.h delete mode 100644 src/test/dl_smt_relation.cpp diff --git a/src/muz_qe/datalog_parser.cpp b/src/muz_qe/datalog_parser.cpp index a1bfc629d..afda12858 100644 --- a/src/muz_qe/datalog_parser.cpp +++ b/src/muz_qe/datalog_parser.cpp @@ -1160,9 +1160,9 @@ class wpa_parser_impl : public wpa_parser, dparser { public: wpa_parser_impl(context & ctx) : dparser(ctx, ctx.get_manager()), - m_bool_sort(ctx.get_manager()), - m_short_sort(ctx.get_manager()), - m_use_map_names(ctx.get_params().get_bool("use_map_names", true)) { + m_bool_sort(ctx.get_manager()), + m_short_sort(ctx.get_manager()), + m_use_map_names(ctx.get_params().use_map_names()) { } ~wpa_parser_impl() { reset_dealloc_values(m_sort_contents); diff --git a/src/muz_qe/dl_bmc_engine.cpp b/src/muz_qe/dl_bmc_engine.cpp index e88e04c5a..dd35cc870 100644 --- a/src/muz_qe/dl_bmc_engine.cpp +++ b/src/muz_qe/dl_bmc_engine.cpp @@ -71,7 +71,7 @@ namespace datalog { m_ctx.set_output_predicate(m_query_pred); m_ctx.apply_default_transformation(mc, m_pc); - if (m_ctx.get_params().get_bool("slice", true)) { + if (m_ctx.get_params().slice()) { datalog::rule_transformer transformer(m_ctx); datalog::mk_slice* slice = alloc(datalog::mk_slice, m_ctx); transformer.register_plugin(slice); @@ -1100,9 +1100,6 @@ namespace datalog { m_solver.reset_statistics(); } - void bmc::collect_params(param_descrs& p) { - } - expr_ref bmc::get_answer() { return m_answer; } diff --git a/src/muz_qe/dl_bmc_engine.h b/src/muz_qe/dl_bmc_engine.h index bd330fa22..5b6e433cd 100644 --- a/src/muz_qe/dl_bmc_engine.h +++ b/src/muz_qe/dl_bmc_engine.h @@ -24,6 +24,7 @@ Revision History: #include "statistics.h" #include "smt_kernel.h" #include "bv_decl_plugin.h" +#include "smt_params.h" namespace datalog { @@ -130,8 +131,6 @@ namespace datalog { void reset_statistics(); expr_ref get_answer(); - - static void collect_params(param_descrs& p); }; }; diff --git a/src/muz_qe/dl_cmds.cpp b/src/muz_qe/dl_cmds.cpp index f45165709..735df8d80 100644 --- a/src/muz_qe/dl_cmds.cpp +++ b/src/muz_qe/dl_cmds.cpp @@ -28,13 +28,15 @@ Notes: #include"cancel_eh.h" #include"scoped_ctrl_c.h" #include"scoped_timer.h" +#include"params2smt_params.h" #include"trail.h" #include -class dl_context { - // PARAM-TODO temp HACK: added m_params field because cmd_context does not have smt_params anymore - smt_params m_params; +struct dl_context { + smt_params m_fparams; + params_ref m_params_ref; + fixedpoint_params m_params; cmd_context & m_cmd; dl_collected_cmds* m_collected_cmds; unsigned m_ref_count; @@ -42,8 +44,8 @@ class dl_context { scoped_ptr m_context; trail_stack m_trail; -public: dl_context(cmd_context & ctx, dl_collected_cmds* collected_cmds): + m_params(m_params_ref), m_cmd(ctx), m_collected_cmds(collected_cmds), m_ref_count(0), @@ -64,7 +66,7 @@ public: void init() { ast_manager& m = m_cmd.m(); if (!m_context) { - m_context = alloc(datalog::context, m, m_params); + m_context = alloc(datalog::context, m, m_fparams, m_params_ref); } if (!m_decl_plugin) { symbol name("datalog_relation"); @@ -212,7 +214,7 @@ public: datalog::context& dlctx = m_dl_ctx->dlctx(); set_background(ctx); dlctx.updt_params(m_params); - unsigned timeout = m_params.get_uint("timeout", UINT_MAX); + unsigned timeout = m_dl_ctx->m_params.timeout(); cancel_eh eh(dlctx); lbool status = l_undef; { @@ -267,10 +269,6 @@ public: virtual void init_pdescrs(cmd_context & ctx, param_descrs & p) { m_dl_ctx->dlctx().collect_params(p); - insert_timeout(p); - p.insert("print_answer", CPK_BOOL, "(default: false) print answer instance(s) to query."); - p.insert("print_certificate", CPK_BOOL, "(default: false) print certificate for reachability or non-reachability."); - p.insert("print_statistics", CPK_BOOL, "(default: false) print statistics."); } @@ -285,7 +283,7 @@ private: } void print_answer(cmd_context& ctx) { - if (m_params.get_bool("print_answer", false)) { + if (m_dl_ctx->m_params.print_answer()) { datalog::context& dlctx = m_dl_ctx->dlctx(); ast_manager& m = ctx.m(); expr_ref query_result(dlctx.get_answer_as_formula(), m); @@ -300,7 +298,7 @@ private: } void print_statistics(cmd_context& ctx) { - if (m_params.get_bool("print_statistics", false)) { + if (m_dl_ctx->m_params.print_statistics()) { statistics st; datalog::context& dlctx = m_dl_ctx->dlctx(); unsigned long long max_mem = memory::get_max_used_memory(); @@ -314,7 +312,7 @@ private: } void print_certificate(cmd_context& ctx) { - if (m_params.get_bool("print_certificate", false)) { + if (m_dl_ctx->m_params.print_certificate()) { datalog::context& dlctx = m_dl_ctx->dlctx(); if (!dlctx.display_certificate(ctx.regular_stream())) { throw cmd_exception("certificates are not supported for the selected engine"); diff --git a/src/muz_qe/dl_context.cpp b/src/muz_qe/dl_context.cpp index 3b7ad6ffc..228dbc572 100644 --- a/src/muz_qe/dl_context.cpp +++ b/src/muz_qe/dl_context.cpp @@ -44,7 +44,6 @@ Revision History: #include"dl_compiler.h" #include"dl_instruction.h" #include"dl_context.h" -#include"dl_smt_relation.h" #ifndef _EXTERNAL_RELEASE #include"dl_skip_table.h" #endif @@ -229,7 +228,8 @@ namespace datalog { context::context(ast_manager & m, smt_params& fp, params_ref const& pa): m(m), m_fparams(fp), - m_params(pa), + m_params_ref(pa), + m_params(m_params_ref), m_decl_util(m), m_rewriter(m), m_var_subst(m), @@ -259,7 +259,6 @@ namespace datalog { #endif //register plugins for builtin relations - get_rmanager().register_plugin(alloc(smt_relation_plugin, get_rmanager())); get_rmanager().register_plugin(alloc(bound_relation_plugin, get_rmanager())); get_rmanager().register_plugin(alloc(interval_relation_plugin, get_rmanager())); @@ -960,66 +959,13 @@ namespace datalog { } void context::collect_params(param_descrs& p) { - p.insert("engine", CPK_SYMBOL, "(default: automatically configured) select 'datalog', PDR 'pdr' engine."); - p.insert("bit_blast", CPK_BOOL, "(default: false) bit-blast bit-vectors (for PDR engine)."); - p.insert("default_table", CPK_SYMBOL, "default table implementation: 'sparse' (default), 'hashtable', 'bitvector', 'interval'"); - p.insert("default_relation", CPK_SYMBOL, "default relation implementation: 'external_relation', 'pentagon'"); - - p.insert("generate_explanations", CPK_BOOL, "if true, signature of relations will be extended to contain explanations for facts"); - p.insert("explanations_on_relation_level", CPK_BOOL, "if true, explanations are generated as history of each relation, " - "rather than per fact (generate_explanations must be set to true for this option to have any effect)"); - - p.insert("magic_sets_for_queries", CPK_BOOL, "magic set transformation will be used for queries"); - p.insert("unbound_compressor", CPK_BOOL, "auxiliary relations will be introduced to avoid unbound variables in rule heads"); - p.insert("similarity_compressor", CPK_BOOL, "rules that differ only in values of constants will be merged into a single rule"); - p.insert("similarity_compressor_threshold", CPK_UINT, "if dl_similiaryt_compressor is on, this value determines how many " - "similar rules there must be in order for them to be merged"); - - p.insert("all_or_nothing_deltas", CPK_BOOL, "compile rules so that it is enough for the delta relation in union and widening " - "operations to determine only whether the updated relation was modified or not"); - p.insert("compile_with_widening", CPK_BOOL, "widening will be used to compile recursive rules"); - p.insert("eager_emptiness_checking", CPK_BOOL, "emptiness of affected relations will be checked after each instruction, " - "so that we may ommit unnecessary instructions"); - p.insert("default_table_checked", CPK_BOOL, - "if true, the detault table will be default_table inside a wrapper that checks that " - "its results are the same as of default_table_checker table"); - - - p.insert("initial_restart_timeout", CPK_UINT, "length of saturation run before the first restart (in ms); zero means no restarts"); - p.insert("restart_timeout_quotient", CPK_UINT, "restart timeout will be multiplied by this number after each restart"); - p.insert("use_map_names", CPK_BOOL, "use names from map files when displaying tuples"); - - p.insert("output_profile", CPK_BOOL, "determines whether profile informations should be output when outputting Datalog rules or instructions"); - p.insert("output_tuples", CPK_BOOL, "determines whether tuples for output predicates should be output"); - p.insert("profile_timeout_milliseconds", CPK_UINT, "instructions and rules that took less than the threshold will not be printed when printed the instruction/rule list"); - - p.insert("print_with_fixedpoint_extensions", CPK_BOOL, "(default true) use SMT-LIB2 fixedpoint extensions, instead of pure SMT2, when printing rules"); - p.insert("print_low_level_smt2", CPK_BOOL, "(default false) use (faster) low-level SMT2 printer (the printer is scalable but the result may not be as readable)"); - p.insert("print_with_variable_declarations", CPK_BOOL, "(default true) use variable declarations when displaying rules (instead of attempting to use original names)"); - -#ifndef _EXTERNAL_RELEASE - p.insert("dbg_fpr_nonempty_relation_signature", CPK_BOOL, - "if true, finite_product_relation will attempt to avoid creating inner relation with empty signature " - "by putting in half of the table columns, if it would have been empty otherwise"); - - p.insert("smt_relation_ground_recursive", CPK_BOOL, "Ensure recursive relation is ground in union"); - p.insert("inline_linear_branch", CPK_BOOL, "try linear inlining method with potential expansion"); -#endif - p.insert("fix_unbound_vars", CPK_BOOL, "fix unbound variables in tail"); - p.insert("default_table_checker", CPK_SYMBOL, "see default_table_checked"); - p.insert("inline_linear", CPK_BOOL, "(default true) try linear inlining method"); - p.insert("inline_eager", CPK_BOOL, "(default true) try eager inlining of rules"); - - - pdr::dl_interface::collect_params(p); - bmc::collect_params(p); + fixedpoint_params::collect_param_descrs(p); insert_timeout(p); } void context::updt_params(params_ref const& p) { - m_params.copy(p); - if (m_pdr.get()) m_pdr->updt_params(); - + m_params_ref.copy(p); + if (m_pdr.get()) m_pdr->updt_params(); } void context::collect_predicates(decl_set & res) { @@ -1190,7 +1136,7 @@ namespace datalog { }; void context::configure_engine() { - symbol e = m_params.get_sym("engine", symbol()); + symbol e = m_params.engine(); if (e == symbol("datalog")) { m_engine = DATALOG_ENGINE; @@ -1668,9 +1614,9 @@ namespace datalog { expr_ref fml(m); expr_ref_vector rules(m); svector names; - bool use_fixedpoint_extensions = m_params.get_bool("print_with_fixedpoint_extensions", true); - bool print_low_level = m_params.get_bool("print_low_level_smt2", false); - bool do_declare_vars = m_params.get_bool("print_with_variable_declarations", true); + bool use_fixedpoint_extensions = m_params.print_with_fixedpoint_extensions(); + bool print_low_level = m_params.print_low_level_smt2(); + bool do_declare_vars = m_params.print_with_variable_declarations(); #define PP(_e_) if (print_low_level) out << mk_smt_pp(_e_, m); else ast_smt2_pp(out, _e_, env); diff --git a/src/muz_qe/dl_context.h b/src/muz_qe/dl_context.h index 9078bc693..5dcb3e1fa 100644 --- a/src/muz_qe/dl_context.h +++ b/src/muz_qe/dl_context.h @@ -24,7 +24,6 @@ Revision History: #undef max #endif #include"arith_decl_plugin.h" -#include"smt_params.h" #include"map.h" #include"th_rewriter.h" #include"str_hashtable.h" @@ -44,6 +43,7 @@ Revision History: #include"model_converter.h" #include"proof_converter.h" #include"model2expr.h" +#include"smt_params.h" namespace datalog { @@ -78,8 +78,9 @@ namespace datalog { typedef vector > fact_vector; ast_manager & m; - smt_params& m_fparams; - params_ref m_params; + smt_params & m_fparams; + params_ref m_params_ref; + fixedpoint_params m_params; dl_decl_util m_decl_util; th_rewriter m_rewriter; var_subst m_var_subst; @@ -122,7 +123,7 @@ namespace datalog { public: - context(ast_manager & m, smt_params& params, params_ref const& p = params_ref()); + context(ast_manager & m, smt_params& fp, params_ref const& p = params_ref()); ~context(); void reset(); @@ -150,31 +151,31 @@ namespace datalog { const relation_manager & get_rmanager() const { return m_rmanager; } rule_manager & get_rule_manager() { return m_rule_manager; } smt_params & get_fparams() const { return m_fparams; } - params_ref const& get_params() const { return m_params; } + fixedpoint_params const& get_params() const { return m_params; } DL_ENGINE get_engine() { configure_engine(); return m_engine; } th_rewriter& get_rewriter() { return m_rewriter; } var_subst & get_var_subst() { return m_var_subst; } dl_decl_util & get_decl_util() { return m_decl_util; } - bool output_profile() const { return m_params.get_bool("output_profile", false); } - bool fix_unbound_vars() const { return m_params.get_bool("fix_unbound_vars", false); } - symbol default_table() const { return m_params.get_sym("default_table", symbol("sparse")); } - symbol default_relation() const { return m_params.get_sym("default_relation", external_relation_plugin::get_name()); } - symbol default_table_checker() const { return m_params.get_sym("default_table_checker", symbol("sparse")); } - bool default_table_checked() const { return m_params.get_bool("default_table_checked", false); } - bool dbg_fpr_nonempty_relation_signature() const { return m_params.get_bool("dbg_fpr_nonempty_relation_signatures", false); } - unsigned dl_profile_milliseconds_threshold() const { return m_params.get_uint("profile_milliseconds_threshold", 0); } - bool all_or_nothing_deltas() const { return m_params.get_bool("all_or_nothing_deltas", false); } - bool compile_with_widening() const { return m_params.get_bool("compile_with_widening", false); } - bool unbound_compressor() const { return m_params.get_bool("unbound_compressor", true); } - bool similarity_compressor() const { return m_params.get_bool("similarity_compressor", true); } - unsigned similarity_compressor_threshold() const { return m_params.get_uint("similarity_compressor_threshold", 11); } + bool output_profile() const { return m_params.output_profile(); } + bool fix_unbound_vars() const { return m_params.fix_unbound_vars(); } + symbol default_table() const { return m_params.default_table(); } + symbol default_relation() const { return m_params.default_relation(); } // external_relation_plugin::get_name()); + symbol default_table_checker() const { return m_params.default_table_checker(); } + bool default_table_checked() const { return m_params.default_table_checked(); } + bool dbg_fpr_nonempty_relation_signature() const { return m_params.dbg_fpr_nonempty_relation_signature(); } + unsigned dl_profile_milliseconds_threshold() const { return m_params.profile_timeout_milliseconds(); } + bool all_or_nothing_deltas() const { return m_params.all_or_nothing_deltas(); } + bool compile_with_widening() const { return m_params.compile_with_widening(); } + bool unbound_compressor() const { return m_params.unbound_compressor(); } + bool similarity_compressor() const { return m_params.similarity_compressor(); } + unsigned similarity_compressor_threshold() const { return m_params.similarity_compressor_threshold(); } unsigned soft_timeout() const { return m_fparams.m_soft_timeout; } - unsigned initial_restart_timeout() const { return m_params.get_uint("initial_restart_timeout", 0); } - bool generate_explanations() const { return m_params.get_bool("generate_explanations", false); } - bool explanations_on_relation_level() const { return m_params.get_bool("explanations_on_relation_level", false); } - bool magic_sets_for_queries() const { return m_params.get_bool("magic_sets_for_queries", false); } - bool eager_emptiness_checking() const { return m_params.get_bool("eager_emptiness_checking", true); } + unsigned initial_restart_timeout() const { return m_params.initial_restart_timeout(); } + bool generate_explanations() const { return m_params.generate_explanations(); } + bool explanations_on_relation_level() const { return m_params.explanations_on_relation_level(); } + bool magic_sets_for_queries() const { return m_params.magic_sets_for_queries(); } + bool eager_emptiness_checking() const { return m_params.eager_emptiness_checking(); } void register_finite_sort(sort * s, sort_kind k); diff --git a/src/muz_qe/dl_mk_bit_blast.cpp b/src/muz_qe/dl_mk_bit_blast.cpp index c523315d9..1fa93a0ca 100644 --- a/src/muz_qe/dl_mk_bit_blast.cpp +++ b/src/muz_qe/dl_mk_bit_blast.cpp @@ -161,7 +161,7 @@ namespace datalog { impl(context& ctx): m_context(ctx), m(ctx.get_manager()), - m_params(ctx.get_params()), + m_params(ctx.get_params().p), m_rules(ctx.get_rule_manager()), m_blaster(ctx.get_manager(), m_params), m_rewriter(ctx.get_manager(), ctx, m_rules) { @@ -172,7 +172,7 @@ namespace datalog { rule_set * operator()(rule_set const & source, model_converter_ref& mc, proof_converter_ref& pc) { // TODO mc, pc - if (!m_context.get_params().get_bool("bit_blast", false)) { + if (!m_context.get_params().bit_blast()) { return 0; } if (m_context.get_engine() != PDR_ENGINE) { diff --git a/src/muz_qe/dl_mk_rule_inliner.cpp b/src/muz_qe/dl_mk_rule_inliner.cpp index cfe532fb6..9c9bf7abb 100644 --- a/src/muz_qe/dl_mk_rule_inliner.cpp +++ b/src/muz_qe/dl_mk_rule_inliner.cpp @@ -750,8 +750,7 @@ namespace datalog { valid.reset(); valid.resize(sz, true); - params_ref const& params = m_context.get_params(); - bool allow_branching = params.get_bool("inline_linear_branch", false); + bool allow_branching = m_context.get_params().inline_linear_branch(); for (unsigned i = 0; i < sz; ++i) { @@ -842,7 +841,6 @@ namespace datalog { bool something_done = false; ref hsmc; ref hpc; - params_ref const& params = m_context.get_params(); if (source.get_num_rules() == 0) { return 0; @@ -867,7 +865,7 @@ namespace datalog { scoped_ptr res = alloc(rule_set, m_context); - if (params.get_bool("inline_eager", true)) { + if (m_context.get_params().inline_eager()) { TRACE("dl", source.display(tout << "before eager inlining\n");); plan_inlining(source); something_done = transform_rules(source, *res); @@ -879,7 +877,7 @@ namespace datalog { TRACE("dl", res->display(tout << "after eager inlining\n");); } - if (params.get_bool("inline_linear", true) && inline_linear(res)) { + if (m_context.get_params().inline_linear() && inline_linear(res)) { something_done = true; } diff --git a/src/muz_qe/dl_smt_relation.cpp b/src/muz_qe/dl_smt_relation.cpp deleted file mode 100644 index ee465a7d8..000000000 --- a/src/muz_qe/dl_smt_relation.cpp +++ /dev/null @@ -1,766 +0,0 @@ -/*++ -Copyright (c) 2010 Microsoft Corporation - -Module Name: - - dl_smt_relation.cpp - -Abstract: - - Relation based on SMT signature. - - -Author: - - Nikolaj Bjorner (nbjorner) 2010-10-10 - -Revision History: - ---*/ -#include -#include "debug.h" -#include "ast_pp.h" -#include "dl_context.h" -#include "dl_smt_relation.h" -#include "expr_abstract.h" -#include "smt_kernel.h" -#include "th_rewriter.h" -#include "qe.h" -#include "datatype_decl_plugin.h" -#include "bv_decl_plugin.h" -#include "ast_ll_pp.h" -#include "expr_context_simplifier.h" -#include "has_free_vars.h" -#include "ast_smt_pp.h" - -namespace datalog { - - - smt_relation::smt_relation(smt_relation_plugin & p, const relation_signature & s, expr* r) - : relation_base(p, s), - m_rel(r, p.get_ast_manager()), - m_bound_vars(p.get_ast_manager()) - { - ast_manager& m = p.get_ast_manager(); - for (unsigned i = 0; m_bound_vars.size() < s.size(); ++i) { - unsigned j = s.size() - i - 1; - m_bound_vars.push_back(m.mk_const(symbol(j), s[j])); - } - SASSERT(is_well_formed()); - } - - smt_relation::~smt_relation() { - } - - bool smt_relation::is_well_formed() const { - ast_manager& m = get_manager(); - ptr_vector bound_sorts; - for (unsigned i = 0; i < m_bound_vars.size(); ++i) { - bound_sorts.push_back(m.get_sort(m_bound_vars[i])); - } - return is_well_formed_vars(bound_sorts, get_relation()); - } - - void smt_relation::instantiate(expr* r, expr_ref& result) const { - ast_manager& m = get_manager(); - var_subst subst(m); - ptr_vector bound_sorts; - for (unsigned i = 0; i < m_bound_vars.size(); ++i) { - bound_sorts.push_back(m.get_sort(m_bound_vars[i])); - } - TRACE("smt_relation", - tout << mk_ll_pp(r, m) << "\n"; - for (unsigned i = 0; i < bound_sorts.size(); ++i) { - tout << mk_pp(bound_sorts[i], m) << " "; - } - tout << "\n"; - ); - SASSERT(is_well_formed_vars(bound_sorts, r)); - - subst(r, m_bound_vars.size(), m_bound_vars.c_ptr(), result); - } - - void smt_relation::mk_abstract(expr* r, expr_ref& result) const { - ast_manager& m = get_manager(); - TRACE("smt_relation", tout << mk_ll_pp(r, m) << "\n";); - expr_abstract(m, 0, m_bound_vars.size(), m_bound_vars.c_ptr(), r, result); - TRACE("smt_relation", tout << mk_ll_pp(result, m) << "\n";); - ptr_vector bound_sorts; - for (unsigned i = 0; i < m_bound_vars.size(); ++i) { - bound_sorts.push_back(m.get_sort(m_bound_vars[i])); - } - SASSERT(is_well_formed_vars(bound_sorts, r)); - } - - void smt_relation::set_relation(expr* r) { - m_rel = r; - is_well_formed(); - } - - void smt_relation::add_relation(expr* s) { - ast_manager& m = get_manager(); - m_rel = m.mk_or(m_rel, s); - is_well_formed(); - } - - void smt_relation::filter_relation(expr* s) { - ast_manager& m = get_manager(); - m_rel = m.mk_and(m_rel, s); - is_well_formed(); - } - - expr* smt_relation::get_relation() const { - return m_rel.get(); - } - - void smt_relation::simplify(expr_ref& fml) const { - th_rewriter rw(get_manager()); - rw(fml); - } - - bool smt_relation::empty() const { - ast_manager& m = get_manager(); - expr* r = get_relation(); - if (m.is_true(r)) { - return false; - } - if (m.is_false(r)) { - return true; - } - IF_VERBOSE(10, verbose_stream() << "Checking emptiness...\n"; ); - - smt_params& params = get_plugin().get_fparams(); - // [Leo]: asserted_formulas do not have support for der. - // We should use the tactics der. - // flet flet2(params.m_der, true); - smt::kernel ctx(m, params); - expr_ref tmp(m); - instantiate(r, tmp); - ctx.assert_expr(tmp); - if (get_plugin().get_fparams().m_dump_goal_as_smt) { - static unsigned n = 0; - std::ostringstream strm; - strm << "File" << n << ".smt2"; - std::ofstream out(strm.str().c_str()); - ast_smt_pp pp(m); - pp.display_smt2(out, tmp); - ++n; - } - return l_false == ctx.check(); - } - - void smt_relation::add_fact(const relation_fact & f) { - SASSERT(f.size() == size()); - ast_manager& m = get_manager(); - expr_ref_vector eqs(m); - for (unsigned i = 0; i < f.size(); ++i) { - eqs.push_back(m.mk_eq(m.mk_var(i,m.get_sort(f[i])), f[i])); - } - expr_ref e1(m.mk_and(eqs.size(), eqs.c_ptr()), m); - add_relation(e1); - } - - - bool smt_relation::contains_fact(const relation_fact & f) const { - ast_manager& m = get_manager(); - expr_ref_vector eqs(m); - expr_ref cond(m); - for (unsigned i = 0; i < f.size(); ++i) { - eqs.push_back(m.mk_eq(m.mk_var(i,m.get_sort(f[i])), f[i])); - } - cond = m.mk_and(eqs.size(), eqs.c_ptr()); - return const_cast(this)->contains(cond); - } - - // - // facts in Rel iff - // facts => Rel iff - // facts & not Rel is unsat - // - bool smt_relation::contains(expr* facts) { - ast_manager& m = get_manager(); - expr_ref fml_free(m), fml_inst(m); - fml_free = m.mk_and(facts, m.mk_not(get_relation())); - instantiate(fml_free, fml_inst); - smt_params& params = get_plugin().get_fparams(); - // [Leo]: asserted_formulas do not have support for qe nor der. - // We should use the tactics qe and der. - // BTW, qe at asserted_formulas was disabled when we moved to codeplex, but the field m_quant_elim was not deleted. - // - // flet flet0(params.m_quant_elim, true); - flet flet1(params.m_nnf_cnf, false); - // flet flet2(params.m_der, true); - smt::kernel ctx(m, params); - ctx.assert_expr(fml_inst); - lbool result = ctx.check(); - TRACE("smt_relation", - display(tout); - tout << mk_pp(facts, m) << "\n"; - tout << ((result == l_false)?"true":"false") << "\n";); - return result == l_false; - } - - smt_relation * smt_relation::clone() const { - return alloc(smt_relation, get_plugin(), get_signature(), get_relation()); - } - - smt_relation * smt_relation::complement(func_decl* p) const { - ast_manager& m = get_manager(); - smt_relation* result = alloc(smt_relation, get_plugin(), get_signature(), m.mk_not(get_relation())); - TRACE("smt_relation", - display(tout<<"src:\n"); - result->display(tout<<"complement:\n");); - return result; - } - - void smt_relation::display(std::ostream & out) const { - if (is_finite_domain()) { - display_finite(out); - } - else { - out << mk_ll_pp(get_relation(), get_manager()) << "\n"; - } - } - - smt_relation_plugin & smt_relation::get_plugin() const { - return static_cast(relation_base::get_plugin()); - } - - bool smt_relation::is_finite_domain() const { - relation_signature const& sig = get_signature(); - for (unsigned i = 0; i < sig.size(); ++i) { - if (!get_plugin().is_finite_domain(sig[i])) { - return false; - } - } - return true; - } - - - void smt_relation::display_finite(std::ostream & out) const { - ast_manager& m = get_manager(); - smt_params& params = get_plugin().get_fparams(); - expr* r = get_relation(); - expr_ref tmp(m); - expr_ref_vector values(m), eqs(m); - unsigned num_vars = m_bound_vars.size(); - values.resize(num_vars); - eqs.resize(num_vars); - instantiate(r, tmp); - flet flet4(params.m_model, true); - smt::kernel ctx(m, params); - ctx.assert_expr(tmp); - - while (true) { - lbool is_sat = ctx.check(); - if (is_sat == l_false) { - break; - } - model_ref mod; - ctx.get_model(mod); - for (unsigned i = 0; i < num_vars; ++i) { - mod->eval(m_bound_vars[i], tmp, true); - values[i] = tmp; - eqs[i] = m.mk_eq(values[i].get(), m_bound_vars[i]); - - } - out << " ("; - for (unsigned i = 0; i < num_vars; ++i) { - unsigned j = num_vars - 1 - i; - out << mk_pp(values[j].get(), m); - if (i + 1 < num_vars) { - out << " "; - } - } - out << ")\n"; - tmp = m.mk_not(m.mk_and(num_vars, eqs.c_ptr())); - ctx.assert_expr(tmp); - } - } - - // ----------------------------------- - // - // smt_relation_plugin - // - // ----------------------------------- - - - smt_relation_plugin::smt_relation_plugin(relation_manager & m) - : relation_plugin(smt_relation_plugin::get_name(), m), m_counter(0) {} - - - relation_base * smt_relation_plugin::mk_empty(const relation_signature & s) { - return alloc(smt_relation, *this, s, get_ast_manager().mk_false()); - } - - - class smt_relation_plugin::join_fn : public convenient_relation_join_fn { - smt_relation_plugin& m_plugin; - expr_ref_vector m_conjs; - public: - join_fn(smt_relation_plugin& p, const relation_signature & o1_sig, const relation_signature & o2_sig, unsigned col_cnt, - const unsigned * cols1, const unsigned * cols2) - : convenient_relation_join_fn(o1_sig, o2_sig, col_cnt, cols1, cols2), - m_plugin(p), - m_conjs(p.get_ast_manager()) { - ast_manager& m = p.get_ast_manager(); - unsigned sz = m_cols1.size(); - for (unsigned i = 0; i < sz; ++i) { - unsigned col1 = m_cols1[i]; - unsigned col2 = m_cols2[i]; - var* v1 = m.mk_var(col1, o1_sig[col1]); - var* v2 = m.mk_var(col2 + o1_sig.size(), o2_sig[col2]); - m_conjs.push_back(m.mk_eq(v1, v2)); - } - } - - virtual relation_base * operator()(const relation_base & r1, const relation_base & r2) { - ast_manager& m = m_plugin.get_ast_manager(); - expr_ref e2(m), res(m); - shift_vars sh(m); - sh(get(r2).get_relation(), r1.get_signature().size(), e2); - m_conjs.push_back(get(r1).get_relation()); - m_conjs.push_back(e2); - res = m.mk_and(m_conjs.size(), m_conjs.c_ptr()); - m_conjs.pop_back(); - m_conjs.pop_back(); - smt_relation* result = alloc(smt_relation, m_plugin, get_result_signature(), res); - TRACE("smt_relation", - get(r1).display(tout << "src1:\n"); - get(r2).display(tout << "src2:\n"); - for (unsigned i = 0; i < m_conjs.size(); ++i) { - tout << m_cols1[i] << " = " << m_cols2[i] << " -- "; - tout << mk_pp(m_conjs[i].get(), m) << "\n"; - } - result->display(tout << "dst:\n"); - ); - return result; - } - }; - - relation_join_fn * smt_relation_plugin::mk_join_fn(const relation_base & r1, const relation_base & r2, - unsigned col_cnt, const unsigned * cols1, const unsigned * cols2) { - if (!check_kind(r1) || !check_kind(r2)) { - return 0; - } - return alloc(join_fn, *this, r1.get_signature(), r2.get_signature(), col_cnt, cols1, cols2); - } - - class smt_relation_plugin::project_fn : public convenient_relation_project_fn { - smt_relation_plugin& m_plugin; - expr_ref_vector m_subst; - sort_ref_vector m_sorts; - svector m_names; - public: - project_fn(smt_relation_plugin& p, - const relation_signature & orig_sig, unsigned removed_col_cnt, const unsigned * removed_cols) - : convenient_relation_project_fn(orig_sig, removed_col_cnt, removed_cols), - m_plugin(p), - m_subst(p.get_ast_manager()), - m_sorts(p.get_ast_manager()) { - ast_manager& m = p.get_ast_manager(); - unsigned_vector const& cols = m_removed_cols; - unsigned num_cols = cols.size(); - - unsigned lo = 0, hi = num_cols; - for (unsigned i = 0, c = 0; i < orig_sig.size(); ++i) { - SASSERT(c <= num_cols); - if (c == num_cols) { - SASSERT(lo == num_cols); - m_subst.push_back(m.mk_var(hi, orig_sig[i])); - ++hi; - continue; - } - SASSERT(c < num_cols); - unsigned col = cols[c]; - SASSERT(i <= col); - if (i == col) { - m_names.push_back(symbol(p.fresh_name())); - m_sorts.push_back(orig_sig[col]); - m_subst.push_back(m.mk_var(lo, orig_sig[i])); - ++lo; - ++c; - continue; - } - m_subst.push_back(m.mk_var(hi, orig_sig[i])); - ++hi; - } - m_subst.reverse(); - m_sorts.reverse(); - m_names.reverse(); - } - - virtual relation_base * operator()(const relation_base & r) { - ast_manager& m = m_plugin.get_ast_manager(); - expr_ref tmp1(m), tmp2(m); - var_subst subst(m); - smt_relation* result = 0; - tmp1 = get(r).get_relation(); - subst(tmp1, m_subst.size(), m_subst.c_ptr(), tmp2); - tmp2 = m.mk_exists(m_sorts.size(), m_sorts.c_ptr(), m_names.c_ptr(), tmp2); - result = alloc(smt_relation, m_plugin, get_result_signature(), tmp2); - TRACE("smt_relation", - tout << "Signature: "; - for (unsigned i = 0; i < r.get_signature().size(); ++i) { - tout << mk_pp(r.get_signature()[i], m) << " "; - } - tout << "Remove: "; - for (unsigned i = 0; i < m_removed_cols.size(); ++i) { - tout << m_removed_cols[i] << " "; - } - tout << "\n"; - tout << "Subst: "; - for (unsigned i = 0; i < m_subst.size(); ++i) { - tout << mk_pp(m_subst[i].get(), m) << " "; - } - tout << "\n"; - get(r).display(tout); - tout << " --> \n"; - result->display(tout);); - return result; - } - }; - - relation_transformer_fn * smt_relation_plugin::mk_project_fn(const relation_base & r, - unsigned col_cnt, const unsigned * removed_cols) { - return alloc(project_fn, *this, r.get_signature(), col_cnt, removed_cols); - } - - - class smt_relation_plugin::rename_fn : public convenient_relation_rename_fn { - smt_relation_plugin& m_plugin; - expr_ref_vector m_subst; - public: - rename_fn(smt_relation_plugin& p, const relation_signature & orig_sig, unsigned cycle_len, const unsigned * cycle) - : convenient_relation_rename_fn(orig_sig, cycle_len, cycle), - m_plugin(p), - m_subst(p.get_ast_manager()) { - - ast_manager& m = p.get_ast_manager(); - for (unsigned i = 0; i < orig_sig.size(); ++i) { - m_subst.push_back(m.mk_var(i, orig_sig[i])); - } - unsigned col1, col2; - for (unsigned i = 0; i +1 < cycle_len; ++i) { - col1 = cycle[i]; - col2 = cycle[i+1]; - m_subst[col2] = m.mk_var(col1, orig_sig[col2]); - } - col1 = cycle[cycle_len-1]; - col2 = cycle[0]; - m_subst[col2] = m.mk_var(col1, orig_sig[col2]); - m_subst.reverse(); - } - - virtual relation_base * operator()(const relation_base & r) { - ast_manager& m = m_plugin.get_ast_manager(); - expr_ref res(m); - var_subst subst(m); - subst(get(r).get_relation(), m_subst.size(), m_subst.c_ptr(), res); - TRACE("smt_relation3", - tout << "cycle: "; - for (unsigned i = 0; i < m_cycle.size(); ++i) { - tout << m_cycle[i] << " "; - } - tout << "\n"; - tout << "old_sig: "; - for (unsigned i = 0; i < r.get_signature().size(); ++i) { - tout << mk_pp(r.get_signature()[i], m) << " "; - } - tout << "\n"; - tout << "new_sig: "; - for (unsigned i = 0; i < get_result_signature().size(); ++i) { - tout << mk_pp(get_result_signature()[i], m) << " "; - } - tout << "\n"; - tout << "subst: "; - for (unsigned i = 0; i < m_subst.size(); ++i) { - tout << mk_pp(m_subst[i].get(), m) << " "; - } - tout << "\n"; - get(r).display(tout << "src:\n"); - tout << "dst:\n" << mk_ll_pp(res, m) << "\n"; - ); - smt_relation* result = alloc(smt_relation, m_plugin, get_result_signature(), res); - - return result; - } - }; - - relation_transformer_fn * smt_relation_plugin::mk_rename_fn(const relation_base & r, - unsigned cycle_len, const unsigned * permutation_cycle) { - if(!check_kind(r)) { - return 0; - } - return alloc(rename_fn, *this, r.get_signature(), cycle_len, permutation_cycle); - } - - - class smt_relation_plugin::union_fn : public relation_union_fn { - smt_relation_plugin& m_plugin; - - public: - union_fn(smt_relation_plugin& p) : - m_plugin(p) { - } - - virtual void operator()(relation_base & r, const relation_base & src, relation_base * delta) { - ast_manager& m = m_plugin.get_ast_manager(); - expr* srcE = get(src).get_relation(); - TRACE("smt_relation", - tout << "dst:\n"; - get(r).display(tout); - tout << "src:\n"; - get(src).display(tout);); - - SASSERT(get(src).is_well_formed()); - SASSERT(get(r).is_well_formed()); - - if (delta) { - // - // delta(a) <- - // exists x . srcE(a, x) & not rE(a, y) - - - expr_ref rInst(m), srcInst(m), tmp(m), tmp1(m); - expr_ref notR(m), srcGround(m); - smt_params& fparams = get(r).get_plugin().get_fparams(); - params_ref const& params = get(r).get_plugin().get_params(); - - get(r).instantiate(get(r).get_relation(), rInst); - get(src).instantiate(get(src).get_relation(), srcInst); - qe::expr_quant_elim_star1 qe(m, fparams); - - IF_VERBOSE(10, verbose_stream() << "Computing delta...\n"; ); - - if (params.get_bool("smt_relation_ground_recursive", false)) { - // ensure R is ground. Simplify S using assumption not R - if (!is_ground(rInst)) { - proof_ref pr(m); - qe(rInst, tmp, pr); - rInst = tmp; - get(r).set_relation(rInst); - } - SASSERT(is_ground(rInst)); - notR = m.mk_not(rInst); - qe.reduce_with_assumption(notR, srcInst, tmp); - SASSERT(is_ground(tmp)); - } - else { - // Simplify not R usng assumption Exists x . S. - expr_ref srcGround(srcInst, m); - app_ref_vector srcVars(m); - qe::hoist_exists(srcGround, srcVars); - SASSERT(is_ground(srcGround)); - notR = m.mk_not(rInst); - qe.reduce_with_assumption(srcGround, notR, tmp1); - tmp = m.mk_and(srcInst, tmp1); - SASSERT(!has_free_vars(tmp)); - TRACE("smt_relation", - tout << "elim_exists result:\n" << mk_ll_pp(tmp, m) << "\n";); - } - - SASSERT(!has_free_vars(tmp)); - get(r).simplify(tmp); - - get(src).mk_abstract(tmp, tmp1); - TRACE("smt_relation", tout << "abstracted:\n"; tout << mk_ll_pp(tmp1, m) << "\n";); - get(*delta).set_relation(tmp1); - get(r).add_relation(tmp1); - } - else { - get(r).add_relation(srcE); - } - TRACE("smt_relation", get(r).display(tout << "dst':\n");); - } - }; - - relation_union_fn * smt_relation_plugin::mk_union_fn(const relation_base & tgt, const relation_base & src, - const relation_base * delta) { - if (!check_kind(tgt) || !check_kind(src) || (delta && !check_kind(*delta))) { - return 0; - } - return alloc(union_fn, *this); - } - - relation_union_fn * smt_relation_plugin::mk_widen_fn(const relation_base & tgt, const relation_base & src, - const relation_base * delta) { - if (!check_kind(tgt) || !check_kind(src) || (delta && !check_kind(*delta))) { - return 0; - } - return alloc(union_fn, *this); - } - - class smt_relation_plugin::filter_interpreted_fn : public relation_mutator_fn { - smt_relation_plugin& m_plugin; - app_ref m_condition; - public: - filter_interpreted_fn(smt_relation_plugin& p, app * condition) - : m_plugin(p), - m_condition(condition, p.get_ast_manager()) { - } - - virtual void operator()(relation_base & r) { - SASSERT(m_plugin.check_kind(r)); - get(r).filter_relation(m_condition); - TRACE("smt_relation", - tout << mk_pp(m_condition, m_plugin.get_ast_manager()) << "\n"; - get(r).display(tout); - ); - } - }; - - relation_mutator_fn * smt_relation_plugin::mk_filter_interpreted_fn(const relation_base & r, app * condition) { - if(!check_kind(r)) { - return 0; - } - return alloc(filter_interpreted_fn, *this, condition); - } - - relation_mutator_fn * smt_relation_plugin::mk_filter_equal_fn(const relation_base & r, - const relation_element & value, unsigned col) { - if(!check_kind(r)) { - return 0; - } - ast_manager& m = get_ast_manager(); - app_ref condition(m); - expr_ref var(m.mk_var(col, r.get_signature()[col]), m); - condition = m.mk_eq(var, value); - return mk_filter_interpreted_fn(r, condition); - } - - class smt_relation_plugin::filter_identical_fn : public relation_mutator_fn { - smt_relation_plugin& m_plugin; - expr_ref m_condition; - public: - filter_identical_fn(smt_relation_plugin& p, const relation_signature & sig, unsigned col_cnt, const unsigned * identical_cols) - : m_plugin(p), - m_condition(p.get_ast_manager()) { - if (col_cnt <= 1) { - return; - } - ast_manager& m = p.get_ast_manager(); - unsigned col = identical_cols[0]; - expr_ref v0(m.mk_var(col, sig[col]), m); - expr_ref_vector eqs(m); - for (unsigned i = 1; i < col_cnt; ++i) { - col = identical_cols[i]; - eqs.push_back(m.mk_eq(v0, m.mk_var(col, sig[col]))); - } - m_condition = m.mk_and(eqs.size(), eqs.c_ptr()); - } - - virtual void operator()(relation_base & r) { - get(r).filter_relation(m_condition); - TRACE("smt_relation", - tout << mk_pp(m_condition, m_plugin.get_ast_manager()) << "\n"; - get(r).display(tout); - ); - } - }; - - relation_mutator_fn * smt_relation_plugin::mk_filter_identical_fn(const relation_base & r, - unsigned col_cnt, const unsigned * identical_cols) { - if (!check_kind(r)) { - return 0; - } - return alloc(filter_identical_fn, *this, r.get_signature(), col_cnt, identical_cols); - } - - - class smt_relation_plugin::negation_filter_fn : public convenient_relation_negation_filter_fn { - smt_relation_plugin& m_plugin; - expr_ref_vector m_conjs; - public: - negation_filter_fn(smt_relation_plugin& p, - const relation_base & tgt, const relation_base & neg_t, - unsigned joined_col_cnt, const unsigned * t_cols, const unsigned * negated_cols) : - convenient_negation_filter_fn(tgt, neg_t, joined_col_cnt, t_cols, negated_cols), - m_plugin(p), - m_conjs(p.get_ast_manager()) { - ast_manager& m = p.get_ast_manager(); - unsigned sz = m_cols1.size(); - for (unsigned i = 0; i < sz; ++i) { - unsigned col1 = m_cols1[i]; - unsigned col2 = m_cols2[i]; - var* v1 = m.mk_var(col1, tgt.get_signature()[col1]); - var* v2 = m.mk_var(col2, neg_t.get_signature()[col2]); - m_conjs.push_back(m.mk_eq(v1, v2)); - } - } - - void operator()(relation_base & t, const relation_base & negated_obj) { - // TBD: fixme. - NOT_IMPLEMENTED_YET(); - ast_manager& m = m_plugin.get_ast_manager(); - expr_ref res(m), e2(m); - shift_vars sh(m); - sh(get(negated_obj).get_relation(), t.get_signature().size(), e2); - m_conjs.push_back(get(t).get_relation()); - m_conjs.push_back(m.mk_not(e2)); - res = m.mk_and(m_conjs.size(), m_conjs.c_ptr()); - m_conjs.pop_back(); - m_conjs.pop_back(); - // TBD: free variables in negation? - } - }; - - relation_intersection_filter_fn * smt_relation_plugin::mk_filter_by_negation_fn(const relation_base & t, - const relation_base & negated_obj, unsigned joined_col_cnt, - const unsigned * t_cols, const unsigned * negated_cols) { - if (!check_kind(t) || !check_kind(negated_obj)) { - return 0; - } - return alloc(negation_filter_fn, *this, t, negated_obj, joined_col_cnt, t_cols, negated_cols); - } - - - smt_relation& smt_relation_plugin::get(relation_base& r) { return dynamic_cast(r); } - - smt_relation const & smt_relation_plugin::get(relation_base const& r) { return dynamic_cast(r); } - - bool smt_relation_plugin::can_handle_signature(relation_signature const& sig) { - // TBD: refine according to theories handled by quantifier elimination - return get_manager().is_non_explanation(sig); - } - - // TBD: when relations are finite domain, they also support table iterators. - - symbol smt_relation_plugin::fresh_name() { - return symbol(m_counter++); - } - - smt_params& smt_relation_plugin::get_fparams() { - return const_cast(get_manager().get_context().get_fparams()); - } - - params_ref const& smt_relation_plugin::get_params() { - return get_manager().get_context().get_params(); - } - - bool smt_relation_plugin::is_finite_domain(sort *s) const { - ast_manager& m = get_ast_manager(); - if (m.is_bool(s)) { - return true; - } - bv_util bv(m); - if (bv.is_bv_sort(s)) { - return true; - } - datatype_util dt(m); - if (dt.is_datatype(s) && !dt.is_recursive(s)) { - ptr_vector const& constrs = *dt.get_datatype_constructors(s); - for (unsigned i = 0; i < constrs.size(); ++i) { - func_decl* f = constrs[i]; - for (unsigned j = 0; j < f->get_arity(); ++j) { - if (!is_finite_domain(f->get_domain(j))) { - return false; - } - } - } - return true; - } - return false; - } -}; - diff --git a/src/muz_qe/dl_smt_relation.h b/src/muz_qe/dl_smt_relation.h deleted file mode 100644 index a1bab918f..000000000 --- a/src/muz_qe/dl_smt_relation.h +++ /dev/null @@ -1,141 +0,0 @@ -/*++ -Copyright (c) 2010 Microsoft Corporation - -Module Name: - - dl_smt_relation.h - -Abstract: - - Relation signature represented by signatures that have quantifier elimination. - -Author: - - Nikolaj Bjorner (nbjorner) 2010-10-10 - -Revision History: - ---*/ -#ifndef _DL_SMT_RELATION_H_ -#define _DL_SMT_RELATION_H_ - -#include "dl_base.h" -#include "smt_params.h" -#include "params.h" - -namespace datalog { - - class smt_relation; - - class smt_relation_plugin : public relation_plugin { - - unsigned m_counter; - - friend class smt_relation; - class join_fn; - class project_fn; - class rename_fn; - class union_fn; - class filter_identical_fn; - class filter_interpreted_fn; - class negation_filter_fn; - - public: - smt_relation_plugin(relation_manager & m); - - virtual bool can_handle_signature(const relation_signature & s); - - static symbol get_name() { return symbol("smt_relation"); } - - virtual relation_base * mk_empty(const relation_signature & s); - - virtual relation_join_fn * mk_join_fn(const relation_base & t1, const relation_base & t2, - unsigned col_cnt, const unsigned * cols1, const unsigned * cols2); - virtual relation_transformer_fn * mk_project_fn(const relation_base & t, unsigned col_cnt, - const unsigned * removed_cols); - virtual relation_transformer_fn * mk_rename_fn(const relation_base & t, unsigned permutation_cycle_len, - const unsigned * permutation_cycle); - virtual relation_union_fn * mk_union_fn(const relation_base & tgt, const relation_base & src, - const relation_base * delta); - virtual relation_union_fn * mk_widen_fn(const relation_base & tgt, const relation_base & src, - const relation_base * delta); - virtual relation_mutator_fn * mk_filter_identical_fn(const relation_base & t, unsigned col_cnt, - const unsigned * identical_cols); - virtual relation_mutator_fn * mk_filter_equal_fn(const relation_base & t, const relation_element & value, - unsigned col); - virtual relation_mutator_fn * mk_filter_interpreted_fn(const relation_base & t, app * condition); - virtual relation_intersection_filter_fn * mk_filter_by_negation_fn(const relation_base & t, - const relation_base & negated_obj, unsigned joined_col_cnt, - const unsigned * t_cols, const unsigned * negated_cols); - - symbol fresh_name(); - - smt_params& get_fparams(); - - params_ref const& get_params(); - - bool is_finite_domain(sort* s) const; - - private: - static smt_relation& get(relation_base& r); - - static smt_relation const & get(relation_base const& r); - }; - - class smt_relation : public relation_base { - friend class smt_relation_plugin; - friend class smt_relation_plugin::join_fn; - friend class smt_relation_plugin::project_fn; - friend class smt_relation_plugin::rename_fn; - friend class smt_relation_plugin::union_fn; - friend class smt_relation_plugin::filter_identical_fn; - friend class smt_relation_plugin::filter_interpreted_fn; - friend class smt_relation_plugin::negation_filter_fn; - - expr_ref m_rel; // relation. - expr_ref_vector m_bound_vars; - - unsigned size() const { return get_signature().size(); } - - ast_manager& get_manager() const { return get_plugin().get_ast_manager(); } - - smt_relation(smt_relation_plugin & p, const relation_signature & s, expr* r); - - virtual ~smt_relation(); - - void instantiate(expr* e, expr_ref& result) const; - - void mk_abstract(expr* e, expr_ref& result) const; - - bool contains(expr* facts); - - bool is_finite_domain() const; - - bool is_well_formed() const; - - void display_finite(std::ostream & out) const; - - void simplify(expr_ref& e) const; - - public: - - virtual bool empty() const; - - virtual void add_fact(const relation_fact & f); - - virtual bool contains_fact(const relation_fact & f) const; - virtual smt_relation * clone() const; - virtual smt_relation * complement(func_decl*) const; - virtual void display(std::ostream & out) const; - virtual void to_formula(expr_ref& fml) const { fml = get_relation(); simplify(fml); } - - expr* get_relation() const; - void set_relation(expr* r); - void add_relation(expr* s); // add s to relation. - void filter_relation(expr* s); // restrict relation with s - smt_relation_plugin& get_plugin() const; - - }; -}; - -#endif diff --git a/src/muz_qe/dl_util.h b/src/muz_qe/dl_util.h index 12ed004ef..d9e437ccc 100644 --- a/src/muz_qe/dl_util.h +++ b/src/muz_qe/dl_util.h @@ -26,6 +26,7 @@ Revision History: #include"horn_subsume_model_converter.h" #include"replace_proof_converter.h" #include"substitution.h" +#include"fixedpoint_params.hpp" namespace datalog { diff --git a/src/muz_qe/fixedpoint_params.pyg b/src/muz_qe/fixedpoint_params.pyg new file mode 100644 index 000000000..aa78dad3d --- /dev/null +++ b/src/muz_qe/fixedpoint_params.pyg @@ -0,0 +1,62 @@ +def_module_params('fixedpoint', + description='fixedpoint parameters', + export=True, + params=(('timeout', UINT, UINT_MAX, 'set timeout'), + ('engine', SYMBOL, 'auto-config', 'Select: auto-config, datalog, pdr, bmc'), + ('default_table', SYMBOL, 'sparse', 'default table implementation: sparse, hashtable, bitvector, interval'), + ('default_relation', SYMBOL, 'pentagon', 'default relation implementation: external_relation, pentagon'), + ('generate_explanations', BOOL, False, '(DATALOG) produce explanations for produced facts when using the datalog engine'), + ('use_map_names', BOOL, True, "(DATALOG) use names from map files when displaying tuples"), + ('bit_blast', BOOL, False, '(PDR) bit-blast bit-vectors'), + ('explanations_on_relation_level', BOOL, False, '(DATALOG) if true, explanations are generated as history of each relation, rather than per fact (generate_explanations must be set to true for this option to have any effect)'), + ('magic_sets_for_queries', BOOL, False, "(DATALOG) magic set transformation will be used for queries"), + ('unbound_compressor', BOOL, True, "auxiliary relations will be introduced to avoid unbound variables in rule heads"), + ('similarity_compressor', BOOL, True, "(DATALOG) rules that differ only in values of constants will be merged into a single rule"), + ('similarity_compressor_threshold', UINT, 11, "(DATALOG) if similarity_compressor is on, this value determines how many similar rules there must be in order for them to be merged"), + ('all_or_nothing_deltas', BOOL, False, "(DATALOG) compile rules so that it is enough for the delta relation in union and widening operations to determine only whether the updated relation was modified or not"), + ('compile_with_widening', BOOL, False, "(DATALOG) widening will be used to compile recursive rules"), + ('eager_emptiness_checking', BOOL, True, "(DATALOG) emptiness of affected relations will be checked after each instruction, so that we may ommit unnecessary instructions"), + ('default_table_checked', BOOL, False, "if true, the detault table will be default_table inside a wrapper that checks that its results are the same as of default_table_checker table"), + ('default_table_checker', SYMBOL, 'null', "see default_table_checked"), + + + ('initial_restart_timeout', UINT, 0, "length of saturation run before the first restart (in ms), zero means no restarts"), + ('output_profile', BOOL, False, "determines whether profile informations should be output when outputting Datalog rules or instructions"), + ('inline_linear', BOOL, True, "try linear inlining method"), + ('inline_eager', BOOL, True, "try eager inlining of rules"), + ('inline_linear_branch', BOOL, False, "try linear inlining method with potential expansion"), + ('fix_unbound_vars', BOOL, False, "fix unbound variables in tail"), + ('output_tuples', BOOL, True, "determines whether tuples for output predicates should be output"), + ('print_with_fixedpoint_extensions', BOOL, True, "use SMT-LIB2 fixedpoint extensions, instead of pure SMT2, when printing rules"), + ('print_low_level_smt2', BOOL, False, "use (faster) low-level SMT2 printer (the printer is scalable but the result may not be as readable)"), + ('print_with_variable_declarations', BOOL, True, "use variable declarations when displaying rules (instead of attempting to use original names)"), + ('bfs_model_search', BOOL, True, "PDR: (default true) use BFS strategy for expanding model search"), + ('use_farkas', BOOL, True, "PDR: (default true) use lemma generator based on Farkas (for linear real arithmetic)"), + ('generate_proof_trace', BOOL, False, "PDR: (default false) trace for 'sat' answer as proof object"), + ('flexible_trace', BOOL, False, "PDR: (default false) allow PDR generate long counter-examples " + "by extending candidate trace within search area"), + ('unfold_rules', UINT, 0, "PDR: (default 0) unfold rules statically using iterative squarring"), + ('use_model_generalizer', BOOL, False, "PDR: (default false) use model for backwards propagation (instead of symbolic simulation)"), + ('validate_result', BOOL, False, "PDR (default false) validate result (by proof checking or model checking)"), + ('simplify_formulas_pre', BOOL, False, "PDR: (default false) simplify derived formulas before inductive propagation"), + ('simplify_formulas_post', BOOL, False, "PDR: (default false) simplify derived formulas after inductive propagation"), + ('slice', BOOL, True, "PDR: (default true) simplify clause set using slicing"), + ('coalesce_rules', BOOL, False, "BMC: (default false) coalesce rules"), + ('use_multicore_generalizer', BOOL, False, "PDR: (default false) extract multiple cores for blocking states"), + ('use_inductive_generalizer', BOOL, True, "PDR: (default true) generalize lemmas using induction strengthening"), + ('cache_mode', UINT, 0, "PDR: use no (0 - default) symbolic (1) or explicit cache (2) for model search"), + ('inductive_reachability_check', BOOL, False, "PDR: (default false) assume negation of the cube on the previous level when " + "checking for reachability (not only during cube weakening)"), + ('max_num_contexts', UINT, 500, "PDR: (default 500) maximal number of contexts to create"), + ('try_minimize_core', BOOL, False, "PDR: (default false) try to reduce core size (before inductive minimization)"), + ('profile_timeout_milliseconds', UINT, 0, "instructions and rules that took less than the threshold will not be printed when printed the instruction/rule list"), + ('dbg_fpr_nonempty_relation_signature', BOOL, False, + "if true, finite_product_relation will attempt to avoid creating inner relation with empty signature " + "by putting in half of the table columns, if it would have been empty otherwise"), + ('print_answer', BOOL, False, 'print answer instance(s) to query'), + ('print_certificate', BOOL, False, 'print certificate for reacahbility or non-reachability'), + ('print_statistics', BOOL, False, 'print statistics'), + )) + + + diff --git a/src/muz_qe/horn_tactic.cpp b/src/muz_qe/horn_tactic.cpp index 1dec1b4fe..98b6130b8 100644 --- a/src/muz_qe/horn_tactic.cpp +++ b/src/muz_qe/horn_tactic.cpp @@ -168,8 +168,8 @@ class horn_tactic : public tactic { bool produce_proofs = g->proofs_enabled(); if (produce_proofs) { - if (!m_ctx.get_params().get_bool("generate_proof_trace", true)) { - params_ref params = m_ctx.get_params(); + if (!m_ctx.get_params().generate_proof_trace()) { + params_ref params = m_ctx.get_params().p; params.set_bool("generate_proof_trace", true); updt_params(params); } diff --git a/src/muz_qe/pdr_context.cpp b/src/muz_qe/pdr_context.cpp index 76b609720..974c9251e 100644 --- a/src/muz_qe/pdr_context.cpp +++ b/src/muz_qe/pdr_context.cpp @@ -1123,17 +1123,17 @@ namespace pdr { context::context( smt_params& fparams, - params_ref const& params, + fixedpoint_params const& params, ast_manager& m ) : m_fparams(fparams), m_params(params), m(m), m_context(0), - m_pm(m_fparams, m_params, m), + m_pm(m_fparams, params, m), m_query_pred(m), m_query(0), - m_search(m_params.get_bool("bfs_model_search", true)), + m_search(m_params.bfs_model_search()), m_last_result(l_undef), m_inductive_lvl(0), m_cancel(false) @@ -1358,7 +1358,7 @@ namespace pdr { }; void context::validate() { - if (!m_params.get_bool("validate_result", false)) { + if (!m_params.validate_result()) { return; } switch(m_last_result) { @@ -1449,34 +1449,26 @@ namespace pdr { void context::init_core_generalizers(datalog::rule_set& rules) { reset_core_generalizers(); classifier_proc classify(m, rules); - bool use_mc = m_params.get_bool("use_multicore_generalizer", false); + bool use_mc = m_params.use_multicore_generalizer(); if (use_mc) { m_core_generalizers.push_back(alloc(core_multi_generalizer, *this, 0)); } - if (m_params.get_bool("use_farkas", true) && !classify.is_bool()) { - if (m_params.get_bool("inline_proof_mode", true)) { - m.toggle_proof_mode(PGM_FINE); - m_fparams.m_proof_mode = PGM_FINE; - m_fparams.m_arith_bound_prop = BP_NONE; - m_fparams.m_arith_auto_config_simplex = true; - m_fparams.m_arith_propagate_eqs = false; - m_fparams.m_arith_eager_eq_axioms = false; - if (classify.is_dl()) { - m_fparams.m_arith_mode = AS_DIFF_LOGIC; - m_fparams.m_arith_expand_eqs = true; - } - } - else { - m_core_generalizers.push_back(alloc(core_farkas_generalizer, *this, m, m_fparams)); + if (m_params.use_farkas() && !classify.is_bool()) { + m.toggle_proof_mode(PGM_FINE); + m_fparams.m_proof_mode = PGM_FINE; + m_fparams.m_arith_bound_prop = BP_NONE; + m_fparams.m_arith_auto_config_simplex = true; + m_fparams.m_arith_propagate_eqs = false; + m_fparams.m_arith_eager_eq_axioms = false; + if (classify.is_dl()) { + m_fparams.m_arith_mode = AS_DIFF_LOGIC; + m_fparams.m_arith_expand_eqs = true; } } - if (!use_mc && m_params.get_bool("use_inductive_generalizer", true)) { + if (!use_mc && m_params.use_inductive_generalizer()) { m_core_generalizers.push_back(alloc(core_bool_inductive_generalizer, *this, 0)); } - if (m_params.get_bool("use_interpolants", false)) { - m_core_generalizers.push_back(alloc(core_interpolant_generalizer, *this)); - } - if (m_params.get_bool("inductive_reachability_check", false)) { + if (m_params.inductive_reachability_check()) { m_core_generalizers.push_back(alloc(core_induction_generalizer, *this)); } } @@ -1588,7 +1580,7 @@ namespace pdr { \brief Retrieve satisfying assignment with explanation. */ expr_ref context::mk_sat_answer() const { - if (m_params.get_bool("generate_proof_trace", false)) { + if (m_params.generate_proof_trace()) { proof_ref pr = get_proof(); return expr_ref(pr.get(), m); } @@ -1709,7 +1701,7 @@ namespace pdr { n.pt().add_property(ncore, uses_level?n.level():infty_level); } CASSERT("pdr",n.level() == 0 || check_invariant(n.level()-1)); - m_search.backtrack_level(!found_invariant && m_params.get_bool("flexible_trace", false), n); + m_search.backtrack_level(!found_invariant && m_params.flexible_trace(), n); break; } case l_undef: { @@ -1731,7 +1723,7 @@ namespace pdr { } void context::propagate(unsigned max_prop_lvl) { - if (m_params.get_bool("simplify_formulas_pre", false)) { + if (m_params.simplify_formulas_pre()) { simplify_formulas(); } for (unsigned lvl = 0; lvl <= max_prop_lvl; lvl++) { @@ -1750,7 +1742,7 @@ namespace pdr { throw inductive_exception(); } } - if (m_params.get_bool("simplify_formulas_post", false)) { + if (m_params.simplify_formulas_post()) { simplify_formulas(); } } @@ -1798,7 +1790,7 @@ namespace pdr { */ void context::create_children(model_node& n) { SASSERT(n.level() > 0); - bool use_model_generalizer = m_params.get_bool("use_model_generalizer", false); + bool use_model_generalizer = m_params.use_model_generalizer(); datalog::scoped_no_proof _sc(m); pred_transformer& pt = n.pt(); diff --git a/src/muz_qe/pdr_context.h b/src/muz_qe/pdr_context.h index f3dd6807e..7491327dd 100644 --- a/src/muz_qe/pdr_context.h +++ b/src/muz_qe/pdr_context.h @@ -30,6 +30,7 @@ Revision History: #include "pdr_prop_solver.h" #include "pdr_reachable_cache.h" + namespace datalog { class rule_set; class context; @@ -291,7 +292,7 @@ namespace pdr { }; smt_params& m_fparams; - params_ref const& m_params; + fixedpoint_params const& m_params; ast_manager& m; datalog::context* m_context; manager m_pm; @@ -349,13 +350,13 @@ namespace pdr { */ context( smt_params& fparams, - params_ref const& params, + fixedpoint_params const& params, ast_manager& m); ~context(); smt_params& get_fparams() const { return m_fparams; } - params_ref const& get_params() const { return m_params; } + fixedpoint_params const& get_params() const { return m_params; } ast_manager& get_manager() const { return m; } manager& get_pdr_manager() { return m_pm; } decl2rel const& get_pred_transformers() const { return m_rels; } diff --git a/src/muz_qe/pdr_dl_interface.cpp b/src/muz_qe/pdr_dl_interface.cpp index cee6cf747..663f634c4 100644 --- a/src/muz_qe/pdr_dl_interface.cpp +++ b/src/muz_qe/pdr_dl_interface.cpp @@ -108,13 +108,13 @@ lbool dl_interface::query(expr * query) { model_converter_ref mc = datalog::mk_skip_model_converter(); proof_converter_ref pc; - if (m_ctx.get_params().get_bool("generate_proof_trace", false)) { + if (m_ctx.get_params().generate_proof_trace()) { pc = datalog::mk_skip_proof_converter(); } m_ctx.set_output_predicate(query_pred); m_ctx.apply_default_transformation(mc, pc); - if (m_ctx.get_params().get_bool("slice", true)) { + if (m_ctx.get_params().slice()) { datalog::rule_transformer transformer(m_ctx); datalog::mk_slice* slice = alloc(datalog::mk_slice, m_ctx); transformer.register_plugin(slice); @@ -133,10 +133,10 @@ lbool dl_interface::query(expr * query) { } } - if (m_ctx.get_params().get_uint("unfold_rules",0) > 0) { - unsigned num_unfolds = m_ctx.get_params().get_uint("unfold_rules", 0); + if (m_ctx.get_params().unfold_rules() > 0) { + unsigned num_unfolds = m_ctx.get_params().unfold_rules(); datalog::rule_transformer transformer1(m_ctx), transformer2(m_ctx); - if (m_ctx.get_params().get_uint("coalesce_rules", false)) { + if (m_ctx.get_params().coalesce_rules()) { transformer1.register_plugin(alloc(datalog::mk_coalesce, m_ctx)); m_ctx.transform_rules(transformer1, mc, pc); } @@ -198,7 +198,7 @@ expr_ref dl_interface::get_cover_delta(int level, func_decl* pred_orig) { } void dl_interface::add_cover(int level, func_decl* pred, expr* property) { - if (m_ctx.get_params().get_bool("slice", true)) { + if (m_ctx.get_params().slice()) { throw default_exception("Covers are incompatible with slicing. Disable slicing before using covers"); } m_context->add_cover(level, pred, property); @@ -246,32 +246,3 @@ model_ref dl_interface::get_model() { proof_ref dl_interface::get_proof() { return m_context->get_proof(); } - -void dl_interface::collect_params(param_descrs& p) { - p.insert("bfs_model_search", CPK_BOOL, "PDR: (default true) use BFS strategy for expanding model search"); - p.insert("use_farkas", CPK_BOOL, "PDR: (default true) use lemma generator based on Farkas (for linear real arithmetic)"); - p.insert("generate_proof_trace", CPK_BOOL, "PDR: (default false) trace for 'sat' answer as proof object"); - p.insert("inline_proofs", CPK_BOOL, "PDR: (default true) run PDR with proof mode turned on and extract " - "Farkas coefficients directly (instead of creating a separate proof object when extracting coefficients)"); - p.insert("flexible_trace", CPK_BOOL, "PDR: (default false) allow PDR generate long counter-examples " - "by extending candidate trace within search area"); - p.insert("unfold_rules", CPK_UINT, "PDR: (default 0) unfold rules statically using iterative squarring"); - p.insert("use_model_generalizer", CPK_BOOL, "PDR: (default false) use model for backwards propagation (instead of symbolic simulation)"); - p.insert("validate_result", CPK_BOOL, "PDR (default false) validate result (by proof checking or model checking)"); -#ifndef _EXTERNAL_RELEASE - p.insert("use_multicore_generalizer", CPK_BOOL, "PDR: (default false) extract multiple cores for blocking states"); - p.insert("use_inductive_generalizer", CPK_BOOL, "PDR: (default true) generalize lemmas using induction strengthening"); - p.insert("use_interpolants", CPK_BOOL, "PDR: (default false) use iZ3 interpolation for lemma generation"); - p.insert("dump_interpolants", CPK_BOOL, "PDR: (default false) display interpolants"); - p.insert("cache_mode", CPK_UINT, "PDR: use no (0 - default) symbolic (1) or explicit cache (2) for model search"); - p.insert("inductive_reachability_check", CPK_BOOL, - "PDR: (default false) assume negation of the cube on the previous level when " - "checking for reachability (not only during cube weakening)"); - p.insert("max_num_contexts", CPK_UINT, "PDR: (default 500) maximal number of contexts to create"); - p.insert("try_minimize_core", CPK_BOOL, "PDR: (default false) try to reduce core size (before inductive minimization)"); -#endif - p.insert("simplify_formulas_pre", CPK_BOOL, "PDR: (default false) simplify derived formulas before inductive propagation"); - p.insert("simplify_formulas_post", CPK_BOOL, "PDR: (default false) simplify derived formulas after inductive propagation"); - p.insert("slice", CPK_BOOL, "PDR: (default true) simplify clause set using slicing"); - p.insert("coalesce_rules", CPK_BOOL, "BMC: (default false) coalesce rules"); -} diff --git a/src/muz_qe/pdr_dl_interface.h b/src/muz_qe/pdr_dl_interface.h index 61f56282e..c4844f892 100644 --- a/src/muz_qe/pdr_dl_interface.h +++ b/src/muz_qe/pdr_dl_interface.h @@ -66,8 +66,6 @@ namespace pdr { expr_ref get_cover_delta(int level, func_decl* pred); void add_cover(int level, func_decl* pred, expr* property); - - static void collect_params(param_descrs& p); void updt_params(); diff --git a/src/muz_qe/pdr_farkas_learner.cpp b/src/muz_qe/pdr_farkas_learner.cpp index 46de8f212..b3d0b4fd0 100644 --- a/src/muz_qe/pdr_farkas_learner.cpp +++ b/src/muz_qe/pdr_farkas_learner.cpp @@ -29,7 +29,6 @@ Revision History: #include "pdr_util.h" #include "pdr_farkas_learner.h" #include "th_rewriter.h" -#include "pdr_interpolant_provider.h" #include "ast_ll_pp.h" #include "arith_bounds_tactic.h" #include "proof_utils.h" diff --git a/src/muz_qe/pdr_generalizers.cpp b/src/muz_qe/pdr_generalizers.cpp index 31bb132c4..5a6ab4240 100644 --- a/src/muz_qe/pdr_generalizers.cpp +++ b/src/muz_qe/pdr_generalizers.cpp @@ -20,7 +20,6 @@ Revision History: #include "pdr_context.h" #include "pdr_farkas_learner.h" -#include "pdr_interpolant_provider.h" #include "pdr_generalizers.h" #include "expr_abstract.h" #include "var_subst.h" @@ -143,77 +142,6 @@ namespace pdr { } - /** - < F, phi, i + 1 > - / \ - < G, psi, i > < H, theta, i > - core - - Given: - 1. psi => core - 2. Gi => not core - 3. phi & psi & theta => F_{i+1} - - Then, by weakening 2: - Gi => (F_{i+1} => not (phi & core & theta)) - - Find interpolant I, such that - - Gi => I, I => (F_{i+1} => not (phi & core' & theta')) - - where core => core', theta => theta' - - This implementation checks if - - Gi => (F_{i+1} => not (phi & theta)) - - */ - void core_interpolant_generalizer::operator()(model_node& n, expr_ref_vector& core, bool& uses_level) { - if (!n.parent()) { - return; - } - manager& pm = n.pt().get_pdr_manager(); - ast_manager& m = n.pt().get_manager(); - model_node& p = *n.parent(); - - // find index of node into parent. - unsigned index = 0; - for (; index < p.children().size() && (&n != p.children()[index]); ++index); - SASSERT(index < p.children().size()); - - expr_ref G(m), F(m), r(m), B(m), I(m), cube(m); - expr_ref_vector fmls(m); - - F = p.pt().get_formulas(p.level(), true); - G = n.pt().get_formulas(n.level(), true); - pm.formula_n2o(index, false, G); - - // get formulas from siblings. - for (unsigned i = 0; i < p.children().size(); ++i) { - if (i != index) { - pm.formula_n2o(p.children()[i]->state(), r, i, true); - fmls.push_back(r); - } - } - fmls.push_back(F); - fmls.push_back(p.state()); - B = pm.mk_and(fmls); - - // when G & B is unsat, find I such that G => I, I => not B - lbool res = pm.get_interpolator().get_interpolant(G, B, I); - - TRACE("pdr", - tout << "Interpolating:\n" << mk_pp(G, m) << "\n" << mk_pp(B, m) << "\n"; - if (res == l_true) tout << mk_pp(I, m) << "\n"; else tout << "failed\n";); - - if(res == l_true) { - pm.formula_o2n(I, cube, index, true); - TRACE("pdr", tout << "After renaming: " << mk_pp(cube, m) << "\n";); - core.reset(); - datalog::flatten_and(cube, core); - uses_level = true; - } - } // @@ -463,7 +391,7 @@ namespace pdr { imp imp(m_ctx); ast_manager& m = core.get_manager(); expr_ref goal = imp.mk_induction_goal(p->pt(), p->level(), depth); - smt::kernel ctx(m, m_ctx.get_fparams(), m_ctx.get_params()); + smt::kernel ctx(m, m_ctx.get_fparams(), m_ctx.get_params().p); ctx.assert_expr(goal); lbool r = ctx.check(); TRACE("pdr", tout << r << "\n"; diff --git a/src/muz_qe/pdr_generalizers.h b/src/muz_qe/pdr_generalizers.h index 543e6d985..5f3393682 100644 --- a/src/muz_qe/pdr_generalizers.h +++ b/src/muz_qe/pdr_generalizers.h @@ -51,13 +51,6 @@ namespace pdr { virtual void operator()(model_node& n, expr_ref_vector const& core, bool uses_level, cores& new_cores); }; - class core_interpolant_generalizer : public core_generalizer { - public: - core_interpolant_generalizer(context& ctx): core_generalizer(ctx) {} - virtual ~core_interpolant_generalizer() {} - virtual void operator()(model_node& n, expr_ref_vector& core, bool& uses_level); - }; - class core_induction_generalizer : public core_generalizer { class imp; public: diff --git a/src/muz_qe/pdr_interpolant_provider.cpp b/src/muz_qe/pdr_interpolant_provider.cpp deleted file mode 100644 index 7c9afd74a..000000000 --- a/src/muz_qe/pdr_interpolant_provider.cpp +++ /dev/null @@ -1,381 +0,0 @@ -/*++ -Copyright (c) 2011 Microsoft Corporation - -Module Name: - - pdr_interpolant_provider.cpp - -Abstract: - - Interface for obtaining interpolants. - - This file is Windows specific. - -Author: - - Krystof Hoder (t-khoder) 2011-10-19. - -Revision History: - ---*/ - -//disables the warning on deprecation of fgets function -- didn't really find by what it should be replaced -#ifdef _WINDOWS -#pragma warning(disable: 4995) -#endif - -#include -#include "ast_smt_pp.h" -#include "cmd_context.h" -#include "for_each_expr.h" -#include "obj_hashtable.h" -#include "smt2parser.h" -#include "rewriter.h" -#include "rewriter_def.h" -#include "pdr_util.h" -#include "pdr_interpolant_provider.h" -#include "expr_context_simplifier.h" - -#ifdef _WINDOWS -#include -#include -#include -#include - -/** -Requirements for the use of this object: - -The directory where the expcutable is must contain also executable -PdrInterpolator.exe. - -This executable takes one argument with a file name that contains -two SMTLIB problem instances, each terminated by string "\n##next##\n". - -The output of the executable is given to the standard output and -is also terminated by the "\n##next##\n" string. - -If formulas in the two input problems are unsatisfiable, they problem -is printed at the output in the format -(assert FORM) - -If the formulas are satisfiable, "0" is output and if the result cannot -be determined, the output is "?". (Both are still followed by "\n##next##\n"). - -*/ -class interpolant_provider_impl : public interpolant_provider -{ - static std::string s_terminator_str; - static std::string s_satisfiable_str; - static std::string s_unknown_str; - - std::string m_exec_name; - params_ref const & m_params; - - /** - If non-empty, contains name of a temporary file that is used for passing the - interpolation problem to the interpolating engine. - */ - std::string m_tmp_file_name; - - simplifier m_simpl; - - PROCESS_INFORMATION m_pi; - STARTUPINFOA m_si; - HANDLE m_in_rd; - HANDLE m_out_rd; - HANDLE m_in_wr; - HANDLE m_out_wr; - - - class used_symbol_inserter { - typedef obj_hashtable func_decl_set; - typedef obj_hashtable sort_set; - - ast_manager& m; - cmd_context& m_cctx; - - func_decl_set m_funcs; - sort_set m_sorts; - - void handle_sort(sort * s) { - if(s->get_family_id()!=null_family_id || m_sorts.contains(s)) { - return; - } - m_sorts.insert(s); - NOT_IMPLEMENTED_YET(); - //we should insert it into the context somehow, but now not sure how and - //we don't deal with user defined sorts (yet)... - //m_cctx.insert(s); - } - void handle_func_decl(func_decl * fn) { - if(fn->get_family_id()!=null_family_id || m_funcs.contains(fn)) { - return; - } - m_funcs.insert(fn); - m_cctx.insert(fn); - } - - public: - - used_symbol_inserter(cmd_context& cctx) : m(cctx.m()), m_cctx(cctx) {} - - void operator()(var * n) { - handle_sort(n->get_sort()); - } - void operator()(app * n) { - if (is_uninterp(n)) { - handle_func_decl(n->get_decl()); - } - handle_sort(n->get_decl()->get_range()); - } - void operator()(quantifier * n) { - unsigned sz = n->get_num_decls(); - for(unsigned i=0; iget_decl_sort(i)); - } - } - }; - - class form_fixer_cfg : public default_rewriter_cfg - { - ast_manager& m; - public: - form_fixer_cfg(ast_manager& m) : m(m) {} - - br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, - proof_ref & result_pr) - { - if(m.is_or(f) && num==0) { - result = m.mk_false(); - return BR_DONE; - } - return BR_FAILED; - } - }; - - - std::string get_tmp_file_name(); - - std::string execute_interpolator(std::string input); - - void simplify_expr(expr* f, expr_ref& result); - void output_interpolant_problem(std::ostream& out, expr * f1, expr * f2); - -public: - - interpolant_provider_impl(ast_manager& m, params_ref const& params, std::string exec_name) - : interpolant_provider(m), - m_params(params), - m_exec_name(exec_name), - m_simpl(m) { - memset(&m_si, 0, sizeof(m_si)); - memset(&m_pi, 0, sizeof(m_pi)); - } - - ~interpolant_provider_impl(); - - - /** - If (f1 /\ f2) is unsatisfiable, return true and into res assign a formula - I such that f1 --> I, I --> ~f2, and the language if I is in the intersection - of languages of f1 and f2. - - If (f1 /\ f2) is satisfiable, return false. - */ - virtual lbool get_interpolant(expr * f1, expr * f2, expr_ref& res); -}; - -std::string interpolant_provider_impl::s_terminator_str = ";##next##"; -std::string interpolant_provider_impl::s_satisfiable_str = ";#sat#"; -std::string interpolant_provider_impl::s_unknown_str = ";#unknown#"; - -interpolant_provider_impl::~interpolant_provider_impl() { - if(m_tmp_file_name.size()!=0) { - DeleteFileA(m_tmp_file_name.c_str()); - } - CloseHandle(m_pi.hProcess); - CloseHandle(m_pi.hThread); - CloseHandle(m_in_rd); - CloseHandle(m_in_wr); - CloseHandle(m_out_rd); - CloseHandle(m_out_wr); -} - -void interpolant_provider_impl::simplify_expr(expr* f, expr_ref& result) { - expr_ref rwr_f(m); - form_fixer_cfg fixer(m); - rewriter_tpl rwr(m, false, fixer); - rwr(f, rwr_f); - proof_ref pr(m); - m_simpl(rwr_f, result, pr); -} - - -std::string interpolant_provider_impl::get_tmp_file_name() { - //return "c:\\test.txt"; - if(m_tmp_file_name.length()!=0) { - return m_tmp_file_name; - } - char path[MAX_PATH]; - if(GetTempPathA(256, path)==0) { - throw default_exception("cannot get temp directory"); - } - - std::stringstream name_prefix_builder; - - name_prefix_builder<<"pdr"<(input.size()), &wr, 0)) { - throw default_exception("Cold not write to pipe"); - } - - std::string result; - char line[256]; - while (true) { - memset(line, 0, sizeof(line)); - if (!ReadFile(m_out_rd, line, sizeof(line)-1, &rd, 0)) { - throw default_exception("Cold not write to pipe"); - } - result += line; - if (strstr(result.c_str(), s_terminator_str.c_str())) { - return result; - } - } -} - -lbool interpolant_provider_impl::get_interpolant(expr * f1, expr * f2, expr_ref& res) { - std::ostringstream prb; - output_interpolant_problem(prb, f1, f2); - std::string res_text = execute_interpolator(prb.str()); - if(strstr(res_text.c_str(), s_satisfiable_str.c_str())) { - return l_false; - } - if(strstr(res_text.c_str(), s_unknown_str.c_str())) { - return l_undef; - } - - cmd_context cctx(false, &m); - for_each_expr(used_symbol_inserter(cctx), f1); - - parse_smt2_commands(cctx, std::istringstream(res_text), false); - - ptr_vector::const_iterator ait = cctx.begin_assertions(); - ptr_vector::const_iterator aend = cctx.end_assertions(); - if(ait+1!=aend) { - throw default_exception("invalid interpolator output"); - } - res = *ait; - if (m_params.get_bool("dump_interpolants", false)) { - interpolant_provider::output_interpolant(m, f1, f2, res); - } - return l_true; -} - -interpolant_provider * interpolant_provider::mk(ast_manager& m, params_ref const& p) -{ - char self_name[MAX_PATH]; - GetModuleFileNameA(NULL, self_name, MAX_PATH); - char * last_backslash = strrchr(self_name,'\\'); - if(last_backslash==NULL) { - throw default_exception("GetModuleFileNameA did not return full path to the executable"); - } - //we cut the string at the last backslash - *last_backslash = 0; - - std::string exec_name = self_name + std::string(".\\PdrInterpolator.exe"); - - return alloc(interpolant_provider_impl, m, p, exec_name); -} - -#else - -interpolant_provider * -interpolant_provider::mk(ast_manager& m, params_ref const& p) { - // interpolations are windows specific and private. - return 0; -} - - -#endif - - -void interpolant_provider::output_interpolant(ast_manager& m, expr* A, expr* B, expr* I) { - static unsigned file_num = 0; - - std::ostringstream filename; - filename << "interpolation_" << file_num++ << ".smt"; - std::ofstream out(filename.str().c_str()); - - ast_smt_pp pp(m); - pp.add_assumption(A); - pp.display(out, B); - std::ostringstream strm; - strm << ";" << mk_pp(I, m) << "\n"; - - buffer buff; - std::string s = strm.str(); - char const* i_str = s.c_str(); - while (*i_str) { - buff.push_back(*i_str); - if (*i_str == '\n') { - buff.push_back(';'); - } - ++i_str; - } - buff.push_back(0); - out << buff.c_ptr(); - out << "##next##\n"; - out.close(); -} diff --git a/src/muz_qe/pdr_interpolant_provider.h b/src/muz_qe/pdr_interpolant_provider.h deleted file mode 100644 index 84197a265..000000000 --- a/src/muz_qe/pdr_interpolant_provider.h +++ /dev/null @@ -1,54 +0,0 @@ -/*++ -Copyright (c) 2011 Microsoft Corporation - -Module Name: - - interpolant_provider.h - -Abstract: - - Interface for obtaining interpolants. - -Author: - - Krystof Hoder (t-khoder) 2011-10-19. - -Revision History: - ---*/ - -#include "ast.h" -#include "lbool.h" -#include "model.h" -#include "params.h" - -#ifndef _PDR_INTERPOLANT_PROVIDER_H_ -#define _PDR_INTERPOLANT_PROVIDER_H_ - -class interpolant_provider -{ -protected: - ast_manager & m; - - interpolant_provider(ast_manager& m) : m(m) {} - -public: - - virtual ~interpolant_provider() {} - - /** - If (f1 /\ f2) is unsatisfiable, return true and into res assign a formula - I such that f1 --> I, I --> ~f2, and the language if I is in the intersection - of languages of f1 and f2. - - If (f1 /\ f2) is satisfiable, return false. - */ - virtual lbool get_interpolant(expr * f1, expr * f2, expr_ref& res) = 0; - - static interpolant_provider * mk(ast_manager& m, params_ref const& p); - - static void output_interpolant(ast_manager& m, expr* A, expr* B, expr* I); -}; - - -#endif diff --git a/src/muz_qe/pdr_manager.cpp b/src/muz_qe/pdr_manager.cpp index 598d8c850..04facc776 100644 --- a/src/muz_qe/pdr_manager.cpp +++ b/src/muz_qe/pdr_manager.cpp @@ -166,7 +166,7 @@ namespace pdr { return res; } - manager::manager(smt_params& fparams, params_ref const& params, ast_manager& manager) : + manager::manager(smt_params& fparams, fixedpoint_params const& params, ast_manager& manager) : m(manager), m_fparams(fparams), m_params(params), @@ -311,17 +311,8 @@ namespace pdr { else { return false; } - } - - - interpolant_provider& manager::get_interpolator() { - if(!m_interpolator) { - m_interpolator = interpolant_provider::mk(m, get_params()); - } - return *m_interpolator; - } - - + } + bool manager::implication_surely_holds(expr * lhs, expr * rhs, expr * bg) { smt::kernel sctx(m, get_fparams()); if(bg) { diff --git a/src/muz_qe/pdr_manager.h b/src/muz_qe/pdr_manager.h index 58b4ffc53..cb2c9b253 100644 --- a/src/muz_qe/pdr_manager.h +++ b/src/muz_qe/pdr_manager.h @@ -32,7 +32,6 @@ Revision History: #include "pdr_util.h" #include "pdr_sym_mux.h" #include "pdr_farkas_learner.h" -#include "pdr_interpolant_provider.h" #include "pdr_smt_context_manager.h" #include "dl_rule.h" @@ -79,7 +78,7 @@ namespace pdr { { ast_manager& m; smt_params& m_fparams; - params_ref const& m_params; + fixedpoint_params const& m_params; mutable bool_rewriter m_brwr; @@ -91,16 +90,6 @@ namespace pdr { /** whenever we need an unique number, we get this one and increase */ unsigned m_next_unique_num; - /** - It would make more sense to have interpolantor inside the prop_solver, - however we have one prop_solver instance in each relation. - Each instance of interpolant_provider creates a temporary file and - interpolant_provider can be shared, so it makes more sence to have - it in pdr_manager which is created only once. - */ - - scoped_ptr m_interpolator; - static vector get_state_suffixes(); @@ -110,12 +99,12 @@ namespace pdr { void add_new_state(func_decl * s); public: - manager(smt_params& fparams, params_ref const& params, + manager(smt_params& fparams, fixedpoint_params const& params, ast_manager & manager); ast_manager& get_manager() const { return m; } smt_params& get_fparams() const { return m_fparams; } - params_ref const& get_params() const { return m_params; } + fixedpoint_params const& get_params() const { return m_params; } bool_rewriter& get_brwr() const { return m_brwr; } expr_ref mk_and(unsigned sz, expr* const* exprs); @@ -298,7 +287,6 @@ namespace pdr { expr* get_background() const { return m_background; } - interpolant_provider& get_interpolator(); /** Return true if we can show that lhs => rhs. The function can have false negatives diff --git a/src/muz_qe/pdr_prop_solver.cpp b/src/muz_qe/pdr_prop_solver.cpp index 5d0bd4e28..43d75b7bf 100644 --- a/src/muz_qe/pdr_prop_solver.cpp +++ b/src/muz_qe/pdr_prop_solver.cpp @@ -212,7 +212,7 @@ namespace pdr { m(pm.get_manager()), m_pm(pm), m_name(name), - m_try_minimize_core(pm.get_params().get_bool("try_minimize_core", false)), + m_try_minimize_core(pm.get_params().try_minimize_core()), m_ctx(pm.mk_fresh()), m_pos_level_atoms(m), m_neg_level_atoms(m), diff --git a/src/muz_qe/pdr_reachable_cache.cpp b/src/muz_qe/pdr_reachable_cache.cpp index f248f4d86..4f4f620de 100644 --- a/src/muz_qe/pdr_reachable_cache.cpp +++ b/src/muz_qe/pdr_reachable_cache.cpp @@ -21,13 +21,13 @@ Revision History: namespace pdr { - reachable_cache::reachable_cache(pdr::manager & pm, params_ref const& params) + reachable_cache::reachable_cache(pdr::manager & pm, fixedpoint_params const& params) : m(pm.get_manager()), m_pm(pm), m_ctx(0), m_ref_holder(m), m_disj_connector(m), - m_cache_mode((datalog::PDR_CACHE_MODE)params.get_uint("cache_mode",0)) { + m_cache_mode((datalog::PDR_CACHE_MODE)params.cache_mode()) { if (m_cache_mode == datalog::CONSTRAINT_CACHE) { m_ctx = pm.mk_fresh(); m_ctx->assert_expr(m_pm.get_background()); diff --git a/src/muz_qe/pdr_reachable_cache.h b/src/muz_qe/pdr_reachable_cache.h index d8096f15c..48caa22a5 100644 --- a/src/muz_qe/pdr_reachable_cache.h +++ b/src/muz_qe/pdr_reachable_cache.h @@ -17,14 +17,13 @@ Revision History: --*/ -#include "ast.h" -#include "params.h" -#include "ref_vector.h" -#include "pdr_manager.h" -#include "pdr_smt_context_manager.h" #ifndef _REACHABLE_CACHE_H_ #define _REACHABLE_CACHE_H_ +#include "ast.h" +#include "ref_vector.h" +#include "pdr_manager.h" +#include "pdr_smt_context_manager.h" namespace pdr { class reachable_cache { @@ -48,7 +47,7 @@ namespace pdr { void add_disjuncted_formula(expr * f); public: - reachable_cache(pdr::manager & pm, params_ref const& params); + reachable_cache(pdr::manager & pm, fixedpoint_params const& params); void add_init(app * f) { add_disjuncted_formula(f); } diff --git a/src/muz_qe/pdr_smt_context_manager.cpp b/src/muz_qe/pdr_smt_context_manager.cpp index 704967686..ca308954c 100644 --- a/src/muz_qe/pdr_smt_context_manager.cpp +++ b/src/muz_qe/pdr_smt_context_manager.cpp @@ -93,10 +93,10 @@ namespace pdr { return m_context.get_proof(); } - smt_context_manager::smt_context_manager(smt_params& fp, params_ref const& p, ast_manager& m): + smt_context_manager::smt_context_manager(smt_params& fp, fixedpoint_params const& p, ast_manager& m): m_fparams(fp), m(m), - m_max_num_contexts(p.get_uint("max_num_contexts", 500)), + m_max_num_contexts(p.max_num_contexts()), m_num_contexts(0), m_predicate_list(m) { } diff --git a/src/muz_qe/pdr_smt_context_manager.h b/src/muz_qe/pdr_smt_context_manager.h index 342100ed0..7d6eebfbd 100644 --- a/src/muz_qe/pdr_smt_context_manager.h +++ b/src/muz_qe/pdr_smt_context_manager.h @@ -23,6 +23,7 @@ Revision History: #include "smt_kernel.h" #include "sat_solver.h" #include "func_decl_dependencies.h" +#include "dl_util.h" namespace pdr { @@ -96,7 +97,7 @@ namespace pdr { app_ref_vector m_predicate_list; func_decl_set m_predicate_set; public: - smt_context_manager(smt_params& fp, params_ref const& p, ast_manager& m); + smt_context_manager(smt_params& fp, fixedpoint_params const& p, ast_manager& m); ~smt_context_manager(); smt_context* mk_fresh(); void collect_statistics(statistics& st) const; diff --git a/src/shell/datalog_frontend.cpp b/src/shell/datalog_frontend.cpp index c4aab9111..1d001c349 100644 --- a/src/shell/datalog_frontend.cpp +++ b/src/shell/datalog_frontend.cpp @@ -26,12 +26,12 @@ Revision History: #undef max #endif #include"smt_params.h" -#include"datalog_parser.h" #include"arith_decl_plugin.h" #include"dl_compiler.h" -#include"dl_context.h" #include"dl_mk_filter_rules.h" #include"dl_finite_product_relation.h" +#include"dl_context.h" +#include"datalog_parser.h" #include"datalog_frontend.h" #include"timeout.h" @@ -71,7 +71,7 @@ static void display_statistics( code.process_all_costs(); { - params_ref p(ctx.get_params()); + params_ref p; p.set_bool("output_profile", true); p.set_uint("profile_milliseconds_threshold", 100); ctx.updt_params(p); @@ -250,7 +250,7 @@ unsigned read_datalog(char const * file) { TRACE("dl_compiler", ctx.display(tout); rules_code.display(ctx, tout);); - if (ctx.get_params().get_bool("output_tuples", true)) { + if (ctx.get_params().output_tuples()) { ctx.display_output_facts(std::cout); } diff --git a/src/test/dl_smt_relation.cpp b/src/test/dl_smt_relation.cpp deleted file mode 100644 index bae1784b0..000000000 --- a/src/test/dl_smt_relation.cpp +++ /dev/null @@ -1,234 +0,0 @@ -#include "dl_smt_relation.h" -#include "arith_decl_plugin.h" -#include "dl_context.h" -#include "z3.h" -#include "z3_private.h" -#include "reg_decl_plugins.h" - - -namespace datalog { - - void test_smt_relation_unit() { - ast_manager m; - reg_decl_plugins(m); - arith_util a(m); - sort* int_sort = a.mk_int(); - sort* real_sort = a.mk_real(); - smt_params params; - context ctx(m, params); - relation_manager & rm = ctx.get_rmanager(); - relation_signature sig1; - sig1.push_back(int_sort); - sig1.push_back(int_sort); - sig1.push_back(real_sort); - - smt_relation_plugin plugin(rm); - - scoped_rel r1 = plugin.mk_empty(sig1); - - // add_fact - relation_fact fact1(m); - fact1.push_back(a.mk_numeral(rational(1), true)); - fact1.push_back(a.mk_numeral(rational(2), true)); - fact1.push_back(a.mk_numeral(rational(3), false)); - - relation_fact fact2(m); - fact2.push_back(a.mk_numeral(rational(2), true)); - fact2.push_back(a.mk_numeral(rational(2), true)); - fact2.push_back(a.mk_numeral(rational(3), false)); - - r1->add_fact(fact1); - r1->display(std::cout << "r1: "); - - - // contains_fact - SASSERT(r1->contains_fact(fact1)); - SASSERT(!r1->contains_fact(fact2)); - - // empty - scoped_rel r2 = plugin.mk_empty(sig1); - SASSERT(!r1->empty()); - SASSERT(r2->empty()); - - // clone - scoped_rel r3 = r1->clone(); - - // complement? - r2->add_fact(fact2); - scoped_rel r4 = dynamic_cast(*r2).complement(0); - r4->display(std::cout << "complement r4: " ); - - // join - unsigned col_cnt = 2; - unsigned cols1[2] = {1, 2}; - unsigned cols2[2] = {0, 2}; - scoped_ptr joinfn = plugin.mk_join_fn(*r1, *r4, col_cnt, cols1, cols2); - scoped_rel r5 = (*joinfn)(*r1, *r4); - r5->display(std::cout<< "join r5: "); - - relation_fact fact3(m); - fact3.push_back(a.mk_numeral(rational(1), true)); - fact3.push_back(a.mk_numeral(rational(2), true)); - fact3.push_back(a.mk_numeral(rational(3), false)); - fact3.push_back(a.mk_numeral(rational(2), true)); - fact3.push_back(a.mk_numeral(rational(2), true)); - fact3.push_back(a.mk_numeral(rational(3), false)); - SASSERT(!r5->contains_fact(fact3)); - fact3[5] = a.mk_numeral(rational(4), false); - SASSERT(!r5->contains_fact(fact3)); - fact3[5] = a.mk_numeral(rational(3), false); - fact3[4] = a.mk_numeral(rational(3), true); - SASSERT(r5->contains_fact(fact3)); - - // project - unsigned removed_cols[2] = { 1, 4 }; - scoped_ptr projfn = plugin.mk_project_fn(*r5, col_cnt, removed_cols); - scoped_rel r6 = (*projfn)(*r5); - r6->display(std::cout<< "project r6: "); - - // rename - unsigned cycle[3] = { 0, 2, 4 }; - unsigned cycle_len = 3; - scoped_rel renamefn = plugin.mk_rename_fn(*r5, cycle_len, cycle); - scoped_rel r7 = (*renamefn)(*r5); - r7->display(std::cout << "rename r7: "); - - // union - // widen - relation_base* delta = 0; - scoped_ptr widenfn = plugin.mk_widen_fn(*r1, *r2, delta); - scoped_ptr unionfn = plugin.mk_union_fn(*r1, *r2, delta); - scoped_rel r8 = r1->clone(); - (*unionfn)(*r8,*r2,0); - r8->display(std::cout << "union r8: "); - - // filter_identical - unsigned identical_cols[2] = { 1, 3 }; - scoped_ptr filti = plugin.mk_filter_identical_fn(*r5, col_cnt, identical_cols); - scoped_rel r9 = r1->clone(); - (*filti)(*r9); - r9->display(std::cout << "filter identical r9: "); - - // filter_equal - app_ref value(m); - value = m.mk_const(symbol("x"), int_sort); - scoped_rel eqn = plugin.mk_filter_equal_fn(*r5, value.get(), 3); - scoped_rel r10 = r1->clone(); - (*eqn)(*r10); - r10->display(std::cout << "filter equal r10: "); - - - // filter_interpreted - app_ref cond(m); - cond = a.mk_lt(m.mk_var(3, int_sort), m.mk_var(4, int_sort)); - scoped_rel filtint = plugin.mk_filter_interpreted_fn(*r5, cond); - scoped_rel r11 = r5->clone(); - (*filtint)(*r11); - r11->display(std::cout << "filter interpreted r11: "); - - } - - void test_smt_relation_api() { - - enable_trace("smt_relation"); - enable_trace("smt_relation2"); - enable_trace("quant_elim"); - Z3_config cfg = Z3_mk_config(); - Z3_set_param_value(cfg, "DL_DEFAULT_RELATION", "smt_relation2"); - Z3_context ctx = Z3_mk_context(cfg); - Z3_fixedpoint dl = Z3_mk_fixedpoint(ctx); - Z3_fixedpoint_inc_ref(ctx,dl); - Z3_del_config(cfg); - - Z3_sort int_sort = Z3_mk_int_sort(ctx); - Z3_sort bool_sort = Z3_mk_bool_sort(ctx); - Z3_func_decl nil_decl, is_nil_decl; - Z3_func_decl cons_decl, is_cons_decl, head_decl, tail_decl; - - Z3_sort list = Z3_mk_list_sort( - ctx, - Z3_mk_string_symbol(ctx, "list"), - int_sort, - &nil_decl, - &is_nil_decl, - &cons_decl, - &is_cons_decl, - &head_decl, - &tail_decl); - - Z3_sort listint[2] = { list, int_sort }; - Z3_symbol p_sym = Z3_mk_string_symbol(ctx, "p"); - Z3_symbol q_sym = Z3_mk_string_symbol(ctx, "q"); - - - Z3_func_decl p = Z3_mk_func_decl(ctx, p_sym, 2, listint, bool_sort); - Z3_func_decl q = Z3_mk_func_decl(ctx, q_sym, 2, listint, bool_sort); - Z3_fixedpoint_register_relation(ctx, dl, p); - Z3_fixedpoint_register_relation(ctx, dl, q); - - - Z3_ast zero = Z3_mk_numeral(ctx, "0", int_sort); - Z3_ast one = Z3_mk_numeral(ctx, "1", int_sort); - Z3_ast two = Z3_mk_numeral(ctx, "2", int_sort); - Z3_ast x = Z3_mk_bound(ctx, 0, list); - Z3_ast y = Z3_mk_bound(ctx, 1, int_sort); - Z3_ast z = Z3_mk_bound(ctx, 2, list); - Z3_ast zero_x[2] = { zero, x }; - Z3_ast fx = Z3_mk_app(ctx, cons_decl, 2, zero_x); - Z3_ast zero_fx[2] = { zero, fx }; - Z3_ast ffx = Z3_mk_app(ctx, cons_decl, 2, zero_fx); - Z3_ast xy[2] = { x, y }; - Z3_ast zy[2] = { z, y }; - // Z3_ast ffxy[2] = { ffx, y }; - // Z3_ast fxy[2] = { fx, y }; - Z3_ast zero_nil[2] = { zero, Z3_mk_app(ctx, nil_decl, 0, 0) }; - Z3_ast f0 = Z3_mk_app(ctx, cons_decl, 2, zero_nil); - Z3_ast zero_f0[2] = { zero, f0 }; - Z3_ast f1 = Z3_mk_app(ctx, cons_decl, 2, zero_f0); - Z3_ast zero_f1[2] = { zero, f1 }; - Z3_ast f2 = Z3_mk_app(ctx, cons_decl, 2, zero_f1); - Z3_ast zero_f2[2] = { zero, f2 }; - Z3_ast f3 = Z3_mk_app(ctx, cons_decl, 2, zero_f2); - Z3_ast zero_f3[2] = { zero, f3 }; - Z3_ast f4 = Z3_mk_app(ctx, cons_decl, 2, zero_f3); - Z3_ast zero_f4[2] = { zero, f4 }; - Z3_ast f5 = Z3_mk_app(ctx, cons_decl, 2, zero_f4); - Z3_ast zero_z[2] = { zero, z }; - Z3_ast fz = Z3_mk_app(ctx, cons_decl, 2, zero_z); - - Z3_ast pxy = Z3_mk_app(ctx, p, 2, xy); - Z3_ast pzy = Z3_mk_app(ctx, p, 2, zy); - Z3_ast qxy = Z3_mk_app(ctx, q, 2, xy); - Z3_ast qzy = Z3_mk_app(ctx, q, 2, zy); - Z3_ast even_y = Z3_mk_eq(ctx, zero, Z3_mk_mod(ctx, y, two)); - Z3_ast odd_y = Z3_mk_eq(ctx, one, Z3_mk_mod(ctx, y, two)); - - - // p(x, y) :- odd(y), p(z,y), f(z) = x . // dead rule. - // q(x, y) :- p(f(f(x)), y). - // p(x, y) :- q(f(x), y) // x decreases - // p(x, y) :- even y, x = f^5(0) // initial condition. - - Z3_ast body1[3] = { pzy, Z3_mk_eq(ctx, fz, x), odd_y }; - Z3_ast body2[2] = { pzy, Z3_mk_eq(ctx, ffx, z) }; - Z3_ast body3[2] = { qzy, Z3_mk_eq(ctx, fx, z) }; - Z3_ast body4[2] = { even_y, Z3_mk_eq(ctx, x, f5) }; - Z3_fixedpoint_add_rule(ctx, dl, Z3_mk_implies(ctx, Z3_mk_and(ctx, 3, body1), pxy), 0); - Z3_fixedpoint_add_rule(ctx, dl, Z3_mk_implies(ctx, Z3_mk_and(ctx, 2, body2), qxy), 0); - Z3_fixedpoint_add_rule(ctx, dl, Z3_mk_implies(ctx, Z3_mk_and(ctx, 2, body3), pxy), 0); - Z3_fixedpoint_add_rule(ctx, dl, Z3_mk_implies(ctx, Z3_mk_and(ctx, 2, body4), pxy), 0); - - Z3_lbool r = Z3_fixedpoint_query(ctx, dl, pxy); - if (r != Z3_L_UNDEF) { - std::cout << Z3_ast_to_string(ctx, Z3_fixedpoint_get_answer(ctx, dl)) << "\n"; - } - - Z3_del_context(ctx); - - } -}; - -void tst_dl_smt_relation() { - datalog::test_smt_relation_api(); - datalog::test_smt_relation_unit(); -} diff --git a/src/test/main.cpp b/src/test/main.cpp index bee889ea2..13ade7714 100644 --- a/src/test/main.cpp +++ b/src/test/main.cpp @@ -166,7 +166,6 @@ int main(int argc, char ** argv) { TST(total_order); TST(dl_table); TST(dl_context); - TST(dl_smt_relation); TST(dl_query); TST(dl_util); TST(dl_product_relation);