From eb3fa254d84c48bbaa65c3d0802c90dac98d7eb1 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Mon, 3 Dec 2012 17:56:42 +0000 Subject: [PATCH 1/5] Java API: bugfix Signed-off-by: Christoph M. Wintersteiger --- src/api/java/AST.java | 38 +++++++++++++++++++++----------------- 1 file changed, 21 insertions(+), 17 deletions(-) diff --git a/src/api/java/AST.java b/src/api/java/AST.java index 418c43e9f..b7d048a1e 100644 --- a/src/api/java/AST.java +++ b/src/api/java/AST.java @@ -37,13 +37,15 @@ public class AST extends Z3Object **/ public boolean equals(Object o) { - AST casted = null; + AST casted = null; - try { - casted = AST.class.cast(o); - } catch (ClassCastException e) { - return false; - } + try + { + casted = AST.class.cast(o); + } catch (ClassCastException e) + { + return false; + } return this.NativeObject() == casted.NativeObject(); } @@ -60,18 +62,20 @@ public class AST extends Z3Object return 1; AST oAST = null; - try { - AST.class.cast(other); - } catch (ClassCastException e) { - return 1; - } + try + { + oAST = AST.class.cast(other); + } catch (ClassCastException e) + { + return 1; + } - if (Id() < oAST.Id()) - return -1; - else if (Id() > oAST.Id()) - return +1; - else - return 0; + if (Id() < oAST.Id()) + return -1; + else if (Id() > oAST.Id()) + return +1; + else + return 0; } /** From 5c11f394cd69f1502ffd496aa104c3b8d1dc1f6b Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 3 Dec 2012 11:01:33 -0800 Subject: [PATCH 2/5] 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); From 67183ea08a5694751d006c13f3d7bc2a70e9a385 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 3 Dec 2012 15:05:43 -0800 Subject: [PATCH 3/5] factor out relation context for datalog Signed-off-by: Nikolaj Bjorner --- src/api/api_datalog.cpp | 4 +- src/muz_qe/datalog_parser.cpp | 3 - src/muz_qe/dl_bmc_engine.cpp | 1 - src/muz_qe/dl_compiler.cpp | 8 +- src/muz_qe/dl_context.cpp | 482 +++---------------- src/muz_qe/dl_context.h | 66 +-- src/muz_qe/dl_costs.cpp | 2 +- src/muz_qe/dl_costs.h | 2 +- src/muz_qe/dl_instruction.cpp | 74 +-- src/muz_qe/dl_instruction.h | 18 +- src/muz_qe/dl_mk_explanations.cpp | 6 +- src/muz_qe/dl_mk_magic_sets.cpp | 2 +- src/muz_qe/dl_mk_partial_equiv.cpp | 2 +- src/muz_qe/dl_mk_rule_inliner.cpp | 2 +- src/muz_qe/dl_mk_similarity_compressor.cpp | 2 +- src/muz_qe/dl_mk_simple_joins.cpp | 9 +- src/muz_qe/dl_mk_subsumption_checker.cpp | 2 +- src/muz_qe/dl_mk_unbound_compressor.cpp | 2 +- src/muz_qe/dl_rule.cpp | 2 +- src/muz_qe/fixedpoint_params.pyg | 34 +- src/muz_qe/pdr_dl_interface.cpp | 1 - src/muz_qe/rel_context.cpp | 517 +++++++++++++++++++++ src/muz_qe/rel_context.h | 115 +++++ src/shell/datalog_frontend.cpp | 12 +- 24 files changed, 799 insertions(+), 569 deletions(-) create mode 100644 src/muz_qe/rel_context.cpp create mode 100644 src/muz_qe/rel_context.h diff --git a/src/api/api_datalog.cpp b/src/api/api_datalog.cpp index 9b7093d1e..28fe3ed33 100644 --- a/src/api/api_datalog.cpp +++ b/src/api/api_datalog.cpp @@ -48,7 +48,7 @@ namespace api { if (!m.has_plugin(name)) { m.register_plugin(name, alloc(datalog::dl_decl_plugin)); } - datalog::relation_manager& r = m_context.get_rmanager(); + datalog::relation_manager& r = m_context.get_rel_context().get_rmanager(); r.register_plugin(alloc(datalog::external_relation_plugin, *this, r)); } @@ -295,7 +295,7 @@ extern "C" { { scoped_timer timer(timeout, &eh); try { - r = to_fixedpoint_ref(d)->ctx().dl_query(num_relations, to_func_decls(relations)); + r = to_fixedpoint_ref(d)->ctx().rel_query(num_relations, to_func_decls(relations)); } catch (z3_exception& ex) { mk_c(c)->handle_exception(ex); diff --git a/src/muz_qe/datalog_parser.cpp b/src/muz_qe/datalog_parser.cpp index afda12858..cfe283410 100644 --- a/src/muz_qe/datalog_parser.cpp +++ b/src/muz_qe/datalog_parser.cpp @@ -1326,9 +1326,6 @@ private: throw default_exception("tuple file %s for undeclared predicate %s", m_current_file.c_str(), predicate_name.bare_str()); } - if(!m_context.can_add_table_fact(pred)) { - NOT_IMPLEMENTED_YET(); - } unsigned pred_arity = pred->get_arity(); sort * const * arg_sorts = pred->get_domain(); diff --git a/src/muz_qe/dl_bmc_engine.cpp b/src/muz_qe/dl_bmc_engine.cpp index dd35cc870..27161320e 100644 --- a/src/muz_qe/dl_bmc_engine.cpp +++ b/src/muz_qe/dl_bmc_engine.cpp @@ -57,7 +57,6 @@ namespace datalog { m_ctx.ensure_opened(); m_rules.reset(); - m_ctx.get_rmanager().reset_relations(); datalog::rule_manager& rule_manager = m_ctx.get_rule_manager(); datalog::rule_set old_rules(m_ctx.get_rules()); datalog::rule_ref_vector query_rules(rule_manager); diff --git a/src/muz_qe/dl_compiler.cpp b/src/muz_qe/dl_compiler.cpp index 99c7b86f5..d403b5b5c 100644 --- a/src/muz_qe/dl_compiler.cpp +++ b/src/muz_qe/dl_compiler.cpp @@ -42,7 +42,7 @@ namespace datalog { return; } relation_signature sig; - m_context.get_rmanager().from_predicate(pred, sig); + m_context.get_rel_context().get_rmanager().from_predicate(pred, sig); reg_idx reg = get_fresh_register(sig); e->get_data().m_value=reg; @@ -563,7 +563,7 @@ namespace datalog { } SASSERT(is_app(e)); relation_sort arg_sort; - m_context.get_rmanager().from_predicate(neg_pred, i, arg_sort); + m_context.get_rel_context().get_rmanager().from_predicate(neg_pred, i, arg_sort); reg_idx new_reg; make_add_constant_column(head_pred, filtered_res, arg_sort, to_app(e), new_reg, acc); @@ -1096,7 +1096,7 @@ namespace datalog { func_decl_set::iterator fdit = preds.begin(); func_decl_set::iterator fdend = preds.end(); for(; fdit!=fdend; ++fdit) { - if(!m_context.get_rmanager().is_saturated(*fdit)) { + if(!m_context.get_rel_context().get_rmanager().is_saturated(*fdit)) { return false; } } @@ -1181,7 +1181,7 @@ namespace datalog { acc.set_observer(0); - TRACE("dl", execution_code.display(m_context, tout);); + TRACE("dl", execution_code.display(m_context.get_rel_context(), tout);); } diff --git a/src/muz_qe/dl_context.cpp b/src/muz_qe/dl_context.cpp index 228dbc572..0f9f1d520 100644 --- a/src/muz_qe/dl_context.cpp +++ b/src/muz_qe/dl_context.cpp @@ -24,18 +24,12 @@ Revision History: #include"arith_decl_plugin.h" #include"bv_decl_plugin.h" #include"dl_table.h" -#include"dl_sparse_table.h" #include"dl_table_relation.h" -#include"dl_bound_relation.h" -#include"dl_interval_relation.h" -#include"dl_finite_product_relation.h" -#include"dl_product_relation.h" #include"dl_rule_transformer.h" #include"dl_mk_coi_filter.h" #include"dl_mk_explanations.h" #include"dl_mk_filter_rules.h" #include"dl_mk_interp_tail_simplifier.h" -#include"dl_mk_magic_sets.h" #include"dl_mk_rule_inliner.h" #include"dl_mk_simple_joins.h" #include"dl_mk_similarity_compressor.h" @@ -44,9 +38,6 @@ Revision History: #include"dl_compiler.h" #include"dl_instruction.h" #include"dl_context.h" -#ifndef _EXTERNAL_RELEASE -#include"dl_skip_table.h" -#endif #include"for_each_expr.h" #include"ast_smt_pp.h" #include"ast_smt2_pp.h" @@ -189,7 +180,6 @@ namespace datalog { virtual ~restore_rules() {} virtual void undo(context& ctx) { - ctx.reset_tables(); ctx.replace_rules(*m_old_rules); reset(); } @@ -209,7 +199,6 @@ namespace datalog { m_trail.push_scope(); m_trail.push(restore_rules(m_rule_set)); m_trail.push(restore_vec_size_trail(m_background)); - m_trail.push(restore_vec_size_trail(m_table_facts)); } void context::pop() { @@ -233,7 +222,6 @@ namespace datalog { m_decl_util(m), m_rewriter(m), m_var_subst(m), - m_rmanager(*this), m_rule_manager(*this), m_trail(*this), m_pinned(m), @@ -243,25 +231,11 @@ namespace datalog { m_background(m), m_closed(false), m_saturation_was_run(false), - m_last_result_relation(0), m_last_answer(m), m_engine(LAST_ENGINE), m_cancel(false) { //register plugins for builtin tables - get_rmanager().register_plugin(alloc(sparse_table_plugin, get_rmanager())); - get_rmanager().register_plugin(alloc(hashtable_table_plugin, get_rmanager())); - get_rmanager().register_plugin(alloc(bitvector_table_plugin, get_rmanager())); - get_rmanager().register_plugin(alloc(equivalence_table_plugin, get_rmanager())); - -#ifndef _EXTERNAL_RELEASE - get_rmanager().register_plugin(alloc(skip_table_plugin, get_rmanager())); -#endif - - //register plugins for builtin relations - - get_rmanager().register_plugin(alloc(bound_relation_plugin, get_rmanager())); - get_rmanager().register_plugin(alloc(interval_relation_plugin, get_rmanager())); } context::~context() { @@ -272,14 +246,12 @@ namespace datalog { m_trail.reset(); m_rule_set.reset(); m_argument_var_names.reset(); - m_output_preds.reset(); m_preds.reset(); m_preds_by_name.reset(); reset_dealloc_values(m_sorts); - if (m_last_result_relation) { - m_last_result_relation->deallocate(); - m_last_result_relation = 0; - } + m_pdr = 0; + m_bmc = 0; + m_rel = 0; } bool context::is_fact(app * head) const { @@ -455,59 +427,13 @@ namespace datalog { return e->get_data().m_value[arg_index]; } - relation_plugin & context::get_ordinary_relation_plugin(symbol relation_name) { - relation_plugin * plugin = get_rmanager().get_relation_plugin(relation_name); - if (!plugin) { - std::stringstream sstm; - sstm << "relation plugin " << relation_name << " does not exist"; - throw default_exception(sstm.str()); - } - if (plugin->is_product_relation()) { - throw default_exception("cannot request product relation directly"); - } - if (plugin->is_sieve_relation()) { - throw default_exception("cannot request sieve relation directly"); - } - if (plugin->is_finite_product_relation()) { - throw default_exception("cannot request finite product relation directly"); - } - return *plugin; - } void context::set_predicate_representation(func_decl * pred, unsigned relation_name_cnt, symbol const * relation_names) { - relation_manager & rmgr = get_rmanager(); - - family_id target_kind = null_family_id; - switch (relation_name_cnt) { - case 0: - return; - case 1: - target_kind = get_ordinary_relation_plugin(relation_names[0]).get_kind(); - break; - default: { - svector rel_kinds; // kinds of plugins that are not table plugins - family_id rel_kind; // the aggregate kind of non-table plugins - for (unsigned i = 0; i < relation_name_cnt; i++) { - relation_plugin & p = get_ordinary_relation_plugin(relation_names[i]); - rel_kinds.push_back(p.get_kind()); - } - if (rel_kinds.size() == 1) { - rel_kind = rel_kinds[0]; - } - else { - relation_signature rel_sig; - //rmgr.from_predicate(pred, rel_sig); - product_relation_plugin & prod_plugin = product_relation_plugin::get_plugin(rmgr); - rel_kind = prod_plugin.get_relation_kind(rel_sig, rel_kinds); - } - target_kind = rel_kind; - break; - } + if (relation_name_cnt > 0) { + ensure_rel(); + m_rel->set_predicate_representation(pred, relation_name_cnt, relation_names); } - - SASSERT(target_kind != null_family_id); - get_rmanager().set_predicate_kind(pred, target_kind); } func_decl * context::mk_fresh_head_predicate(symbol const & prefix, symbol const & suffix, @@ -517,19 +443,25 @@ namespace datalog { register_predicate(new_pred); - if (orig_pred) { - family_id target_kind = get_rmanager().get_requested_predicate_kind(orig_pred); - if (target_kind != null_family_id) { - get_rmanager().set_predicate_kind(new_pred, target_kind); - } + if (m_rel.get()) { + m_rel->inherit_predicate_kind(new_pred, orig_pred); } return new_pred; } void context::set_output_predicate(func_decl * pred) { - if (!m_output_preds.contains(pred)) { - m_output_preds.insert(pred); - } + ensure_rel(); + m_rel->set_output_predicate(pred); + } + + bool context::is_output_predicate(func_decl * pred) { + ensure_rel(); + return m_rel->is_output_predicate(pred); + } + + const decl_set & context::get_output_predicates() { + ensure_rel(); + return m_rel->get_output_predicates(); } void context::add_rule(expr* rl, symbol const& name) { @@ -562,7 +494,6 @@ namespace datalog { throw default_exception(strm.str()); } rule_ref r(rules[0].get(), rm); - get_rmanager().reset_saturated_marks(); rule_ref_vector const& rls = m_rule_set.get_rules(); rule* old_rule = 0; for (unsigned i = 0; i < rls.size(); ++i) { @@ -795,7 +726,6 @@ namespace datalog { } void context::add_rule(rule_ref& r) { - get_rmanager().reset_saturated_marks(); m_rule_set.add_rule(r); } @@ -809,12 +739,10 @@ namespace datalog { void context::add_fact(func_decl * pred, const relation_fact & fact) { if (get_engine() == DATALOG_ENGINE) { - get_rmanager().reset_saturated_marks(); - get_relation(pred).add_fact(fact); - m_table_facts.push_back(std::make_pair(pred, fact)); + ensure_rel(); + m_rel->add_fact(pred, fact); } else { - ast_manager& m = get_manager(); expr_ref rule(m.mk_app(pred, fact.size(), (expr*const*)fact.c_ptr()), m); add_rule(rule, symbol::null); } @@ -832,26 +760,18 @@ namespace datalog { add_fact(head->get_decl(), fact); } - bool context::can_add_table_fact(func_decl * pred) { - return get_relation(pred).from_table(); - } - void context::add_table_fact(func_decl * pred, const table_fact & fact) { - relation_base & rel0 = get_relation(pred); - if (get_engine() != DATALOG_ENGINE || - !can_add_table_fact(pred) || - !rel0.from_table()) { + if (get_engine() == DATALOG_ENGINE) { + ensure_rel(); + m_rel->add_fact(pred, fact); + } + else { relation_fact rfact(m); for (unsigned i = 0; i < fact.size(); ++i) { rfact.push_back(m_decl_util.mk_numeral(fact[i], pred->get_domain()[i])); } add_fact(pred, rfact); } - else { - get_rmanager().reset_saturated_marks(); - table_relation & rel = static_cast(rel0); - rel.add_table_fact(fact); - } } void context::add_table_fact(func_decl * pred, unsigned num_args, unsigned args[]) { @@ -968,117 +888,14 @@ namespace datalog { if (m_pdr.get()) m_pdr->updt_params(); } - void context::collect_predicates(decl_set & res) { - unsigned rule_cnt = m_rule_set.get_num_rules(); - for (unsigned rindex=0; rindexget_head()->get_decl()); - unsigned tail_len = r->get_uninterpreted_tail_size(); - for (unsigned tindex=0; tindexget_tail(tindex)->get_decl()); - } - } - decl_set::iterator oit = m_output_preds.begin(); - decl_set::iterator oend = m_output_preds.end(); - for (; oit!=oend; ++oit) { - res.insert(*oit); - } - get_rmanager().collect_predicates(res); + void context::collect_predicates(decl_set& res) { + ensure_rel(); + m_rel->collect_predicates(res); } - - void context::restrict_predicates( const decl_set & res ) { - set_intersection(m_output_preds, res); - get_rmanager().restrict_predicates(res); - } - - lbool context::dl_saturate() { - if (!m_closed) { - close(); - } - bool time_limit = soft_timeout()!=0; - unsigned remaining_time_limit = soft_timeout(); - unsigned restart_time = initial_restart_timeout(); - - rule_set original_rules(get_rules()); - decl_set original_predicates; - collect_predicates(original_predicates); - - instruction_block rules_code; - instruction_block termination_code; - execution_context ex_ctx(*this); - lbool result; - - TRACE("dl", display(tout);); - - while (true) { - model_converter_ref mc; // Ignored in Datalog mode - proof_converter_ref pc; // Ignored in Datalog mode - transform_rules(mc, pc); - compiler::compile(*this, get_rules(), rules_code, termination_code); - - TRACE("dl", rules_code.display(*this, tout); ); - - bool timeout_after_this_round = time_limit && (restart_time==0 || remaining_time_limit<=restart_time); - - if (time_limit || restart_time!=0) { - unsigned timeout = time_limit ? (restart_time!=0) ? - std::min(remaining_time_limit, restart_time) - : remaining_time_limit : restart_time; - ex_ctx.set_timelimit(timeout); - } - - bool early_termination = !rules_code.perform(ex_ctx); - ex_ctx.reset_timelimit(); - VERIFY( termination_code.perform(ex_ctx) ); - - rules_code.process_all_costs(); - - IF_VERBOSE(10, ex_ctx.report_big_relations(1000, verbose_stream());); - - if (!early_termination) { - m_last_status = OK; - result = l_true; - break; - } - - if (memory::above_high_watermark()) { - m_last_status = MEMOUT; - result = l_undef; - break; - } - if (timeout_after_this_round || m_cancel) { - m_last_status = TIMEOUT; - result = l_undef; - break; - } - SASSERT(restart_time!=0); - if (time_limit) { - SASSERT(remaining_time_limit>restart_time); - remaining_time_limit-=restart_time; - } - uint64 new_restart_time = static_cast(restart_time)*initial_restart_timeout(); - if (new_restart_time>UINT_MAX) { - restart_time=UINT_MAX; - } - else { - restart_time=static_cast(new_restart_time); - } - - rules_code.reset(); - termination_code.reset(); - ex_ctx.reset(); - reopen(); - restrict_predicates(original_predicates); - replace_rules(original_rules); - close(); - } - reopen(); - restrict_predicates(original_predicates); - replace_rules(original_rules); - close(); - TRACE("dl", ex_ctx.report_big_relations(100, tout);); - return result; + void context::restrict_predicates(decl_set const& res) { + ensure_rel(); + m_rel->restrict_predicates(res); } expr_ref context::get_background_assertion() { @@ -1101,6 +918,7 @@ namespace datalog { m_cancel = true; if (m_pdr.get()) m_pdr->cancel(); if (m_bmc.get()) m_bmc->cancel(); + if (m_rel.get()) m_rel->cancel(); } void context::cleanup() { @@ -1180,7 +998,7 @@ namespace datalog { switch(get_engine()) { case DATALOG_ENGINE: - return dl_query(query); + return rel_query(query); case PDR_ENGINE: case QPDR_ENGINE: return pdr_query(query); @@ -1189,18 +1007,14 @@ namespace datalog { return bmc_query(query); default: UNREACHABLE(); - return dl_query(query); + return rel_query(query); } } void context::new_query() { flush_add_rules(); - if (m_last_result_relation) { - m_last_result_relation->deallocate(); - m_last_result_relation = 0; - } m_last_status = OK; - m_last_answer = get_manager().mk_true(); + m_last_answer = 0; } model_ref context::get_model() { @@ -1233,7 +1047,6 @@ namespace datalog { lbool context::pdr_query(expr* query) { ensure_pdr(); - m_last_answer = 0; return m_pdr->query(query); } @@ -1245,218 +1058,25 @@ namespace datalog { lbool context::bmc_query(expr* query) { ensure_bmc(); - m_last_answer = 0; return m_bmc->query(query); } -#define BEGIN_QUERY() \ - rule_set original_rules(get_rules()); \ - decl_set original_preds; \ - collect_predicates(original_preds); \ - bool was_closed = m_closed; \ - if (m_closed) { \ - reopen(); \ - } \ - -#define END_QUERY() \ - reopen(); \ - replace_rules(original_rules); \ - restrict_predicates(original_preds); \ - \ - if (was_closed) { \ - close(); \ - } \ - - lbool context::dl_query(unsigned num_rels, func_decl * const* rels) { - BEGIN_QUERY(); - for (unsigned i = 0; i < num_rels; ++i) { - set_output_predicate(rels[i]); + void context::ensure_rel() { + if (!m_rel.get()) { + m_rel = alloc(rel_context, *this); } - close(); - reset_negated_tables(); - lbool res = dl_saturate(); + } - switch(res) { - case l_true: { - expr_ref_vector ans(m); - expr_ref e(m); - bool some_non_empty = num_rels == 0; - for (unsigned i = 0; i < num_rels; ++i) { - relation_base& rel = get_relation(rels[i]); - if (!rel.empty()) { - some_non_empty = true; - } - rel.to_formula(e); - ans.push_back(e); - } - SASSERT(!m_last_result_relation); - if (some_non_empty) { - m_last_answer = m.mk_and(ans.size(), ans.c_ptr()); - } - else { - m_last_answer = m.mk_false(); - res = l_false; - } - break; - } - case l_false: - m_last_answer = m.mk_false(); - break; - case l_undef: - break; - } - END_QUERY(); - return res; + lbool context::rel_query(unsigned num_rels, func_decl * const* rels) { + ensure_rel(); + return m_rel->query(num_rels, rels); } - lbool context::dl_query(expr* query) { - BEGIN_QUERY(); - rule_manager& rm = get_rule_manager(); - rule_ref qrule(rm); - rule_ref_vector qrules(rm); - func_decl_ref query_pred(get_manager()); - try { - rm.mk_query(query, query_pred, qrules, qrule); - } - catch(default_exception& exn) { - close(); - m_last_status = INPUT_ERROR; - throw exn; - } - try { - add_rules(qrules); - } - catch (default_exception& exn) { - close(); - m_last_status = INPUT_ERROR; - throw exn; - } - - set_output_predicate(qrule->get_head()->get_decl()); - close(); - reset_negated_tables(); - - if (generate_explanations()) { - model_converter_ref mc; // ignored in Datalog mode - proof_converter_ref pc; // ignored in Datalog mode - rule_transformer transformer(*this); - //expl_plugin is deallocated when transformer goes out of scope - mk_explanations * expl_plugin = - alloc(mk_explanations, *this, explanations_on_relation_level()); - transformer.register_plugin(expl_plugin); - transform_rules(transformer, mc, pc); - - //we will retrieve the predicate with explanations instead of the original query predicate - query_pred = expl_plugin->get_e_decl(query_pred); - const rule_vector & query_rules = get_rules().get_predicate_rules(query_pred); - SASSERT(query_rules.size()==1); - qrule = query_rules.back(); - } - - if (magic_sets_for_queries()) { - model_converter_ref mc; // Ignored in Datalog mode - proof_converter_ref pc; // Ignored in Datalog mode - rule_transformer transformer(*this); - transformer.register_plugin(alloc(mk_magic_sets, *this, qrule.get())); - transform_rules(transformer, mc, pc); - } - - lbool res = dl_saturate(); - - if (res != l_undef) { - m_last_result_relation = get_relation(query_pred).clone(); - if (m_last_result_relation->empty()) { - res = l_false; - m_last_answer = m.mk_false(); - } - else { - m_last_result_relation->to_formula(m_last_answer); - } - } - - END_QUERY(); - return res; + lbool context::rel_query(expr* query) { + ensure_rel(); + return m_rel->query(query); } - void context::reset_tables() { - get_rmanager().reset_saturated_marks(); - rule_set::decl2rules::iterator it = m_rule_set.begin_grouped_rules(); - rule_set::decl2rules::iterator end = m_rule_set.end_grouped_rules(); - for (; it != end; ++it) { - func_decl* p = it->m_key; - relation_base & rel = get_relation(p); - rel.reset(); - } - for (unsigned i = 0; i < m_table_facts.size(); ++i) { - func_decl* pred = m_table_facts[i].first; - relation_fact const& fact = m_table_facts[i].second; - get_relation(pred).add_fact(fact); - } - } - - void context::reset_negated_tables() { - rule_set::pred_set_vector const & pred_sets = m_rule_set.get_strats(); - bool non_empty = false; - for (unsigned i = 1; i < pred_sets.size(); ++i) { - func_decl_set::iterator it = pred_sets[i]->begin(), end = pred_sets[i]->end(); - for (; it != end; ++it) { - func_decl* pred = *it; - relation_base & rel = get_relation(pred); - if (!rel.empty()) { - non_empty = true; - break; - } - } - } - if (!non_empty) { - return; - } - // collect predicates that depend on negation. - func_decl_set depends_on_negation; - for (unsigned i = 1; i < pred_sets.size(); ++i) { - bool change = true; - while (change) { - change = false; - func_decl_set::iterator it = pred_sets[i]->begin(), end = pred_sets[i]->end(); - for (; it != end; ++it) { - func_decl* pred = *it; - if (depends_on_negation.contains(pred)) { - continue; - } - rule_vector const& rules = m_rule_set.get_predicate_rules(pred); - bool inserted = false; - for (unsigned j = 0; !inserted && j < rules.size(); ++j) { - rule* r = rules[j]; - unsigned psz = r->get_positive_tail_size(); - unsigned tsz = r->get_uninterpreted_tail_size(); - if (psz < tsz) { - depends_on_negation.insert(pred); - change = true; - inserted = true; - } - for (unsigned k = 0; !inserted && k < tsz; ++k) { - func_decl* tail_decl = r->get_tail(k)->get_decl(); - if (depends_on_negation.contains(tail_decl)) { - depends_on_negation.insert(pred); - change = true; - inserted = true; - } - } - } - } - } - } - func_decl_set::iterator it = depends_on_negation.begin(), end = depends_on_negation.end(); - for (; it != end; ++it) { - func_decl* pred = *it; - relation_base & rel = get_relation(pred); - - if (!rel.empty()) { - TRACE("dl", tout << "Resetting: " << mk_ismt2_pp(pred, m) << "\n";); - rel.reset(); - } - } - } expr* context::get_answer_as_formula() { if (m_last_answer) { @@ -1473,6 +1093,10 @@ namespace datalog { ensure_bmc(); m_last_answer = m_bmc->get_answer(); return m_last_answer.get(); + case DATALOG_ENGINE: + ensure_rel(); + m_last_answer = m_rel->get_last_answer(); + return m_last_answer.get(); default: UNREACHABLE(); } @@ -1533,8 +1157,8 @@ namespace datalog { execution_result context::get_status() { return m_last_status; } bool context::result_contains_fact(relation_fact const& f) { - SASSERT(m_last_result_relation); - return m_last_result_relation->contains_fact(f); + ensure_rel(); + return m_rel->result_contains_fact(f); } // TBD: algebraic data-types declarations will not be printed. diff --git a/src/muz_qe/dl_context.h b/src/muz_qe/dl_context.h index 5dcb3e1fa..89446ce3b 100644 --- a/src/muz_qe/dl_context.h +++ b/src/muz_qe/dl_context.h @@ -35,11 +35,11 @@ Revision History: #include"dl_rule_set.h" #include"pdr_dl_interface.h" #include"dl_bmc_engine.h" +#include"rel_context.h" #include"lbool.h" #include"statistics.h" #include"params.h" #include"trail.h" -#include"dl_external_relation.h" #include"model_converter.h" #include"proof_converter.h" #include"model2expr.h" @@ -75,7 +75,6 @@ namespace datalog { typedef map sym2decl; typedef obj_map > pred2syms; typedef obj_map sort_domain_map; - typedef vector > fact_vector; ast_manager & m; smt_params & m_fparams; @@ -84,7 +83,6 @@ namespace datalog { dl_decl_util m_decl_util; th_rewriter m_rewriter; var_subst m_var_subst; - relation_manager m_rmanager; rule_manager m_rule_manager; trail_stack m_trail; @@ -94,7 +92,6 @@ namespace datalog { func_decl_set m_preds; sym2decl m_preds_by_name; pred2syms m_argument_var_names; - decl_set m_output_preds; rule_set m_rule_set; expr_ref_vector m_rule_fmls; svector m_rule_names; @@ -102,23 +99,20 @@ namespace datalog { scoped_ptr m_pdr; scoped_ptr m_bmc; + scoped_ptr m_rel; bool m_closed; bool m_saturation_was_run; execution_result m_last_status; - relation_base * m_last_result_relation; expr_ref m_last_answer; DL_ENGINE m_engine; volatile bool m_cancel; - fact_vector m_table_facts; bool is_fact(app * head) const; bool has_sort_domain(relation_sort s) const; sort_domain & get_sort_domain(relation_sort s); const sort_domain & get_sort_domain(relation_sort s) const; - relation_plugin & get_ordinary_relation_plugin(symbol relation_name); - class engine_type_proc; @@ -130,25 +124,12 @@ namespace datalog { void push(); void pop(); - relation_base & get_relation(func_decl * pred) { return get_rmanager().get_relation(pred); } - relation_base * try_get_relation(func_decl * pred) const { return get_rmanager().try_get_relation(pred); } - bool saturation_was_run() const { return m_saturation_was_run; } void notify_saturation_was_run() { m_saturation_was_run = true; } - /** - \brief Store the relation \c rel under the predicate \c pred. The \c context object - takes over the ownership of the relation object. - */ - void store_relation(func_decl * pred, relation_base * rel) { - get_rmanager().store_relation(pred, rel); - } - void configure_engine(); ast_manager & get_manager() const { return m; } - relation_manager & get_rmanager() { return m_rmanager; } - 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; } fixedpoint_params const& get_params() const { return m_params; } @@ -247,8 +228,8 @@ namespace datalog { symbol const * relation_names); void set_output_predicate(func_decl * pred); - bool is_output_predicate(func_decl * pred) { return m_output_preds.contains(pred); } - const decl_set & get_output_predicates() const { return m_output_preds; } + bool is_output_predicate(func_decl * pred); + const decl_set & get_output_predicates(); rule_set const & get_rules() { flush_add_rules(); return m_rule_set; } @@ -314,7 +295,6 @@ namespace datalog { and there is no transformation of relation values before they are put into the table. */ - bool can_add_table_fact(func_decl * pred); void add_table_fact(func_decl * pred, const table_fact & fact); void add_table_fact(func_decl * pred, unsigned num_args, unsigned args[]); @@ -323,6 +303,7 @@ namespace datalog { */ void close(); void ensure_closed(); + bool is_closed() { return m_closed; } /** \brief Undo the effect of the \c close operation. @@ -351,13 +332,10 @@ namespace datalog { void display_rules(std::ostream & out) const { m_rule_set.display(out); } - void display_facts(std::ostream & out) const { - m_rmanager.display(out); - } void display(std::ostream & out) const { display_rules(out); - display_facts(out); + if (m_rel) m_rel->display_facts(out); } void display_smt2(unsigned num_queries, expr* const* queries, std::ostream& out); @@ -407,23 +385,16 @@ namespace datalog { /** Query multiple output relations. */ - lbool dl_query(unsigned num_rels, func_decl * const* rels); + lbool rel_query(unsigned num_rels, func_decl * const* rels); - /** - Reset tables that are under negation. - */ - void reset_negated_tables(); - - /** - Just reset all tables. - */ - void reset_tables(); /** \brief retrieve last proof status. */ execution_result get_status(); + void set_status(execution_result r) { m_last_status = r; } + /** \brief retrieve formula corresponding to query that returns l_true. The formula describes one or more instances of the existential variables @@ -446,29 +417,36 @@ namespace datalog { */ bool result_contains_fact(relation_fact const& f); +#if 0 /** \brief display facts generated for query. */ void display_output_facts(std::ostream & out) const { - m_rmanager.display_output_tables(out); + get_rel_context().get_rmanager().display_output_tables(out); } +#endif - /** - \brief expose datalog saturation for test. - */ - lbool dl_saturate(); + rel_context& get_rel_context() { ensure_rel(); return *m_rel; } private: + /** + Just reset all tables. + */ + void reset_tables(); + + void flush_add_rules(); void ensure_pdr(); void ensure_bmc(); + void ensure_rel(); + void new_query(); - lbool dl_query(expr* query); + lbool rel_query(expr* query); lbool pdr_query(expr* query); diff --git a/src/muz_qe/dl_costs.cpp b/src/muz_qe/dl_costs.cpp index 0b7641093..fe085d7f7 100644 --- a/src/muz_qe/dl_costs.cpp +++ b/src/muz_qe/dl_costs.cpp @@ -115,7 +115,7 @@ namespace datalog { } - void accounted_object::output_profile(context & ctx, std::ostream & out) const { + void accounted_object::output_profile(std::ostream & out) const { costs c; get_total_cost(c); c.output(out); diff --git a/src/muz_qe/dl_costs.h b/src/muz_qe/dl_costs.h index 0fc60451d..16cfc16b1 100644 --- a/src/muz_qe/dl_costs.h +++ b/src/muz_qe/dl_costs.h @@ -79,7 +79,7 @@ namespace datalog { void process_costs(); bool passes_output_thresholds(context & ctx) const; - void output_profile(context & ctx, std::ostream & out) const; + void output_profile(std::ostream & out) const; private: //private and undefined copy constructor and operator= to avoid the default ones diff --git a/src/muz_qe/dl_instruction.cpp b/src/muz_qe/dl_instruction.cpp index 9d6e9036f..503ffec3b 100644 --- a/src/muz_qe/dl_instruction.cpp +++ b/src/muz_qe/dl_instruction.cpp @@ -33,11 +33,11 @@ namespace datalog { // // ----------------------------------- - execution_context::execution_context(context & datalog_context) - : m_datalog_context(datalog_context), + execution_context::execution_context(context & context) + : m_context(context), m_stopwatch(0), m_timelimit_ms(0), - m_eager_emptiness_checking(datalog_context.eager_emptiness_checking()) {} + m_eager_emptiness_checking(context.eager_emptiness_checking()) {} execution_context::~execution_context() { reset(); @@ -135,12 +135,12 @@ namespace datalog { process_costs(); } - void instruction::display_indented(context & ctx, std::ostream & out, std::string indentation) const { + void instruction::display_indented(rel_context & ctx, std::ostream & out, std::string indentation) const { out << indentation; display_head_impl(ctx, out); if (ctx.output_profile()) { out << " {"; - output_profile(ctx, out); + output_profile(out); out << '}'; } out << "\n"; @@ -157,10 +157,10 @@ namespace datalog { virtual bool perform(execution_context & ctx) { if (m_store) { if (ctx.reg(m_reg)) { - ctx.get_datalog_context().store_relation(m_pred, ctx.release_reg(m_reg)); + ctx.get_rel_context().store_relation(m_pred, ctx.release_reg(m_reg)); } else { - context & dctx = ctx.get_datalog_context(); + rel_context & dctx = ctx.get_rel_context(); relation_base * empty_rel; //the object referenced by sig is valid only until we call dctx.store_relation() const relation_signature & sig = dctx.get_relation(m_pred).get_signature(); @@ -169,7 +169,7 @@ namespace datalog { } } else { - relation_base& rel = ctx.get_datalog_context().get_relation(m_pred); + relation_base& rel = ctx.get_rel_context().get_relation(m_pred); if ((!ctx.eager_emptiness_checking() || !rel.empty())) { ctx.set_reg(m_reg, rel.clone()); } @@ -182,7 +182,7 @@ namespace datalog { virtual void make_annotations(execution_context & ctx) { ctx.set_register_annotation(m_reg, m_pred->get_name().bare_str()); } - virtual void display_head_impl(context & ctx, std::ostream & out) const { + virtual void display_head_impl(rel_context & ctx, std::ostream & out) const { const char * rel_name = m_pred->get_name().bare_str(); if (m_store) { out << "store " << m_reg << " into " << rel_name; @@ -213,7 +213,7 @@ namespace datalog { virtual void make_annotations(execution_context & ctx) { ctx.set_register_annotation(m_reg, "alloc"); } - virtual void display_head_impl(context & ctx, std::ostream & out) const { + virtual void display_head_impl(rel_context & ctx, std::ostream & out) const { out << "dealloc " << m_reg; } }; @@ -248,7 +248,7 @@ namespace datalog { ctx.set_register_annotation(m_src, str); } } - virtual void display_head_impl(context & ctx, std::ostream & out) const { + virtual void display_head_impl(rel_context & ctx, std::ostream & out) const { out << (m_clone ? "clone " : "move ") << m_src << " into " << m_tgt; } }; @@ -304,11 +304,11 @@ namespace datalog { virtual void make_annotations(execution_context & ctx) { m_body->make_annotations(ctx); } - virtual void display_head_impl(context & ctx, std::ostream & out) const { + virtual void display_head_impl(rel_context & ctx, std::ostream & out) const { out << "while"; print_container(m_controls, out); } - virtual void display_body_impl(context & ctx, std::ostream & out, std::string indentation) const { + virtual void display_body_impl(rel_context & ctx, std::ostream & out, std::string indentation) const { m_body->display_indented(ctx, out, indentation+" "); } }; @@ -349,9 +349,9 @@ namespace datalog { } TRACE("dl", - r1.get_signature().output(ctx.get_datalog_context().get_manager(), tout); + r1.get_signature().output(ctx.get_rel_context().get_manager(), tout); tout<<":"<\n";); try { @@ -371,7 +371,7 @@ namespace datalog { } TRACE("dl", - ctx.reg(m_res)->get_signature().output(ctx.get_datalog_context().get_manager(), tout); + ctx.reg(m_res)->get_signature().output(ctx.get_rel_context().get_manager(), tout); tout<<":"<get_size_estimate_rows()<<"\n";); if (ctx.eager_emptiness_checking() && ctx.reg(m_res)->empty()) { @@ -385,7 +385,7 @@ namespace datalog { ctx.get_register_annotation(m_rel1, a1); ctx.set_register_annotation(m_res, "join " + a1 + " " + a2); } - virtual void display_head_impl(context & ctx, std::ostream & out) const { + virtual void display_head_impl(rel_context & ctx, std::ostream & out) const { out << "join " << m_rel1; print_container(m_cols1, out); out << " and " << m_rel2; @@ -431,10 +431,10 @@ namespace datalog { } virtual void make_annotations(execution_context & ctx) { std::stringstream a; - a << "filter_equal " << m_col << " val: " << ctx.get_datalog_context().get_rmanager().to_nice_string(m_value); + a << "filter_equal " << m_col << " val: " << ctx.get_rel_context().get_rmanager().to_nice_string(m_value); ctx.set_register_annotation(m_reg, a.str()); } - virtual void display_head_impl(context & ctx, std::ostream & out) const { + virtual void display_head_impl(rel_context & ctx, std::ostream & out) const { out << "filter_equal " << m_reg << " col: " << m_col << " val: " << ctx.get_rmanager().to_nice_string(m_value); } @@ -476,7 +476,7 @@ namespace datalog { } return true; } - virtual void display_head_impl(context & ctx, std::ostream & out) const { + virtual void display_head_impl(rel_context & ctx, std::ostream & out) const { out << "filter_identical " << m_reg << " "; print_container(m_cols, out); } @@ -519,7 +519,7 @@ namespace datalog { } return true; } - virtual void display_head_impl(context & ctx, std::ostream & out) const { + virtual void display_head_impl(rel_context & ctx, std::ostream & out) const { out << "filter_interpreted " << m_reg << " using " << mk_pp(m_cond, m_cond.get_manager()); } @@ -624,7 +624,7 @@ namespace datalog { ctx.set_register_annotation(m_delta, "delta of "+str); } } - virtual void display_head_impl(context & ctx, std::ostream & out) const { + virtual void display_head_impl(rel_context & ctx, std::ostream & out) const { out << (m_widen ? "widen " : "union ") << m_src << " into " << m_tgt; if (m_delta!=execution_context::void_register) { out << " with delta " << m_delta; @@ -678,7 +678,7 @@ namespace datalog { return true; } - virtual void display_head_impl(context & ctx, std::ostream & out) const { + virtual void display_head_impl(rel_context & ctx, std::ostream & out) const { out << (m_projection ? "project " : "rename ") << m_src << " into " << m_tgt; out << (m_projection ? " deleting columns " : " with cycle "); print_container(m_cols, out); @@ -739,7 +739,7 @@ namespace datalog { } return true; } - virtual void display_head_impl(context & ctx, std::ostream & out) const { + virtual void display_head_impl(rel_context & ctx, std::ostream & out) const { out << "join_project " << m_rel1; print_container(m_cols1, out); out << " and " << m_rel2; @@ -800,7 +800,7 @@ namespace datalog { } return true; } - virtual void display_head_impl(context & ctx, std::ostream & out) const { + virtual void display_head_impl(rel_context & ctx, std::ostream & out) const { out << "select_equal_and_project " << m_src <<" into " << m_result << " col: " << m_col << " val: " << ctx.get_rmanager().to_nice_string(m_value); } @@ -809,7 +809,7 @@ namespace datalog { std::string s1 = "src"; ctx.get_register_annotation(m_src, s1); s << "select equal project col " << m_col << " val: " - << ctx.get_datalog_context().get_rmanager().to_nice_string(m_value) << " " << s1; + << ctx.get_rel_context().get_rmanager().to_nice_string(m_value) << " " << s1; ctx.set_register_annotation(m_result, s.str()); } }; @@ -854,7 +854,7 @@ namespace datalog { } return true; } - virtual void display_head_impl(context & ctx, std::ostream & out) const { + virtual void display_head_impl(rel_context & ctx, std::ostream & out) const { out << "filter_by_negation on " << m_tgt; print_container(m_cols1, out); out << " with " << m_neg_rel; @@ -887,12 +887,12 @@ namespace datalog { } virtual bool perform(execution_context & ctx) { ctx.make_empty(m_tgt); - relation_base * rel = ctx.get_datalog_context().get_rmanager().mk_empty_relation(m_sig, m_pred); + relation_base * rel = ctx.get_rel_context().get_rmanager().mk_empty_relation(m_sig, m_pred); rel->add_fact(m_fact); ctx.set_reg(m_tgt, rel); return true; } - virtual void display_head_impl(context & ctx, std::ostream & out) const { + virtual void display_head_impl(rel_context & ctx, std::ostream & out) const { out << "mk_unary_singleton into " << m_tgt << " sort:" << ctx.get_rmanager().to_nice_string(m_sig[0]) << " val:" << ctx.get_rmanager().to_nice_string(m_sig[0], m_fact[0]); @@ -919,10 +919,10 @@ namespace datalog { instr_mk_total(const relation_signature & sig, func_decl* p, reg_idx tgt) : m_sig(sig), m_pred(p), m_tgt(tgt) {} virtual bool perform(execution_context & ctx) { ctx.make_empty(m_tgt); - ctx.set_reg(m_tgt, ctx.get_datalog_context().get_rmanager().mk_full_relation(m_sig, m_pred)); + ctx.set_reg(m_tgt, ctx.get_rel_context().get_rmanager().mk_full_relation(m_sig, m_pred)); return true; } - virtual void display_head_impl(context & ctx, std::ostream & out) const { + virtual void display_head_impl(rel_context & ctx, std::ostream & out) const { out << "mk_total into " << m_tgt << " sort:" << ctx.get_rmanager().to_nice_string(m_sig); } @@ -944,10 +944,10 @@ namespace datalog { instr_mark_saturated(ast_manager & m, func_decl * pred) : m_pred(pred, m) {} virtual bool perform(execution_context & ctx) { - ctx.get_datalog_context().get_rmanager().mark_saturated(m_pred); + ctx.get_rel_context().get_rmanager().mark_saturated(m_pred); return true; } - virtual void display_head_impl(context & ctx, std::ostream & out) const { + virtual void display_head_impl(rel_context & ctx, std::ostream & out) const { out << "mark_saturated " << m_pred->get_name().bare_str(); } virtual void make_annotations(execution_context & ctx) { @@ -970,7 +970,7 @@ namespace datalog { } return true; } - virtual void display_head_impl(context & ctx, std::ostream & out) const { + virtual void display_head_impl(rel_context & ctx, std::ostream & out) const { out << "instr_assert_signature of " << m_tgt << " signature:"; print_container(m_sig, out); } @@ -1019,7 +1019,7 @@ namespace datalog { TRACE("dl", tout <<"% "; - instr->display_head_impl(ctx.get_datalog_context(), tout); + instr->display_head_impl(ctx.get_rel_context(), tout); tout <<"\n";); success = !ctx.should_terminate() && instr->perform(ctx); } @@ -1042,12 +1042,12 @@ namespace datalog { } } - void instruction_block::display_indented(context & ctx, std::ostream & out, std::string indentation) const { + void instruction_block::display_indented(rel_context & ctx, std::ostream & out, std::string indentation) const { instr_seq_type::const_iterator it = m_data.begin(); instr_seq_type::const_iterator end = m_data.end(); for(; it!=end; ++it) { instruction * i = (*it); - if (i->passes_output_thresholds(ctx) || i->being_recorded()) { + if (i->passes_output_thresholds(ctx.get_context()) || i->being_recorded()) { i->display_indented(ctx, out, indentation); } } diff --git a/src/muz_qe/dl_instruction.h b/src/muz_qe/dl_instruction.h index c44c860a0..89f95c860 100644 --- a/src/muz_qe/dl_instruction.h +++ b/src/muz_qe/dl_instruction.h @@ -58,7 +58,7 @@ namespace datalog { private: typedef u_map reg_annotations; - context & m_datalog_context; + context & m_context; reg_vector m_registers; reg_annotations m_reg_annotation; @@ -73,12 +73,12 @@ namespace datalog { */ bool m_eager_emptiness_checking; public: - execution_context(context & datalog_context); + execution_context(context & context); ~execution_context(); void reset(); - context & get_datalog_context() { return m_datalog_context; }; + rel_context & get_rel_context() { return m_context.get_rel_context(); }; void set_timelimit(unsigned time_in_ms); void reset_timelimit(); @@ -208,7 +208,7 @@ namespace datalog { The newline character at the end should not be printed. */ - virtual void display_head_impl(context & ctx, std::ostream & out) const { + virtual void display_head_impl(rel_context & ctx, std::ostream & out) const { out << ""; } /** @@ -216,7 +216,7 @@ namespace datalog { Each line must be prepended by \c indentation and ended by a newline character. */ - virtual void display_body_impl(context & ctx, std::ostream & out, std::string indentation) const {} + virtual void display_body_impl(rel_context & ctx, std::ostream & out, std::string indentation) const {} public: typedef execution_context::reg_type reg_type; typedef execution_context::reg_idx reg_idx; @@ -227,10 +227,10 @@ namespace datalog { virtual void make_annotations(execution_context & ctx) = 0; - void display(context & ctx, std::ostream & out) const { + void display(rel_context & ctx, std::ostream & out) const { display_indented(ctx, out, ""); } - void display_indented(context & ctx, std::ostream & out, std::string indentation) const; + void display_indented(rel_context & ctx, std::ostream & out, std::string indentation) const; static instruction * mk_load(ast_manager & m, func_decl * pred, reg_idx tgt); /** @@ -329,10 +329,10 @@ namespace datalog { void make_annotations(execution_context & ctx); - void display(context & ctx, std::ostream & out) const { + void display(rel_context & ctx, std::ostream & out) const { display_indented(ctx, out, ""); } - void display_indented(context & ctx, std::ostream & out, std::string indentation) const; + void display_indented(rel_context & ctx, std::ostream & out, std::string indentation) const; }; diff --git a/src/muz_qe/dl_mk_explanations.cpp b/src/muz_qe/dl_mk_explanations.cpp index 425d3fb60..b4683bdbe 100644 --- a/src/muz_qe/dl_mk_explanations.cpp +++ b/src/muz_qe/dl_mk_explanations.cpp @@ -607,7 +607,7 @@ namespace datalog { m_e_sort = m_decl_util.mk_rule_sort(); m_pinned.push_back(m_e_sort); - relation_manager & rmgr = ctx.get_rmanager(); + relation_manager & rmgr = ctx.get_rel_context().get_rmanager(); symbol er_symbol = explanation_relation_plugin::get_name(relation_level); m_er_plugin = static_cast(rmgr.get_relation_plugin(er_symbol)); if(!m_er_plugin) { @@ -640,7 +640,7 @@ namespace datalog { void mk_explanations::assign_rel_level_kind(func_decl * e_decl, func_decl * orig) { SASSERT(m_relation_level); - relation_manager & rmgr = m_context.get_rmanager(); + relation_manager & rmgr = m_context.get_rel_context().get_rmanager(); unsigned sz = e_decl->get_arity(); relation_signature sig; rmgr.from_predicate(e_decl, sig); @@ -884,7 +884,7 @@ namespace datalog { m_context.collect_predicates(m_original_preds); rule_set * res = alloc(rule_set, m_context); - transform_facts(m_context.get_rmanager()); + transform_facts(m_context.get_rel_context().get_rmanager()); transform_rules(source, *res); return res; } diff --git a/src/muz_qe/dl_mk_magic_sets.cpp b/src/muz_qe/dl_mk_magic_sets.cpp index 668cbf939..373a90969 100644 --- a/src/muz_qe/dl_mk_magic_sets.cpp +++ b/src/muz_qe/dl_mk_magic_sets.cpp @@ -365,7 +365,7 @@ namespace datalog { rule * r = *it; transform_rule(task.m_adornment, r); } - if(!m_context.get_relation(task.m_pred).empty()) { + if(!m_context.get_rel_context().get_relation(task.m_pred).empty()) { //we need a rule to copy facts that are already in a relation into the adorned //relation (since out intentional predicates can have facts, not only rules) create_transfer_rule(task); diff --git a/src/muz_qe/dl_mk_partial_equiv.cpp b/src/muz_qe/dl_mk_partial_equiv.cpp index 68f333b1b..367a15743 100644 --- a/src/muz_qe/dl_mk_partial_equiv.cpp +++ b/src/muz_qe/dl_mk_partial_equiv.cpp @@ -97,7 +97,7 @@ namespace datalog { return 0; } - relation_manager & rm = m_context.get_rmanager(); + relation_manager & rm = m_context.get_rel_context().get_rmanager(); rule_set::decl2rules::iterator it = source.begin_grouped_rules(); rule_set::decl2rules::iterator end = source.end_grouped_rules(); diff --git a/src/muz_qe/dl_mk_rule_inliner.cpp b/src/muz_qe/dl_mk_rule_inliner.cpp index 9c9bf7abb..fa532ee6c 100644 --- a/src/muz_qe/dl_mk_rule_inliner.cpp +++ b/src/muz_qe/dl_mk_rule_inliner.cpp @@ -205,7 +205,7 @@ namespace datalog { void mk_rule_inliner::count_pred_occurrences(rule_set const & orig) { - m_context.get_rmanager().collect_non_empty_predicates(m_preds_with_facts); + m_context.get_rel_context().get_rmanager().collect_non_empty_predicates(m_preds_with_facts); rule_set::iterator rend = orig.end(); for (rule_set::iterator rit = orig.begin(); rit!=rend; ++rit) { diff --git a/src/muz_qe/dl_mk_similarity_compressor.cpp b/src/muz_qe/dl_mk_similarity_compressor.cpp index 8225aa315..42a5ba367 100644 --- a/src/muz_qe/dl_mk_similarity_compressor.cpp +++ b/src/muz_qe/dl_mk_similarity_compressor.cpp @@ -361,7 +361,7 @@ namespace datalog { collect_orphan_consts(*it, const_infos, val_fact); m_context.add_fact(aux_pred, val_fact); } - m_context.get_rmanager().mark_saturated(aux_pred); + m_context.get_rel_context().get_rmanager().mark_saturated(aux_pred); app * new_head = r->get_head(); ptr_vector new_tail; diff --git a/src/muz_qe/dl_mk_simple_joins.cpp b/src/muz_qe/dl_mk_simple_joins.cpp index da1f80a53..363a4f0f7 100644 --- a/src/muz_qe/dl_mk_simple_joins.cpp +++ b/src/muz_qe/dl_mk_simple_joins.cpp @@ -569,10 +569,11 @@ namespace datalog { cost estimate_size(app * t) const { func_decl * pred = t->get_decl(); unsigned n=pred->get_arity(); - if( (m_context.saturation_was_run() && m_context.get_rmanager().try_get_relation(pred)) - || m_context.get_rmanager().is_saturated(pred)) { - SASSERT(m_context.get_rmanager().try_get_relation(pred)); //if it is saturated, it should exist - unsigned rel_size_int = m_context.get_relation(pred).get_size_estimate_rows(); + relation_manager& rm = m_context.get_rel_context().get_rmanager(); + if( (m_context.saturation_was_run() && rm.try_get_relation(pred)) + || rm.is_saturated(pred)) { + SASSERT(rm.try_get_relation(pred)); //if it is saturated, it should exist + unsigned rel_size_int = m_context.get_rel_context().get_relation(pred).get_size_estimate_rows(); if(rel_size_int!=0) { cost rel_size = static_cast(rel_size_int); cost curr_size = rel_size; diff --git a/src/muz_qe/dl_mk_subsumption_checker.cpp b/src/muz_qe/dl_mk_subsumption_checker.cpp index d20ad5055..19c28c036 100644 --- a/src/muz_qe/dl_mk_subsumption_checker.cpp +++ b/src/muz_qe/dl_mk_subsumption_checker.cpp @@ -250,7 +250,7 @@ namespace datalog { } void mk_subsumption_checker::scan_for_relations_total_due_to_facts() { - relation_manager& rm = m_context.get_rmanager(); + relation_manager& rm = m_context.get_rel_context().get_rmanager(); decl_set candidate_preds; m_context.collect_predicates(candidate_preds); diff --git a/src/muz_qe/dl_mk_unbound_compressor.cpp b/src/muz_qe/dl_mk_unbound_compressor.cpp index 000a70b22..e3db82759 100644 --- a/src/muz_qe/dl_mk_unbound_compressor.cpp +++ b/src/muz_qe/dl_mk_unbound_compressor.cpp @@ -337,7 +337,7 @@ namespace datalog { // TODO mc, pc m_modified = false; - m_context.get_rmanager().collect_non_empty_predicates(m_non_empty_rels); + m_context.get_rel_context().get_rmanager().collect_non_empty_predicates(m_non_empty_rels); unsigned init_rule_cnt = source.get_num_rules(); SASSERT(m_rules.empty()); diff --git a/src/muz_qe/dl_rule.cpp b/src/muz_qe/dl_rule.cpp index 9b0af2554..dedd37a78 100644 --- a/src/muz_qe/dl_rule.cpp +++ b/src/muz_qe/dl_rule.cpp @@ -1014,7 +1014,7 @@ namespace datalog { out << '.'; if (ctx.output_profile()) { out << " {"; - output_profile(ctx, out); + output_profile(out); out << '}'; } out << '\n'; diff --git a/src/muz_qe/fixedpoint_params.pyg b/src/muz_qe/fixedpoint_params.pyg index aa78dad3d..61f993c0a 100644 --- a/src/muz_qe/fixedpoint_params.pyg +++ b/src/muz_qe/fixedpoint_params.pyg @@ -30,25 +30,25 @@ def_module_params('fixedpoint', ('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 " + ('bfs_model_search', BOOL, True, "PDR: use BFS strategy for expanding model search"), + ('use_farkas', BOOL, True, "PDR: use lemma generator based on Farkas (for linear real arithmetic)"), + ('generate_proof_trace', BOOL, False, "PDR: trace for 'sat' answer as proof object"), + ('flexible_trace', BOOL, False, "PDR: 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 " + ('unfold_rules', UINT, 0, "PDR: unfold rules statically using iterative squarring"), + ('use_model_generalizer', BOOL, False, "PDR: use model for backwards propagation (instead of symbolic simulation)"), + ('validate_result', BOOL, False, "PDR validate result (by proof checking or model checking)"), + ('simplify_formulas_pre', BOOL, False, "PDR: simplify derived formulas before inductive propagation"), + ('simplify_formulas_post', BOOL, False, "PDR: simplify derived formulas after inductive propagation"), + ('slice', BOOL, True, "PDR: simplify clause set using slicing"), + ('coalesce_rules', BOOL, False, "BMC: coalesce rules"), + ('use_multicore_generalizer', BOOL, False, "PDR: extract multiple cores for blocking states"), + ('use_inductive_generalizer', BOOL, True, "PDR: generalize lemmas using induction strengthening"), + ('cache_mode', UINT, 0, "PDR: use no (0), symbolic (1) or explicit cache (2) for model search"), + ('inductive_reachability_check', BOOL, False, "PDR: 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)"), + ('max_num_contexts', UINT, 500, "PDR: maximal number of contexts to create"), + ('try_minimize_core', BOOL, False, "PDR: 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 " diff --git a/src/muz_qe/pdr_dl_interface.cpp b/src/muz_qe/pdr_dl_interface.cpp index 663f634c4..0482ece05 100644 --- a/src/muz_qe/pdr_dl_interface.cpp +++ b/src/muz_qe/pdr_dl_interface.cpp @@ -83,7 +83,6 @@ lbool dl_interface::query(expr * query) { m_pdr_rules.reset(); m_refs.reset(); m_pred2slice.reset(); - m_ctx.get_rmanager().reset_relations(); ast_manager& m = m_ctx.get_manager(); datalog::rule_manager& rule_manager = m_ctx.get_rule_manager(); datalog::rule_set old_rules(m_ctx.get_rules()); diff --git a/src/muz_qe/rel_context.cpp b/src/muz_qe/rel_context.cpp new file mode 100644 index 000000000..1b4042ab9 --- /dev/null +++ b/src/muz_qe/rel_context.cpp @@ -0,0 +1,517 @@ +/*++ +Copyright (c) 2012 Microsoft Corporation + +Module Name: + + rel_context.cpp + +Abstract: + + context for relational datalog engine. + +Author: + + Nikolaj Bjorner (nbjorner) 2012-12-3. + +Revision History: + + Extracted from dl_context + +--*/ +#include"rel_context.h" +#include"dl_context.h" +#include"dl_compiler.h" +#include"dl_instruction.h" +#include"dl_mk_explanations.h" +#include"dl_mk_magic_sets.h" +#include"dl_product_relation.h" +#include"dl_bound_relation.h" +#include"dl_interval_relation.h" +#include"dl_finite_product_relation.h" +#include"dl_sparse_table.h" +#include"dl_table.h" +#include"dl_table_relation.h" +#ifndef _EXTERNAL_RELEASE +#include"dl_skip_table.h" +#endif + +namespace datalog { + + rel_context::rel_context(context& ctx) + : m_context(ctx), + m(ctx.get_manager()), + m_rmanager(ctx), + m_answer(m), + m_cancel(false), + m_last_result_relation(0) { + get_rmanager().register_plugin(alloc(sparse_table_plugin, get_rmanager())); + get_rmanager().register_plugin(alloc(hashtable_table_plugin, get_rmanager())); + get_rmanager().register_plugin(alloc(bitvector_table_plugin, get_rmanager())); + get_rmanager().register_plugin(alloc(equivalence_table_plugin, get_rmanager())); + +#ifndef _EXTERNAL_RELEASE + get_rmanager().register_plugin(alloc(skip_table_plugin, get_rmanager())); +#endif + + //register plugins for builtin relations + + get_rmanager().register_plugin(alloc(bound_relation_plugin, get_rmanager())); + get_rmanager().register_plugin(alloc(interval_relation_plugin, get_rmanager())); + +} + + rel_context::~rel_context() { + if (m_last_result_relation) { + m_last_result_relation->deallocate(); + m_last_result_relation = 0; + } + } + + void rel_context::collect_predicates(decl_set & res) { + unsigned rule_cnt = m_context.get_rules().get_num_rules(); + for (unsigned rindex=0; rindexget_head()->get_decl()); + unsigned tail_len = r->get_uninterpreted_tail_size(); + for (unsigned tindex=0; tindexget_tail(tindex)->get_decl()); + } + } + decl_set::iterator oit = m_output_preds.begin(); + decl_set::iterator oend = m_output_preds.end(); + for (; oit!=oend; ++oit) { + res.insert(*oit); + } + get_rmanager().collect_predicates(res); + } + + + lbool rel_context::saturate() { + m_context.ensure_closed(); + + bool time_limit = m_context.soft_timeout()!=0; + unsigned remaining_time_limit = m_context.soft_timeout(); + unsigned restart_time = m_context.initial_restart_timeout(); + + rule_set original_rules(m_context.get_rules()); + decl_set original_predicates; + m_context.collect_predicates(original_predicates); + + instruction_block rules_code; + instruction_block termination_code; + execution_context ex_ctx(m_context); + + lbool result; + + TRACE("dl", m_context.display(tout);); + + while (true) { + model_converter_ref mc; // Ignored in Datalog mode + proof_converter_ref pc; // Ignored in Datalog mode + m_context.transform_rules(mc, pc); + compiler::compile(m_context, m_context.get_rules(), rules_code, termination_code); + + TRACE("dl", rules_code.display(*this, tout); ); + + bool timeout_after_this_round = time_limit && (restart_time==0 || remaining_time_limit<=restart_time); + + if (time_limit || restart_time!=0) { + unsigned timeout = time_limit ? (restart_time!=0) ? + std::min(remaining_time_limit, restart_time) + : remaining_time_limit : restart_time; + ex_ctx.set_timelimit(timeout); + } + + bool early_termination = !rules_code.perform(ex_ctx); + ex_ctx.reset_timelimit(); + VERIFY( termination_code.perform(ex_ctx) ); + + rules_code.process_all_costs(); + + IF_VERBOSE(10, ex_ctx.report_big_relations(1000, verbose_stream());); + + if (!early_termination) { + m_context.set_status(OK); + result = l_true; + break; + } + + if (memory::above_high_watermark()) { + m_context.set_status(MEMOUT); + result = l_undef; + break; + } + if (timeout_after_this_round || m_cancel) { + m_context.set_status(TIMEOUT); + result = l_undef; + break; + } + SASSERT(restart_time != 0); + if (time_limit) { + SASSERT(remaining_time_limit>restart_time); + remaining_time_limit -= restart_time; + } + uint64 new_restart_time = static_cast(restart_time)*m_context.initial_restart_timeout(); + if (new_restart_time > UINT_MAX) { + restart_time = UINT_MAX; + } + else { + restart_time = static_cast(new_restart_time); + } + + rules_code.reset(); + termination_code.reset(); + ex_ctx.reset(); + m_context.reopen(); + restrict_predicates(original_predicates); + m_context.replace_rules(original_rules); + m_context.close(); + } + m_context.reopen(); + restrict_predicates(original_predicates); + m_context.replace_rules(original_rules); + m_context.close(); + TRACE("dl", ex_ctx.report_big_relations(100, tout);); + m_cancel = false; + return result; + } + +#define BEGIN_QUERY() \ + rule_set original_rules(m_context.get_rules()); \ + decl_set original_preds; \ + m_context.collect_predicates(original_preds); \ + bool was_closed = m_context.is_closed(); \ + if (was_closed) { \ + m_context.reopen(); \ + } \ + +#define END_QUERY() \ + m_context.reopen(); \ + m_context.replace_rules(original_rules); \ + restrict_predicates(original_preds); \ + \ + if (was_closed) { \ + m_context.close(); \ + } \ + + lbool rel_context::query(unsigned num_rels, func_decl * const* rels) { + get_rmanager().reset_saturated_marks(); + BEGIN_QUERY(); + for (unsigned i = 0; i < num_rels; ++i) { + set_output_predicate(rels[i]); + } + m_context.close(); + reset_negated_tables(); + lbool res = saturate(); + + switch(res) { + case l_true: { + expr_ref_vector ans(m); + expr_ref e(m); + bool some_non_empty = num_rels == 0; + for (unsigned i = 0; i < num_rels; ++i) { + relation_base& rel = get_relation(rels[i]); + if (!rel.empty()) { + some_non_empty = true; + } + rel.to_formula(e); + ans.push_back(e); + } + SASSERT(!m_last_result_relation); + if (some_non_empty) { + m_answer = m.mk_and(ans.size(), ans.c_ptr()); + } + else { + m_answer = m.mk_false(); + res = l_false; + } + break; + } + case l_false: + m_answer = m.mk_false(); + break; + case l_undef: + break; + } + END_QUERY(); + return res; + } + + lbool rel_context::query(expr* query) { + get_rmanager().reset_saturated_marks(); + BEGIN_QUERY(); + rule_manager& rm = m_context.get_rule_manager(); + rule_ref qrule(rm); + rule_ref_vector qrules(rm); + func_decl_ref query_pred(m); + try { + rm.mk_query(query, query_pred, qrules, qrule); + } + catch(default_exception& exn) { + m_context.close(); + m_context.set_status(INPUT_ERROR); + throw exn; + } + try { + m_context.add_rules(qrules); + } + catch (default_exception& exn) { + m_context.close(); + m_context.set_status(INPUT_ERROR); + throw exn; + } + + set_output_predicate(qrule->get_head()->get_decl()); + m_context.close(); + reset_negated_tables(); + + if (m_context.generate_explanations()) { + model_converter_ref mc; // ignored in Datalog mode + proof_converter_ref pc; // ignored in Datalog mode + rule_transformer transformer(m_context); + //expl_plugin is deallocated when transformer goes out of scope + mk_explanations * expl_plugin = + alloc(mk_explanations, m_context, m_context.explanations_on_relation_level()); + transformer.register_plugin(expl_plugin); + m_context.transform_rules(transformer, mc, pc); + + //we will retrieve the predicate with explanations instead of the original query predicate + query_pred = expl_plugin->get_e_decl(query_pred); + const rule_vector & query_rules = m_context.get_rules().get_predicate_rules(query_pred); + SASSERT(query_rules.size()==1); + qrule = query_rules.back(); + } + + if (m_context.magic_sets_for_queries()) { + model_converter_ref mc; // Ignored in Datalog mode + proof_converter_ref pc; // Ignored in Datalog mode + rule_transformer transformer(m_context); + transformer.register_plugin(alloc(mk_magic_sets, m_context, qrule.get())); + m_context.transform_rules(transformer, mc, pc); + } + + lbool res = saturate(); + + if (res != l_undef) { + m_last_result_relation = get_relation(query_pred).clone(); + if (m_last_result_relation->empty()) { + res = l_false; + m_answer = m.mk_false(); + } + else { + m_last_result_relation->to_formula(m_answer); + } + } + + END_QUERY(); + return res; + } + + void rel_context::reset_negated_tables() { + rule_set::pred_set_vector const & pred_sets = m_context.get_rules().get_strats(); + bool non_empty = false; + for (unsigned i = 1; i < pred_sets.size(); ++i) { + func_decl_set::iterator it = pred_sets[i]->begin(), end = pred_sets[i]->end(); + for (; it != end; ++it) { + func_decl* pred = *it; + relation_base & rel = get_relation(pred); + if (!rel.empty()) { + non_empty = true; + break; + } + } + } + if (!non_empty) { + return; + } + // collect predicates that depend on negation. + func_decl_set depends_on_negation; + for (unsigned i = 1; i < pred_sets.size(); ++i) { + bool change = true; + while (change) { + change = false; + func_decl_set::iterator it = pred_sets[i]->begin(), end = pred_sets[i]->end(); + for (; it != end; ++it) { + func_decl* pred = *it; + if (depends_on_negation.contains(pred)) { + continue; + } + rule_vector const& rules = m_context.get_rules().get_predicate_rules(pred); + bool inserted = false; + for (unsigned j = 0; !inserted && j < rules.size(); ++j) { + rule* r = rules[j]; + unsigned psz = r->get_positive_tail_size(); + unsigned tsz = r->get_uninterpreted_tail_size(); + if (psz < tsz) { + depends_on_negation.insert(pred); + change = true; + inserted = true; + } + for (unsigned k = 0; !inserted && k < tsz; ++k) { + func_decl* tail_decl = r->get_tail(k)->get_decl(); + if (depends_on_negation.contains(tail_decl)) { + depends_on_negation.insert(pred); + change = true; + inserted = true; + } + } + } + } + } + } + func_decl_set::iterator it = depends_on_negation.begin(), end = depends_on_negation.end(); + for (; it != end; ++it) { + func_decl* pred = *it; + relation_base & rel = get_relation(pred); + + if (!rel.empty()) { + TRACE("dl", tout << "Resetting: " << mk_ismt2_pp(pred, m) << "\n";); + rel.reset(); + } + } + } + + void rel_context::set_output_predicate(func_decl * pred) { + if (!m_output_preds.contains(pred)) { + m_output_preds.insert(pred); + } + } + + void rel_context::restrict_predicates( const decl_set & res ) { + set_intersection(m_output_preds, res); + get_rmanager().restrict_predicates(res); + } + + relation_base & rel_context::get_relation(func_decl * pred) { return get_rmanager().get_relation(pred); } + relation_base * rel_context::try_get_relation(func_decl * pred) const { return get_rmanager().try_get_relation(pred); } + + relation_manager & rel_context::get_rmanager() { return m_rmanager; } + + const relation_manager & rel_context::get_rmanager() const { return m_rmanager; } + + bool rel_context::output_profile() const { return m_context.output_profile(); } + + + void rel_context::set_predicate_representation(func_decl * pred, unsigned relation_name_cnt, + symbol const * relation_names) { + + relation_manager & rmgr = get_rmanager(); + + family_id target_kind = null_family_id; + switch (relation_name_cnt) { + case 0: + return; + case 1: + target_kind = get_ordinary_relation_plugin(relation_names[0]).get_kind(); + break; + default: { + svector rel_kinds; // kinds of plugins that are not table plugins + family_id rel_kind; // the aggregate kind of non-table plugins + for (unsigned i = 0; i < relation_name_cnt; i++) { + relation_plugin & p = get_ordinary_relation_plugin(relation_names[i]); + rel_kinds.push_back(p.get_kind()); + } + if (rel_kinds.size() == 1) { + rel_kind = rel_kinds[0]; + } + else { + relation_signature rel_sig; + //rmgr.from_predicate(pred, rel_sig); + product_relation_plugin & prod_plugin = product_relation_plugin::get_plugin(rmgr); + rel_kind = prod_plugin.get_relation_kind(rel_sig, rel_kinds); + } + target_kind = rel_kind; + break; + } + } + + SASSERT(target_kind != null_family_id); + get_rmanager().set_predicate_kind(pred, target_kind); + } + + relation_plugin & rel_context::get_ordinary_relation_plugin(symbol relation_name) { + relation_plugin * plugin = get_rmanager().get_relation_plugin(relation_name); + if (!plugin) { + std::stringstream sstm; + sstm << "relation plugin " << relation_name << " does not exist"; + throw default_exception(sstm.str()); + } + if (plugin->is_product_relation()) { + throw default_exception("cannot request product relation directly"); + } + if (plugin->is_sieve_relation()) { + throw default_exception("cannot request sieve relation directly"); + } + if (plugin->is_finite_product_relation()) { + throw default_exception("cannot request finite product relation directly"); + } + return *plugin; + } + + bool rel_context::result_contains_fact(relation_fact const& f) { + SASSERT(m_last_result_relation); + return m_last_result_relation->contains_fact(f); + } + + void rel_context::reset_tables() { + get_rmanager().reset_saturated_marks(); + rule_set::decl2rules::iterator it = m_context.get_rules().begin_grouped_rules(); + rule_set::decl2rules::iterator end = m_context.get_rules().end_grouped_rules(); + for (; it != end; ++it) { + func_decl* p = it->m_key; + relation_base & rel = get_relation(p); + rel.reset(); + } + for (unsigned i = 0; i < m_table_facts.size(); ++i) { + func_decl* pred = m_table_facts[i].first; + relation_fact const& fact = m_table_facts[i].second; + get_relation(pred).add_fact(fact); + } + } + + void rel_context::add_fact(func_decl* pred, relation_fact const& fact) { + get_rmanager().reset_saturated_marks(); + get_relation(pred).add_fact(fact); + m_table_facts.push_back(std::make_pair(pred, fact)); + } + + void rel_context::add_fact(func_decl* pred, table_fact const& fact) { + get_rmanager().reset_saturated_marks(); + relation_base & rel0 = get_relation(pred); + if (rel0.from_table()) { + table_relation & rel = static_cast(rel0); + rel.add_table_fact(fact); + // TODO: table facts? + } + else { + relation_fact rfact(m); + for (unsigned i = 0; i < fact.size(); ++i) { + rfact.push_back(m_context.get_decl_util().mk_numeral(fact[i], pred->get_domain()[i])); + } + add_fact(pred, rfact); + } + } + + void rel_context::store_relation(func_decl * pred, relation_base * rel) { + get_rmanager().store_relation(pred, rel); + } + + void rel_context::inherit_predicate_kind(func_decl* new_pred, func_decl* orig_pred) { + if (orig_pred) { + family_id target_kind = get_rmanager().get_requested_predicate_kind(orig_pred); + if (target_kind != null_family_id) { + get_rmanager().set_predicate_kind(new_pred, target_kind); + } + } + } + + void rel_context::display_output_facts(std::ostream & out) const { + get_rmanager().display_output_tables(out); + } + + void rel_context::display_facts(std::ostream& out) const { + get_rmanager().display(out); + } + + +}; diff --git a/src/muz_qe/rel_context.h b/src/muz_qe/rel_context.h new file mode 100644 index 000000000..8e0ea4a16 --- /dev/null +++ b/src/muz_qe/rel_context.h @@ -0,0 +1,115 @@ +/*++ +Copyright (c) 2012 Microsoft Corporation + +Module Name: + + rel_context.h + +Abstract: + + context for relational datalog engine. + +Author: + + Nikolaj Bjorner (nbjorner) 2012-12-3. + +Revision History: + + Extracted from dl_context + +--*/ +#ifndef _REL_CONTEXT_H_ +#define _REL_CONTEXT_H_ +#include "ast.h" +#include "dl_relation_manager.h" +#include "lbool.h" + +namespace datalog { + + class context; + + class rel_context { + typedef vector > fact_vector; + + context& m_context; + ast_manager& m; + relation_manager m_rmanager; + expr_ref m_answer; + volatile bool m_cancel; + relation_base * m_last_result_relation; + decl_set m_output_preds; + fact_vector m_table_facts; + + void reset_negated_tables(); + + lbool saturate(); + + relation_plugin & get_ordinary_relation_plugin(symbol relation_name); + + void reset_tables(); + + public: + rel_context(context& ctx); + + ~rel_context(); + + relation_manager & get_rmanager(); + const relation_manager & get_rmanager() const; + ast_manager& get_manager() { return m; } + context& get_context() { return m_context; } + relation_base & get_relation(func_decl * pred); + relation_base * try_get_relation(func_decl * pred) const; + expr_ref get_last_answer() { return m_answer; } + + bool output_profile() const; + + + lbool query(expr* q); + lbool query(unsigned num_rels, func_decl * const* rels); + + void set_predicate_representation(func_decl * pred, unsigned relation_name_cnt, + symbol const * relation_names); + + void inherit_predicate_kind(func_decl* new_pred, func_decl* orig_pred); + + void cancel() { m_cancel = true; } + + + + /** + \brief Restrict the set of used predicates to \c res. + + The function deallocates unsused relations, it does not deal with rules. + */ + void restrict_predicates(const decl_set & res); + + void collect_predicates(decl_set & res); + + void set_output_predicate(func_decl * pred); + bool is_output_predicate(func_decl * pred) { return m_output_preds.contains(pred); } + const decl_set & get_output_predicates() const { return m_output_preds; } + + + /** + \brief query result if it contains fact. + */ + bool result_contains_fact(relation_fact const& f); + + void add_fact(func_decl* pred, relation_fact const& fact); + + void add_fact(func_decl* pred, table_fact const& fact); + + /** + \brief Store the relation \c rel under the predicate \c pred. The \c context object + takes over the ownership of the relation object. + */ + void store_relation(func_decl * pred, relation_base * rel); + + void display_output_facts(std::ostream & out) const; + void display_facts(std::ostream & out) const; + + + }; +}; + +#endif /* _REL_CONTEXT_H_ */ diff --git a/src/shell/datalog_frontend.cpp b/src/shell/datalog_frontend.cpp index 1d001c349..44a9d9b66 100644 --- a/src/shell/datalog_frontend.cpp +++ b/src/shell/datalog_frontend.cpp @@ -86,7 +86,7 @@ static void display_statistics( out << "--------------\n"; out << "instructions \n"; - code.display(ctx, out); + code.display(ctx.get_rel_context(), out); out << "--------------\n"; out << "big relations \n"; @@ -94,7 +94,7 @@ static void display_statistics( } out << "--------------\n"; out << "relation sizes\n"; - ctx.get_rmanager().display_relation_sizes(out); + ctx.get_rel_context().get_rmanager().display_relation_sizes(out); if (verbose) { out << "--------------\n"; @@ -139,7 +139,7 @@ unsigned read_datalog(char const * file) { params.set_bool("default_table_checked", dl_params.m_default_table_checked); datalog::context ctx(m, s_params, params); - datalog::relation_manager & rmgr = ctx.get_rmanager(); + datalog::relation_manager & rmgr = ctx.get_rel_context().get_rmanager(); datalog::relation_plugin & inner_plg = *rmgr.get_relation_plugin(symbol("tr_hashtable")); SASSERT(&inner_plg); rmgr.register_plugin(alloc(datalog::finite_product_relation_plugin, inner_plg, rmgr)); @@ -206,7 +206,7 @@ unsigned read_datalog(char const * file) { datalog::compiler::compile(ctx, ctx.get_rules(), rules_code, termination_code); - TRACE("dl_compiler", rules_code.display(ctx, tout);); + TRACE("dl_compiler", rules_code.display(ctx.get_rel_context(), tout);); rules_code.make_annotations(ex_ctx); @@ -248,10 +248,10 @@ unsigned read_datalog(char const * file) { TRACE("dl_compiler", ctx.display(tout); - rules_code.display(ctx, tout);); + rules_code.display(ctx.get_rel_context(), tout);); if (ctx.get_params().output_tuples()) { - ctx.display_output_facts(std::cout); + ctx.get_rel_context().display_output_facts(std::cout); } display_statistics( From 72e09759ee7ff96123834177746d9805d8b6d237 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 3 Dec 2012 15:13:45 -0800 Subject: [PATCH 4/5] factor out relation context for datalog Signed-off-by: Nikolaj Bjorner --- src/muz_qe/dl_cmds.cpp | 13 +++++++++---- 1 file changed, 9 insertions(+), 4 deletions(-) diff --git a/src/muz_qe/dl_cmds.cpp b/src/muz_qe/dl_cmds.cpp index 735df8d80..8c4e26db7 100644 --- a/src/muz_qe/dl_cmds.cpp +++ b/src/muz_qe/dl_cmds.cpp @@ -44,6 +44,11 @@ struct dl_context { scoped_ptr m_context; trail_stack m_trail; + fixedpoint_params const& get_params() { + init(); + return m_context->get_params(); + } + dl_context(cmd_context & ctx, dl_collected_cmds* collected_cmds): m_params(m_params_ref), m_cmd(ctx), @@ -214,7 +219,7 @@ public: datalog::context& dlctx = m_dl_ctx->dlctx(); set_background(ctx); dlctx.updt_params(m_params); - unsigned timeout = m_dl_ctx->m_params.timeout(); + unsigned timeout = m_dl_ctx->get_params().timeout(); cancel_eh eh(dlctx); lbool status = l_undef; { @@ -283,7 +288,7 @@ private: } void print_answer(cmd_context& ctx) { - if (m_dl_ctx->m_params.print_answer()) { + if (m_dl_ctx->get_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); @@ -298,7 +303,7 @@ private: } void print_statistics(cmd_context& ctx) { - if (m_dl_ctx->m_params.print_statistics()) { + if (m_dl_ctx->get_params().print_statistics()) { statistics st; datalog::context& dlctx = m_dl_ctx->dlctx(); unsigned long long max_mem = memory::get_max_used_memory(); @@ -312,7 +317,7 @@ private: } void print_certificate(cmd_context& ctx) { - if (m_dl_ctx->m_params.print_certificate()) { + if (m_dl_ctx->get_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"); From 1cd1a42618a62f321b58cfe3e2cb8d208508c7cd Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 3 Dec 2012 16:02:04 -0800 Subject: [PATCH 5/5] cleanup, fix repeated use of fmls in validator Signed-off-by: Nikolaj Bjorner --- src/muz_qe/dl_context.cpp | 7 +++--- src/muz_qe/dl_context.h | 9 ------- src/muz_qe/pdr_context.cpp | 3 ++- src/muz_qe/pdr_util.cpp | 50 -------------------------------------- src/muz_qe/rel_context.h | 3 ++- 5 files changed, 8 insertions(+), 64 deletions(-) diff --git a/src/muz_qe/dl_context.cpp b/src/muz_qe/dl_context.cpp index 0f9f1d520..7a46228ce 100644 --- a/src/muz_qe/dl_context.cpp +++ b/src/muz_qe/dl_context.cpp @@ -925,13 +925,14 @@ namespace datalog { m_cancel = false; if (m_pdr.get()) m_pdr->cleanup(); if (m_bmc.get()) m_bmc->cleanup(); + if (m_rel.get()) m_rel->cleanup(); } class context::engine_type_proc { - ast_manager& m; - arith_util a; + ast_manager& m; + arith_util a; datatype_util dt; - DL_ENGINE m_engine; + DL_ENGINE m_engine; public: engine_type_proc(ast_manager& m): m(m), a(m), dt(m), m_engine(DATALOG_ENGINE) {} diff --git a/src/muz_qe/dl_context.h b/src/muz_qe/dl_context.h index 89446ce3b..f84050e68 100644 --- a/src/muz_qe/dl_context.h +++ b/src/muz_qe/dl_context.h @@ -417,15 +417,6 @@ namespace datalog { */ bool result_contains_fact(relation_fact const& f); -#if 0 - /** - \brief display facts generated for query. - */ - void display_output_facts(std::ostream & out) const { - get_rel_context().get_rmanager().display_output_tables(out); - } -#endif - rel_context& get_rel_context() { ensure_rel(); return *m_rel; } private: diff --git a/src/muz_qe/pdr_context.cpp b/src/muz_qe/pdr_context.cpp index 974c9251e..9faee3ab0 100644 --- a/src/muz_qe/pdr_context.cpp +++ b/src/muz_qe/pdr_context.cpp @@ -1387,7 +1387,7 @@ namespace pdr { break; } case l_false: { - expr_ref_vector refs(m), fmls(m); + expr_ref_vector refs(m); expr_ref tmp(m); model_ref model; vector rs; @@ -1402,6 +1402,7 @@ namespace pdr { for (unsigned i = 0; i < rules.size(); ++i) { datalog::rule& r = *rules[i]; model->eval(r.get_head(), tmp); + expr_ref_vector fmls(m); fmls.push_back(m.mk_not(tmp)); unsigned utsz = r.get_uninterpreted_tail_size(); unsigned tsz = r.get_tail_size(); diff --git a/src/muz_qe/pdr_util.cpp b/src/muz_qe/pdr_util.cpp index 515f61338..fd08b1aad 100644 --- a/src/muz_qe/pdr_util.cpp +++ b/src/muz_qe/pdr_util.cpp @@ -86,48 +86,6 @@ namespace pdr { return res.str(); } - ///////////////////////// - // select elimination rewriter - // - - class select_elim { - ast_manager& m; - array_util a; - model_ref m_model; - public: - select_elim(ast_manager& m, model_ref& md): m(m), a(m), m_model(md) {} - - br_status mk_app_core(func_decl* f, unsigned num_args, expr* const* args, expr_ref& result) { - if (a.is_select(f)) { - expr_ref tmp(m); - tmp = m.mk_app(f, num_args, args); - m_model->eval(tmp, result); - return BR_DONE; - } - else { - return BR_FAILED; - } - } - }; - - struct select_elim_cfg: public default_rewriter_cfg { - select_elim m_r; - bool rewrite_patterns() const { return false; } - br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) { - return m_r.mk_app_core(f, num, args, result); - } - select_elim_cfg(ast_manager & m, model_ref& md, params_ref const & p):m_r(m, md) {} - }; - - - class select_elim_star : public rewriter_tpl { - select_elim_cfg m_cfg; - public: - select_elim_star(ast_manager & m, model_ref& md, params_ref const & p = params_ref()): - rewriter_tpl(m, false, m_cfg), - m_cfg(m, md, p) {} - }; - ///////////////////////// @@ -238,13 +196,6 @@ namespace pdr { result.push_back(m.mk_not(e)); } } -#if 0 - select_elim_star select_elim(m, m_model); - for (unsigned i = 0; i < result.size(); ++i) { - select_elim(result[i].get(), tmp); - result[i] = tmp; - } -#endif reset(); TRACE("pdr", tout << "minimized model:\n"; @@ -1266,6 +1217,5 @@ namespace pdr { template class rewriter_tpl; -template class rewriter_tpl; diff --git a/src/muz_qe/rel_context.h b/src/muz_qe/rel_context.h index 8e0ea4a16..5fa2486b4 100644 --- a/src/muz_qe/rel_context.h +++ b/src/muz_qe/rel_context.h @@ -73,7 +73,8 @@ namespace datalog { void inherit_predicate_kind(func_decl* new_pred, func_decl* orig_pred); void cancel() { m_cancel = true; } - + + void cleanup() { m_cancel = false; } /**