move some configuration parameters into dl_context, add notes to udoc_relation

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

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(); }

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);
 

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);

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);

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()) {}
 

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),

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 { 

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<const char*>(m_context.get_params().print_aig().c_ptr());
+            if (m_context.print_aig().size()) {
+                const char *filename = static_cast<const char*>(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));
         }
     }

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"

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) {

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();