mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable
This commit is contained in:
commit
6255f5a178
|
@ -151,7 +151,7 @@ public:
|
|||
void set_index(int idx) { m_symbol_index = idx; }
|
||||
};
|
||||
|
||||
TreeNode* MkToken(alloc_region& r, char* token, int symbolIndex) {
|
||||
TreeNode* MkToken(alloc_region& r, char const* token, int symbolIndex) {
|
||||
TreeNode* ss;
|
||||
char* symbol = tptp_lval[symbolIndex];
|
||||
ss = new (r) TreeNode(r, symbol, NULL,NULL,NULL,NULL,NULL,NULL,NULL,NULL,NULL,NULL);
|
||||
|
|
|
@ -27,6 +27,7 @@ Revision History:
|
|||
#include"ast_smt2_pp.h"
|
||||
#include"datatype_decl_plugin.h"
|
||||
#include"scoped_proof.h"
|
||||
#include"fixedpoint_params.hpp"
|
||||
|
||||
|
||||
namespace datalog {
|
||||
|
@ -199,7 +200,7 @@ namespace datalog {
|
|||
m_register_engine(re),
|
||||
m_fparams(fp),
|
||||
m_params_ref(pa),
|
||||
m_params(m_params_ref),
|
||||
m_params(alloc(fixedpoint_params, m_params_ref)),
|
||||
m_decl_util(m),
|
||||
m_rewriter(m),
|
||||
m_var_subst(m),
|
||||
|
@ -263,6 +264,31 @@ namespace datalog {
|
|||
return *m_sorts.find(s);
|
||||
}
|
||||
|
||||
|
||||
bool context::generate_proof_trace() const { return m_params->generate_proof_trace(); }
|
||||
bool context::output_profile() const { return m_params->output_profile(); }
|
||||
bool context::output_tuples() const { return m_params->output_tuples(); }
|
||||
bool context::use_map_names() const { return m_params->use_map_names(); }
|
||||
bool context::fix_unbound_vars() const { return m_params->fix_unbound_vars(); }
|
||||
symbol context::default_table() const { return m_params->default_table(); }
|
||||
symbol context::default_relation() const { return m_params->default_relation(); } // external_relation_plugin::get_name());
|
||||
symbol context::default_table_checker() const { return m_params->default_table_checker(); }
|
||||
bool context::default_table_checked() const { return m_params->default_table_checked(); }
|
||||
bool context::dbg_fpr_nonempty_relation_signature() const { return m_params->dbg_fpr_nonempty_relation_signature(); }
|
||||
unsigned context::dl_profile_milliseconds_threshold() const { return m_params->profile_timeout_milliseconds(); }
|
||||
bool context::all_or_nothing_deltas() const { return m_params->all_or_nothing_deltas(); }
|
||||
bool context::compile_with_widening() const { return m_params->compile_with_widening(); }
|
||||
bool context::unbound_compressor() const { return m_params->unbound_compressor(); }
|
||||
bool context::similarity_compressor() const { return m_params->similarity_compressor(); }
|
||||
unsigned context::similarity_compressor_threshold() const { return m_params->similarity_compressor_threshold(); }
|
||||
unsigned context::soft_timeout() const { return m_fparams.m_soft_timeout; }
|
||||
unsigned context::initial_restart_timeout() const { return m_params->initial_restart_timeout(); }
|
||||
bool context::generate_explanations() const { return m_params->generate_explanations(); }
|
||||
bool context::explanations_on_relation_level() const { return m_params->explanations_on_relation_level(); }
|
||||
bool context::magic_sets_for_queries() const { return m_params->magic_sets_for_queries(); }
|
||||
bool context::eager_emptiness_checking() const { return m_params->eager_emptiness_checking(); }
|
||||
|
||||
|
||||
void context::register_finite_sort(sort * s, sort_kind k) {
|
||||
m_pinned.push_back(s);
|
||||
SASSERT(!m_sorts.contains(s));
|
||||
|
@ -861,7 +887,7 @@ namespace datalog {
|
|||
};
|
||||
|
||||
void context::configure_engine() {
|
||||
symbol e = m_params.engine();
|
||||
symbol e = m_params->engine();
|
||||
|
||||
if (e == symbol("datalog")) {
|
||||
m_engine_type = DATALOG_ENGINE;
|
||||
|
@ -1082,9 +1108,9 @@ namespace datalog {
|
|||
expr_ref fml(m);
|
||||
expr_ref_vector rules(m);
|
||||
svector<symbol> names;
|
||||
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();
|
||||
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);
|
||||
|
||||
|
|
|
@ -43,6 +43,8 @@ Revision History:
|
|||
#include"expr_functors.h"
|
||||
#include"dl_engine_base.h"
|
||||
|
||||
struct fixedpoint_params;
|
||||
|
||||
namespace datalog {
|
||||
|
||||
enum execution_result {
|
||||
|
@ -168,7 +170,7 @@ namespace datalog {
|
|||
register_engine_base& m_register_engine;
|
||||
smt_params & m_fparams;
|
||||
params_ref m_params_ref;
|
||||
fixedpoint_params m_params;
|
||||
fixedpoint_params* m_params;
|
||||
dl_decl_util m_decl_util;
|
||||
th_rewriter m_rewriter;
|
||||
var_subst m_var_subst;
|
||||
|
@ -231,33 +233,35 @@ namespace datalog {
|
|||
ast_manager & get_manager() const { return m; }
|
||||
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; }
|
||||
fixedpoint_params const& get_params() const { return *m_params; }
|
||||
DL_ENGINE get_engine() { configure_engine(); return m_engine_type; }
|
||||
register_engine_base& get_register_engine() { return m_register_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 generate_proof_trace() const { return m_params.generate_proof_trace(); }
|
||||
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.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(); }
|
||||
bool generate_proof_trace() const;
|
||||
bool output_profile() const;
|
||||
bool output_tuples() const;
|
||||
bool use_map_names() const;
|
||||
bool fix_unbound_vars() const;
|
||||
symbol default_table() const;
|
||||
symbol default_relation() const;
|
||||
symbol default_table_checker() const;
|
||||
bool default_table_checked() const;
|
||||
bool dbg_fpr_nonempty_relation_signature() const;
|
||||
unsigned dl_profile_milliseconds_threshold() const;
|
||||
bool all_or_nothing_deltas() const;
|
||||
bool compile_with_widening() const;
|
||||
bool unbound_compressor() const;
|
||||
bool similarity_compressor() 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 eager_emptiness_checking() const;
|
||||
|
||||
void register_finite_sort(sort * s, sort_kind k);
|
||||
|
||||
|
|
|
@ -30,9 +30,32 @@ Revision History:
|
|||
#include"dl_context.h"
|
||||
#include"dl_rule.h"
|
||||
#include"dl_util.h"
|
||||
#include"stopwatch.h"
|
||||
|
||||
namespace datalog {
|
||||
|
||||
static unsigned verbose_action_inside = 0;
|
||||
|
||||
verbose_action::verbose_action(char const* msg, unsigned lvl): m_lvl(lvl), m_sw(0) {
|
||||
IF_VERBOSE(m_lvl,
|
||||
(verbose_stream() << msg << "...").flush();
|
||||
m_sw = alloc(stopwatch);
|
||||
m_sw->start(););
|
||||
}
|
||||
|
||||
verbose_action::~verbose_action() {
|
||||
double sec = 0.0;
|
||||
if (m_sw) m_sw->stop();
|
||||
sec = m_sw?m_sw->get_seconds():0.0;
|
||||
if (sec < 0.001) sec = 0.0;
|
||||
IF_VERBOSE(m_lvl,
|
||||
(verbose_stream() << sec << "s\n").flush();
|
||||
);
|
||||
dealloc(m_sw);
|
||||
}
|
||||
|
||||
|
||||
|
||||
|
||||
bool contains_var(expr * trm, unsigned var_idx) {
|
||||
ptr_vector<sort> vars;
|
||||
|
|
|
@ -26,7 +26,6 @@ Revision History:
|
|||
#include"horn_subsume_model_converter.h"
|
||||
#include"replace_proof_converter.h"
|
||||
#include"substitution.h"
|
||||
#include"fixedpoint_params.hpp"
|
||||
#include"ast_counter.h"
|
||||
#include"statistics.h"
|
||||
#include"lbool.h"
|
||||
|
@ -43,6 +42,14 @@ namespace datalog {
|
|||
class relation_fact;
|
||||
class relation_signature;
|
||||
|
||||
class verbose_action {
|
||||
unsigned m_lvl;
|
||||
class stopwatch* m_sw;
|
||||
public:
|
||||
verbose_action(char const* msg, unsigned lvl = 1);
|
||||
~verbose_action();
|
||||
};
|
||||
|
||||
enum PDR_CACHE_MODE {
|
||||
NO_CACHE,
|
||||
HASH_CACHE,
|
||||
|
@ -706,29 +713,6 @@ namespace datalog {
|
|||
dealloc(ptr);
|
||||
}
|
||||
|
||||
template<typename T>
|
||||
class scoped_rel {
|
||||
T* m_t;
|
||||
public:
|
||||
scoped_rel(T* t) : m_t(t) {}
|
||||
~scoped_rel() { if (m_t) { universal_delete(m_t); } }
|
||||
scoped_rel() : m_t(0) {}
|
||||
scoped_rel& operator=(T* t) { if (m_t) { universal_delete(m_t); } m_t = t; return *this; }
|
||||
T* operator->() { return m_t; }
|
||||
const T* operator->() const { return m_t; }
|
||||
T& operator*() { return *m_t; }
|
||||
const T& operator*() const { return *m_t; }
|
||||
operator bool() const { return m_t!=0; }
|
||||
T* get() const { return m_t; }
|
||||
/**
|
||||
\brief Remove object from \c scoped_rel without deleting it.
|
||||
*/
|
||||
T* release() {
|
||||
T* res = m_t;
|
||||
m_t = 0;
|
||||
return res;
|
||||
}
|
||||
};
|
||||
|
||||
/**
|
||||
\brief If it is possible to convert the beginning of \c s to uint64,
|
||||
|
|
|
@ -32,6 +32,7 @@ Revision History:
|
|||
#include "dl_transforms.h"
|
||||
#include "dl_mk_rule_inliner.h"
|
||||
#include "scoped_proof.h"
|
||||
#include"fixedpoint_params.hpp"
|
||||
|
||||
namespace datalog {
|
||||
|
||||
|
|
|
@ -1164,7 +1164,7 @@ public:
|
|||
: dparser(ctx, ctx.get_manager()),
|
||||
m_bool_sort(ctx.get_manager()),
|
||||
m_short_sort(ctx.get_manager()),
|
||||
m_use_map_names(ctx.get_params().use_map_names()) {
|
||||
m_use_map_names(ctx.use_map_names()) {
|
||||
}
|
||||
~wpa_parser_impl() {
|
||||
reset_dealloc_values(m_sort_contents);
|
||||
|
|
|
@ -30,6 +30,7 @@ Notes:
|
|||
#include"scoped_ctrl_c.h"
|
||||
#include"scoped_timer.h"
|
||||
#include"trail.h"
|
||||
#include"fixedpoint_params.hpp"
|
||||
#include<iomanip>
|
||||
|
||||
|
||||
|
|
|
@ -27,6 +27,7 @@ Revision History:
|
|||
#include"dl_mk_slice.h"
|
||||
#include"filter_model_converter.h"
|
||||
#include"dl_transforms.h"
|
||||
#include"fixedpoint_params.hpp"
|
||||
|
||||
class horn_tactic : public tactic {
|
||||
struct imp {
|
||||
|
|
|
@ -77,9 +77,9 @@ 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, head->get_name()),
|
||||
m_sig(m), m_solver(pm, ctx.get_params(), head->get_name()),
|
||||
m_invariants(m), m_transition(m), m_initial_state(m),
|
||||
m_reachable(pm, pm.get_params()) {}
|
||||
m_reachable(pm, (datalog::PDR_CACHE_MODE)ctx.get_params().cache_mode()) {}
|
||||
|
||||
pred_transformer::~pred_transformer() {
|
||||
rule2inst::iterator it2 = m_rule2inst.begin(), end2 = m_rule2inst.end();
|
||||
|
@ -1239,7 +1239,7 @@ namespace pdr {
|
|||
m_params(params),
|
||||
m(m),
|
||||
m_context(0),
|
||||
m_pm(m_fparams, params, m),
|
||||
m_pm(m_fparams, params.max_num_contexts(), m),
|
||||
m_query_pred(m),
|
||||
m_query(0),
|
||||
m_search(m_params.bfs_model_search()),
|
||||
|
|
|
@ -28,6 +28,7 @@ Revision History:
|
|||
#include "pdr_manager.h"
|
||||
#include "pdr_prop_solver.h"
|
||||
#include "pdr_reachable_cache.h"
|
||||
#include "fixedpoint_params.hpp"
|
||||
|
||||
|
||||
namespace datalog {
|
||||
|
|
|
@ -166,14 +166,13 @@ namespace pdr {
|
|||
return res;
|
||||
}
|
||||
|
||||
manager::manager(smt_params& fparams, fixedpoint_params const& params, ast_manager& manager) :
|
||||
manager::manager(smt_params& fparams, unsigned max_num_contexts, ast_manager& manager) :
|
||||
m(manager),
|
||||
m_fparams(fparams),
|
||||
m_params(params),
|
||||
m_brwr(m),
|
||||
m_mux(m, get_state_suffixes()),
|
||||
m_background(m.mk_true(), m),
|
||||
m_contexts(fparams, params, m),
|
||||
m_contexts(fparams, max_num_contexts, m),
|
||||
m_next_unique_num(0)
|
||||
{
|
||||
}
|
||||
|
|
|
@ -78,7 +78,6 @@ namespace pdr {
|
|||
{
|
||||
ast_manager& m;
|
||||
smt_params& m_fparams;
|
||||
fixedpoint_params const& m_params;
|
||||
|
||||
mutable bool_rewriter m_brwr;
|
||||
|
||||
|
@ -99,12 +98,10 @@ namespace pdr {
|
|||
void add_new_state(func_decl * s);
|
||||
|
||||
public:
|
||||
manager(smt_params& fparams, fixedpoint_params const& params,
|
||||
ast_manager & manager);
|
||||
manager(smt_params& fparams, unsigned max_num_contexts, ast_manager & manager);
|
||||
|
||||
ast_manager& get_manager() const { return m; }
|
||||
smt_params& get_fparams() const { return m_fparams; }
|
||||
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);
|
||||
|
|
|
@ -30,6 +30,7 @@ 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
|
||||
|
@ -225,12 +226,12 @@ namespace pdr {
|
|||
};
|
||||
|
||||
|
||||
prop_solver::prop_solver(manager& pm, symbol const& name) :
|
||||
prop_solver::prop_solver(manager& pm, fixedpoint_params const& p, symbol const& name) :
|
||||
m_fparams(pm.get_fparams()),
|
||||
m(pm.get_manager()),
|
||||
m_pm(pm),
|
||||
m_name(name),
|
||||
m_try_minimize_core(pm.get_params().try_minimize_core()),
|
||||
m_try_minimize_core(p.try_minimize_core()),
|
||||
m_ctx(pm.mk_fresh()),
|
||||
m_pos_level_atoms(m),
|
||||
m_neg_level_atoms(m),
|
||||
|
|
|
@ -31,6 +31,8 @@ Revision History:
|
|||
#include "pdr_manager.h"
|
||||
#include "pdr_smt_context_manager.h"
|
||||
|
||||
struct fixedpoint_params;
|
||||
|
||||
namespace pdr {
|
||||
class prop_solver {
|
||||
|
||||
|
@ -73,7 +75,7 @@ namespace pdr {
|
|||
|
||||
|
||||
public:
|
||||
prop_solver(pdr::manager& pm, symbol const& name);
|
||||
prop_solver(pdr::manager& pm, fixedpoint_params const& p, symbol const& name);
|
||||
|
||||
/** return true is s is a symbol introduced by prop_solver */
|
||||
bool is_aux_symbol(func_decl * s) const {
|
||||
|
|
|
@ -21,13 +21,13 @@ Revision History:
|
|||
|
||||
namespace pdr {
|
||||
|
||||
reachable_cache::reachable_cache(pdr::manager & pm, fixedpoint_params const& params)
|
||||
reachable_cache::reachable_cache(pdr::manager & pm, datalog::PDR_CACHE_MODE cm)
|
||||
: 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.cache_mode()) {
|
||||
m_cache_mode(cm) {
|
||||
if (m_cache_mode == datalog::CONSTRAINT_CACHE) {
|
||||
m_ctx = pm.mk_fresh();
|
||||
m_ctx->assert_expr(m_pm.get_background());
|
||||
|
|
|
@ -47,7 +47,7 @@ namespace pdr {
|
|||
void add_disjuncted_formula(expr * f);
|
||||
|
||||
public:
|
||||
reachable_cache(pdr::manager & pm, fixedpoint_params const& params);
|
||||
reachable_cache(pdr::manager & pm, datalog::PDR_CACHE_MODE cm);
|
||||
|
||||
void add_init(app * f) { add_disjuncted_formula(f); }
|
||||
|
||||
|
|
|
@ -113,10 +113,10 @@ namespace pdr {
|
|||
return m_context.get_proof();
|
||||
}
|
||||
|
||||
smt_context_manager::smt_context_manager(smt_params& fp, fixedpoint_params const& p, ast_manager& m):
|
||||
smt_context_manager::smt_context_manager(smt_params& fp, unsigned max_num_contexts, ast_manager& m):
|
||||
m_fparams(fp),
|
||||
m(m),
|
||||
m_max_num_contexts(p.max_num_contexts()),
|
||||
m_max_num_contexts(max_num_contexts),
|
||||
m_num_contexts(0),
|
||||
m_predicate_list(m) {
|
||||
}
|
||||
|
|
|
@ -97,7 +97,7 @@ namespace pdr {
|
|||
app_ref_vector m_predicate_list;
|
||||
func_decl_set m_predicate_set;
|
||||
public:
|
||||
smt_context_manager(smt_params& fp, fixedpoint_params const& p, ast_manager& m);
|
||||
smt_context_manager(smt_params& fp, unsigned max_num_contexts, ast_manager& m);
|
||||
~smt_context_manager();
|
||||
smt_context* mk_fresh();
|
||||
void collect_statistics(statistics& st) const;
|
||||
|
|
|
@ -37,7 +37,6 @@ Notes:
|
|||
#include "rewriter_def.h"
|
||||
#include "util.h"
|
||||
#include "pdr_manager.h"
|
||||
#include "pdr_prop_solver.h"
|
||||
#include "pdr_util.h"
|
||||
#include "arith_decl_plugin.h"
|
||||
#include "expr_replacer.h"
|
||||
|
|
|
@ -35,6 +35,30 @@ namespace datalog {
|
|||
class context;
|
||||
class relation_manager;
|
||||
|
||||
template<typename T>
|
||||
class scoped_rel {
|
||||
T* m_t;
|
||||
public:
|
||||
scoped_rel(T* t) : m_t(t) {}
|
||||
~scoped_rel() { if (m_t) { universal_delete(m_t); } }
|
||||
scoped_rel() : m_t(0) {}
|
||||
scoped_rel& operator=(T* t) { if (m_t && t != m_t) { universal_delete(m_t); } m_t = t; return *this; }
|
||||
T* operator->() { return m_t; }
|
||||
const T* operator->() const { return m_t; }
|
||||
T& operator*() { return *m_t; }
|
||||
const T& operator*() const { return *m_t; }
|
||||
operator bool() const { return m_t!=0; }
|
||||
T* get() const { return m_t; }
|
||||
/**
|
||||
\brief Remove object from \c scoped_rel without deleting it.
|
||||
*/
|
||||
T* release() {
|
||||
T* res = m_t;
|
||||
m_t = 0;
|
||||
return res;
|
||||
}
|
||||
};
|
||||
|
||||
ast_manager & get_ast_manager_from_rel_manager(const relation_manager & rm);
|
||||
context & get_context_from_rel_manager(const relation_manager & rm);
|
||||
|
||||
|
@ -208,6 +232,11 @@ namespace datalog {
|
|||
virtual void operator()(base_object & t, const base_object & intersected_obj) = 0;
|
||||
};
|
||||
|
||||
class intersection_join_filter_fn : public base_fn {
|
||||
public:
|
||||
virtual void operator()(base_object & t, const base_object & inter1, const base_object& inter2) = 0;
|
||||
};
|
||||
|
||||
class default_join_project_fn;
|
||||
|
||||
/**
|
||||
|
@ -303,6 +332,7 @@ namespace datalog {
|
|||
protected:
|
||||
//see \c relation_manager for documentation of the operations
|
||||
|
||||
|
||||
virtual join_fn * mk_join_fn(const base_object & t1, const base_object & t2,
|
||||
unsigned col_cnt, const unsigned * cols1, const unsigned * cols2) { return 0; }
|
||||
|
||||
|
@ -348,10 +378,22 @@ namespace datalog {
|
|||
const unsigned * t_cols, const unsigned * src_cols)
|
||||
{ return 0; }
|
||||
|
||||
|
||||
virtual intersection_filter_fn * mk_filter_by_negation_fn(const base_object & t,
|
||||
const base_object & negated_obj, unsigned joined_col_cnt,
|
||||
const unsigned * t_cols, const unsigned * negated_cols)
|
||||
{ return 0; }
|
||||
|
||||
virtual intersection_join_filter_fn * mk_filter_by_negated_join_fn(
|
||||
const base_object & t,
|
||||
const base_object & src1,
|
||||
const base_object & src2,
|
||||
unsigned_vector const& t_cols,
|
||||
unsigned_vector const& src_cols,
|
||||
unsigned_vector const& src1_cols,
|
||||
unsigned_vector const& src2_cols)
|
||||
{ return 0; }
|
||||
|
||||
};
|
||||
|
||||
class base_ancestor {
|
||||
|
@ -685,6 +727,7 @@ namespace datalog {
|
|||
typedef relation_infrastructure::union_fn relation_union_fn;
|
||||
typedef relation_infrastructure::mutator_fn relation_mutator_fn;
|
||||
typedef relation_infrastructure::intersection_filter_fn relation_intersection_filter_fn;
|
||||
typedef relation_infrastructure::intersection_join_filter_fn relation_intersection_join_filter_fn;
|
||||
|
||||
typedef relation_infrastructure::convenient_join_fn convenient_relation_join_fn;
|
||||
typedef relation_infrastructure::convenient_join_project_fn convenient_relation_join_project_fn;
|
||||
|
@ -807,6 +850,7 @@ namespace datalog {
|
|||
typedef table_infrastructure::union_fn table_union_fn;
|
||||
typedef table_infrastructure::mutator_fn table_mutator_fn;
|
||||
typedef table_infrastructure::intersection_filter_fn table_intersection_filter_fn;
|
||||
typedef table_infrastructure::intersection_join_filter_fn table_intersection_join_filter_fn;
|
||||
|
||||
typedef table_infrastructure::convenient_join_fn convenient_table_join_fn;
|
||||
typedef table_infrastructure::convenient_join_project_fn convenient_table_join_project_fn;
|
||||
|
|
|
@ -882,7 +882,8 @@ namespace datalog {
|
|||
for (unsigned j = 0; j < neg_len; ++j) {
|
||||
expr * e = neg_tail->get_arg(j);
|
||||
if (is_var(e)) {
|
||||
neg_vars.insert(to_var(e)->get_idx(), e);
|
||||
unsigned idx = to_var(e)->get_idx();
|
||||
neg_vars.insert(idx, e);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
@ -893,7 +894,7 @@ namespace datalog {
|
|||
pos_vars.insert(to_var(e)->get_idx());
|
||||
}
|
||||
}
|
||||
// add negative variables that are not in positive:
|
||||
// add negative variables that are not in positive
|
||||
u_map<expr*>::iterator it = neg_vars.begin(), end = neg_vars.end();
|
||||
for (; it != end; ++it) {
|
||||
unsigned v = it->m_key;
|
||||
|
|
468
src/muz/rel/dl_lazy_table.cpp
Normal file
468
src/muz/rel/dl_lazy_table.cpp
Normal file
|
@ -0,0 +1,468 @@
|
|||
/*++
|
||||
Copyright (c) 2013 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
dl_lazy_table.cpp
|
||||
|
||||
Abstract:
|
||||
|
||||
<abstract>
|
||||
|
||||
Author:
|
||||
|
||||
Nikolaj Bjorner (nbjorner) 2013-09-04
|
||||
|
||||
Revision History:
|
||||
|
||||
--*/
|
||||
|
||||
#include "dl_lazy_table.h"
|
||||
#include "dl_relation_manager.h"
|
||||
#include <strstream>
|
||||
|
||||
namespace datalog {
|
||||
|
||||
// ------------------
|
||||
// lazy_table_plugin:
|
||||
|
||||
symbol lazy_table_plugin::mk_name(table_plugin& p) {
|
||||
std::ostringstream strm;
|
||||
strm << "lazy_" << p.get_name();
|
||||
return symbol(strm.str().c_str());
|
||||
}
|
||||
|
||||
table_base * lazy_table_plugin::mk_empty(const table_signature & s) {
|
||||
return alloc(lazy_table, alloc(lazy_table_base, *this, m_plugin.mk_empty(s)));
|
||||
}
|
||||
|
||||
lazy_table const& lazy_table_plugin::get(table_base const& tb) { return dynamic_cast<lazy_table const&>(tb); }
|
||||
lazy_table& lazy_table_plugin::get(table_base& tb) { return dynamic_cast<lazy_table&>(tb); }
|
||||
lazy_table const* lazy_table_plugin::get(table_base const* tb) { return dynamic_cast<lazy_table const*>(tb); }
|
||||
lazy_table* lazy_table_plugin::get(table_base* tb) { return dynamic_cast<lazy_table*>(tb); }
|
||||
|
||||
// --------------------------
|
||||
// lazy_table_plugin::join_fn
|
||||
|
||||
class lazy_table_plugin::join_fn : public convenient_table_join_fn {
|
||||
public:
|
||||
join_fn(table_signature const& s1, table_signature const& s2, unsigned col_cnt,
|
||||
unsigned const* cols1, unsigned const* cols2):
|
||||
convenient_table_join_fn(s1, s2, col_cnt, cols1, cols2) {}
|
||||
|
||||
virtual table_base* operator()(const table_base& _t1, const table_base& _t2) {
|
||||
lazy_table const& t1 = get(_t1);
|
||||
lazy_table const& t2 = get(_t2);
|
||||
lazy_table_plugin& p = t1.get_lplugin();
|
||||
lazy_table_ref* tr = alloc(lazy_table_join, m_cols1.size(), m_cols1.c_ptr(), m_cols2.c_ptr(), t1, t2, get_result_signature());
|
||||
return alloc(lazy_table, tr);
|
||||
}
|
||||
};
|
||||
|
||||
table_join_fn * lazy_table_plugin::mk_join_fn(
|
||||
const table_base & t1, const table_base & t2,
|
||||
unsigned col_cnt, const unsigned * cols1, const unsigned * cols2) {
|
||||
if (check_kind(t1) && check_kind(t2)) {
|
||||
return alloc(join_fn, t1.get_signature(), t2.get_signature(), col_cnt, cols1, cols2);
|
||||
}
|
||||
else {
|
||||
return 0;
|
||||
}
|
||||
}
|
||||
|
||||
// ------------------------
|
||||
// lazy_table_plugin::union
|
||||
|
||||
class lazy_table_plugin::union_fn : public table_union_fn {
|
||||
public:
|
||||
void operator()(table_base & _tgt, const table_base & _src,
|
||||
table_base * _delta) {
|
||||
lazy_table& tgt = get(_tgt);
|
||||
lazy_table const& src = get(_src);
|
||||
lazy_table* delta = get(_delta);
|
||||
table_base const* t_src = src.eval();
|
||||
table_base * t_tgt = tgt.eval();
|
||||
table_base * t_delta = delta?delta->eval():0;
|
||||
verbose_action _t("union");
|
||||
table_union_fn* m = tgt.get_lplugin().get_manager().mk_union_fn(*t_tgt, *t_src, t_delta);
|
||||
SASSERT(m);
|
||||
(*m)(*t_tgt, *t_src, t_delta);
|
||||
dealloc(m);
|
||||
}
|
||||
};
|
||||
|
||||
|
||||
table_union_fn* lazy_table_plugin::mk_union_fn(
|
||||
const table_base & tgt, const table_base & src,
|
||||
const table_base * delta) {
|
||||
if (check_kind(tgt) && check_kind(src) && (!delta || check_kind(*delta))) {
|
||||
return alloc(union_fn);
|
||||
}
|
||||
else {
|
||||
return 0;
|
||||
}
|
||||
}
|
||||
|
||||
// --------------------------
|
||||
// lazy_table_plugin::project
|
||||
|
||||
class lazy_table_plugin::project_fn : public convenient_table_project_fn {
|
||||
public:
|
||||
project_fn(table_signature const& orig_sig, unsigned cnt, unsigned const* cols):
|
||||
convenient_table_project_fn(orig_sig, cnt, cols)
|
||||
{}
|
||||
|
||||
virtual table_base* operator()(table_base const& _t) {
|
||||
lazy_table const& t = get(_t);
|
||||
return alloc(lazy_table, alloc(lazy_table_project, m_removed_cols.size(), m_removed_cols.c_ptr(), t, get_result_signature()));
|
||||
}
|
||||
};
|
||||
|
||||
table_transformer_fn * lazy_table_plugin::mk_project_fn(
|
||||
const table_base & t, unsigned col_cnt,
|
||||
const unsigned * removed_cols) {
|
||||
if (check_kind(t)) {
|
||||
return alloc(project_fn, t.get_signature(), col_cnt, removed_cols);
|
||||
}
|
||||
else {
|
||||
return 0;
|
||||
}
|
||||
}
|
||||
|
||||
// -------------------------
|
||||
// lazy_table_plugin::rename
|
||||
|
||||
class lazy_table_plugin::rename_fn : public convenient_table_rename_fn {
|
||||
public:
|
||||
rename_fn(table_signature const& orig_sig, unsigned cnt, unsigned const* cols):
|
||||
convenient_table_rename_fn(orig_sig, cnt, cols)
|
||||
{}
|
||||
|
||||
virtual table_base* operator()(table_base const& _t) {
|
||||
lazy_table const& t = get(_t);
|
||||
return alloc(lazy_table, alloc(lazy_table_rename, m_cycle.size(), m_cycle.c_ptr(), t, get_result_signature()));
|
||||
}
|
||||
};
|
||||
|
||||
table_transformer_fn * lazy_table_plugin::mk_rename_fn(
|
||||
const table_base & t, unsigned col_cnt,
|
||||
const unsigned * removed_cols) {
|
||||
if (check_kind(t)) {
|
||||
return alloc(rename_fn, t.get_signature(), col_cnt, removed_cols);
|
||||
}
|
||||
else {
|
||||
return 0;
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
// -----------------------------------
|
||||
// lazy_table_plugin::filter_identical
|
||||
|
||||
class lazy_table_plugin::filter_identical_fn : public table_mutator_fn {
|
||||
unsigned_vector m_cols;
|
||||
public:
|
||||
filter_identical_fn(unsigned cnt, unsigned const* cols): m_cols(cnt, cols) {}
|
||||
|
||||
virtual void operator()(table_base& _t) {
|
||||
lazy_table& t = get(_t);
|
||||
t.set(alloc(lazy_table_filter_identical, m_cols.size(), m_cols.c_ptr(), t));
|
||||
}
|
||||
};
|
||||
|
||||
table_mutator_fn * lazy_table_plugin::mk_filter_identical_fn(
|
||||
const table_base & t, unsigned col_cnt, const unsigned * identical_cols) {
|
||||
if (check_kind(t)) {
|
||||
return alloc(filter_identical_fn, col_cnt, identical_cols);
|
||||
}
|
||||
else {
|
||||
return 0;
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
// -------------------------------------
|
||||
// lazy_table_plugin::filter_interpreted
|
||||
|
||||
class lazy_table_plugin::filter_interpreted_fn : public table_mutator_fn {
|
||||
app_ref m_condition;
|
||||
public:
|
||||
filter_interpreted_fn(app_ref& p): m_condition(p) {}
|
||||
|
||||
virtual void operator()(table_base& _t) {
|
||||
lazy_table& t = get(_t);
|
||||
t.set(alloc(lazy_table_filter_interpreted, t, m_condition));
|
||||
}
|
||||
};
|
||||
|
||||
table_mutator_fn * lazy_table_plugin::mk_filter_interpreted_fn(
|
||||
const table_base & t, app* condition) {
|
||||
if (check_kind(t)) {
|
||||
app_ref cond(condition, get_ast_manager());
|
||||
return alloc(filter_interpreted_fn, cond);
|
||||
}
|
||||
else {
|
||||
return 0;
|
||||
}
|
||||
}
|
||||
|
||||
// -------------------------------------
|
||||
// lazy_table_plugin::filter_by_negation
|
||||
|
||||
class lazy_table_plugin::filter_by_negation_fn : public table_intersection_filter_fn {
|
||||
unsigned_vector m_cols1;
|
||||
unsigned_vector m_cols2;
|
||||
public:
|
||||
filter_by_negation_fn(unsigned cnt, unsigned const* cols1, unsigned const* cols2):
|
||||
m_cols1(cnt, cols1), m_cols2(cnt, cols2) {}
|
||||
virtual void operator()(table_base & _t, const table_base & _intersected_obj) {
|
||||
lazy_table& t = get(_t);
|
||||
lazy_table const& it = get(_intersected_obj);
|
||||
t.set(alloc(lazy_table_filter_by_negation, t, it, m_cols1, m_cols2));
|
||||
}
|
||||
};
|
||||
|
||||
table_intersection_filter_fn * lazy_table_plugin::mk_filter_by_negation_fn(
|
||||
const table_base & t,
|
||||
const table_base & negated_obj, unsigned joined_col_cnt,
|
||||
const unsigned * t_cols, const unsigned * negated_cols) {
|
||||
if (check_kind(t) && check_kind(negated_obj)) {
|
||||
return alloc(filter_by_negation_fn, joined_col_cnt, t_cols, negated_cols);
|
||||
}
|
||||
else {
|
||||
return 0;
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
// -------------------------------
|
||||
// lazy_table_plugin::filter_equal
|
||||
|
||||
class lazy_table_plugin::filter_equal_fn : public table_mutator_fn {
|
||||
table_element m_value;
|
||||
unsigned m_col;
|
||||
public:
|
||||
filter_equal_fn(const table_element & value, unsigned col):
|
||||
m_value(value),
|
||||
m_col(col)
|
||||
{ }
|
||||
|
||||
virtual void operator()(table_base& _t) {
|
||||
lazy_table& t = get(_t);
|
||||
t.set(alloc(lazy_table_filter_equal, m_col, m_value, t));
|
||||
}
|
||||
};
|
||||
|
||||
table_mutator_fn * lazy_table_plugin::mk_filter_equal_fn(
|
||||
const table_base & t, const table_element & value, unsigned col) {
|
||||
if (check_kind(t)) {
|
||||
return alloc(filter_equal_fn, value, col);
|
||||
}
|
||||
else {
|
||||
return 0;
|
||||
}
|
||||
}
|
||||
|
||||
table_plugin* lazy_table_plugin::mk_sparse(relation_manager& rm) {
|
||||
table_plugin* sp = rm.get_table_plugin(symbol("sparse"));
|
||||
SASSERT(sp);
|
||||
if (sp) {
|
||||
return alloc(lazy_table_plugin, *sp);
|
||||
}
|
||||
else {
|
||||
return 0;
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
// ----------
|
||||
// lazy_table
|
||||
|
||||
table_base * lazy_table::clone() const {
|
||||
table_base* t = eval();
|
||||
verbose_action _t("clone");
|
||||
return alloc(lazy_table, alloc(lazy_table_base, get_lplugin(), t->clone()));
|
||||
}
|
||||
table_base * lazy_table::complement(func_decl* p, const table_element * func_columns) const {
|
||||
table_base* t = eval()->complement(p, func_columns);
|
||||
return alloc(lazy_table, alloc(lazy_table_base, get_lplugin(), t));
|
||||
}
|
||||
bool lazy_table::empty() const {
|
||||
return m_ref->eval()->empty();
|
||||
}
|
||||
bool lazy_table::contains_fact(const table_fact & f) const {
|
||||
return m_ref->eval()->contains_fact(f);
|
||||
}
|
||||
void lazy_table::remove_fact(table_element const* fact) {
|
||||
m_ref->eval()->remove_fact(fact);
|
||||
}
|
||||
void lazy_table::remove_facts(unsigned fact_cnt, const table_fact * facts) {
|
||||
m_ref->eval()->remove_facts(fact_cnt, facts);
|
||||
}
|
||||
void lazy_table::remove_facts(unsigned fact_cnt, const table_element * facts) {
|
||||
m_ref->eval()->remove_facts(fact_cnt, facts);
|
||||
}
|
||||
void lazy_table::reset() {
|
||||
m_ref = alloc(lazy_table_base, get_lplugin(), get_lplugin().m_plugin.mk_empty(get_signature()));
|
||||
}
|
||||
void lazy_table::add_fact(table_fact const& f) {
|
||||
m_ref->eval()->add_fact(f);
|
||||
}
|
||||
table_base::iterator lazy_table::begin() const {
|
||||
return eval()->begin();
|
||||
}
|
||||
table_base::iterator lazy_table::end() const {
|
||||
return eval()->end();
|
||||
}
|
||||
table_base* lazy_table::eval() const {
|
||||
return m_ref->eval();
|
||||
}
|
||||
|
||||
// -------------------------
|
||||
// eval
|
||||
|
||||
|
||||
table_base* lazy_table_join::force() {
|
||||
SASSERT(!m_table);
|
||||
table_base* t1 = m_t1->eval();
|
||||
table_base* t2 = m_t2->eval();
|
||||
verbose_action _t("join");
|
||||
table_join_fn* join = rm().mk_join_fn(*t1, *t2, m_cols1.size(), m_cols1.c_ptr(), m_cols2.c_ptr());
|
||||
m_table = (*join)(*t1, *t2);
|
||||
dealloc(join);
|
||||
return m_table.get();
|
||||
}
|
||||
|
||||
table_base* lazy_table_project::force() {
|
||||
SASSERT(!m_table);
|
||||
switch(m_src->kind()) {
|
||||
case LAZY_TABLE_JOIN: {
|
||||
lazy_table_join& src = dynamic_cast<lazy_table_join&>(*m_src);
|
||||
table_base* t1 = src.t1()->eval();
|
||||
table_base* t2 = src.t2()->eval();
|
||||
table_join_fn* j_fn = rm().mk_join_project_fn(*t1, *t2, src.cols1(), src.cols2(), m_cols);
|
||||
if (j_fn) {
|
||||
verbose_action _t("join_project");
|
||||
m_table = (*j_fn)(*t1, *t2);
|
||||
dealloc(j_fn);
|
||||
}
|
||||
break;
|
||||
}
|
||||
case LAZY_TABLE_FILTER_INTERPRETED: {
|
||||
lazy_table_filter_interpreted& src = dynamic_cast<lazy_table_filter_interpreted&>(*m_src);
|
||||
table_transformer_fn* tr = rm().mk_filter_interpreted_and_project_fn(*src.eval(), src.condition(), m_cols.size(), m_cols.c_ptr());
|
||||
if (tr) {
|
||||
verbose_action _t("filter_interpreted_project");
|
||||
m_table = (*tr)(*src.eval());
|
||||
dealloc(tr);
|
||||
}
|
||||
break;
|
||||
}
|
||||
case LAZY_TABLE_FILTER_EQUAL: {
|
||||
lazy_table_filter_equal& src = dynamic_cast<lazy_table_filter_equal&>(*m_src);
|
||||
table_base* t = src.eval();
|
||||
table_transformer_fn* tr = rm().mk_select_equal_and_project_fn(*t, src.value(), src.col());
|
||||
if (tr) {
|
||||
verbose_action _t("select_equal_project");
|
||||
m_table = (*tr)(*t);
|
||||
dealloc(tr);
|
||||
}
|
||||
break;
|
||||
}
|
||||
default:
|
||||
break;
|
||||
}
|
||||
if (m_table) {
|
||||
return m_table.get();
|
||||
}
|
||||
table_base* src = m_src->eval();
|
||||
verbose_action _t("project");
|
||||
table_transformer_fn* project = rm().mk_project_fn(*src, m_cols.size(), m_cols.c_ptr());
|
||||
SASSERT(project);
|
||||
m_table = (*project)(*src);
|
||||
dealloc(project);
|
||||
return m_table.get();
|
||||
}
|
||||
|
||||
table_base* lazy_table_rename::force() {
|
||||
SASSERT(!m_table);
|
||||
table_base* src = m_src->eval();
|
||||
verbose_action _t("rename");
|
||||
table_transformer_fn* rename = rm().mk_rename_fn(*src, m_cols.size(), m_cols.c_ptr());
|
||||
m_table = (*rename)(*src);
|
||||
dealloc(rename);
|
||||
return m_table.get();
|
||||
}
|
||||
|
||||
table_base* lazy_table_filter_identical::force() {
|
||||
SASSERT(!m_table);
|
||||
m_table = m_src->eval();
|
||||
m_src->release_table();
|
||||
m_src = 0;
|
||||
verbose_action _t("filter_identical");
|
||||
table_mutator_fn* m = rm().mk_filter_identical_fn(*m_table, m_cols.size(), m_cols.c_ptr());
|
||||
SASSERT(m);
|
||||
(*m)(*m_table);
|
||||
dealloc(m);
|
||||
return m_table.get();
|
||||
}
|
||||
|
||||
table_base* lazy_table_filter_equal::force() {
|
||||
SASSERT(!m_table);
|
||||
m_table = m_src->eval();
|
||||
m_src->release_table();
|
||||
m_src = 0;
|
||||
verbose_action _t("filter_equal");
|
||||
table_mutator_fn* m = rm().mk_filter_equal_fn(*m_table, m_value, m_col);
|
||||
SASSERT(m);
|
||||
(*m)(*m_table);
|
||||
dealloc(m);
|
||||
return m_table.get();
|
||||
}
|
||||
|
||||
table_base* lazy_table_filter_interpreted::force() {
|
||||
SASSERT(!m_table);
|
||||
m_table = m_src->eval();
|
||||
m_src->release_table();
|
||||
m_src = 0;
|
||||
verbose_action _t("filter_interpreted");
|
||||
table_mutator_fn* m = rm().mk_filter_interpreted_fn(*m_table, m_condition);
|
||||
SASSERT(m);
|
||||
(*m)(*m_table);
|
||||
dealloc(m);
|
||||
return m_table.get();
|
||||
}
|
||||
|
||||
table_base* lazy_table_filter_by_negation::force() {
|
||||
SASSERT(!m_table);
|
||||
m_table = m_tgt->eval();
|
||||
m_tgt->release_table();
|
||||
m_tgt = 0;
|
||||
|
||||
switch(m_src->kind()) {
|
||||
|
||||
case LAZY_TABLE_JOIN: {
|
||||
lazy_table_join& src = dynamic_cast<lazy_table_join&>(*m_src);
|
||||
table_base* t1 = src.t1()->eval();
|
||||
table_base* t2 = src.t2()->eval();
|
||||
verbose_action _t("filter_by_negation_join");
|
||||
table_intersection_join_filter_fn* jn = rm().mk_filter_by_negated_join_fn(*m_table, *t1, *t2, cols1(), cols2(), src.cols1(), src.cols2());
|
||||
if (jn) {
|
||||
(*jn)(*m_table, *t1, *t2);
|
||||
dealloc(jn);
|
||||
return m_table.get();
|
||||
}
|
||||
break;
|
||||
}
|
||||
default:
|
||||
break;
|
||||
}
|
||||
table_base* src = m_src->eval();
|
||||
verbose_action _t("filter_by_negation");
|
||||
table_intersection_filter_fn* m = rm().mk_filter_by_negation_fn(*m_table, *src, m_cols1, m_cols2);
|
||||
SASSERT(m);
|
||||
(*m)(*m_table, *src);
|
||||
dealloc(m);
|
||||
return m_table.get();
|
||||
}
|
||||
}
|
305
src/muz/rel/dl_lazy_table.h
Normal file
305
src/muz/rel/dl_lazy_table.h
Normal file
|
@ -0,0 +1,305 @@
|
|||
/*++
|
||||
Copyright (c) 2013 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
dl_lazy_table.h
|
||||
|
||||
Abstract:
|
||||
|
||||
Structure for delaying table operations.
|
||||
|
||||
|
||||
Author:
|
||||
|
||||
Nikolaj Bjorner (nbjorner) 2013-09-04
|
||||
|
||||
Revision History:
|
||||
|
||||
--*/
|
||||
|
||||
#ifndef _DL_LAZY_TABLE_H_
|
||||
#define _DL_LAZY_TABLE_H_
|
||||
|
||||
#include "dl_base.h"
|
||||
#include "ref.h"
|
||||
|
||||
namespace datalog {
|
||||
|
||||
class lazy_table;
|
||||
|
||||
class lazy_table_plugin : public table_plugin {
|
||||
friend class lazy_table;
|
||||
class join_fn;
|
||||
class project_fn;
|
||||
class union_fn;
|
||||
class rename_fn;
|
||||
class filter_equal_fn;
|
||||
class filter_identical_fn;
|
||||
class filter_interpreted_fn;
|
||||
class filter_by_negation_fn;
|
||||
|
||||
table_plugin& m_plugin;
|
||||
|
||||
static symbol mk_name(table_plugin& p);
|
||||
|
||||
public:
|
||||
lazy_table_plugin(table_plugin& p):
|
||||
table_plugin(mk_name(p), p.get_manager()),
|
||||
m_plugin(p) {}
|
||||
|
||||
virtual bool can_handle_signature(const table_signature & s) {
|
||||
return m_plugin.can_handle_signature(s);
|
||||
}
|
||||
|
||||
virtual table_base * mk_empty(const table_signature & s);
|
||||
|
||||
virtual void set_cancel(bool f) { m_plugin.set_cancel(f); }
|
||||
|
||||
static table_plugin* mk_sparse(relation_manager& rm);
|
||||
|
||||
protected:
|
||||
virtual table_join_fn * mk_join_fn(
|
||||
const table_base & t1, const table_base & t2,
|
||||
unsigned col_cnt, const unsigned * cols1, const unsigned * cols2);
|
||||
virtual table_union_fn * mk_union_fn(
|
||||
const table_base & tgt, const table_base & src,
|
||||
const table_base * delta);
|
||||
virtual table_transformer_fn * mk_project_fn(
|
||||
const table_base & t, unsigned col_cnt,
|
||||
const unsigned * removed_cols);
|
||||
virtual table_transformer_fn * mk_rename_fn(
|
||||
const table_base & t, unsigned permutation_cycle_len,
|
||||
const unsigned * permutation_cycle);
|
||||
virtual table_mutator_fn * mk_filter_identical_fn(
|
||||
const table_base & t, unsigned col_cnt, const unsigned * identical_cols);
|
||||
virtual table_mutator_fn * mk_filter_equal_fn(
|
||||
const table_base & t, const table_element & value, unsigned col);
|
||||
virtual table_mutator_fn * mk_filter_interpreted_fn(
|
||||
const table_base & t, app * condition);
|
||||
virtual table_intersection_filter_fn * mk_filter_by_negation_fn(
|
||||
const table_base & t,
|
||||
const table_base & negated_obj, unsigned joined_col_cnt,
|
||||
const unsigned * t_cols, const unsigned * negated_cols);
|
||||
|
||||
static lazy_table const& get(table_base const& tb);
|
||||
static lazy_table& get(table_base& tb);
|
||||
static lazy_table const* get(table_base const* tb);
|
||||
static lazy_table* get(table_base* tb);
|
||||
};
|
||||
|
||||
enum lazy_table_kind {
|
||||
LAZY_TABLE_BASE,
|
||||
LAZY_TABLE_JOIN,
|
||||
LAZY_TABLE_PROJECT,
|
||||
LAZY_TABLE_RENAME,
|
||||
LAZY_TABLE_FILTER_IDENTICAL,
|
||||
LAZY_TABLE_FILTER_EQUAL,
|
||||
LAZY_TABLE_FILTER_INTERPRETED,
|
||||
LAZY_TABLE_FILTER_BY_NEGATION
|
||||
};
|
||||
|
||||
class lazy_table_ref {
|
||||
protected:
|
||||
lazy_table_plugin& m_plugin;
|
||||
table_signature m_signature;
|
||||
unsigned m_ref;
|
||||
scoped_rel<table_base> m_table;
|
||||
relation_manager& rm() { return m_plugin.get_manager(); }
|
||||
virtual table_base* force() = 0;
|
||||
public:
|
||||
lazy_table_ref(lazy_table_plugin& p, table_signature const& sig):
|
||||
m_plugin(p), m_signature(sig), m_ref(0) {}
|
||||
virtual ~lazy_table_ref() {}
|
||||
void inc_ref() { ++m_ref; }
|
||||
void dec_ref() { --m_ref; if (0 == m_ref) dealloc(this); }
|
||||
void release_table() { m_table.release(); }
|
||||
|
||||
virtual lazy_table_kind kind() const = 0;
|
||||
table_signature const& get_signature() const { return m_signature; }
|
||||
lazy_table_plugin & get_lplugin() const { return m_plugin; }
|
||||
table_base* eval() { if (!m_table) { m_table = force(); } SASSERT(m_table); return m_table.get(); }
|
||||
};
|
||||
|
||||
class lazy_table : public table_base {
|
||||
protected:
|
||||
mutable ref<lazy_table_ref> m_ref;
|
||||
|
||||
public:
|
||||
lazy_table(lazy_table_ref* t):
|
||||
table_base(t->get_lplugin(), t->get_signature()),
|
||||
m_ref(t)
|
||||
{}
|
||||
|
||||
virtual ~lazy_table() {}
|
||||
|
||||
lazy_table_plugin& get_lplugin() const {
|
||||
return dynamic_cast<lazy_table_plugin&>(table_base::get_plugin());
|
||||
}
|
||||
|
||||
virtual table_base * clone() const;
|
||||
virtual table_base * complement(func_decl* p, const table_element * func_columns = 0) const;
|
||||
virtual bool empty() const;
|
||||
virtual bool contains_fact(const table_fact & f) const;
|
||||
virtual void remove_fact(table_element const* fact);
|
||||
virtual void remove_facts(unsigned fact_cnt, const table_fact * facts);
|
||||
virtual void remove_facts(unsigned fact_cnt, const table_element * facts);
|
||||
virtual void reset();
|
||||
virtual void add_fact(table_fact const& f);
|
||||
|
||||
virtual unsigned get_size_estimate_rows() const { return 1; }
|
||||
virtual unsigned get_size_estimate_bytes() const { return 1; }
|
||||
virtual bool knows_exact_size() const { return false; }
|
||||
|
||||
table_base* eval() const;
|
||||
|
||||
virtual table_base::iterator begin() const;
|
||||
virtual table_base::iterator end() const;
|
||||
|
||||
lazy_table_ref* ref() const { return m_ref.get(); }
|
||||
void set(lazy_table_ref* r) { m_ref = r; }
|
||||
};
|
||||
|
||||
class lazy_table_base : public lazy_table_ref {
|
||||
public:
|
||||
lazy_table_base(lazy_table_plugin & p, table_base* table)
|
||||
: lazy_table_ref(p, table->get_signature()) {
|
||||
m_table = table;
|
||||
// SASSERT(&p.m_plugin == &table->get_lplugin());
|
||||
}
|
||||
virtual ~lazy_table_base() {}
|
||||
virtual lazy_table_kind kind() const { return LAZY_TABLE_BASE; }
|
||||
virtual table_base* force() { return m_table.get(); }
|
||||
};
|
||||
|
||||
class lazy_table_join : public lazy_table_ref {
|
||||
unsigned_vector m_cols1;
|
||||
unsigned_vector m_cols2;
|
||||
ref<lazy_table_ref> m_t1;
|
||||
ref<lazy_table_ref> m_t2;
|
||||
public:
|
||||
lazy_table_join(unsigned col_cnt,
|
||||
const unsigned * cols1, const unsigned * cols2,
|
||||
lazy_table const& t1, lazy_table const& t2, table_signature const& sig)
|
||||
: lazy_table_ref(t1.get_lplugin(), sig),
|
||||
m_cols1(col_cnt, cols1),
|
||||
m_cols2(col_cnt, cols2),
|
||||
m_t1(t1.ref()),
|
||||
m_t2(t2.ref()) { }
|
||||
virtual ~lazy_table_join() {}
|
||||
virtual lazy_table_kind kind() const { return LAZY_TABLE_JOIN; }
|
||||
unsigned_vector const& cols1() const { return m_cols1; }
|
||||
unsigned_vector const& cols2() const { return m_cols2; }
|
||||
lazy_table_ref* t1() const { return m_t1.get(); }
|
||||
lazy_table_ref* t2() const { return m_t2.get(); }
|
||||
virtual table_base* force();
|
||||
};
|
||||
|
||||
|
||||
class lazy_table_project : public lazy_table_ref {
|
||||
unsigned_vector m_cols;
|
||||
ref<lazy_table_ref> m_src;
|
||||
public:
|
||||
lazy_table_project(unsigned col_cnt, const unsigned * cols, lazy_table const& src, table_signature const& sig)
|
||||
: lazy_table_ref(src.get_lplugin(), sig),
|
||||
m_cols(col_cnt, cols),
|
||||
m_src(src.ref()) {}
|
||||
virtual ~lazy_table_project() {}
|
||||
|
||||
virtual lazy_table_kind kind() const { return LAZY_TABLE_PROJECT; }
|
||||
unsigned_vector const& cols() const { return m_cols; }
|
||||
lazy_table_ref* src() const { return m_src.get(); }
|
||||
virtual table_base* force();
|
||||
};
|
||||
|
||||
class lazy_table_rename : public lazy_table_ref {
|
||||
unsigned_vector m_cols;
|
||||
ref<lazy_table_ref> m_src;
|
||||
public:
|
||||
lazy_table_rename(unsigned col_cnt, const unsigned * cols, lazy_table const& src, table_signature const& sig)
|
||||
: lazy_table_ref(src.get_lplugin(), sig),
|
||||
m_cols(col_cnt, cols),
|
||||
m_src(src.ref()) {}
|
||||
virtual ~lazy_table_rename() {}
|
||||
|
||||
virtual lazy_table_kind kind() const { return LAZY_TABLE_RENAME; }
|
||||
unsigned_vector const& cols() const { return m_cols; }
|
||||
lazy_table_ref* src() const { return m_src.get(); }
|
||||
virtual table_base* force();
|
||||
};
|
||||
|
||||
class lazy_table_filter_identical : public lazy_table_ref {
|
||||
unsigned_vector m_cols;
|
||||
ref<lazy_table_ref> m_src;
|
||||
public:
|
||||
lazy_table_filter_identical(unsigned col_cnt, const unsigned * cols, lazy_table const& src)
|
||||
: lazy_table_ref(src.get_lplugin(), src.get_signature()), m_cols(col_cnt, cols), m_src(src.ref()) {}
|
||||
virtual ~lazy_table_filter_identical() {}
|
||||
|
||||
virtual lazy_table_kind kind() const { return LAZY_TABLE_FILTER_IDENTICAL; }
|
||||
unsigned_vector const& cols() const { return m_cols; }
|
||||
lazy_table_ref* src() const { return m_src.get(); }
|
||||
virtual table_base* force();
|
||||
};
|
||||
|
||||
class lazy_table_filter_equal : public lazy_table_ref {
|
||||
unsigned m_col;
|
||||
table_element m_value;
|
||||
ref<lazy_table_ref> m_src;
|
||||
public:
|
||||
lazy_table_filter_equal(unsigned col, table_element value, lazy_table const& src)
|
||||
: lazy_table_ref(src.get_lplugin(), src.get_signature()),
|
||||
m_col(col),
|
||||
m_value(value),
|
||||
m_src(src.ref()) {}
|
||||
virtual ~lazy_table_filter_equal() {}
|
||||
|
||||
virtual lazy_table_kind kind() const { return LAZY_TABLE_FILTER_EQUAL; }
|
||||
unsigned col() const { return m_col; }
|
||||
table_element value() const { return m_value; }
|
||||
lazy_table_ref* src() const { return m_src.get(); }
|
||||
virtual table_base* force();
|
||||
};
|
||||
|
||||
class lazy_table_filter_interpreted : public lazy_table_ref {
|
||||
app_ref m_condition;
|
||||
ref<lazy_table_ref> m_src;
|
||||
public:
|
||||
lazy_table_filter_interpreted(lazy_table const& src, app* condition)
|
||||
: lazy_table_ref(src.get_lplugin(), src.get_signature()),
|
||||
m_condition(condition, src.get_lplugin().get_ast_manager()), m_src(src.ref()) {}
|
||||
virtual ~lazy_table_filter_interpreted() {}
|
||||
|
||||
virtual lazy_table_kind kind() const { return LAZY_TABLE_FILTER_INTERPRETED; }
|
||||
app* condition() const { return m_condition; }
|
||||
lazy_table_ref* src() const { return m_src.get(); }
|
||||
virtual table_base* force();
|
||||
};
|
||||
|
||||
|
||||
class lazy_table_filter_by_negation : public lazy_table_ref {
|
||||
ref<lazy_table_ref> m_tgt;
|
||||
ref<lazy_table_ref> m_src;
|
||||
unsigned_vector m_cols1;
|
||||
unsigned_vector m_cols2;
|
||||
public:
|
||||
lazy_table_filter_by_negation(lazy_table const& tgt, lazy_table const& src,
|
||||
unsigned_vector const& c1, unsigned_vector const& c2)
|
||||
: lazy_table_ref(tgt.get_lplugin(), tgt.get_signature()),
|
||||
m_tgt(tgt.ref()),
|
||||
m_src(src.ref()),
|
||||
m_cols1(c1),
|
||||
m_cols2(c2) {}
|
||||
virtual ~lazy_table_filter_by_negation() {}
|
||||
virtual lazy_table_kind kind() const { return LAZY_TABLE_FILTER_BY_NEGATION; }
|
||||
lazy_table_ref* tgt() const { return m_tgt.get(); }
|
||||
lazy_table_ref* src() const { return m_src.get(); }
|
||||
unsigned_vector const& cols1() const { return m_cols1; }
|
||||
unsigned_vector const& cols2() const { return m_cols2; }
|
||||
virtual table_base* force();
|
||||
};
|
||||
|
||||
|
||||
}
|
||||
|
||||
#endif
|
|
@ -167,8 +167,13 @@ namespace datalog {
|
|||
register_relation_plugin_impl(tr_plugin);
|
||||
m_table_relation_plugins.insert(plugin, tr_plugin);
|
||||
|
||||
if (plugin->get_name()==get_context().default_table()) {
|
||||
m_favourite_table_plugin = plugin;
|
||||
m_favourite_relation_plugin = tr_plugin;
|
||||
}
|
||||
|
||||
symbol checker_name = get_context().default_table_checker();
|
||||
if(get_context().default_table_checked() && get_table_plugin(checker_name)) {
|
||||
if (get_context().default_table_checked() && get_table_plugin(checker_name)) {
|
||||
if( m_favourite_table_plugin &&
|
||||
(plugin==m_favourite_table_plugin || plugin->get_name()==checker_name) ) {
|
||||
symbol checked_name = get_context().default_table();
|
||||
|
@ -178,7 +183,7 @@ namespace datalog {
|
|||
register_plugin(checking_plugin);
|
||||
m_favourite_table_plugin = checking_plugin;
|
||||
}
|
||||
if(m_favourite_relation_plugin && m_favourite_relation_plugin->from_table()) {
|
||||
if (m_favourite_relation_plugin && m_favourite_relation_plugin->from_table()) {
|
||||
table_relation_plugin * fav_rel_plugin =
|
||||
static_cast<table_relation_plugin *>(m_favourite_relation_plugin);
|
||||
if(&fav_rel_plugin->get_table_plugin()==plugin || plugin->get_name()==checker_name) {
|
||||
|
@ -577,6 +582,7 @@ namespace datalog {
|
|||
relation_plugin * p2 = &t2.get_plugin();
|
||||
|
||||
relation_join_fn * res = p1->mk_join_fn(t1, t2, col_cnt, cols1, cols2);
|
||||
|
||||
if(!res && p1!=p2) {
|
||||
res = p2->mk_join_fn(t1, t2, col_cnt, cols1, cols2);
|
||||
}
|
||||
|
@ -1538,6 +1544,19 @@ namespace datalog {
|
|||
return res;
|
||||
}
|
||||
|
||||
|
||||
table_intersection_join_filter_fn* relation_manager::mk_filter_by_negated_join_fn(
|
||||
const table_base & t,
|
||||
const table_base & src1,
|
||||
const table_base & src2,
|
||||
unsigned_vector const& t_cols,
|
||||
unsigned_vector const& src_cols,
|
||||
unsigned_vector const& src1_cols,
|
||||
unsigned_vector const& src2_cols) {
|
||||
return t.get_plugin().mk_filter_by_negated_join_fn(t, src1, src2, t_cols, src_cols, src1_cols, src2_cols);
|
||||
}
|
||||
|
||||
|
||||
|
||||
class relation_manager::default_table_select_equal_and_project_fn : public table_transformer_fn {
|
||||
scoped_ptr<table_mutator_fn> m_filter;
|
||||
|
|
|
@ -564,6 +564,19 @@ namespace datalog {
|
|||
return mk_filter_by_negation_fn(t, negated_obj, t_cols.size(), t_cols.c_ptr(), negated_cols.c_ptr());
|
||||
}
|
||||
|
||||
/**
|
||||
combined filter by negation with a join.
|
||||
*/
|
||||
table_intersection_join_filter_fn* mk_filter_by_negated_join_fn(
|
||||
const table_base & t,
|
||||
const table_base & src1,
|
||||
const table_base & src2,
|
||||
unsigned_vector const& t_cols,
|
||||
unsigned_vector const& src_cols,
|
||||
unsigned_vector const& src1_cols,
|
||||
unsigned_vector const& src2_cols);
|
||||
|
||||
|
||||
/**
|
||||
\c t must contain at least one functional column.
|
||||
|
||||
|
|
|
@ -24,6 +24,7 @@ Revision History:
|
|||
|
||||
namespace datalog {
|
||||
|
||||
|
||||
// -----------------------------------
|
||||
//
|
||||
// entry_storage
|
||||
|
@ -415,7 +416,7 @@ namespace datalog {
|
|||
}
|
||||
//We will change the content of the reserve; which does not change the 'high-level'
|
||||
//content of the table.
|
||||
sparse_table & t = const_cast<sparse_table &>(m_table);
|
||||
sparse_table & t = const_cast<sparse_table&>(m_table);
|
||||
t.write_into_reserve(m_key_fact.c_ptr());
|
||||
|
||||
store_offset res;
|
||||
|
@ -461,6 +462,8 @@ namespace datalog {
|
|||
|
||||
sparse_table::key_indexer& sparse_table::get_key_indexer(unsigned key_len,
|
||||
const unsigned * key_cols) const {
|
||||
verbose_action _va("get_key_indexer");
|
||||
|
||||
#if Z3DEBUG
|
||||
//We allow indexes only on non-functional columns because we want to be able to modify them
|
||||
//without having to worry about updating indexes.
|
||||
|
@ -506,6 +509,7 @@ namespace datalog {
|
|||
}
|
||||
|
||||
bool sparse_table::add_fact(const char * data) {
|
||||
verbose_action _va("add_fact", 3);
|
||||
m_data.write_into_reserve(data);
|
||||
return add_reserve_content();
|
||||
}
|
||||
|
@ -520,6 +524,7 @@ namespace datalog {
|
|||
}
|
||||
|
||||
bool sparse_table::contains_fact(const table_fact & f) const {
|
||||
verbose_action _va("contains_fact", 2);
|
||||
sparse_table & t = const_cast<sparse_table &>(*this);
|
||||
t.write_into_reserve(f.c_ptr());
|
||||
unsigned func_col_cnt = get_signature().functional_columns();
|
||||
|
@ -542,6 +547,7 @@ namespace datalog {
|
|||
}
|
||||
|
||||
bool sparse_table::fetch_fact(table_fact & f) const {
|
||||
verbose_action _va("fetch_fact", 2);
|
||||
const table_signature & sig = get_signature();
|
||||
SASSERT(f.size() == sig.size());
|
||||
if (sig.functional_columns() == 0) {
|
||||
|
@ -567,6 +573,7 @@ namespace datalog {
|
|||
This is ok as long as we do not allow indexing on functional columns.
|
||||
*/
|
||||
void sparse_table::ensure_fact(const table_fact & f) {
|
||||
verbose_action _va("ensure_fact", 2);
|
||||
const table_signature & sig = get_signature();
|
||||
if (sig.functional_columns() == 0) {
|
||||
add_fact(f);
|
||||
|
@ -586,6 +593,7 @@ namespace datalog {
|
|||
}
|
||||
|
||||
void sparse_table::remove_fact(const table_element* f) {
|
||||
verbose_action _va("remove_fact", 2);
|
||||
//first insert the fact so that we find it's original location and remove it
|
||||
write_into_reserve(f);
|
||||
if (!m_data.remove_reserve_content()) {
|
||||
|
@ -638,6 +646,7 @@ namespace datalog {
|
|||
unsigned joined_col_cnt, const unsigned * t1_joined_cols, const unsigned * t2_joined_cols,
|
||||
const unsigned * removed_cols, bool tables_swapped, sparse_table & result) {
|
||||
|
||||
verbose_action _va("join_project", 1);
|
||||
unsigned t1_entry_size = t1.m_fact_size;
|
||||
unsigned t2_entry_size = t2.m_fact_size;
|
||||
|
||||
|
@ -737,15 +746,21 @@ namespace datalog {
|
|||
reset();
|
||||
}
|
||||
|
||||
sparse_table const& sparse_table_plugin::get(table_base const& t) { return dynamic_cast<sparse_table const&>(t); }
|
||||
sparse_table& sparse_table_plugin::get(table_base& t) { return dynamic_cast<sparse_table&>(t); }
|
||||
sparse_table const* sparse_table_plugin::get(table_base const* t) { return dynamic_cast<sparse_table const*>(t); }
|
||||
sparse_table* sparse_table_plugin::get(table_base* t) { return dynamic_cast<sparse_table*>(t); }
|
||||
|
||||
|
||||
void sparse_table_plugin::reset() {
|
||||
table_pool::iterator it = m_pool.begin();
|
||||
table_pool::iterator end = m_pool.end();
|
||||
for (; it!=end; ++it) {
|
||||
sp_table_vector * vect = it->m_value;
|
||||
sp_table_vector::iterator it = vect->begin();
|
||||
sp_table_vector::iterator end = vect->end();
|
||||
for (; it!=end; ++it) {
|
||||
(*it)->destroy(); //calling deallocate() would only put the table back into the pool
|
||||
sp_table_vector::iterator vit = vect->begin();
|
||||
sp_table_vector::iterator vend = vect->end();
|
||||
for (; vit!=vend; ++vit) {
|
||||
(*vit)->destroy(); //calling deallocate() would only put the table back into the pool
|
||||
}
|
||||
dealloc(vect);
|
||||
}
|
||||
|
@ -759,6 +774,7 @@ namespace datalog {
|
|||
}
|
||||
|
||||
void sparse_table_plugin::recycle(sparse_table * t) {
|
||||
verbose_action _va("recycle", 2);
|
||||
const table_signature & sig = t->get_signature();
|
||||
t->reset();
|
||||
|
||||
|
@ -785,7 +801,7 @@ namespace datalog {
|
|||
}
|
||||
|
||||
sparse_table * sparse_table_plugin::mk_clone(const sparse_table & t) {
|
||||
sparse_table * res = static_cast<sparse_table *>(mk_empty(t.get_signature()));
|
||||
sparse_table * res = get(mk_empty(t.get_signature()));
|
||||
res->m_data = t.m_data;
|
||||
return res;
|
||||
}
|
||||
|
@ -813,12 +829,13 @@ namespace datalog {
|
|||
|
||||
virtual table_base * operator()(const table_base & tb1, const table_base & tb2) {
|
||||
|
||||
const sparse_table & t1 = static_cast<const sparse_table &>(tb1);
|
||||
const sparse_table & t2 = static_cast<const sparse_table &>(tb2);
|
||||
verbose_action _va("join_project");
|
||||
const sparse_table & t1 = get(tb1);
|
||||
const sparse_table & t2 = get(tb2);
|
||||
|
||||
sparse_table_plugin & plugin = t1.get_plugin();
|
||||
|
||||
sparse_table * res = static_cast<sparse_table *>(plugin.mk_empty(get_result_signature()));
|
||||
sparse_table * res = get(plugin.mk_empty(get_result_signature()));
|
||||
|
||||
//If we join with some intersection, want to iterate over the smaller table and
|
||||
//do indexing into the bigger one. If we simply do a product, we want the bigger
|
||||
|
@ -868,10 +885,10 @@ namespace datalog {
|
|||
class sparse_table_plugin::union_fn : public table_union_fn {
|
||||
public:
|
||||
virtual void operator()(table_base & tgt0, const table_base & src0, table_base * delta0) {
|
||||
|
||||
sparse_table & tgt = static_cast<sparse_table &>(tgt0);
|
||||
const sparse_table & src = static_cast<const sparse_table &>(src0);
|
||||
sparse_table * delta = static_cast<sparse_table *>(delta0);
|
||||
verbose_action _va("union");
|
||||
sparse_table & tgt = get(tgt0);
|
||||
const sparse_table & src = get(src0);
|
||||
sparse_table * delta = get(delta0);
|
||||
|
||||
unsigned fact_size = tgt.m_fact_size;
|
||||
const char* ptr = src.m_data.begin();
|
||||
|
@ -927,12 +944,13 @@ namespace datalog {
|
|||
}
|
||||
|
||||
virtual table_base * operator()(const table_base & tb) {
|
||||
const sparse_table & t = static_cast<const sparse_table &>(tb);
|
||||
verbose_action _va("project");
|
||||
const sparse_table & t = get(tb);
|
||||
|
||||
unsigned t_fact_size = t.m_fact_size;
|
||||
|
||||
sparse_table_plugin & plugin = t.get_plugin();
|
||||
sparse_table * res = static_cast<sparse_table *>(plugin.mk_empty(get_result_signature()));
|
||||
sparse_table * res = get(plugin.mk_empty(get_result_signature()));
|
||||
|
||||
const sparse_table::column_layout & src_layout = t.m_column_layout;
|
||||
const sparse_table::column_layout & tgt_layout = res->m_column_layout;
|
||||
|
@ -970,10 +988,11 @@ namespace datalog {
|
|||
}
|
||||
|
||||
virtual table_base * operator()(const table_base & tb) {
|
||||
const sparse_table & t = static_cast<const sparse_table &>(tb);
|
||||
verbose_action _va("select_equal_and_project");
|
||||
const sparse_table & t = get(tb);
|
||||
|
||||
sparse_table_plugin & plugin = t.get_plugin();
|
||||
sparse_table * res = static_cast<sparse_table *>(plugin.mk_empty(get_result_signature()));
|
||||
sparse_table * res = get(plugin.mk_empty(get_result_signature()));
|
||||
|
||||
const sparse_table::column_layout & t_layout = t.m_column_layout;
|
||||
const sparse_table::column_layout & res_layout = res->m_column_layout;
|
||||
|
@ -1056,13 +1075,14 @@ namespace datalog {
|
|||
}
|
||||
|
||||
virtual table_base * operator()(const table_base & tb) {
|
||||
verbose_action _va("rename");
|
||||
|
||||
const sparse_table & t = static_cast<const sparse_table &>(tb);
|
||||
const sparse_table & t = get(tb);
|
||||
|
||||
unsigned t_fact_size = t.m_fact_size;
|
||||
|
||||
sparse_table_plugin & plugin = t.get_plugin();
|
||||
sparse_table * res = static_cast<sparse_table *>(plugin.mk_empty(get_result_signature()));
|
||||
sparse_table * res = get(plugin.mk_empty(get_result_signature()));
|
||||
|
||||
size_t res_fact_size = res->m_fact_size;
|
||||
size_t res_data_size = res_fact_size*t.row_count();
|
||||
|
@ -1112,17 +1132,18 @@ namespace datalog {
|
|||
If tgt_is_first is false, contains the same items as \c res.
|
||||
*/
|
||||
idx_set m_intersection_content;
|
||||
|
||||
|
||||
public:
|
||||
negation_filter_fn(const table_base & tgt, const table_base & neg,
|
||||
unsigned joined_col_cnt, const unsigned * t_cols, const unsigned * negated_cols)
|
||||
: convenient_table_negation_filter_fn(tgt, neg, joined_col_cnt, t_cols, negated_cols) {
|
||||
unsigned neg_fisrt_func = neg.get_signature().first_functional();
|
||||
unsigned neg_first_func = neg.get_signature().first_functional();
|
||||
counter ctr;
|
||||
ctr.count(m_cols2);
|
||||
m_joining_neg_non_functional = ctr.get_max_counter_value() == 1
|
||||
&& ctr.get_positive_count() == neg_fisrt_func
|
||||
&& (neg_fisrt_func == 0 || ctr.get_max_positive() == neg_fisrt_func-1);
|
||||
&& ctr.get_positive_count() == neg_first_func
|
||||
&& (neg_first_func == 0 || ctr.get_max_positive() == neg_first_func-1);
|
||||
}
|
||||
|
||||
/**
|
||||
|
@ -1133,9 +1154,7 @@ namespace datalog {
|
|||
bool tgt_is_first, svector<store_offset> & res) {
|
||||
SASSERT(res.empty());
|
||||
|
||||
if (!tgt_is_first) {
|
||||
m_intersection_content.reset();
|
||||
}
|
||||
m_intersection_content.reset();
|
||||
|
||||
unsigned joined_col_cnt = m_cols1.size();
|
||||
unsigned t1_entry_size = t1.m_data.entry_size();
|
||||
|
@ -1194,8 +1213,10 @@ namespace datalog {
|
|||
}
|
||||
|
||||
virtual void operator()(table_base & tgt0, const table_base & neg0) {
|
||||
sparse_table & tgt = static_cast<sparse_table &>(tgt0);
|
||||
const sparse_table & neg = static_cast<const sparse_table &>(neg0);
|
||||
sparse_table & tgt = get(tgt0);
|
||||
const sparse_table & neg = get(neg0);
|
||||
|
||||
verbose_action _va("filter_by_negation");
|
||||
|
||||
if (m_cols1.size() == 0) {
|
||||
if (!neg.empty()) {
|
||||
|
@ -1215,12 +1236,9 @@ namespace datalog {
|
|||
collect_intersection_offsets(tgt, neg, true, to_remove);
|
||||
}
|
||||
|
||||
if (to_remove.empty()) {
|
||||
return;
|
||||
}
|
||||
|
||||
//the largest offsets are at the end, so we can remove them one by one
|
||||
while(!to_remove.empty()) {
|
||||
while (!to_remove.empty()) {
|
||||
store_offset removed_ofs = to_remove.back();
|
||||
to_remove.pop_back();
|
||||
tgt.m_data.remove_offset(removed_ofs);
|
||||
|
@ -1241,6 +1259,148 @@ namespace datalog {
|
|||
return alloc(negation_filter_fn, t, negated_obj, joined_col_cnt, t_cols, negated_cols);
|
||||
}
|
||||
|
||||
/**
|
||||
T \ (S1 Join S2)
|
||||
|
||||
t_cols - columns from T
|
||||
s_cols - columns from (S1 Join S2) that are equated
|
||||
src1_cols - columns from S1 equated with columns from S2
|
||||
src2_cols - columns from S2 equated with columns from S1
|
||||
|
||||
t1_cols - columns from T that map into S1
|
||||
s1_cols - matching columns from s_cols for t1_cols
|
||||
t2s1_cols - columns from T that map into S2, and columns from src1 that join src2
|
||||
s2_cols - matching columns from t2s1_cols
|
||||
|
||||
columns from s2 that are equal to a column from s1 that is in s_cols:
|
||||
|
||||
- ...
|
||||
|
||||
*/
|
||||
|
||||
class sparse_table_plugin::negated_join_fn : public table_intersection_join_filter_fn {
|
||||
typedef sparse_table::store_offset store_offset;
|
||||
typedef sparse_table::key_value key_value;
|
||||
typedef sparse_table::key_indexer key_indexer;
|
||||
unsigned_vector m_t1_cols;
|
||||
unsigned_vector m_s1_cols;
|
||||
unsigned_vector m_t2_cols;
|
||||
unsigned_vector m_s2_cols;
|
||||
unsigned_vector m_src1_cols;
|
||||
public:
|
||||
negated_join_fn(
|
||||
table_base const& src1,
|
||||
unsigned_vector const& t_cols,
|
||||
unsigned_vector const& src_cols,
|
||||
unsigned_vector const& src1_cols,
|
||||
unsigned_vector const& src2_cols):
|
||||
m_src1_cols(src1_cols) {
|
||||
|
||||
// split t_cols and src_cols according to src1, and src2
|
||||
|
||||
unsigned src1_size = src1.get_signature().size();
|
||||
for (unsigned i = 0; i < t_cols.size(); ++i) {
|
||||
if (src_cols[i] < src1_size) {
|
||||
m_t1_cols.push_back(t_cols[i]);
|
||||
m_s1_cols.push_back(src_cols[i]);
|
||||
}
|
||||
else {
|
||||
m_t2_cols.push_back(t_cols[i]);
|
||||
m_s2_cols.push_back(src_cols[i]);
|
||||
}
|
||||
}
|
||||
m_s2_cols.append(src2_cols);
|
||||
}
|
||||
|
||||
virtual void operator()(table_base & _t, const table_base & _s1, const table_base& _s2) {
|
||||
|
||||
verbose_action _va("negated_join");
|
||||
sparse_table& t = get(_t);
|
||||
svector<store_offset> to_remove;
|
||||
collect_to_remove(t, get(_s1), get(_s2), to_remove);
|
||||
for (unsigned i = 0; i < to_remove.size(); ++i) {
|
||||
t.m_data.remove_offset(to_remove[i]);
|
||||
}
|
||||
t.reset_indexes();
|
||||
}
|
||||
|
||||
private:
|
||||
void collect_to_remove(sparse_table& t, sparse_table const& s1, sparse_table const& s2, svector<store_offset>& to_remove) {
|
||||
key_value s1_key, s2_key;
|
||||
SASSERT(&s1 != &s2);
|
||||
SASSERT(m_s1_cols.size() == m_t1_cols.size());
|
||||
SASSERT(m_s2_cols.size() == m_t2_cols.size() + m_src1_cols.size());
|
||||
s1_key.resize(m_s1_cols.size());
|
||||
s2_key.resize(m_s2_cols.size());
|
||||
key_indexer & s1_indexer = s1.get_key_indexer(m_s1_cols.size(), m_s1_cols.c_ptr());
|
||||
key_indexer & s2_indexer = s2.get_key_indexer(m_s2_cols.size(), m_s2_cols.c_ptr());
|
||||
|
||||
store_offset t_after_last = t.m_data.after_last_offset();
|
||||
key_indexer::query_result s1_offsets, s2_offsets;
|
||||
unsigned t_entry_size = t.m_data.entry_size();
|
||||
for (store_offset t_ofs = 0; t_ofs < t_after_last; t_ofs += t_entry_size) {
|
||||
|
||||
if (update_key(s1_key, 0, t, t_ofs, m_t1_cols)) {
|
||||
s1_offsets = s1_indexer.get_matching_offsets(s1_key);
|
||||
}
|
||||
key_indexer::offset_iterator it = s1_offsets.begin();
|
||||
key_indexer::offset_iterator end = s1_offsets.end();
|
||||
for (; it != end; ++it) {
|
||||
store_offset s1_ofs = *it;
|
||||
bool upd1 = update_key(s2_key, 0, t, t_ofs, m_t2_cols);
|
||||
bool upd2 = update_key(s2_key, m_t2_cols.size(), s1, s1_ofs, m_src1_cols);
|
||||
if (upd1 || upd2) {
|
||||
s2_offsets = s2_indexer.get_matching_offsets(s2_key);
|
||||
}
|
||||
if (!s2_offsets.empty()) {
|
||||
to_remove.push_back(t_ofs);
|
||||
break;
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
inline bool update_key(key_value& key, unsigned key_offset, sparse_table const& t, store_offset ofs, unsigned_vector const& cols) {
|
||||
bool modified = false;
|
||||
unsigned sz = cols.size();
|
||||
for (unsigned i = 0; i < sz; ++i) {
|
||||
table_element val = t.get_cell(ofs, cols[i]);
|
||||
modified = update_key(key[i+key_offset], val) || modified;
|
||||
}
|
||||
return modified;
|
||||
}
|
||||
|
||||
inline bool update_key(table_element& tgt, table_element src) {
|
||||
if (tgt == src) {
|
||||
return false;
|
||||
}
|
||||
else {
|
||||
tgt = src;
|
||||
return true;
|
||||
}
|
||||
}
|
||||
|
||||
};
|
||||
|
||||
table_intersection_join_filter_fn* sparse_table_plugin::mk_filter_by_negated_join_fn(
|
||||
const table_base & t,
|
||||
|
||||
|
||||
const table_base & src1,
|
||||
const table_base & src2,
|
||||
unsigned_vector const& t_cols,
|
||||
unsigned_vector const& src_cols,
|
||||
unsigned_vector const& src1_cols,
|
||||
unsigned_vector const& src2_cols) {
|
||||
if (check_kind(t) && check_kind(src1) && check_kind(src2)) {
|
||||
return alloc(negated_join_fn, src1, t_cols, src_cols, src1_cols, src2_cols);
|
||||
}
|
||||
else {
|
||||
return 0;
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
unsigned sparse_table::get_size_estimate_bytes() const {
|
||||
unsigned sz = 0;
|
||||
sz += m_data.get_size_estimate_bytes();
|
||||
|
|
|
@ -48,6 +48,7 @@ namespace datalog {
|
|||
class project_fn;
|
||||
class negation_filter_fn;
|
||||
class select_equal_and_project_fn;
|
||||
class negated_join_fn;
|
||||
|
||||
typedef ptr_vector<sparse_table> sp_table_vector;
|
||||
typedef map<table_signature, sp_table_vector *,
|
||||
|
@ -93,6 +94,20 @@ namespace datalog {
|
|||
virtual table_intersection_filter_fn * mk_filter_by_negation_fn(const table_base & t,
|
||||
const table_base & negated_obj, unsigned joined_col_cnt,
|
||||
const unsigned * t_cols, const unsigned * negated_cols);
|
||||
virtual table_intersection_join_filter_fn* mk_filter_by_negated_join_fn(
|
||||
const table_base & t,
|
||||
const table_base & src1,
|
||||
const table_base & src2,
|
||||
unsigned_vector const& t_cols,
|
||||
unsigned_vector const& src_cols,
|
||||
unsigned_vector const& src1_cols,
|
||||
unsigned_vector const& src2_cols);
|
||||
|
||||
static sparse_table const& get(table_base const&);
|
||||
static sparse_table& get(table_base&);
|
||||
static sparse_table const* get(table_base const*);
|
||||
static sparse_table* get(table_base*);
|
||||
|
||||
};
|
||||
|
||||
class entry_storage {
|
||||
|
|
|
@ -39,16 +39,15 @@ namespace datalog {
|
|||
|
||||
bool table_relation_plugin::can_handle_signature(const relation_signature & s) {
|
||||
table_signature tsig;
|
||||
if(!get_manager().relation_signature_to_table(s, tsig)) {
|
||||
return false;
|
||||
}
|
||||
return m_table_plugin.can_handle_signature(tsig);
|
||||
return
|
||||
get_manager().relation_signature_to_table(s, tsig) &&
|
||||
m_table_plugin.can_handle_signature(tsig);
|
||||
}
|
||||
|
||||
|
||||
relation_base * table_relation_plugin::mk_empty(const relation_signature & s) {
|
||||
table_signature tsig;
|
||||
if(!get_manager().relation_signature_to_table(s, tsig)) {
|
||||
if (!get_manager().relation_signature_to_table(s, tsig)) {
|
||||
return 0;
|
||||
}
|
||||
table_base * t = m_table_plugin.mk_empty(tsig);
|
||||
|
@ -92,6 +91,7 @@ namespace datalog {
|
|||
|
||||
TRACE("dl_table_relation", tout << "# join => "; tres->display(tout););
|
||||
if(&tres->get_plugin()!=&plugin.m_table_plugin) {
|
||||
IF_VERBOSE(1, verbose_stream() << "new type returned\n";);
|
||||
//Operation returned a table of different type than the one which is associated with
|
||||
//this plugin. We need to get a correct table_relation_plugin and create the relation
|
||||
//using it.
|
||||
|
|
|
@ -31,6 +31,7 @@ Revision History:
|
|||
#include"dl_interval_relation.h"
|
||||
#include"karr_relation.h"
|
||||
#include"dl_finite_product_relation.h"
|
||||
#include"dl_lazy_table.h"
|
||||
#include"dl_sparse_table.h"
|
||||
#include"dl_table.h"
|
||||
#include"dl_table_relation.h"
|
||||
|
@ -45,6 +46,7 @@ Revision History:
|
|||
#include"dl_mk_rule_inliner.h"
|
||||
#include"dl_mk_interp_tail_simplifier.h"
|
||||
#include"dl_mk_bit_blast.h"
|
||||
#include"fixedpoint_params.hpp"
|
||||
|
||||
|
||||
namespace datalog {
|
||||
|
@ -96,17 +98,19 @@ namespace datalog {
|
|||
|
||||
// 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()));
|
||||
relation_manager& rm = get_rmanager();
|
||||
|
||||
rm.register_plugin(alloc(sparse_table_plugin, rm));
|
||||
rm.register_plugin(alloc(hashtable_table_plugin, rm));
|
||||
rm.register_plugin(alloc(bitvector_table_plugin, rm));
|
||||
rm.register_plugin(alloc(equivalence_table_plugin, rm));
|
||||
rm.register_plugin(lazy_table_plugin::mk_sparse(rm));
|
||||
|
||||
// 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()));
|
||||
get_rmanager().register_plugin(alloc(karr_relation_plugin, get_rmanager()));
|
||||
rm.register_plugin(alloc(bound_relation_plugin, rm));
|
||||
rm.register_plugin(alloc(interval_relation_plugin, rm));
|
||||
rm.register_plugin(alloc(karr_relation_plugin, rm));
|
||||
}
|
||||
|
||||
rel_context::~rel_context() {
|
||||
|
|
|
@ -30,6 +30,7 @@ Revision History:
|
|||
#include "for_each_expr.h"
|
||||
#include "matcher.h"
|
||||
#include "scoped_proof.h"
|
||||
#include "fixedpoint_params.hpp"
|
||||
|
||||
namespace tb {
|
||||
|
||||
|
|
|
@ -24,6 +24,7 @@ Revision History:
|
|||
#include "expr_safe_replace.h"
|
||||
#include "filter_model_converter.h"
|
||||
#include "dl_mk_interp_tail_simplifier.h"
|
||||
#include "fixedpoint_params.hpp"
|
||||
|
||||
namespace datalog {
|
||||
|
||||
|
|
|
@ -52,14 +52,10 @@ namespace datalog {
|
|||
ptr_vector<func_decl> todo;
|
||||
rule_set::decl2rules body2rules;
|
||||
// initialization for reachability
|
||||
rel_context_base* rc = m_context.get_rel_context();
|
||||
for (rule_set::iterator it = source.begin(); it != source.end(); ++it) {
|
||||
rule * r = *it;
|
||||
all.insert(r->get_decl());
|
||||
bool non_empty =
|
||||
(rc && !rc->is_empty_relation(r->get_decl())) ||
|
||||
r->get_uninterpreted_tail_size() == 0;
|
||||
if (non_empty) {
|
||||
if (r->get_uninterpreted_tail_size() == 0) {
|
||||
if (!reached.contains(r->get_decl())) {
|
||||
reached.insert(r->get_decl());
|
||||
todo.insert(r->get_decl());
|
||||
|
@ -77,6 +73,17 @@ namespace datalog {
|
|||
}
|
||||
}
|
||||
}
|
||||
rel_context_base* rc = m_context.get_rel_context();
|
||||
if (rc) {
|
||||
func_decl_set::iterator fit = all.begin(), fend = all.end();
|
||||
for (; fit != fend; ++fit) {
|
||||
if (!rc->is_empty_relation(*fit) &&
|
||||
!reached.contains(*fit)) {
|
||||
reached.insert(*fit);
|
||||
todo.insert(*fit);
|
||||
}
|
||||
}
|
||||
}
|
||||
// reachability computation
|
||||
while (!todo.empty()) {
|
||||
func_decl * d = todo.back();
|
||||
|
|
|
@ -39,6 +39,7 @@ Revision History:
|
|||
#include"dl_mk_karr_invariants.h"
|
||||
#include"dl_mk_backwards.h"
|
||||
#include"dl_mk_loop_counter.h"
|
||||
#include"fixedpoint_params.hpp"
|
||||
|
||||
namespace datalog {
|
||||
|
||||
|
|
|
@ -54,6 +54,7 @@ Revision History:
|
|||
|
||||
#include"dl_mk_magic_symbolic.h"
|
||||
#include"dl_context.h"
|
||||
#include"fixedpoint_params.hpp"
|
||||
|
||||
namespace datalog {
|
||||
|
||||
|
|
|
@ -23,6 +23,8 @@ Revision History:
|
|||
#include "dl_context.h"
|
||||
#include "expr_safe_replace.h"
|
||||
#include "expr_abstract.h"
|
||||
#include"fixedpoint_params.hpp"
|
||||
|
||||
|
||||
namespace datalog {
|
||||
|
||||
|
|
|
@ -26,6 +26,8 @@ Revision History:
|
|||
#include "dl_mk_quantifier_instantiation.h"
|
||||
#include "dl_context.h"
|
||||
#include "pattern_inference.h"
|
||||
#include "fixedpoint_params.hpp"
|
||||
|
||||
|
||||
namespace datalog {
|
||||
|
||||
|
|
|
@ -52,6 +52,7 @@ Subsumption transformation (remove rule):
|
|||
#include "rewriter.h"
|
||||
#include "rewriter_def.h"
|
||||
#include "dl_mk_rule_inliner.h"
|
||||
#include "fixedpoint_params.hpp"
|
||||
|
||||
namespace datalog {
|
||||
|
||||
|
|
|
@ -18,6 +18,7 @@ Revision History:
|
|||
|
||||
#include"dl_mk_scale.h"
|
||||
#include"dl_context.h"
|
||||
#include"fixedpoint_params.hpp"
|
||||
|
||||
namespace datalog {
|
||||
|
||||
|
|
|
@ -33,6 +33,7 @@ Revision History:
|
|||
#include"dl_mk_quantifier_instantiation.h"
|
||||
#include"dl_mk_subsumption_checker.h"
|
||||
#include"dl_mk_scale.h"
|
||||
#include"fixedpoint_params.hpp"
|
||||
|
||||
namespace datalog {
|
||||
|
||||
|
|
|
@ -232,10 +232,9 @@ unsigned read_datalog(char const * file) {
|
|||
TRACE("dl_compiler", ctx.display(tout);
|
||||
rules_code.display(*ctx.get_rel_context(), tout););
|
||||
|
||||
if (ctx.get_params().output_tuples()) {
|
||||
if (ctx.output_tuples()) {
|
||||
ctx.get_rel_context()->display_output_facts(ctx.get_rules(), std::cout);
|
||||
}
|
||||
|
||||
display_statistics(
|
||||
std::cout,
|
||||
ctx,
|
||||
|
|
Loading…
Reference in a new issue