diff --git a/src/muz/base/dl_context.cpp b/src/muz/base/dl_context.cpp index f19fae369..1271532db 100644 --- a/src/muz/base/dl_context.cpp +++ b/src/muz/base/dl_context.cpp @@ -278,6 +278,7 @@ namespace datalog { symbol context::default_table() const { return m_params->datalog_default_table(); } symbol context::default_relation() const { return m_default_relation; } void context::set_default_relation(symbol const& s) { m_default_relation = s; } + symbol context::print_aig() const { return m_params->print_aig(); } symbol context::check_relation() const { return m_params->datalog_check_relation(); } symbol context::default_table_checker() const { return m_params->datalog_default_table_checker(); } bool context::default_table_checked() const { return m_params->datalog_default_table_checked(); } @@ -294,8 +295,9 @@ namespace datalog { bool context::generate_explanations() const { return m_params->datalog_generate_explanations(); } bool context::explanations_on_relation_level() const { return m_params->datalog_explanations_on_relation_level(); } bool context::magic_sets_for_queries() const { return m_params->datalog_magic_sets_for_queries(); } - - bool context::bit_blast() const { return m_params->xform_bit_blast(); } + symbol context::tab_selection() const { return m_params->tab_selection(); } + bool context::xform_slice() const { return m_params->xform_slice(); } + bool context::xform_bit_blast() const { return m_params->xform_bit_blast(); } bool context::karr() const { return m_params->xform_karr(); } bool context::scale() const { return m_params->xform_scale(); } bool context::magic() const { return m_params->xform_magic(); } diff --git a/src/muz/base/dl_context.h b/src/muz/base/dl_context.h index 285726026..10b93a4c1 100644 --- a/src/muz/base/dl_context.h +++ b/src/muz/base/dl_context.h @@ -172,9 +172,9 @@ namespace datalog { smt_params & m_fparams; params_ref m_params_ref; fixedpoint_params* m_params; - bool m_generate_proof_trace; - bool m_unbound_compressor; - symbol m_default_relation; + bool m_generate_proof_trace; // cached configuration parameter + bool m_unbound_compressor; // cached configuration parameter + symbol m_default_relation; // cached configuration parameter dl_decl_util m_decl_util; th_rewriter m_rewriter; var_subst m_var_subst; @@ -260,18 +260,21 @@ namespace datalog { bool unbound_compressor() const; void set_unbound_compressor(bool f); bool similarity_compressor() const; + symbol print_aig() const; + symbol tab_selection() const; unsigned similarity_compressor_threshold() const; unsigned soft_timeout() const; unsigned initial_restart_timeout() const; bool generate_explanations() const; bool explanations_on_relation_level() const; bool magic_sets_for_queries() const; - bool bit_blast() const; bool karr() const; bool scale() const; bool magic() const; bool quantify_arrays() const; bool instantiate_quantifiers() const; + bool xform_bit_blast() const; + bool xform_slice() const; void register_finite_sort(sort * s, sort_kind k); diff --git a/src/muz/bmc/dl_bmc_engine.cpp b/src/muz/bmc/dl_bmc_engine.cpp index 2b970e4fa..57e4ba8cb 100644 --- a/src/muz/bmc/dl_bmc_engine.cpp +++ b/src/muz/bmc/dl_bmc_engine.cpp @@ -32,7 +32,6 @@ Revision History: #include "dl_transforms.h" #include "dl_mk_rule_inliner.h" #include "scoped_proof.h" -#include"fixedpoint_params.hpp" namespace datalog { @@ -1444,7 +1443,7 @@ namespace datalog { expr_ref bg_assertion = m_ctx.get_background_assertion(); apply_default_transformation(m_ctx); - if (m_ctx.get_params().xform_slice()) { + if (m_ctx.xform_slice()) { datalog::rule_transformer transformer(m_ctx); datalog::mk_slice* slice = alloc(datalog::mk_slice, m_ctx); transformer.register_plugin(slice); diff --git a/src/muz/fp/horn_tactic.cpp b/src/muz/fp/horn_tactic.cpp index a1c556baf..6032b3f02 100644 --- a/src/muz/fp/horn_tactic.cpp +++ b/src/muz/fp/horn_tactic.cpp @@ -190,7 +190,7 @@ class horn_tactic : public tactic { bool produce_proofs = g->proofs_enabled(); if (produce_proofs) { - if (!m_ctx.get_params().generate_proof_trace()) { + if (!m_ctx.generate_proof_trace()) { params_ref params = m_ctx.get_params().p; params.set_bool("generate_proof_trace", true); updt_params(params); @@ -316,7 +316,7 @@ class horn_tactic : public tactic { m_ctx.get_rules(); // flush adding rules. apply_default_transformation(m_ctx); - if (m_ctx.get_params().xform_slice()) { + if (m_ctx.xform_slice()) { datalog::rule_transformer transformer(m_ctx); datalog::mk_slice* slice = alloc(datalog::mk_slice, m_ctx); transformer.register_plugin(slice); diff --git a/src/muz/pdr/pdr_context.cpp b/src/muz/pdr/pdr_context.cpp index 722661e38..ea8eca6f4 100644 --- a/src/muz/pdr/pdr_context.cpp +++ b/src/muz/pdr/pdr_context.cpp @@ -80,7 +80,7 @@ namespace pdr { pred_transformer::pred_transformer(context& ctx, manager& pm, func_decl* head): pm(pm), m(pm.get_manager()), ctx(ctx), m_head(head, m), - m_sig(m), m_solver(pm, ctx.get_params(), head->get_name()), + m_sig(m), m_solver(pm, ctx.get_params().pdr_try_minimize_core(), head->get_name()), m_invariants(m), m_transition(m), m_initial_state(m), m_reachable(pm, (datalog::PDR_CACHE_MODE)ctx.get_params().pdr_cache_mode()) {} diff --git a/src/muz/pdr/pdr_prop_solver.cpp b/src/muz/pdr/pdr_prop_solver.cpp index 06f858608..a7d0a02bf 100644 --- a/src/muz/pdr/pdr_prop_solver.cpp +++ b/src/muz/pdr/pdr_prop_solver.cpp @@ -30,7 +30,6 @@ Revision History: #include "pdr_farkas_learner.h" #include "ast_smt2_pp.h" #include "expr_replacer.h" -#include "fixedpoint_params.hpp" // // Auxiliary structure to introduce propositional names for assumptions that are not @@ -226,12 +225,12 @@ namespace pdr { }; - prop_solver::prop_solver(manager& pm, fixedpoint_params const& p, symbol const& name) : + prop_solver::prop_solver(manager& pm, bool try_minimize_core, symbol const& name) : m_fparams(pm.get_fparams()), m(pm.get_manager()), m_pm(pm), m_name(name), - m_try_minimize_core(p.pdr_try_minimize_core()), + m_try_minimize_core(try_minimize_core), m_ctx(pm.mk_fresh()), m_pos_level_atoms(m), m_neg_level_atoms(m), diff --git a/src/muz/pdr/pdr_prop_solver.h b/src/muz/pdr/pdr_prop_solver.h index a63ec2bf4..d7f13a603 100644 --- a/src/muz/pdr/pdr_prop_solver.h +++ b/src/muz/pdr/pdr_prop_solver.h @@ -31,7 +31,6 @@ Revision History: #include "pdr_manager.h" #include "pdr_smt_context_manager.h" -struct fixedpoint_params; namespace pdr { class prop_solver { @@ -75,7 +74,7 @@ namespace pdr { public: - prop_solver(pdr::manager& pm, fixedpoint_params const& p, symbol const& name); + prop_solver(pdr::manager& pm, bool try_minimize_core, symbol const& name); /** return true is s is a symbol introduced by prop_solver */ bool is_aux_symbol(func_decl * s) const { diff --git a/src/muz/rel/rel_context.cpp b/src/muz/rel/rel_context.cpp index 36ba98781..4b099c9b4 100644 --- a/src/muz/rel/rel_context.cpp +++ b/src/muz/rel/rel_context.cpp @@ -51,7 +51,6 @@ Revision History: #include"dl_mk_interp_tail_simplifier.h" #include"dl_mk_bit_blast.h" #include"dl_mk_separate_negated_tails.h" -#include"fixedpoint_params.hpp" namespace datalog { @@ -159,8 +158,8 @@ namespace datalog { TRACE("dl", m_context.display(tout);); //IF_VERBOSE(3, m_context.display_smt2(0,0,verbose_stream());); - if (m_context.get_params().print_aig().size()) { - const char *filename = static_cast(m_context.get_params().print_aig().c_ptr()); + if (m_context.print_aig().size()) { + const char *filename = static_cast(m_context.print_aig().c_ptr()); aig_exporter aig(m_context.get_rules(), get_context(), &m_table_facts); std::ofstream strm(filename, std::ios_base::binary); aig(strm); @@ -300,7 +299,7 @@ namespace datalog { transf.register_plugin(alloc(mk_interp_tail_simplifier, m_context)); transf.register_plugin(alloc(mk_separate_negated_tails, m_context)); - if (m_context.get_params().xform_bit_blast()) { + if (m_context.xform_bit_blast()) { transf.register_plugin(alloc(mk_bit_blast, m_context, 22000)); transf.register_plugin(alloc(mk_interp_tail_simplifier, m_context, 21000)); } @@ -541,7 +540,7 @@ namespace datalog { void rel_context::add_fact(func_decl* pred, relation_fact const& fact) { get_rmanager().reset_saturated_marks(); get_relation(pred).add_fact(fact); - if (m_context.get_params().print_aig().size()) { + if (m_context.print_aig().size()) { m_table_facts.push_back(std::make_pair(pred, fact)); } } diff --git a/src/muz/rel/udoc_relation.cpp b/src/muz/rel/udoc_relation.cpp index 1e448f861..f23dfbf70 100644 --- a/src/muz/rel/udoc_relation.cpp +++ b/src/muz/rel/udoc_relation.cpp @@ -1,3 +1,65 @@ +/*++ +Copyright (c) 2014 Microsoft Corporation + +Module Name: + + udoc_relation.cpp + +Abstract: + + Relation based on union of DOCs. + +Author: + + Nuno Lopes (a-nlopes) 2013-03-01 + Nikolaj Bjorner (nbjorner) 2014-09-15 + +Revision History: + + Revised version of dl_hassel_diff facilities. + +Notes: + + Current pending items: + - Fix the incomplete non-emptiness check in doc.cpp + It can fall back to a sat_solver call in the worst case. + The sat_solver.h interface gives a way to add clauses to a sat solver + and check for satisfiability. It can be used from scratch each time. + - Profile and fix bottlnecks: + - Potential bottleneck in projection exercised in some benchmarks. + Projection is asymptotically very expensive. We are here interested in + handling common/cheap cases efficiently. + - Simplification of udoc and utbv (from negated tails) after operations such as join and union. + - The current simplification is between cheap and expensive. Some low-cost simplification + based on sorting + coallescing and detecting empty docs could be used. + - There are several places where code copies a sequence of bits from one vector to another. + Any such places in udoc_relation should be shifted down to 'doc_manager'. Loops in 'doc_manager' + should be shifted down to 'tbv_manager' and loops there should be moved to 'fixed_bitvector_manager'. + Finally, more efficient and general implementations of non-aligned copies are useful where such + bottlnecks show up on the radar. + - Fix filter_by_negated. + Current implementation seems incorrect. The fast path seems right, but the slow path does not. + Recall the semantics: + filter_by_negation(tgt, neg, columns in tgt: c1,...,cN, + corresponding columns in neg: d1,...,dN): + tgt := {x: x\in tgt_0 && ! \exists y: ( y \in neg & pi_c1(x)= pi_d1(y) & ... & pi_cN(x)= pi_dN(y) ) } + We are given tgt, and neg as two udocs. + The fast pass removes doc's t from tgt where we can establish + that for every x in t there is a n in neg and a y in n, + such that projections(x) = projections(y). + This is claimed to be the case if projections(n) contains projections(t). + + The slow pass uses the projection to create a doc n' from each n that has the same signature as tgt. + It then subtracts each n'. The way n' is created is by copying bits from n. + This seems wrong, for example if the projection contains overlapping regions. + Here is a possible corrected version: + define join_project(tgt, neg, c1, .., cN, d1, .. , dN) as + exists y : y \in neg & x in tgt & pi_c1(x)= pi_d1(y) & ... & pi_cN(x)= pi_dN(y) ) + return tgt \ join_project(tgt, neg, c1, .., cN, d1, .. , dN) + We have most of the facilities required for a join project operation. + For example, the filter_project function uses both equalities and deleted columns. + +--*/ #include "udoc_relation.h" #include "dl_relation_manager.h" #include "qe_util.h" diff --git a/src/muz/tab/tab_context.cpp b/src/muz/tab/tab_context.cpp index d75ebe20e..3175d1622 100644 --- a/src/muz/tab/tab_context.cpp +++ b/src/muz/tab/tab_context.cpp @@ -765,7 +765,7 @@ namespace tb { m_weight_multiply(1.0), m_update_frequency(20), m_next_update(20) { - set_strategy(ctx.get_params().tab_selection()); + set_strategy(ctx.tab_selection()); } void init(rules const& rs) { diff --git a/src/muz/transforms/dl_mk_bit_blast.cpp b/src/muz/transforms/dl_mk_bit_blast.cpp index fcd20d78f..8f4c840eb 100644 --- a/src/muz/transforms/dl_mk_bit_blast.cpp +++ b/src/muz/transforms/dl_mk_bit_blast.cpp @@ -262,7 +262,7 @@ namespace datalog { rule_set * operator()(rule_set const & source) { // TODO pc - if (!m_context.bit_blast()) { + if (!m_context.xform_bit_blast()) { return 0; } rule_manager& rm = m_context.get_rule_manager();