mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 10:25:18 +00:00
Code Activity

Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable

Browse source
This commit is contained in:
Leonardo de Moura 2012-12-03 16:58:56 -08:00
parent 54e452a1af 1cd1a42618
commit f0f90eecaa
50 changed files with 986 additions and 2517 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/api/api_datalog.cpp
View file

@ -48,7 +48,7 @@ namespace api {
if (!m.has_plugin(name)) {
m.register_plugin(name, alloc(datalog::dl_decl_plugin));
}
datalog::relation_manager& r = m_context.get_rmanager();
datalog::relation_manager& r = m_context.get_rel_context().get_rmanager();
r.register_plugin(alloc(datalog::external_relation_plugin, *this, r));
}
@ -295,7 +295,7 @@ extern "C" {
{
scoped_timer timer(timeout, &eh);
try {
r = to_fixedpoint_ref(d)->ctx().dl_query(num_relations, to_func_decls(relations));
r = to_fixedpoint_ref(d)->ctx().rel_query(num_relations, to_func_decls(relations));
}
catch (z3_exception& ex) {
mk_c(c)->handle_exception(ex);

38
src/api/java/AST.java
View file

@ -37,13 +37,15 @@ public class AST extends Z3Object
**/
public boolean equals(Object o)
{
AST casted = null;
AST casted = null;
try {
casted = AST.class.cast(o);
} catch (ClassCastException e) {
return false;
}
try
{
casted = AST.class.cast(o);
} catch (ClassCastException e)
{
return false;
}
return this.NativeObject() == casted.NativeObject();
}
@ -60,18 +62,20 @@ public class AST extends Z3Object
return 1;
AST oAST = null;
try {
AST.class.cast(other);
} catch (ClassCastException e) {
return 1;
}
try
{
oAST = AST.class.cast(other);
} catch (ClassCastException e)
{
return 1;
}
if (Id() < oAST.Id())
return -1;
else if (Id() > oAST.Id())
return +1;
else
return 0;
if (Id() < oAST.Id())
return -1;
else if (Id() > oAST.Id())
return +1;
else
return 0;
}
/**

9
src/muz_qe/datalog_parser.cpp
View file

@ -1160,9 +1160,9 @@ class wpa_parser_impl : public wpa_parser, dparser {
public:
wpa_parser_impl(context & ctx)
: dparser(ctx, ctx.get_manager()),
m_bool_sort(ctx.get_manager()),
m_short_sort(ctx.get_manager()),
m_use_map_names(ctx.get_params().get_bool("use_map_names", true)) {
m_bool_sort(ctx.get_manager()),
m_short_sort(ctx.get_manager()),
m_use_map_names(ctx.get_params().use_map_names()) {
}
~wpa_parser_impl() {
reset_dealloc_values(m_sort_contents);
@ -1326,9 +1326,6 @@ private:
throw default_exception("tuple file %s for undeclared predicate %s",
m_current_file.c_str(), predicate_name.bare_str());
}
if(!m_context.can_add_table_fact(pred)) {
NOT_IMPLEMENTED_YET();
}
unsigned pred_arity = pred->get_arity();
sort * const * arg_sorts = pred->get_domain();

6
src/muz_qe/dl_bmc_engine.cpp
View file

@ -57,7 +57,6 @@ namespace datalog {
m_ctx.ensure_opened();
m_rules.reset();
m_ctx.get_rmanager().reset_relations();
datalog::rule_manager& rule_manager = m_ctx.get_rule_manager();
datalog::rule_set old_rules(m_ctx.get_rules());
datalog::rule_ref_vector query_rules(rule_manager);
@ -71,7 +70,7 @@ namespace datalog {
m_ctx.set_output_predicate(m_query_pred);
m_ctx.apply_default_transformation(mc, m_pc);
if (m_ctx.get_params().get_bool("slice", true)) {
if (m_ctx.get_params().slice()) {
datalog::rule_transformer transformer(m_ctx);
datalog::mk_slice* slice = alloc(datalog::mk_slice, m_ctx);
transformer.register_plugin(slice);
@ -1100,9 +1099,6 @@ namespace datalog {
m_solver.reset_statistics();
}
void bmc::collect_params(param_descrs& p) {
}
expr_ref bmc::get_answer() {
return m_answer;
}

3
src/muz_qe/dl_bmc_engine.h
View file

@ -24,6 +24,7 @@ Revision History:
#include "statistics.h"
#include "smt_kernel.h"
#include "bv_decl_plugin.h"
#include "smt_params.h"
namespace datalog {
@ -130,8 +131,6 @@ namespace datalog {
void reset_statistics();
expr_ref get_answer();
static void collect_params(param_descrs& p);
};
};

29
src/muz_qe/dl_cmds.cpp
View file

@ -28,13 +28,15 @@ Notes:
#include"cancel_eh.h"
#include"scoped_ctrl_c.h"
#include"scoped_timer.h"
#include"params2smt_params.h"
#include"trail.h"
#include<iomanip>
class dl_context {
// PARAM-TODO temp HACK: added m_params field because cmd_context does not have smt_params anymore
smt_params m_params;
struct dl_context {
smt_params m_fparams;
params_ref m_params_ref;
fixedpoint_params m_params;
cmd_context & m_cmd;
dl_collected_cmds* m_collected_cmds;
unsigned m_ref_count;
@ -42,8 +44,13 @@ class dl_context {
scoped_ptr<datalog::context> m_context;
trail_stack<dl_context> m_trail;
public:
fixedpoint_params const& get_params() {
init();
return m_context->get_params();
}
dl_context(cmd_context & ctx, dl_collected_cmds* collected_cmds):
m_params(m_params_ref),
m_cmd(ctx),
m_collected_cmds(collected_cmds),
m_ref_count(0),
@ -64,7 +71,7 @@ public:
void init() {
ast_manager& m = m_cmd.m();
if (!m_context) {
m_context = alloc(datalog::context, m, m_params);
m_context = alloc(datalog::context, m, m_fparams, m_params_ref);
}
if (!m_decl_plugin) {
symbol name("datalog_relation");
@ -212,7 +219,7 @@ public:
datalog::context& dlctx = m_dl_ctx->dlctx();
set_background(ctx);
dlctx.updt_params(m_params);
unsigned timeout = m_params.get_uint("timeout", UINT_MAX);
unsigned timeout = m_dl_ctx->get_params().timeout();
cancel_eh<datalog::context> eh(dlctx);
lbool status = l_undef;
{
@ -267,10 +274,6 @@ public:
virtual void init_pdescrs(cmd_context & ctx, param_descrs & p) {
m_dl_ctx->dlctx().collect_params(p);
insert_timeout(p);
p.insert("print_answer", CPK_BOOL, "(default: false) print answer instance(s) to query.");
p.insert("print_certificate", CPK_BOOL, "(default: false) print certificate for reachability or non-reachability.");
p.insert("print_statistics", CPK_BOOL, "(default: false) print statistics.");
}
@ -285,7 +288,7 @@ private:
}
void print_answer(cmd_context& ctx) {
if (m_params.get_bool("print_answer", false)) {
if (m_dl_ctx->get_params().print_answer()) {
datalog::context& dlctx = m_dl_ctx->dlctx();
ast_manager& m = ctx.m();
expr_ref query_result(dlctx.get_answer_as_formula(), m);
@ -300,7 +303,7 @@ private:
}
void print_statistics(cmd_context& ctx) {
if (m_params.get_bool("print_statistics", false)) {
if (m_dl_ctx->get_params().print_statistics()) {
statistics st;
datalog::context& dlctx = m_dl_ctx->dlctx();
unsigned long long max_mem = memory::get_max_used_memory();
@ -314,7 +317,7 @@ private:
}
void print_certificate(cmd_context& ctx) {
if (m_params.get_bool("print_certificate", false)) {
if (m_dl_ctx->get_params().print_certificate()) {
datalog::context& dlctx = m_dl_ctx->dlctx();
if (!dlctx.display_certificate(ctx.regular_stream())) {
throw cmd_exception("certificates are not supported for the selected engine");

8
src/muz_qe/dl_compiler.cpp
View file

@ -42,7 +42,7 @@ namespace datalog {
return;
}
relation_signature sig;
m_context.get_rmanager().from_predicate(pred, sig);
m_context.get_rel_context().get_rmanager().from_predicate(pred, sig);
reg_idx reg = get_fresh_register(sig);
e->get_data().m_value=reg;
@ -563,7 +563,7 @@ namespace datalog {
}
SASSERT(is_app(e));
relation_sort arg_sort;
m_context.get_rmanager().from_predicate(neg_pred, i, arg_sort);
m_context.get_rel_context().get_rmanager().from_predicate(neg_pred, i, arg_sort);
reg_idx new_reg;
make_add_constant_column(head_pred, filtered_res, arg_sort, to_app(e), new_reg, acc);
@ -1096,7 +1096,7 @@ namespace datalog {
func_decl_set::iterator fdit = preds.begin();
func_decl_set::iterator fdend = preds.end();
for(; fdit!=fdend; ++fdit) {
if(!m_context.get_rmanager().is_saturated(*fdit)) {
if(!m_context.get_rel_context().get_rmanager().is_saturated(*fdit)) {
return false;
}
}
@ -1181,7 +1181,7 @@ namespace datalog {
acc.set_observer(0);
TRACE("dl", execution_code.display(m_context, tout););
TRACE("dl", execution_code.display(m_context.get_rel_context(), tout););
}

561
src/muz_qe/dl_context.cpp
View file

@ -24,18 +24,12 @@ Revision History:
#include"arith_decl_plugin.h"
#include"bv_decl_plugin.h"
#include"dl_table.h"
#include"dl_sparse_table.h"
#include"dl_table_relation.h"
#include"dl_bound_relation.h"
#include"dl_interval_relation.h"
#include"dl_finite_product_relation.h"
#include"dl_product_relation.h"
#include"dl_rule_transformer.h"
#include"dl_mk_coi_filter.h"
#include"dl_mk_explanations.h"
#include"dl_mk_filter_rules.h"
#include"dl_mk_interp_tail_simplifier.h"
#include"dl_mk_magic_sets.h"
#include"dl_mk_rule_inliner.h"
#include"dl_mk_simple_joins.h"
#include"dl_mk_similarity_compressor.h"
@ -44,10 +38,6 @@ Revision History:
#include"dl_compiler.h"
#include"dl_instruction.h"
#include"dl_context.h"
#include"dl_smt_relation.h"
#ifndef _EXTERNAL_RELEASE
#include"dl_skip_table.h"
#endif
#include"for_each_expr.h"
#include"ast_smt_pp.h"
#include"ast_smt2_pp.h"
@ -190,7 +180,6 @@ namespace datalog {
virtual ~restore_rules() {}
virtual void undo(context& ctx) {
ctx.reset_tables();
ctx.replace_rules(*m_old_rules);
reset();
}
@ -210,7 +199,6 @@ namespace datalog {
m_trail.push_scope();
m_trail.push(restore_rules(m_rule_set));
m_trail.push(restore_vec_size_trail<context,expr_ref_vector>(m_background));
m_trail.push(restore_vec_size_trail<context,fact_vector>(m_table_facts));
}
void context::pop() {
@ -229,11 +217,11 @@ namespace datalog {
context::context(ast_manager & m, smt_params& fp, params_ref const& pa):
m(m),
m_fparams(fp),
m_params(pa),
m_params_ref(pa),
m_params(m_params_ref),
m_decl_util(m),
m_rewriter(m),
m_var_subst(m),
m_rmanager(*this),
m_rule_manager(*this),
m_trail(*this),
m_pinned(m),
@ -243,26 +231,11 @@ namespace datalog {
m_background(m),
m_closed(false),
m_saturation_was_run(false),
m_last_result_relation(0),
m_last_answer(m),
m_engine(LAST_ENGINE),
m_cancel(false) {
//register plugins for builtin tables
get_rmanager().register_plugin(alloc(sparse_table_plugin, get_rmanager()));
get_rmanager().register_plugin(alloc(hashtable_table_plugin, get_rmanager()));
get_rmanager().register_plugin(alloc(bitvector_table_plugin, get_rmanager()));
get_rmanager().register_plugin(alloc(equivalence_table_plugin, get_rmanager()));
#ifndef _EXTERNAL_RELEASE
get_rmanager().register_plugin(alloc(skip_table_plugin, get_rmanager()));
#endif
//register plugins for builtin relations
get_rmanager().register_plugin(alloc(smt_relation_plugin, get_rmanager()));
get_rmanager().register_plugin(alloc(bound_relation_plugin, get_rmanager()));
get_rmanager().register_plugin(alloc(interval_relation_plugin, get_rmanager()));
}
context::~context() {
@ -273,14 +246,12 @@ namespace datalog {
m_trail.reset();
m_rule_set.reset();
m_argument_var_names.reset();
m_output_preds.reset();
m_preds.reset();
m_preds_by_name.reset();
reset_dealloc_values(m_sorts);
if (m_last_result_relation) {
m_last_result_relation->deallocate();
m_last_result_relation = 0;
}
m_pdr = 0;
m_bmc = 0;
m_rel = 0;
}
bool context::is_fact(app * head) const {
@ -456,59 +427,13 @@ namespace datalog {
return e->get_data().m_value[arg_index];
}
relation_plugin & context::get_ordinary_relation_plugin(symbol relation_name) {
relation_plugin * plugin = get_rmanager().get_relation_plugin(relation_name);
if (!plugin) {
std::stringstream sstm;
sstm << "relation plugin " << relation_name << " does not exist";
throw default_exception(sstm.str());
}
if (plugin->is_product_relation()) {
throw default_exception("cannot request product relation directly");
}
if (plugin->is_sieve_relation()) {
throw default_exception("cannot request sieve relation directly");
}
if (plugin->is_finite_product_relation()) {
throw default_exception("cannot request finite product relation directly");
}
return *plugin;
}
void context::set_predicate_representation(func_decl * pred, unsigned relation_name_cnt,
symbol const * relation_names) {
relation_manager & rmgr = get_rmanager();
family_id target_kind = null_family_id;
switch (relation_name_cnt) {
case 0:
return;
case 1:
target_kind = get_ordinary_relation_plugin(relation_names[0]).get_kind();
break;
default: {
svector<family_id> rel_kinds; // kinds of plugins that are not table plugins
family_id rel_kind; // the aggregate kind of non-table plugins
for (unsigned i = 0; i < relation_name_cnt; i++) {
relation_plugin & p = get_ordinary_relation_plugin(relation_names[i]);
rel_kinds.push_back(p.get_kind());
}
if (rel_kinds.size() == 1) {
rel_kind = rel_kinds[0];
}
else {
relation_signature rel_sig;
//rmgr.from_predicate(pred, rel_sig);
product_relation_plugin & prod_plugin = product_relation_plugin::get_plugin(rmgr);
rel_kind = prod_plugin.get_relation_kind(rel_sig, rel_kinds);
}
target_kind = rel_kind;
break;
}
if (relation_name_cnt > 0) {
ensure_rel();
m_rel->set_predicate_representation(pred, relation_name_cnt, relation_names);
}
SASSERT(target_kind != null_family_id);
get_rmanager().set_predicate_kind(pred, target_kind);
}
func_decl * context::mk_fresh_head_predicate(symbol const & prefix, symbol const & suffix,
@ -518,19 +443,25 @@ namespace datalog {
register_predicate(new_pred);
if (orig_pred) {
family_id target_kind = get_rmanager().get_requested_predicate_kind(orig_pred);
if (target_kind != null_family_id) {
get_rmanager().set_predicate_kind(new_pred, target_kind);
}
if (m_rel.get()) {
m_rel->inherit_predicate_kind(new_pred, orig_pred);
}
return new_pred;
}
void context::set_output_predicate(func_decl * pred) {
if (!m_output_preds.contains(pred)) {
m_output_preds.insert(pred);
}
ensure_rel();
m_rel->set_output_predicate(pred);
}
bool context::is_output_predicate(func_decl * pred) {
ensure_rel();
return m_rel->is_output_predicate(pred);
}
const decl_set & context::get_output_predicates() {
ensure_rel();
return m_rel->get_output_predicates();
}
void context::add_rule(expr* rl, symbol const& name) {
@ -563,7 +494,6 @@ namespace datalog {
throw default_exception(strm.str());
}
rule_ref r(rules[0].get(), rm);
get_rmanager().reset_saturated_marks();
rule_ref_vector const& rls = m_rule_set.get_rules();
rule* old_rule = 0;
for (unsigned i = 0; i < rls.size(); ++i) {
@ -796,7 +726,6 @@ namespace datalog {
}
void context::add_rule(rule_ref& r) {
get_rmanager().reset_saturated_marks();
m_rule_set.add_rule(r);
}
@ -810,12 +739,10 @@ namespace datalog {
void context::add_fact(func_decl * pred, const relation_fact & fact) {
if (get_engine() == DATALOG_ENGINE) {
get_rmanager().reset_saturated_marks();
get_relation(pred).add_fact(fact);
m_table_facts.push_back(std::make_pair(pred, fact));
ensure_rel();
m_rel->add_fact(pred, fact);
}
else {
ast_manager& m = get_manager();
expr_ref rule(m.mk_app(pred, fact.size(), (expr*const*)fact.c_ptr()), m);
add_rule(rule, symbol::null);
}
@ -833,26 +760,18 @@ namespace datalog {
add_fact(head->get_decl(), fact);
}
bool context::can_add_table_fact(func_decl * pred) {
return get_relation(pred).from_table();
}
void context::add_table_fact(func_decl * pred, const table_fact & fact) {
relation_base & rel0 = get_relation(pred);
if (get_engine() != DATALOG_ENGINE ||
!can_add_table_fact(pred) ||
!rel0.from_table()) {
if (get_engine() == DATALOG_ENGINE) {
ensure_rel();
m_rel->add_fact(pred, fact);
}
else {
relation_fact rfact(m);
for (unsigned i = 0; i < fact.size(); ++i) {
rfact.push_back(m_decl_util.mk_numeral(fact[i], pred->get_domain()[i]));
}
add_fact(pred, rfact);
}
else {
get_rmanager().reset_saturated_marks();
table_relation & rel = static_cast<table_relation &>(rel0);
rel.add_table_fact(fact);
}
}
void context::add_table_fact(func_decl * pred, unsigned num_args, unsigned args[]) {
@ -960,179 +879,23 @@ namespace datalog {
}
void context::collect_params(param_descrs& p) {
p.insert("engine", CPK_SYMBOL, "(default: automatically configured) select 'datalog', PDR 'pdr' engine.");
p.insert("bit_blast", CPK_BOOL, "(default: false) bit-blast bit-vectors (for PDR engine).");
p.insert("default_table", CPK_SYMBOL, "default table implementation: 'sparse' (default), 'hashtable', 'bitvector', 'interval'");
p.insert("default_relation", CPK_SYMBOL, "default relation implementation: 'external_relation', 'pentagon'");
p.insert("generate_explanations", CPK_BOOL, "if true, signature of relations will be extended to contain explanations for facts");
p.insert("explanations_on_relation_level", CPK_BOOL, "if true, explanations are generated as history of each relation, "
"rather than per fact (generate_explanations must be set to true for this option to have any effect)");
p.insert("magic_sets_for_queries", CPK_BOOL, "magic set transformation will be used for queries");
p.insert("unbound_compressor", CPK_BOOL, "auxiliary relations will be introduced to avoid unbound variables in rule heads");
p.insert("similarity_compressor", CPK_BOOL, "rules that differ only in values of constants will be merged into a single rule");
p.insert("similarity_compressor_threshold", CPK_UINT, "if dl_similiaryt_compressor is on, this value determines how many "
"similar rules there must be in order for them to be merged");
p.insert("all_or_nothing_deltas", CPK_BOOL, "compile rules so that it is enough for the delta relation in union and widening "
"operations to determine only whether the updated relation was modified or not");
p.insert("compile_with_widening", CPK_BOOL, "widening will be used to compile recursive rules");
p.insert("eager_emptiness_checking", CPK_BOOL, "emptiness of affected relations will be checked after each instruction, "
"so that we may ommit unnecessary instructions");
p.insert("default_table_checked", CPK_BOOL,
"if true, the detault table will be default_table inside a wrapper that checks that "
"its results are the same as of default_table_checker table");
p.insert("initial_restart_timeout", CPK_UINT, "length of saturation run before the first restart (in ms); zero means no restarts");
p.insert("restart_timeout_quotient", CPK_UINT, "restart timeout will be multiplied by this number after each restart");
p.insert("use_map_names", CPK_BOOL, "use names from map files when displaying tuples");
p.insert("output_profile", CPK_BOOL, "determines whether profile informations should be output when outputting Datalog rules or instructions");
p.insert("output_tuples", CPK_BOOL, "determines whether tuples for output predicates should be output");
p.insert("profile_timeout_milliseconds", CPK_UINT, "instructions and rules that took less than the threshold will not be printed when printed the instruction/rule list");
p.insert("print_with_fixedpoint_extensions", CPK_BOOL, "(default true) use SMT-LIB2 fixedpoint extensions, instead of pure SMT2, when printing rules");
p.insert("print_low_level_smt2", CPK_BOOL, "(default false) use (faster) low-level SMT2 printer (the printer is scalable but the result may not be as readable)");
p.insert("print_with_variable_declarations", CPK_BOOL, "(default true) use variable declarations when displaying rules (instead of attempting to use original names)");
#ifndef _EXTERNAL_RELEASE
p.insert("dbg_fpr_nonempty_relation_signature", CPK_BOOL,
"if true, finite_product_relation will attempt to avoid creating inner relation with empty signature "
"by putting in half of the table columns, if it would have been empty otherwise");
p.insert("smt_relation_ground_recursive", CPK_BOOL, "Ensure recursive relation is ground in union");
p.insert("inline_linear_branch", CPK_BOOL, "try linear inlining method with potential expansion");
#endif
p.insert("fix_unbound_vars", CPK_BOOL, "fix unbound variables in tail");
p.insert("default_table_checker", CPK_SYMBOL, "see default_table_checked");
p.insert("inline_linear", CPK_BOOL, "(default true) try linear inlining method");
p.insert("inline_eager", CPK_BOOL, "(default true) try eager inlining of rules");
pdr::dl_interface::collect_params(p);
bmc::collect_params(p);
fixedpoint_params::collect_param_descrs(p);
insert_timeout(p);
}
void context::updt_params(params_ref const& p) {
m_params.copy(p);
if (m_pdr.get()) m_pdr->updt_params();
m_params_ref.copy(p);
if (m_pdr.get()) m_pdr->updt_params();
}
void context::collect_predicates(decl_set & res) {
unsigned rule_cnt = m_rule_set.get_num_rules();
for (unsigned rindex=0; rindex<rule_cnt; rindex++) {
rule * r = m_rule_set.get_rule(rindex);
res.insert(r->get_head()->get_decl());
unsigned tail_len = r->get_uninterpreted_tail_size();
for (unsigned tindex=0; tindex<tail_len; tindex++) {
res.insert(r->get_tail(tindex)->get_decl());
}
}
decl_set::iterator oit = m_output_preds.begin();
decl_set::iterator oend = m_output_preds.end();
for (; oit!=oend; ++oit) {
res.insert(*oit);
}
get_rmanager().collect_predicates(res);
void context::collect_predicates(decl_set& res) {
ensure_rel();
m_rel->collect_predicates(res);
}
void context::restrict_predicates( const decl_set & res ) {
set_intersection(m_output_preds, res);
get_rmanager().restrict_predicates(res);
}
lbool context::dl_saturate() {
if (!m_closed) {
close();
}
bool time_limit = soft_timeout()!=0;
unsigned remaining_time_limit = soft_timeout();
unsigned restart_time = initial_restart_timeout();
rule_set original_rules(get_rules());
decl_set original_predicates;
collect_predicates(original_predicates);
instruction_block rules_code;
instruction_block termination_code;
execution_context ex_ctx(*this);
lbool result;
TRACE("dl", display(tout););
while (true) {
model_converter_ref mc; // Ignored in Datalog mode
proof_converter_ref pc; // Ignored in Datalog mode
transform_rules(mc, pc);
compiler::compile(*this, get_rules(), rules_code, termination_code);
TRACE("dl", rules_code.display(*this, tout); );
bool timeout_after_this_round = time_limit && (restart_time==0 || remaining_time_limit<=restart_time);
if (time_limit || restart_time!=0) {
unsigned timeout = time_limit ? (restart_time!=0) ?
std::min(remaining_time_limit, restart_time)
: remaining_time_limit : restart_time;
ex_ctx.set_timelimit(timeout);
}
bool early_termination = !rules_code.perform(ex_ctx);
ex_ctx.reset_timelimit();
VERIFY( termination_code.perform(ex_ctx) );
rules_code.process_all_costs();
IF_VERBOSE(10, ex_ctx.report_big_relations(1000, verbose_stream()););
if (!early_termination) {
m_last_status = OK;
result = l_true;
break;
}
if (memory::above_high_watermark()) {
m_last_status = MEMOUT;
result = l_undef;
break;
}
if (timeout_after_this_round || m_cancel) {
m_last_status = TIMEOUT;
result = l_undef;
break;
}
SASSERT(restart_time!=0);
if (time_limit) {
SASSERT(remaining_time_limit>restart_time);
remaining_time_limit-=restart_time;
}
uint64 new_restart_time = static_cast<uint64>(restart_time)*initial_restart_timeout();
if (new_restart_time>UINT_MAX) {
restart_time=UINT_MAX;
}
else {
restart_time=static_cast<unsigned>(new_restart_time);
}
rules_code.reset();
termination_code.reset();
ex_ctx.reset();
reopen();
restrict_predicates(original_predicates);
replace_rules(original_rules);
close();
}
reopen();
restrict_predicates(original_predicates);
replace_rules(original_rules);
close();
TRACE("dl", ex_ctx.report_big_relations(100, tout););
return result;
void context::restrict_predicates(decl_set const& res) {
ensure_rel();
m_rel->restrict_predicates(res);
}
expr_ref context::get_background_assertion() {
@ -1155,19 +918,21 @@ namespace datalog {
m_cancel = true;
if (m_pdr.get()) m_pdr->cancel();
if (m_bmc.get()) m_bmc->cancel();
if (m_rel.get()) m_rel->cancel();
}
void context::cleanup() {
m_cancel = false;
if (m_pdr.get()) m_pdr->cleanup();
if (m_bmc.get()) m_bmc->cleanup();
if (m_rel.get()) m_rel->cleanup();
}
class context::engine_type_proc {
ast_manager& m;
arith_util a;
ast_manager& m;
arith_util a;
datatype_util dt;
DL_ENGINE m_engine;
DL_ENGINE m_engine;
public:
engine_type_proc(ast_manager& m): m(m), a(m), dt(m), m_engine(DATALOG_ENGINE) {}
@ -1190,7 +955,7 @@ namespace datalog {
};
void context::configure_engine() {
symbol e = m_params.get_sym("engine", symbol());
symbol e = m_params.engine();
if (e == symbol("datalog")) {
m_engine = DATALOG_ENGINE;
@ -1234,7 +999,7 @@ namespace datalog {
switch(get_engine()) {
case DATALOG_ENGINE:
return dl_query(query);
return rel_query(query);
case PDR_ENGINE:
case QPDR_ENGINE:
return pdr_query(query);
@ -1243,18 +1008,14 @@ namespace datalog {
return bmc_query(query);
default:
UNREACHABLE();
return dl_query(query);
return rel_query(query);
}
}
void context::new_query() {
flush_add_rules();
if (m_last_result_relation) {
m_last_result_relation->deallocate();
m_last_result_relation = 0;
}
m_last_status = OK;
m_last_answer = get_manager().mk_true();
m_last_answer = 0;
}
model_ref context::get_model() {
@ -1287,7 +1048,6 @@ namespace datalog {
lbool context::pdr_query(expr* query) {
ensure_pdr();
m_last_answer = 0;
return m_pdr->query(query);
}
@ -1299,218 +1059,25 @@ namespace datalog {
lbool context::bmc_query(expr* query) {
ensure_bmc();
m_last_answer = 0;
return m_bmc->query(query);
}
#define BEGIN_QUERY() \
rule_set original_rules(get_rules()); \
decl_set original_preds; \
collect_predicates(original_preds); \
bool was_closed = m_closed; \
if (m_closed) { \
reopen(); \
} \
#define END_QUERY() \
reopen(); \
replace_rules(original_rules); \
restrict_predicates(original_preds); \
\
if (was_closed) { \
close(); \
} \
lbool context::dl_query(unsigned num_rels, func_decl * const* rels) {
BEGIN_QUERY();
for (unsigned i = 0; i < num_rels; ++i) {
set_output_predicate(rels[i]);
void context::ensure_rel() {
if (!m_rel.get()) {
m_rel = alloc(rel_context, *this);
}
close();
reset_negated_tables();
lbool res = dl_saturate();
}
switch(res) {
case l_true: {
expr_ref_vector ans(m);
expr_ref e(m);
bool some_non_empty = num_rels == 0;
for (unsigned i = 0; i < num_rels; ++i) {
relation_base& rel = get_relation(rels[i]);
if (!rel.empty()) {
some_non_empty = true;
}
rel.to_formula(e);
ans.push_back(e);
}
SASSERT(!m_last_result_relation);
if (some_non_empty) {
m_last_answer = m.mk_and(ans.size(), ans.c_ptr());
}
else {
m_last_answer = m.mk_false();
res = l_false;
}
break;
}
case l_false:
m_last_answer = m.mk_false();
break;
case l_undef:
break;
}
END_QUERY();
return res;
lbool context::rel_query(unsigned num_rels, func_decl * const* rels) {
ensure_rel();
return m_rel->query(num_rels, rels);
}
lbool context::dl_query(expr* query) {
BEGIN_QUERY();
rule_manager& rm = get_rule_manager();
rule_ref qrule(rm);
rule_ref_vector qrules(rm);
func_decl_ref query_pred(get_manager());
try {
rm.mk_query(query, query_pred, qrules, qrule);
}
catch(default_exception& exn) {
close();
m_last_status = INPUT_ERROR;
throw exn;
}
try {
add_rules(qrules);
}
catch (default_exception& exn) {
close();
m_last_status = INPUT_ERROR;
throw exn;
}
set_output_predicate(qrule->get_head()->get_decl());
close();
reset_negated_tables();
if (generate_explanations()) {
model_converter_ref mc; // ignored in Datalog mode
proof_converter_ref pc; // ignored in Datalog mode
rule_transformer transformer(*this);
//expl_plugin is deallocated when transformer goes out of scope
mk_explanations * expl_plugin =
alloc(mk_explanations, *this, explanations_on_relation_level());
transformer.register_plugin(expl_plugin);
transform_rules(transformer, mc, pc);
//we will retrieve the predicate with explanations instead of the original query predicate
query_pred = expl_plugin->get_e_decl(query_pred);
const rule_vector & query_rules = get_rules().get_predicate_rules(query_pred);
SASSERT(query_rules.size()==1);
qrule = query_rules.back();
}
if (magic_sets_for_queries()) {
model_converter_ref mc; // Ignored in Datalog mode
proof_converter_ref pc; // Ignored in Datalog mode
rule_transformer transformer(*this);
transformer.register_plugin(alloc(mk_magic_sets, *this, qrule.get()));
transform_rules(transformer, mc, pc);
}
lbool res = dl_saturate();
if (res != l_undef) {
m_last_result_relation = get_relation(query_pred).clone();
if (m_last_result_relation->empty()) {
res = l_false;
m_last_answer = m.mk_false();
}
else {
m_last_result_relation->to_formula(m_last_answer);
}
}
END_QUERY();
return res;
lbool context::rel_query(expr* query) {
ensure_rel();
return m_rel->query(query);
}
void context::reset_tables() {
get_rmanager().reset_saturated_marks();
rule_set::decl2rules::iterator it = m_rule_set.begin_grouped_rules();
rule_set::decl2rules::iterator end = m_rule_set.end_grouped_rules();
for (; it != end; ++it) {
func_decl* p = it->m_key;
relation_base & rel = get_relation(p);
rel.reset();
}
for (unsigned i = 0; i < m_table_facts.size(); ++i) {
func_decl* pred = m_table_facts[i].first;
relation_fact const& fact = m_table_facts[i].second;
get_relation(pred).add_fact(fact);
}
}
void context::reset_negated_tables() {
rule_set::pred_set_vector const & pred_sets = m_rule_set.get_strats();
bool non_empty = false;
for (unsigned i = 1; i < pred_sets.size(); ++i) {
func_decl_set::iterator it = pred_sets[i]->begin(), end = pred_sets[i]->end();
for (; it != end; ++it) {
func_decl* pred = *it;
relation_base & rel = get_relation(pred);
if (!rel.empty()) {
non_empty = true;
break;
}
}
}
if (!non_empty) {
return;
}
// collect predicates that depend on negation.
func_decl_set depends_on_negation;
for (unsigned i = 1; i < pred_sets.size(); ++i) {
bool change = true;
while (change) {
change = false;
func_decl_set::iterator it = pred_sets[i]->begin(), end = pred_sets[i]->end();
for (; it != end; ++it) {
func_decl* pred = *it;
if (depends_on_negation.contains(pred)) {
continue;
}
rule_vector const& rules = m_rule_set.get_predicate_rules(pred);
bool inserted = false;
for (unsigned j = 0; !inserted && j < rules.size(); ++j) {
rule* r = rules[j];
unsigned psz = r->get_positive_tail_size();
unsigned tsz = r->get_uninterpreted_tail_size();
if (psz < tsz) {
depends_on_negation.insert(pred);
change = true;
inserted = true;
}
for (unsigned k = 0; !inserted && k < tsz; ++k) {
func_decl* tail_decl = r->get_tail(k)->get_decl();
if (depends_on_negation.contains(tail_decl)) {
depends_on_negation.insert(pred);
change = true;
inserted = true;
}
}
}
}
}
}
func_decl_set::iterator it = depends_on_negation.begin(), end = depends_on_negation.end();
for (; it != end; ++it) {
func_decl* pred = *it;
relation_base & rel = get_relation(pred);
if (!rel.empty()) {
TRACE("dl", tout << "Resetting: " << mk_ismt2_pp(pred, m) << "\n";);
rel.reset();
}
}
}
expr* context::get_answer_as_formula() {
if (m_last_answer) {
@ -1527,6 +1094,10 @@ namespace datalog {
ensure_bmc();
m_last_answer = m_bmc->get_answer();
return m_last_answer.get();
case DATALOG_ENGINE:
ensure_rel();
m_last_answer = m_rel->get_last_answer();
return m_last_answer.get();
default:
UNREACHABLE();
}
@ -1587,8 +1158,8 @@ namespace datalog {
execution_result context::get_status() { return m_last_status; }
bool context::result_contains_fact(relation_fact const& f) {
SASSERT(m_last_result_relation);
return m_last_result_relation->contains_fact(f);
ensure_rel();
return m_rel->result_contains_fact(f);
}
// TBD: algebraic data-types declarations will not be printed.
@ -1668,9 +1239,9 @@ namespace datalog {
expr_ref fml(m);
expr_ref_vector rules(m);
svector<symbol> names;
bool use_fixedpoint_extensions = m_params.get_bool("print_with_fixedpoint_extensions", true);
bool print_low_level = m_params.get_bool("print_low_level_smt2", false);
bool do_declare_vars = m_params.get_bool("print_with_variable_declarations", true);
bool use_fixedpoint_extensions = m_params.print_with_fixedpoint_extensions();
bool print_low_level = m_params.print_low_level_smt2();
bool do_declare_vars = m_params.print_with_variable_declarations();
#define PP(_e_) if (print_low_level) out << mk_smt_pp(_e_, m); else ast_smt2_pp(out, _e_, env);

116
src/muz_qe/dl_context.h
View file

@ -24,7 +24,6 @@ Revision History:
#undef max
#endif
#include"arith_decl_plugin.h"
#include"smt_params.h"
#include"map.h"
#include"th_rewriter.h"
#include"str_hashtable.h"
@ -36,14 +35,15 @@ Revision History:
#include"dl_rule_set.h"
#include"pdr_dl_interface.h"
#include"dl_bmc_engine.h"
#include"rel_context.h"
#include"lbool.h"
#include"statistics.h"
#include"params.h"
#include"trail.h"
#include"dl_external_relation.h"
#include"model_converter.h"
#include"proof_converter.h"
#include"model2expr.h"
#include"smt_params.h"
namespace datalog {
@ -75,15 +75,14 @@ namespace datalog {
typedef map<symbol, func_decl*, symbol_hash_proc, symbol_eq_proc> sym2decl;
typedef obj_map<const func_decl, svector<symbol> > pred2syms;
typedef obj_map<const sort, sort_domain*> sort_domain_map;
typedef vector<std::pair<func_decl*,relation_fact> > fact_vector;
ast_manager & m;
smt_params& m_fparams;
params_ref m_params;
smt_params & m_fparams;
params_ref m_params_ref;
fixedpoint_params m_params;
dl_decl_util m_decl_util;
th_rewriter m_rewriter;
var_subst m_var_subst;
relation_manager m_rmanager;
rule_manager m_rule_manager;
trail_stack<context> m_trail;
@ -93,7 +92,6 @@ namespace datalog {
func_decl_set m_preds;
sym2decl m_preds_by_name;
pred2syms m_argument_var_names;
decl_set m_output_preds;
rule_set m_rule_set;
expr_ref_vector m_rule_fmls;
svector<symbol> m_rule_names;
@ -101,80 +99,64 @@ namespace datalog {
scoped_ptr<pdr::dl_interface> m_pdr;
scoped_ptr<bmc> m_bmc;
scoped_ptr<rel_context> m_rel;
bool m_closed;
bool m_saturation_was_run;
execution_result m_last_status;
relation_base * m_last_result_relation;
expr_ref m_last_answer;
DL_ENGINE m_engine;
volatile bool m_cancel;
fact_vector m_table_facts;
bool is_fact(app * head) const;
bool has_sort_domain(relation_sort s) const;
sort_domain & get_sort_domain(relation_sort s);
const sort_domain & get_sort_domain(relation_sort s) const;
relation_plugin & get_ordinary_relation_plugin(symbol relation_name);
class engine_type_proc;
public:
context(ast_manager & m, smt_params& params, params_ref const& p = params_ref());
context(ast_manager & m, smt_params& fp, params_ref const& p = params_ref());
~context();
void reset();
void push();
void pop();
relation_base & get_relation(func_decl * pred) { return get_rmanager().get_relation(pred); }
relation_base * try_get_relation(func_decl * pred) const { return get_rmanager().try_get_relation(pred); }
bool saturation_was_run() const { return m_saturation_was_run; }
void notify_saturation_was_run() { m_saturation_was_run = true; }
/**
\brief Store the relation \c rel under the predicate \c pred. The \c context object
takes over the ownership of the relation object.
*/
void store_relation(func_decl * pred, relation_base * rel) {
get_rmanager().store_relation(pred, rel);
}
void configure_engine();
ast_manager & get_manager() const { return m; }
relation_manager & get_rmanager() { return m_rmanager; }
const relation_manager & get_rmanager() const { return m_rmanager; }
rule_manager & get_rule_manager() { return m_rule_manager; }
smt_params & get_fparams() const { return m_fparams; }
params_ref const& get_params() const { return m_params; }
fixedpoint_params const& get_params() const { return m_params; }
DL_ENGINE get_engine() { configure_engine(); return m_engine; }
th_rewriter& get_rewriter() { return m_rewriter; }
var_subst & get_var_subst() { return m_var_subst; }
dl_decl_util & get_decl_util() { return m_decl_util; }
bool output_profile() const { return m_params.get_bool("output_profile", false); }
bool fix_unbound_vars() const { return m_params.get_bool("fix_unbound_vars", false); }
symbol default_table() const { return m_params.get_sym("default_table", symbol("sparse")); }
symbol default_relation() const { return m_params.get_sym("default_relation", external_relation_plugin::get_name()); }
symbol default_table_checker() const { return m_params.get_sym("default_table_checker", symbol("sparse")); }
bool default_table_checked() const { return m_params.get_bool("default_table_checked", false); }
bool dbg_fpr_nonempty_relation_signature() const { return m_params.get_bool("dbg_fpr_nonempty_relation_signatures", false); }
unsigned dl_profile_milliseconds_threshold() const { return m_params.get_uint("profile_milliseconds_threshold", 0); }
bool all_or_nothing_deltas() const { return m_params.get_bool("all_or_nothing_deltas", false); }
bool compile_with_widening() const { return m_params.get_bool("compile_with_widening", false); }
bool unbound_compressor() const { return m_params.get_bool("unbound_compressor", true); }
bool similarity_compressor() const { return m_params.get_bool("similarity_compressor", true); }
unsigned similarity_compressor_threshold() const { return m_params.get_uint("similarity_compressor_threshold", 11); }
bool output_profile() const { return m_params.output_profile(); }
bool fix_unbound_vars() const { return m_params.fix_unbound_vars(); }
symbol default_table() const { return m_params.default_table(); }
symbol default_relation() const { return m_params.default_relation(); } // external_relation_plugin::get_name());
symbol default_table_checker() const { return m_params.default_table_checker(); }
bool default_table_checked() const { return m_params.default_table_checked(); }
bool dbg_fpr_nonempty_relation_signature() const { return m_params.dbg_fpr_nonempty_relation_signature(); }
unsigned dl_profile_milliseconds_threshold() const { return m_params.profile_timeout_milliseconds(); }
bool all_or_nothing_deltas() const { return m_params.all_or_nothing_deltas(); }
bool compile_with_widening() const { return m_params.compile_with_widening(); }
bool unbound_compressor() const { return m_params.unbound_compressor(); }
bool similarity_compressor() const { return m_params.similarity_compressor(); }
unsigned similarity_compressor_threshold() const { return m_params.similarity_compressor_threshold(); }
unsigned soft_timeout() const { return m_fparams.m_soft_timeout; }
unsigned initial_restart_timeout() const { return m_params.get_uint("initial_restart_timeout", 0); }
bool generate_explanations() const { return m_params.get_bool("generate_explanations", false); }
bool explanations_on_relation_level() const { return m_params.get_bool("explanations_on_relation_level", false); }
bool magic_sets_for_queries() const { return m_params.get_bool("magic_sets_for_queries", false); }
bool eager_emptiness_checking() const { return m_params.get_bool("eager_emptiness_checking", true); }
unsigned initial_restart_timeout() const { return m_params.initial_restart_timeout(); }
bool generate_explanations() const { return m_params.generate_explanations(); }
bool explanations_on_relation_level() const { return m_params.explanations_on_relation_level(); }
bool magic_sets_for_queries() const { return m_params.magic_sets_for_queries(); }
bool eager_emptiness_checking() const { return m_params.eager_emptiness_checking(); }
void register_finite_sort(sort * s, sort_kind k);
@ -246,8 +228,8 @@ namespace datalog {
symbol const * relation_names);
void set_output_predicate(func_decl * pred);
bool is_output_predicate(func_decl * pred) { return m_output_preds.contains(pred); }
const decl_set & get_output_predicates() const { return m_output_preds; }
bool is_output_predicate(func_decl * pred);
const decl_set & get_output_predicates();
rule_set const & get_rules() { flush_add_rules(); return m_rule_set; }
@ -313,7 +295,6 @@ namespace datalog {
and there is no transformation of relation values before they are put into the
table.
*/
bool can_add_table_fact(func_decl * pred);
void add_table_fact(func_decl * pred, const table_fact & fact);
void add_table_fact(func_decl * pred, unsigned num_args, unsigned args[]);
@ -322,6 +303,7 @@ namespace datalog {
*/
void close();
void ensure_closed();
bool is_closed() { return m_closed; }
/**
\brief Undo the effect of the \c close operation.
@ -350,13 +332,10 @@ namespace datalog {
void display_rules(std::ostream & out) const {
m_rule_set.display(out);
}
void display_facts(std::ostream & out) const {
m_rmanager.display(out);
}
void display(std::ostream & out) const {
display_rules(out);
display_facts(out);
if (m_rel) m_rel->display_facts(out);
}
void display_smt2(unsigned num_queries, expr* const* queries, std::ostream& out);
@ -406,23 +385,16 @@ namespace datalog {
/**
Query multiple output relations.
*/
lbool dl_query(unsigned num_rels, func_decl * const* rels);
lbool rel_query(unsigned num_rels, func_decl * const* rels);
/**
Reset tables that are under negation.
*/
void reset_negated_tables();
/**
Just reset all tables.
*/
void reset_tables();
/**
\brief retrieve last proof status.
*/
execution_result get_status();
void set_status(execution_result r) { m_last_status = r; }
/**
\brief retrieve formula corresponding to query that returns l_true.
The formula describes one or more instances of the existential variables
@ -445,29 +417,27 @@ namespace datalog {
*/
bool result_contains_fact(relation_fact const& f);
/**
\brief display facts generated for query.
*/
void display_output_facts(std::ostream & out) const {
m_rmanager.display_output_tables(out);
}
/**
\brief expose datalog saturation for test.
*/
lbool dl_saturate();
rel_context& get_rel_context() { ensure_rel(); return *m_rel; }
private:
/**
Just reset all tables.
*/
void reset_tables();
void flush_add_rules();
void ensure_pdr();
void ensure_bmc();
void ensure_rel();
void new_query();
lbool dl_query(expr* query);
lbool rel_query(expr* query);
lbool pdr_query(expr* query);

2
src/muz_qe/dl_costs.cpp
View file

@ -115,7 +115,7 @@ namespace datalog {
}
void accounted_object::output_profile(context & ctx, std::ostream & out) const {
void accounted_object::output_profile(std::ostream & out) const {
costs c;
get_total_cost(c);
c.output(out);

2
src/muz_qe/dl_costs.h
View file

@ -79,7 +79,7 @@ namespace datalog {
void process_costs();
bool passes_output_thresholds(context & ctx) const;
void output_profile(context & ctx, std::ostream & out) const;
void output_profile(std::ostream & out) const;
private:
//private and undefined copy constructor and operator= to avoid the default ones

74
src/muz_qe/dl_instruction.cpp
View file

@ -33,11 +33,11 @@ namespace datalog {
//
// -----------------------------------
execution_context::execution_context(context & datalog_context)
: m_datalog_context(datalog_context),
execution_context::execution_context(context & context)
: m_context(context),
m_stopwatch(0),
m_timelimit_ms(0),
m_eager_emptiness_checking(datalog_context.eager_emptiness_checking()) {}
m_eager_emptiness_checking(context.eager_emptiness_checking()) {}
execution_context::~execution_context() {
reset();
@ -135,12 +135,12 @@ namespace datalog {
process_costs();
}
void instruction::display_indented(context & ctx, std::ostream & out, std::string indentation) const {
void instruction::display_indented(rel_context & ctx, std::ostream & out, std::string indentation) const {
out << indentation;
display_head_impl(ctx, out);
if (ctx.output_profile()) {
out << " {";
output_profile(ctx, out);
output_profile(out);
out << '}';
}
out << "\n";
@ -157,10 +157,10 @@ namespace datalog {
virtual bool perform(execution_context & ctx) {
if (m_store) {
if (ctx.reg(m_reg)) {
ctx.get_datalog_context().store_relation(m_pred, ctx.release_reg(m_reg));
ctx.get_rel_context().store_relation(m_pred, ctx.release_reg(m_reg));
}
else {
context & dctx = ctx.get_datalog_context();
rel_context & dctx = ctx.get_rel_context();
relation_base * empty_rel;
//the object referenced by sig is valid only until we call dctx.store_relation()
const relation_signature & sig = dctx.get_relation(m_pred).get_signature();
@ -169,7 +169,7 @@ namespace datalog {
}
}
else {
relation_base& rel = ctx.get_datalog_context().get_relation(m_pred);
relation_base& rel = ctx.get_rel_context().get_relation(m_pred);
if ((!ctx.eager_emptiness_checking() || !rel.empty())) {
ctx.set_reg(m_reg, rel.clone());
}
@ -182,7 +182,7 @@ namespace datalog {
virtual void make_annotations(execution_context & ctx) {
ctx.set_register_annotation(m_reg, m_pred->get_name().bare_str());
}
virtual void display_head_impl(context & ctx, std::ostream & out) const {
virtual void display_head_impl(rel_context & ctx, std::ostream & out) const {
const char * rel_name = m_pred->get_name().bare_str();
if (m_store) {
out << "store " << m_reg << " into " << rel_name;
@ -213,7 +213,7 @@ namespace datalog {
virtual void make_annotations(execution_context & ctx) {
ctx.set_register_annotation(m_reg, "alloc");
}
virtual void display_head_impl(context & ctx, std::ostream & out) const {
virtual void display_head_impl(rel_context & ctx, std::ostream & out) const {
out << "dealloc " << m_reg;
}
};
@ -248,7 +248,7 @@ namespace datalog {
ctx.set_register_annotation(m_src, str);
}
}
virtual void display_head_impl(context & ctx, std::ostream & out) const {
virtual void display_head_impl(rel_context & ctx, std::ostream & out) const {
out << (m_clone ? "clone " : "move ") << m_src << " into " << m_tgt;
}
};
@ -304,11 +304,11 @@ namespace datalog {
virtual void make_annotations(execution_context & ctx) {
m_body->make_annotations(ctx);
}
virtual void display_head_impl(context & ctx, std::ostream & out) const {
virtual void display_head_impl(rel_context & ctx, std::ostream & out) const {
out << "while";
print_container(m_controls, out);
}
virtual void display_body_impl(context & ctx, std::ostream & out, std::string indentation) const {
virtual void display_body_impl(rel_context & ctx, std::ostream & out, std::string indentation) const {
m_body->display_indented(ctx, out, indentation+" ");
}
};
@ -349,9 +349,9 @@ namespace datalog {
}
TRACE("dl",
r1.get_signature().output(ctx.get_datalog_context().get_manager(), tout);
r1.get_signature().output(ctx.get_rel_context().get_manager(), tout);
tout<<":"<<r1.get_size_estimate_rows()<<" x ";
r2.get_signature().output(ctx.get_datalog_context().get_manager(), tout);
r2.get_signature().output(ctx.get_rel_context().get_manager(), tout);
tout<<":"<<r2.get_size_estimate_rows()<<" ->\n";);
try {
@ -371,7 +371,7 @@ namespace datalog {
}
TRACE("dl",
ctx.reg(m_res)->get_signature().output(ctx.get_datalog_context().get_manager(), tout);
ctx.reg(m_res)->get_signature().output(ctx.get_rel_context().get_manager(), tout);
tout<<":"<<ctx.reg(m_res)->get_size_estimate_rows()<<"\n";);
if (ctx.eager_emptiness_checking() && ctx.reg(m_res)->empty()) {
@ -385,7 +385,7 @@ namespace datalog {
ctx.get_register_annotation(m_rel1, a1);
ctx.set_register_annotation(m_res, "join " + a1 + " " + a2);
}
virtual void display_head_impl(context & ctx, std::ostream & out) const {
virtual void display_head_impl(rel_context & ctx, std::ostream & out) const {
out << "join " << m_rel1;
print_container(m_cols1, out);
out << " and " << m_rel2;
@ -431,10 +431,10 @@ namespace datalog {
}
virtual void make_annotations(execution_context & ctx) {
std::stringstream a;
a << "filter_equal " << m_col << " val: " << ctx.get_datalog_context().get_rmanager().to_nice_string(m_value);
a << "filter_equal " << m_col << " val: " << ctx.get_rel_context().get_rmanager().to_nice_string(m_value);
ctx.set_register_annotation(m_reg, a.str());
}
virtual void display_head_impl(context & ctx, std::ostream & out) const {
virtual void display_head_impl(rel_context & ctx, std::ostream & out) const {
out << "filter_equal " << m_reg << " col: " << m_col << " val: "
<< ctx.get_rmanager().to_nice_string(m_value);
}
@ -476,7 +476,7 @@ namespace datalog {
}
return true;
}
virtual void display_head_impl(context & ctx, std::ostream & out) const {
virtual void display_head_impl(rel_context & ctx, std::ostream & out) const {
out << "filter_identical " << m_reg << " ";
print_container(m_cols, out);
}
@ -519,7 +519,7 @@ namespace datalog {
}
return true;
}
virtual void display_head_impl(context & ctx, std::ostream & out) const {
virtual void display_head_impl(rel_context & ctx, std::ostream & out) const {
out << "filter_interpreted " << m_reg << " using "
<< mk_pp(m_cond, m_cond.get_manager());
}
@ -624,7 +624,7 @@ namespace datalog {
ctx.set_register_annotation(m_delta, "delta of "+str);
}
}
virtual void display_head_impl(context & ctx, std::ostream & out) const {
virtual void display_head_impl(rel_context & ctx, std::ostream & out) const {
out << (m_widen ? "widen " : "union ") << m_src << " into " << m_tgt;
if (m_delta!=execution_context::void_register) {
out << " with delta " << m_delta;
@ -678,7 +678,7 @@ namespace datalog {
return true;
}
virtual void display_head_impl(context & ctx, std::ostream & out) const {
virtual void display_head_impl(rel_context & ctx, std::ostream & out) const {
out << (m_projection ? "project " : "rename ") << m_src << " into " << m_tgt;
out << (m_projection ? " deleting columns " : " with cycle ");
print_container(m_cols, out);
@ -739,7 +739,7 @@ namespace datalog {
}
return true;
}
virtual void display_head_impl(context & ctx, std::ostream & out) const {
virtual void display_head_impl(rel_context & ctx, std::ostream & out) const {
out << "join_project " << m_rel1;
print_container(m_cols1, out);
out << " and " << m_rel2;
@ -800,7 +800,7 @@ namespace datalog {
}
return true;
}
virtual void display_head_impl(context & ctx, std::ostream & out) const {
virtual void display_head_impl(rel_context & ctx, std::ostream & out) const {
out << "select_equal_and_project " << m_src <<" into " << m_result << " col: " << m_col
<< " val: " << ctx.get_rmanager().to_nice_string(m_value);
}
@ -809,7 +809,7 @@ namespace datalog {
std::string s1 = "src";
ctx.get_register_annotation(m_src, s1);
s << "select equal project col " << m_col << " val: "
<< ctx.get_datalog_context().get_rmanager().to_nice_string(m_value) << " " << s1;
<< ctx.get_rel_context().get_rmanager().to_nice_string(m_value) << " " << s1;
ctx.set_register_annotation(m_result, s.str());
}
};
@ -854,7 +854,7 @@ namespace datalog {
}
return true;
}
virtual void display_head_impl(context & ctx, std::ostream & out) const {
virtual void display_head_impl(rel_context & ctx, std::ostream & out) const {
out << "filter_by_negation on " << m_tgt;
print_container(m_cols1, out);
out << " with " << m_neg_rel;
@ -887,12 +887,12 @@ namespace datalog {
}
virtual bool perform(execution_context & ctx) {
ctx.make_empty(m_tgt);
relation_base * rel = ctx.get_datalog_context().get_rmanager().mk_empty_relation(m_sig, m_pred);
relation_base * rel = ctx.get_rel_context().get_rmanager().mk_empty_relation(m_sig, m_pred);
rel->add_fact(m_fact);
ctx.set_reg(m_tgt, rel);
return true;
}
virtual void display_head_impl(context & ctx, std::ostream & out) const {
virtual void display_head_impl(rel_context & ctx, std::ostream & out) const {
out << "mk_unary_singleton into " << m_tgt << " sort:"
<< ctx.get_rmanager().to_nice_string(m_sig[0]) << " val:"
<< ctx.get_rmanager().to_nice_string(m_sig[0], m_fact[0]);
@ -919,10 +919,10 @@ namespace datalog {
instr_mk_total(const relation_signature & sig, func_decl* p, reg_idx tgt) : m_sig(sig), m_pred(p), m_tgt(tgt) {}
virtual bool perform(execution_context & ctx) {
ctx.make_empty(m_tgt);
ctx.set_reg(m_tgt, ctx.get_datalog_context().get_rmanager().mk_full_relation(m_sig, m_pred));
ctx.set_reg(m_tgt, ctx.get_rel_context().get_rmanager().mk_full_relation(m_sig, m_pred));
return true;
}
virtual void display_head_impl(context & ctx, std::ostream & out) const {
virtual void display_head_impl(rel_context & ctx, std::ostream & out) const {
out << "mk_total into " << m_tgt << " sort:"
<< ctx.get_rmanager().to_nice_string(m_sig);
}
@ -944,10 +944,10 @@ namespace datalog {
instr_mark_saturated(ast_manager & m, func_decl * pred)
: m_pred(pred, m) {}
virtual bool perform(execution_context & ctx) {
ctx.get_datalog_context().get_rmanager().mark_saturated(m_pred);
ctx.get_rel_context().get_rmanager().mark_saturated(m_pred);
return true;
}
virtual void display_head_impl(context & ctx, std::ostream & out) const {
virtual void display_head_impl(rel_context & ctx, std::ostream & out) const {
out << "mark_saturated " << m_pred->get_name().bare_str();
}
virtual void make_annotations(execution_context & ctx) {
@ -970,7 +970,7 @@ namespace datalog {
}
return true;
}
virtual void display_head_impl(context & ctx, std::ostream & out) const {
virtual void display_head_impl(rel_context & ctx, std::ostream & out) const {
out << "instr_assert_signature of " << m_tgt << " signature:";
print_container(m_sig, out);
}
@ -1019,7 +1019,7 @@ namespace datalog {
TRACE("dl",
tout <<"% ";
instr->display_head_impl(ctx.get_datalog_context(), tout);
instr->display_head_impl(ctx.get_rel_context(), tout);
tout <<"\n";);
success = !ctx.should_terminate() && instr->perform(ctx);
}
@ -1042,12 +1042,12 @@ namespace datalog {
}
}
void instruction_block::display_indented(context & ctx, std::ostream & out, std::string indentation) const {
void instruction_block::display_indented(rel_context & ctx, std::ostream & out, std::string indentation) const {
instr_seq_type::const_iterator it = m_data.begin();
instr_seq_type::const_iterator end = m_data.end();
for(; it!=end; ++it) {
instruction * i = (*it);
if (i->passes_output_thresholds(ctx) || i->being_recorded()) {
if (i->passes_output_thresholds(ctx.get_context()) || i->being_recorded()) {
i->display_indented(ctx, out, indentation);
}
}

18
src/muz_qe/dl_instruction.h
View file

@ -58,7 +58,7 @@ namespace datalog {
private:
typedef u_map<std::string> reg_annotations;
context & m_datalog_context;
context & m_context;
reg_vector m_registers;
reg_annotations m_reg_annotation;
@ -73,12 +73,12 @@ namespace datalog {
*/
bool m_eager_emptiness_checking;
public:
execution_context(context & datalog_context);
execution_context(context & context);
~execution_context();
void reset();
context & get_datalog_context() { return m_datalog_context; };
rel_context & get_rel_context() { return m_context.get_rel_context(); };
void set_timelimit(unsigned time_in_ms);
void reset_timelimit();
@ -208,7 +208,7 @@ namespace datalog {
The newline character at the end should not be printed.
*/
virtual void display_head_impl(context & ctx, std::ostream & out) const {
virtual void display_head_impl(rel_context & ctx, std::ostream & out) const {
out << "<instruction>";
}
/**
@ -216,7 +216,7 @@ namespace datalog {
Each line must be prepended by \c indentation and ended by a newline character.
*/
virtual void display_body_impl(context & ctx, std::ostream & out, std::string indentation) const {}
virtual void display_body_impl(rel_context & ctx, std::ostream & out, std::string indentation) const {}
public:
typedef execution_context::reg_type reg_type;
typedef execution_context::reg_idx reg_idx;
@ -227,10 +227,10 @@ namespace datalog {
virtual void make_annotations(execution_context & ctx) = 0;
void display(context & ctx, std::ostream & out) const {
void display(rel_context & ctx, std::ostream & out) const {
display_indented(ctx, out, "");
}
void display_indented(context & ctx, std::ostream & out, std::string indentation) const;
void display_indented(rel_context & ctx, std::ostream & out, std::string indentation) const;
static instruction * mk_load(ast_manager & m, func_decl * pred, reg_idx tgt);
/**
@ -329,10 +329,10 @@ namespace datalog {
void make_annotations(execution_context & ctx);
void display(context & ctx, std::ostream & out) const {
void display(rel_context & ctx, std::ostream & out) const {
display_indented(ctx, out, "");
}
void display_indented(context & ctx, std::ostream & out, std::string indentation) const;
void display_indented(rel_context & ctx, std::ostream & out, std::string indentation) const;
};

4
src/muz_qe/dl_mk_bit_blast.cpp
View file

@ -161,7 +161,7 @@ namespace datalog {
impl(context& ctx):
m_context(ctx),
m(ctx.get_manager()),
m_params(ctx.get_params()),
m_params(ctx.get_params().p),
m_rules(ctx.get_rule_manager()),
m_blaster(ctx.get_manager(), m_params),
m_rewriter(ctx.get_manager(), ctx, m_rules) {
@ -172,7 +172,7 @@ namespace datalog {
rule_set * operator()(rule_set const & source, model_converter_ref& mc, proof_converter_ref& pc) {
// TODO mc, pc
if (!m_context.get_params().get_bool("bit_blast", false)) {
if (!m_context.get_params().bit_blast()) {
return 0;
}
if (m_context.get_engine() != PDR_ENGINE) {

6
src/muz_qe/dl_mk_explanations.cpp
View file

@ -607,7 +607,7 @@ namespace datalog {
m_e_sort = m_decl_util.mk_rule_sort();
m_pinned.push_back(m_e_sort);
relation_manager & rmgr = ctx.get_rmanager();
relation_manager & rmgr = ctx.get_rel_context().get_rmanager();
symbol er_symbol = explanation_relation_plugin::get_name(relation_level);
m_er_plugin = static_cast<explanation_relation_plugin *>(rmgr.get_relation_plugin(er_symbol));
if(!m_er_plugin) {
@ -640,7 +640,7 @@ namespace datalog {
void mk_explanations::assign_rel_level_kind(func_decl * e_decl, func_decl * orig) {
SASSERT(m_relation_level);
relation_manager & rmgr = m_context.get_rmanager();
relation_manager & rmgr = m_context.get_rel_context().get_rmanager();
unsigned sz = e_decl->get_arity();
relation_signature sig;
rmgr.from_predicate(e_decl, sig);
@ -884,7 +884,7 @@ namespace datalog {
m_context.collect_predicates(m_original_preds);
rule_set * res = alloc(rule_set, m_context);
transform_facts(m_context.get_rmanager());
transform_facts(m_context.get_rel_context().get_rmanager());
transform_rules(source, *res);
return res;
}

2
src/muz_qe/dl_mk_magic_sets.cpp
View file

@ -365,7 +365,7 @@ namespace datalog {
rule * r = *it;
transform_rule(task.m_adornment, r);
}
if(!m_context.get_relation(task.m_pred).empty()) {
if(!m_context.get_rel_context().get_relation(task.m_pred).empty()) {
//we need a rule to copy facts that are already in a relation into the adorned
//relation (since out intentional predicates can have facts, not only rules)
create_transfer_rule(task);

2
src/muz_qe/dl_mk_partial_equiv.cpp
View file

@ -97,7 +97,7 @@ namespace datalog {
return 0;
}
relation_manager & rm = m_context.get_rmanager();
relation_manager & rm = m_context.get_rel_context().get_rmanager();
rule_set::decl2rules::iterator it = source.begin_grouped_rules();
rule_set::decl2rules::iterator end = source.end_grouped_rules();

10
src/muz_qe/dl_mk_rule_inliner.cpp
View file

@ -205,7 +205,7 @@ namespace datalog {
void mk_rule_inliner::count_pred_occurrences(rule_set const & orig)
{
m_context.get_rmanager().collect_non_empty_predicates(m_preds_with_facts);
m_context.get_rel_context().get_rmanager().collect_non_empty_predicates(m_preds_with_facts);
rule_set::iterator rend = orig.end();
for (rule_set::iterator rit = orig.begin(); rit!=rend; ++rit) {
@ -750,8 +750,7 @@ namespace datalog {
valid.reset();
valid.resize(sz, true);
params_ref const& params = m_context.get_params();
bool allow_branching = params.get_bool("inline_linear_branch", false);
bool allow_branching = m_context.get_params().inline_linear_branch();
for (unsigned i = 0; i < sz; ++i) {
@ -842,7 +841,6 @@ namespace datalog {
bool something_done = false;
ref<horn_subsume_model_converter> hsmc;
ref<replace_proof_converter> hpc;
params_ref const& params = m_context.get_params();
if (source.get_num_rules() == 0) {
return 0;
@ -867,7 +865,7 @@ namespace datalog {
scoped_ptr<rule_set> res = alloc(rule_set, m_context);
if (params.get_bool("inline_eager", true)) {
if (m_context.get_params().inline_eager()) {
TRACE("dl", source.display(tout << "before eager inlining\n"););
plan_inlining(source);
something_done = transform_rules(source, *res);
@ -879,7 +877,7 @@ namespace datalog {
TRACE("dl", res->display(tout << "after eager inlining\n"););
}
if (params.get_bool("inline_linear", true) && inline_linear(res)) {
if (m_context.get_params().inline_linear() && inline_linear(res)) {
something_done = true;
}

2
src/muz_qe/dl_mk_similarity_compressor.cpp
View file

@ -361,7 +361,7 @@ namespace datalog {
collect_orphan_consts(*it, const_infos, val_fact);
m_context.add_fact(aux_pred, val_fact);
}
m_context.get_rmanager().mark_saturated(aux_pred);
m_context.get_rel_context().get_rmanager().mark_saturated(aux_pred);
app * new_head = r->get_head();
ptr_vector<app> new_tail;

9
src/muz_qe/dl_mk_simple_joins.cpp
View file

@ -569,10 +569,11 @@ namespace datalog {
cost estimate_size(app * t) const {
func_decl * pred = t->get_decl();
unsigned n=pred->get_arity();
if( (m_context.saturation_was_run() && m_context.get_rmanager().try_get_relation(pred))
|| m_context.get_rmanager().is_saturated(pred)) {
SASSERT(m_context.get_rmanager().try_get_relation(pred)); //if it is saturated, it should exist
unsigned rel_size_int = m_context.get_relation(pred).get_size_estimate_rows();
relation_manager& rm = m_context.get_rel_context().get_rmanager();
if( (m_context.saturation_was_run() && rm.try_get_relation(pred))
|| rm.is_saturated(pred)) {
SASSERT(rm.try_get_relation(pred)); //if it is saturated, it should exist
unsigned rel_size_int = m_context.get_rel_context().get_relation(pred).get_size_estimate_rows();
if(rel_size_int!=0) {
cost rel_size = static_cast<cost>(rel_size_int);
cost curr_size = rel_size;

2
src/muz_qe/dl_mk_subsumption_checker.cpp
View file

@ -250,7 +250,7 @@ namespace datalog {
}
void mk_subsumption_checker::scan_for_relations_total_due_to_facts() {
relation_manager& rm = m_context.get_rmanager();
relation_manager& rm = m_context.get_rel_context().get_rmanager();
decl_set candidate_preds;
m_context.collect_predicates(candidate_preds);

2
src/muz_qe/dl_mk_unbound_compressor.cpp
View file

@ -337,7 +337,7 @@ namespace datalog {
// TODO mc, pc
m_modified = false;
m_context.get_rmanager().collect_non_empty_predicates(m_non_empty_rels);
m_context.get_rel_context().get_rmanager().collect_non_empty_predicates(m_non_empty_rels);
unsigned init_rule_cnt = source.get_num_rules();
SASSERT(m_rules.empty());

2
src/muz_qe/dl_rule.cpp
View file

@ -1014,7 +1014,7 @@ namespace datalog {
out << '.';
if (ctx.output_profile()) {
out << " {";
output_profile(ctx, out);
output_profile(out);
out << '}';
}
out << '\n';

766
src/muz_qe/dl_smt_relation.cpp
View file

@ -1,766 +0,0 @@
/*++
Copyright (c) 2010 Microsoft Corporation
Module Name:
dl_smt_relation.cpp
Abstract:
Relation based on SMT signature.
Author:
Nikolaj Bjorner (nbjorner) 2010-10-10
Revision History:
--*/
#include <sstream>
#include "debug.h"
#include "ast_pp.h"
#include "dl_context.h"
#include "dl_smt_relation.h"
#include "expr_abstract.h"
#include "smt_kernel.h"
#include "th_rewriter.h"
#include "qe.h"
#include "datatype_decl_plugin.h"
#include "bv_decl_plugin.h"
#include "ast_ll_pp.h"
#include "expr_context_simplifier.h"
#include "has_free_vars.h"
#include "ast_smt_pp.h"
namespace datalog {
smt_relation::smt_relation(smt_relation_plugin & p, const relation_signature & s, expr* r)
: relation_base(p, s),
m_rel(r, p.get_ast_manager()),
m_bound_vars(p.get_ast_manager())
{
ast_manager& m = p.get_ast_manager();
for (unsigned i = 0; m_bound_vars.size() < s.size(); ++i) {
unsigned j = s.size() - i - 1;
m_bound_vars.push_back(m.mk_const(symbol(j), s[j]));
}
SASSERT(is_well_formed());
}
smt_relation::~smt_relation() {
}
bool smt_relation::is_well_formed() const {
ast_manager& m = get_manager();
ptr_vector<sort> bound_sorts;
for (unsigned i = 0; i < m_bound_vars.size(); ++i) {
bound_sorts.push_back(m.get_sort(m_bound_vars[i]));
}
return is_well_formed_vars(bound_sorts, get_relation());
}
void smt_relation::instantiate(expr* r, expr_ref& result) const {
ast_manager& m = get_manager();
var_subst subst(m);
ptr_vector<sort> bound_sorts;
for (unsigned i = 0; i < m_bound_vars.size(); ++i) {
bound_sorts.push_back(m.get_sort(m_bound_vars[i]));
}
TRACE("smt_relation",
tout << mk_ll_pp(r, m) << "\n";
for (unsigned i = 0; i < bound_sorts.size(); ++i) {
tout << mk_pp(bound_sorts[i], m) << " ";
}
tout << "\n";
);
SASSERT(is_well_formed_vars(bound_sorts, r));
subst(r, m_bound_vars.size(), m_bound_vars.c_ptr(), result);
}
void smt_relation::mk_abstract(expr* r, expr_ref& result) const {
ast_manager& m = get_manager();
TRACE("smt_relation", tout << mk_ll_pp(r, m) << "\n";);
expr_abstract(m, 0, m_bound_vars.size(), m_bound_vars.c_ptr(), r, result);
TRACE("smt_relation", tout << mk_ll_pp(result, m) << "\n";);
ptr_vector<sort> bound_sorts;
for (unsigned i = 0; i < m_bound_vars.size(); ++i) {
bound_sorts.push_back(m.get_sort(m_bound_vars[i]));
}
SASSERT(is_well_formed_vars(bound_sorts, r));
}
void smt_relation::set_relation(expr* r) {
m_rel = r;
is_well_formed();
}
void smt_relation::add_relation(expr* s) {
ast_manager& m = get_manager();
m_rel = m.mk_or(m_rel, s);
is_well_formed();
}
void smt_relation::filter_relation(expr* s) {
ast_manager& m = get_manager();
m_rel = m.mk_and(m_rel, s);
is_well_formed();
}
expr* smt_relation::get_relation() const {
return m_rel.get();
}
void smt_relation::simplify(expr_ref& fml) const {
th_rewriter rw(get_manager());
rw(fml);
}
bool smt_relation::empty() const {
ast_manager& m = get_manager();
expr* r = get_relation();
if (m.is_true(r)) {
return false;
}
if (m.is_false(r)) {
return true;
}
IF_VERBOSE(10, verbose_stream() << "Checking emptiness...\n"; );
smt_params& params = get_plugin().get_fparams();
// [Leo]: asserted_formulas do not have support for der.
// We should use the tactics der.
// flet<bool> flet2(params.m_der, true);
smt::kernel ctx(m, params);
expr_ref tmp(m);
instantiate(r, tmp);
ctx.assert_expr(tmp);
if (get_plugin().get_fparams().m_dump_goal_as_smt) {
static unsigned n = 0;
std::ostringstream strm;
strm << "File" << n << ".smt2";
std::ofstream out(strm.str().c_str());
ast_smt_pp pp(m);
pp.display_smt2(out, tmp);
++n;
}
return l_false == ctx.check();
}
void smt_relation::add_fact(const relation_fact & f) {
SASSERT(f.size() == size());
ast_manager& m = get_manager();
expr_ref_vector eqs(m);
for (unsigned i = 0; i < f.size(); ++i) {
eqs.push_back(m.mk_eq(m.mk_var(i,m.get_sort(f[i])), f[i]));
}
expr_ref e1(m.mk_and(eqs.size(), eqs.c_ptr()), m);
add_relation(e1);
}
bool smt_relation::contains_fact(const relation_fact & f) const {
ast_manager& m = get_manager();
expr_ref_vector eqs(m);
expr_ref cond(m);
for (unsigned i = 0; i < f.size(); ++i) {
eqs.push_back(m.mk_eq(m.mk_var(i,m.get_sort(f[i])), f[i]));
}
cond = m.mk_and(eqs.size(), eqs.c_ptr());
return const_cast<smt_relation*>(this)->contains(cond);
}
//
// facts in Rel iff
// facts => Rel iff
// facts & not Rel is unsat
//
bool smt_relation::contains(expr* facts) {
ast_manager& m = get_manager();
expr_ref fml_free(m), fml_inst(m);
fml_free = m.mk_and(facts, m.mk_not(get_relation()));
instantiate(fml_free, fml_inst);
smt_params& params = get_plugin().get_fparams();
// [Leo]: asserted_formulas do not have support for qe nor der.
// We should use the tactics qe and der.
// BTW, qe at asserted_formulas was disabled when we moved to codeplex, but the field m_quant_elim was not deleted.
//
// flet<bool> flet0(params.m_quant_elim, true);
flet<bool> flet1(params.m_nnf_cnf, false);
// flet<bool> flet2(params.m_der, true);
smt::kernel ctx(m, params);
ctx.assert_expr(fml_inst);
lbool result = ctx.check();
TRACE("smt_relation",
display(tout);
tout << mk_pp(facts, m) << "\n";
tout << ((result == l_false)?"true":"false") << "\n";);
return result == l_false;
}
smt_relation * smt_relation::clone() const {
return alloc(smt_relation, get_plugin(), get_signature(), get_relation());
}
smt_relation * smt_relation::complement(func_decl* p) const {
ast_manager& m = get_manager();
smt_relation* result = alloc(smt_relation, get_plugin(), get_signature(), m.mk_not(get_relation()));
TRACE("smt_relation",
display(tout<<"src:\n");
result->display(tout<<"complement:\n"););
return result;
}
void smt_relation::display(std::ostream & out) const {
if (is_finite_domain()) {
display_finite(out);
}
else {
out << mk_ll_pp(get_relation(), get_manager()) << "\n";
}
}
smt_relation_plugin & smt_relation::get_plugin() const {
return static_cast<smt_relation_plugin &>(relation_base::get_plugin());
}
bool smt_relation::is_finite_domain() const {
relation_signature const& sig = get_signature();
for (unsigned i = 0; i < sig.size(); ++i) {
if (!get_plugin().is_finite_domain(sig[i])) {
return false;
}
}
return true;
}
void smt_relation::display_finite(std::ostream & out) const {
ast_manager& m = get_manager();
smt_params& params = get_plugin().get_fparams();
expr* r = get_relation();
expr_ref tmp(m);
expr_ref_vector values(m), eqs(m);
unsigned num_vars = m_bound_vars.size();
values.resize(num_vars);
eqs.resize(num_vars);
instantiate(r, tmp);
flet<bool> flet4(params.m_model, true);
smt::kernel ctx(m, params);
ctx.assert_expr(tmp);
while (true) {
lbool is_sat = ctx.check();
if (is_sat == l_false) {
break;
}
model_ref mod;
ctx.get_model(mod);
for (unsigned i = 0; i < num_vars; ++i) {
mod->eval(m_bound_vars[i], tmp, true);
values[i] = tmp;
eqs[i] = m.mk_eq(values[i].get(), m_bound_vars[i]);
}
out << " (";
for (unsigned i = 0; i < num_vars; ++i) {
unsigned j = num_vars - 1 - i;
out << mk_pp(values[j].get(), m);
if (i + 1 < num_vars) {
out << " ";
}
}
out << ")\n";
tmp = m.mk_not(m.mk_and(num_vars, eqs.c_ptr()));
ctx.assert_expr(tmp);
}
}
// -----------------------------------
//
// smt_relation_plugin
//
// -----------------------------------
smt_relation_plugin::smt_relation_plugin(relation_manager & m)
: relation_plugin(smt_relation_plugin::get_name(), m), m_counter(0) {}
relation_base * smt_relation_plugin::mk_empty(const relation_signature & s) {
return alloc(smt_relation, *this, s, get_ast_manager().mk_false());
}
class smt_relation_plugin::join_fn : public convenient_relation_join_fn {
smt_relation_plugin& m_plugin;
expr_ref_vector m_conjs;
public:
join_fn(smt_relation_plugin& p, const relation_signature & o1_sig, const relation_signature & o2_sig, unsigned col_cnt,
const unsigned * cols1, const unsigned * cols2)
: convenient_relation_join_fn(o1_sig, o2_sig, col_cnt, cols1, cols2),
m_plugin(p),
m_conjs(p.get_ast_manager()) {
ast_manager& m = p.get_ast_manager();
unsigned sz = m_cols1.size();
for (unsigned i = 0; i < sz; ++i) {
unsigned col1 = m_cols1[i];
unsigned col2 = m_cols2[i];
var* v1 = m.mk_var(col1, o1_sig[col1]);
var* v2 = m.mk_var(col2 + o1_sig.size(), o2_sig[col2]);
m_conjs.push_back(m.mk_eq(v1, v2));
}
}
virtual relation_base * operator()(const relation_base & r1, const relation_base & r2) {
ast_manager& m = m_plugin.get_ast_manager();
expr_ref e2(m), res(m);
shift_vars sh(m);
sh(get(r2).get_relation(), r1.get_signature().size(), e2);
m_conjs.push_back(get(r1).get_relation());
m_conjs.push_back(e2);
res = m.mk_and(m_conjs.size(), m_conjs.c_ptr());
m_conjs.pop_back();
m_conjs.pop_back();
smt_relation* result = alloc(smt_relation, m_plugin, get_result_signature(), res);
TRACE("smt_relation",
get(r1).display(tout << "src1:\n");
get(r2).display(tout << "src2:\n");
for (unsigned i = 0; i < m_conjs.size(); ++i) {
tout << m_cols1[i] << " = " << m_cols2[i] << " -- ";
tout << mk_pp(m_conjs[i].get(), m) << "\n";
}
result->display(tout << "dst:\n");
);
return result;
}
};
relation_join_fn * smt_relation_plugin::mk_join_fn(const relation_base & r1, const relation_base & r2,
unsigned col_cnt, const unsigned * cols1, const unsigned * cols2) {
if (!check_kind(r1) || !check_kind(r2)) {
return 0;
}
return alloc(join_fn, *this, r1.get_signature(), r2.get_signature(), col_cnt, cols1, cols2);
}
class smt_relation_plugin::project_fn : public convenient_relation_project_fn {
smt_relation_plugin& m_plugin;
expr_ref_vector m_subst;
sort_ref_vector m_sorts;
svector<symbol> m_names;
public:
project_fn(smt_relation_plugin& p,
const relation_signature & orig_sig, unsigned removed_col_cnt, const unsigned * removed_cols)
: convenient_relation_project_fn(orig_sig, removed_col_cnt, removed_cols),
m_plugin(p),
m_subst(p.get_ast_manager()),
m_sorts(p.get_ast_manager()) {
ast_manager& m = p.get_ast_manager();
unsigned_vector const& cols = m_removed_cols;
unsigned num_cols = cols.size();
unsigned lo = 0, hi = num_cols;
for (unsigned i = 0, c = 0; i < orig_sig.size(); ++i) {
SASSERT(c <= num_cols);
if (c == num_cols) {
SASSERT(lo == num_cols);
m_subst.push_back(m.mk_var(hi, orig_sig[i]));
++hi;
continue;
}
SASSERT(c < num_cols);
unsigned col = cols[c];
SASSERT(i <= col);
if (i == col) {
m_names.push_back(symbol(p.fresh_name()));
m_sorts.push_back(orig_sig[col]);
m_subst.push_back(m.mk_var(lo, orig_sig[i]));
++lo;
++c;
continue;
}
m_subst.push_back(m.mk_var(hi, orig_sig[i]));
++hi;
}
m_subst.reverse();
m_sorts.reverse();
m_names.reverse();
}
virtual relation_base * operator()(const relation_base & r) {
ast_manager& m = m_plugin.get_ast_manager();
expr_ref tmp1(m), tmp2(m);
var_subst subst(m);
smt_relation* result = 0;
tmp1 = get(r).get_relation();
subst(tmp1, m_subst.size(), m_subst.c_ptr(), tmp2);
tmp2 = m.mk_exists(m_sorts.size(), m_sorts.c_ptr(), m_names.c_ptr(), tmp2);
result = alloc(smt_relation, m_plugin, get_result_signature(), tmp2);
TRACE("smt_relation",
tout << "Signature: ";
for (unsigned i = 0; i < r.get_signature().size(); ++i) {
tout << mk_pp(r.get_signature()[i], m) << " ";
}
tout << "Remove: ";
for (unsigned i = 0; i < m_removed_cols.size(); ++i) {
tout << m_removed_cols[i] << " ";
}
tout << "\n";
tout << "Subst: ";
for (unsigned i = 0; i < m_subst.size(); ++i) {
tout << mk_pp(m_subst[i].get(), m) << " ";
}
tout << "\n";
get(r).display(tout);
tout << " --> \n";
result->display(tout););
return result;
}
};
relation_transformer_fn * smt_relation_plugin::mk_project_fn(const relation_base & r,
unsigned col_cnt, const unsigned * removed_cols) {
return alloc(project_fn, *this, r.get_signature(), col_cnt, removed_cols);
}
class smt_relation_plugin::rename_fn : public convenient_relation_rename_fn {
smt_relation_plugin& m_plugin;
expr_ref_vector m_subst;
public:
rename_fn(smt_relation_plugin& p, const relation_signature & orig_sig, unsigned cycle_len, const unsigned * cycle)
: convenient_relation_rename_fn(orig_sig, cycle_len, cycle),
m_plugin(p),
m_subst(p.get_ast_manager()) {
ast_manager& m = p.get_ast_manager();
for (unsigned i = 0; i < orig_sig.size(); ++i) {
m_subst.push_back(m.mk_var(i, orig_sig[i]));
}
unsigned col1, col2;
for (unsigned i = 0; i +1 < cycle_len; ++i) {
col1 = cycle[i];
col2 = cycle[i+1];
m_subst[col2] = m.mk_var(col1, orig_sig[col2]);
}
col1 = cycle[cycle_len-1];
col2 = cycle[0];
m_subst[col2] = m.mk_var(col1, orig_sig[col2]);
m_subst.reverse();
}
virtual relation_base * operator()(const relation_base & r) {
ast_manager& m = m_plugin.get_ast_manager();
expr_ref res(m);
var_subst subst(m);
subst(get(r).get_relation(), m_subst.size(), m_subst.c_ptr(), res);
TRACE("smt_relation3",
tout << "cycle: ";
for (unsigned i = 0; i < m_cycle.size(); ++i) {
tout << m_cycle[i] << " ";
}
tout << "\n";
tout << "old_sig: ";
for (unsigned i = 0; i < r.get_signature().size(); ++i) {
tout << mk_pp(r.get_signature()[i], m) << " ";
}
tout << "\n";
tout << "new_sig: ";
for (unsigned i = 0; i < get_result_signature().size(); ++i) {
tout << mk_pp(get_result_signature()[i], m) << " ";
}
tout << "\n";
tout << "subst: ";
for (unsigned i = 0; i < m_subst.size(); ++i) {
tout << mk_pp(m_subst[i].get(), m) << " ";
}
tout << "\n";
get(r).display(tout << "src:\n");
tout << "dst:\n" << mk_ll_pp(res, m) << "\n";
);
smt_relation* result = alloc(smt_relation, m_plugin, get_result_signature(), res);
return result;
}
};
relation_transformer_fn * smt_relation_plugin::mk_rename_fn(const relation_base & r,
unsigned cycle_len, const unsigned * permutation_cycle) {
if(!check_kind(r)) {
return 0;
}
return alloc(rename_fn, *this, r.get_signature(), cycle_len, permutation_cycle);
}
class smt_relation_plugin::union_fn : public relation_union_fn {
smt_relation_plugin& m_plugin;
public:
union_fn(smt_relation_plugin& p) :
m_plugin(p) {
}
virtual void operator()(relation_base & r, const relation_base & src, relation_base * delta) {
ast_manager& m = m_plugin.get_ast_manager();
expr* srcE = get(src).get_relation();
TRACE("smt_relation",
tout << "dst:\n";
get(r).display(tout);
tout << "src:\n";
get(src).display(tout););
SASSERT(get(src).is_well_formed());
SASSERT(get(r).is_well_formed());
if (delta) {
//
// delta(a) <-
// exists x . srcE(a, x) & not rE(a, y)
expr_ref rInst(m), srcInst(m), tmp(m), tmp1(m);
expr_ref notR(m), srcGround(m);
smt_params& fparams = get(r).get_plugin().get_fparams();
params_ref const& params = get(r).get_plugin().get_params();
get(r).instantiate(get(r).get_relation(), rInst);
get(src).instantiate(get(src).get_relation(), srcInst);
qe::expr_quant_elim_star1 qe(m, fparams);
IF_VERBOSE(10, verbose_stream() << "Computing delta...\n"; );
if (params.get_bool("smt_relation_ground_recursive", false)) {
// ensure R is ground. Simplify S using assumption not R
if (!is_ground(rInst)) {
proof_ref pr(m);
qe(rInst, tmp, pr);
rInst = tmp;
get(r).set_relation(rInst);
}
SASSERT(is_ground(rInst));
notR = m.mk_not(rInst);
qe.reduce_with_assumption(notR, srcInst, tmp);
SASSERT(is_ground(tmp));
}
else {
// Simplify not R usng assumption Exists x . S.
expr_ref srcGround(srcInst, m);
app_ref_vector srcVars(m);
qe::hoist_exists(srcGround, srcVars);
SASSERT(is_ground(srcGround));
notR = m.mk_not(rInst);
qe.reduce_with_assumption(srcGround, notR, tmp1);
tmp = m.mk_and(srcInst, tmp1);
SASSERT(!has_free_vars(tmp));
TRACE("smt_relation",
tout << "elim_exists result:\n" << mk_ll_pp(tmp, m) << "\n";);
}
SASSERT(!has_free_vars(tmp));
get(r).simplify(tmp);
get(src).mk_abstract(tmp, tmp1);
TRACE("smt_relation", tout << "abstracted:\n"; tout << mk_ll_pp(tmp1, m) << "\n";);
get(*delta).set_relation(tmp1);
get(r).add_relation(tmp1);
}
else {
get(r).add_relation(srcE);
}
TRACE("smt_relation", get(r).display(tout << "dst':\n"););
}
};
relation_union_fn * smt_relation_plugin::mk_union_fn(const relation_base & tgt, const relation_base & src,
const relation_base * delta) {
if (!check_kind(tgt) || !check_kind(src) || (delta && !check_kind(*delta))) {
return 0;
}
return alloc(union_fn, *this);
}
relation_union_fn * smt_relation_plugin::mk_widen_fn(const relation_base & tgt, const relation_base & src,
const relation_base * delta) {
if (!check_kind(tgt) || !check_kind(src) || (delta && !check_kind(*delta))) {
return 0;
}
return alloc(union_fn, *this);
}
class smt_relation_plugin::filter_interpreted_fn : public relation_mutator_fn {
smt_relation_plugin& m_plugin;
app_ref m_condition;
public:
filter_interpreted_fn(smt_relation_plugin& p, app * condition)
: m_plugin(p),
m_condition(condition, p.get_ast_manager()) {
}
virtual void operator()(relation_base & r) {
SASSERT(m_plugin.check_kind(r));
get(r).filter_relation(m_condition);
TRACE("smt_relation",
tout << mk_pp(m_condition, m_plugin.get_ast_manager()) << "\n";
get(r).display(tout);
);
}
};
relation_mutator_fn * smt_relation_plugin::mk_filter_interpreted_fn(const relation_base & r, app * condition) {
if(!check_kind(r)) {
return 0;
}
return alloc(filter_interpreted_fn, *this, condition);
}
relation_mutator_fn * smt_relation_plugin::mk_filter_equal_fn(const relation_base & r,
const relation_element & value, unsigned col) {
if(!check_kind(r)) {
return 0;
}
ast_manager& m = get_ast_manager();
app_ref condition(m);
expr_ref var(m.mk_var(col, r.get_signature()[col]), m);
condition = m.mk_eq(var, value);
return mk_filter_interpreted_fn(r, condition);
}
class smt_relation_plugin::filter_identical_fn : public relation_mutator_fn {
smt_relation_plugin& m_plugin;
expr_ref m_condition;
public:
filter_identical_fn(smt_relation_plugin& p, const relation_signature & sig, unsigned col_cnt, const unsigned * identical_cols)
: m_plugin(p),
m_condition(p.get_ast_manager()) {
if (col_cnt <= 1) {
return;
}
ast_manager& m = p.get_ast_manager();
unsigned col = identical_cols[0];
expr_ref v0(m.mk_var(col, sig[col]), m);
expr_ref_vector eqs(m);
for (unsigned i = 1; i < col_cnt; ++i) {
col = identical_cols[i];
eqs.push_back(m.mk_eq(v0, m.mk_var(col, sig[col])));
}
m_condition = m.mk_and(eqs.size(), eqs.c_ptr());
}
virtual void operator()(relation_base & r) {
get(r).filter_relation(m_condition);
TRACE("smt_relation",
tout << mk_pp(m_condition, m_plugin.get_ast_manager()) << "\n";
get(r).display(tout);
);
}
};
relation_mutator_fn * smt_relation_plugin::mk_filter_identical_fn(const relation_base & r,
unsigned col_cnt, const unsigned * identical_cols) {
if (!check_kind(r)) {
return 0;
}
return alloc(filter_identical_fn, *this, r.get_signature(), col_cnt, identical_cols);
}
class smt_relation_plugin::negation_filter_fn : public convenient_relation_negation_filter_fn {
smt_relation_plugin& m_plugin;
expr_ref_vector m_conjs;
public:
negation_filter_fn(smt_relation_plugin& p,
const relation_base & tgt, const relation_base & neg_t,
unsigned joined_col_cnt, const unsigned * t_cols, const unsigned * negated_cols) :
convenient_negation_filter_fn(tgt, neg_t, joined_col_cnt, t_cols, negated_cols),
m_plugin(p),
m_conjs(p.get_ast_manager()) {
ast_manager& m = p.get_ast_manager();
unsigned sz = m_cols1.size();
for (unsigned i = 0; i < sz; ++i) {
unsigned col1 = m_cols1[i];
unsigned col2 = m_cols2[i];
var* v1 = m.mk_var(col1, tgt.get_signature()[col1]);
var* v2 = m.mk_var(col2, neg_t.get_signature()[col2]);
m_conjs.push_back(m.mk_eq(v1, v2));
}
}
void operator()(relation_base & t, const relation_base & negated_obj) {
// TBD: fixme.
NOT_IMPLEMENTED_YET();
ast_manager& m = m_plugin.get_ast_manager();
expr_ref res(m), e2(m);
shift_vars sh(m);
sh(get(negated_obj).get_relation(), t.get_signature().size(), e2);
m_conjs.push_back(get(t).get_relation());
m_conjs.push_back(m.mk_not(e2));
res = m.mk_and(m_conjs.size(), m_conjs.c_ptr());
m_conjs.pop_back();
m_conjs.pop_back();
// TBD: free variables in negation?
}
};
relation_intersection_filter_fn * smt_relation_plugin::mk_filter_by_negation_fn(const relation_base & t,
const relation_base & negated_obj, unsigned joined_col_cnt,
const unsigned * t_cols, const unsigned * negated_cols) {
if (!check_kind(t) || !check_kind(negated_obj)) {
return 0;
}
return alloc(negation_filter_fn, *this, t, negated_obj, joined_col_cnt, t_cols, negated_cols);
}
smt_relation& smt_relation_plugin::get(relation_base& r) { return dynamic_cast<smt_relation&>(r); }
smt_relation const & smt_relation_plugin::get(relation_base const& r) { return dynamic_cast<smt_relation const&>(r); }
bool smt_relation_plugin::can_handle_signature(relation_signature const& sig) {
// TBD: refine according to theories handled by quantifier elimination
return get_manager().is_non_explanation(sig);
}
// TBD: when relations are finite domain, they also support table iterators.
symbol smt_relation_plugin::fresh_name() {
return symbol(m_counter++);
}
smt_params& smt_relation_plugin::get_fparams() {
return const_cast<smt_params&>(get_manager().get_context().get_fparams());
}
params_ref const& smt_relation_plugin::get_params() {
return get_manager().get_context().get_params();
}
bool smt_relation_plugin::is_finite_domain(sort *s) const {
ast_manager& m = get_ast_manager();
if (m.is_bool(s)) {
return true;
}
bv_util bv(m);
if (bv.is_bv_sort(s)) {
return true;
}
datatype_util dt(m);
if (dt.is_datatype(s) && !dt.is_recursive(s)) {
ptr_vector<func_decl> const& constrs = *dt.get_datatype_constructors(s);
for (unsigned i = 0; i < constrs.size(); ++i) {
func_decl* f = constrs[i];
for (unsigned j = 0; j < f->get_arity(); ++j) {
if (!is_finite_domain(f->get_domain(j))) {
return false;
}
}
}
return true;
}
return false;
}
};

141
src/muz_qe/dl_smt_relation.h
View file

@ -1,141 +0,0 @@
/*++
Copyright (c) 2010 Microsoft Corporation
Module Name:
dl_smt_relation.h
Abstract:
Relation signature represented by signatures that have quantifier elimination.
Author:
Nikolaj Bjorner (nbjorner) 2010-10-10
Revision History:
--*/
#ifndef _DL_SMT_RELATION_H_
#define _DL_SMT_RELATION_H_
#include "dl_base.h"
#include "smt_params.h"
#include "params.h"
namespace datalog {
class smt_relation;
class smt_relation_plugin : public relation_plugin {
unsigned m_counter;
friend class smt_relation;
class join_fn;
class project_fn;
class rename_fn;
class union_fn;
class filter_identical_fn;
class filter_interpreted_fn;
class negation_filter_fn;
public:
smt_relation_plugin(relation_manager & m);
virtual bool can_handle_signature(const relation_signature & s);
static symbol get_name() { return symbol("smt_relation"); }
virtual relation_base * mk_empty(const relation_signature & s);
virtual relation_join_fn * mk_join_fn(const relation_base & t1, const relation_base & t2,
unsigned col_cnt, const unsigned * cols1, const unsigned * cols2);
virtual relation_transformer_fn * mk_project_fn(const relation_base & t, unsigned col_cnt,
const unsigned * removed_cols);
virtual relation_transformer_fn * mk_rename_fn(const relation_base & t, unsigned permutation_cycle_len,
const unsigned * permutation_cycle);
virtual relation_union_fn * mk_union_fn(const relation_base & tgt, const relation_base & src,
const relation_base * delta);
virtual relation_union_fn * mk_widen_fn(const relation_base & tgt, const relation_base & src,
const relation_base * delta);
virtual relation_mutator_fn * mk_filter_identical_fn(const relation_base & t, unsigned col_cnt,
const unsigned * identical_cols);
virtual relation_mutator_fn * mk_filter_equal_fn(const relation_base & t, const relation_element & value,
unsigned col);
virtual relation_mutator_fn * mk_filter_interpreted_fn(const relation_base & t, app * condition);
virtual relation_intersection_filter_fn * mk_filter_by_negation_fn(const relation_base & t,
const relation_base & negated_obj, unsigned joined_col_cnt,
const unsigned * t_cols, const unsigned * negated_cols);
symbol fresh_name();
smt_params& get_fparams();
params_ref const& get_params();
bool is_finite_domain(sort* s) const;
private:
static smt_relation& get(relation_base& r);
static smt_relation const & get(relation_base const& r);
};
class smt_relation : public relation_base {
friend class smt_relation_plugin;
friend class smt_relation_plugin::join_fn;
friend class smt_relation_plugin::project_fn;
friend class smt_relation_plugin::rename_fn;
friend class smt_relation_plugin::union_fn;
friend class smt_relation_plugin::filter_identical_fn;
friend class smt_relation_plugin::filter_interpreted_fn;
friend class smt_relation_plugin::negation_filter_fn;
expr_ref m_rel; // relation.
expr_ref_vector m_bound_vars;
unsigned size() const { return get_signature().size(); }
ast_manager& get_manager() const { return get_plugin().get_ast_manager(); }
smt_relation(smt_relation_plugin & p, const relation_signature & s, expr* r);
virtual ~smt_relation();
void instantiate(expr* e, expr_ref& result) const;
void mk_abstract(expr* e, expr_ref& result) const;
bool contains(expr* facts);
bool is_finite_domain() const;
bool is_well_formed() const;
void display_finite(std::ostream & out) const;
void simplify(expr_ref& e) const;
public:
virtual bool empty() const;
virtual void add_fact(const relation_fact & f);
virtual bool contains_fact(const relation_fact & f) const;
virtual smt_relation * clone() const;
virtual smt_relation * complement(func_decl*) const;
virtual void display(std::ostream & out) const;
virtual void to_formula(expr_ref& fml) const { fml = get_relation(); simplify(fml); }
expr* get_relation() const;
void set_relation(expr* r);
void add_relation(expr* s); // add s to relation.
void filter_relation(expr* s); // restrict relation with s
smt_relation_plugin& get_plugin() const;
};
};
#endif

1
src/muz_qe/dl_util.h
View file

@ -26,6 +26,7 @@ Revision History:
#include"horn_subsume_model_converter.h"
#include"replace_proof_converter.h"
#include"substitution.h"
#include"fixedpoint_params.hpp"
namespace datalog {

62
src/muz_qe/fixedpoint_params.pyg Normal file
View file

@ -0,0 +1,62 @@
def_module_params('fixedpoint',
description='fixedpoint parameters',
export=True,
params=(('timeout', UINT, UINT_MAX, 'set timeout'),
('engine', SYMBOL, 'auto-config', 'Select: auto-config, datalog, pdr, bmc'),
('default_table', SYMBOL, 'sparse', 'default table implementation: sparse, hashtable, bitvector, interval'),
('default_relation', SYMBOL, 'pentagon', 'default relation implementation: external_relation, pentagon'),
('generate_explanations', BOOL, False, '(DATALOG) produce explanations for produced facts when using the datalog engine'),
('use_map_names', BOOL, True, "(DATALOG) use names from map files when displaying tuples"),
('bit_blast', BOOL, False, '(PDR) bit-blast bit-vectors'),
('explanations_on_relation_level', BOOL, False, '(DATALOG) if true, explanations are generated as history of each relation, rather than per fact (generate_explanations must be set to true for this option to have any effect)'),
('magic_sets_for_queries', BOOL, False, "(DATALOG) magic set transformation will be used for queries"),
('unbound_compressor', BOOL, True, "auxiliary relations will be introduced to avoid unbound variables in rule heads"),
('similarity_compressor', BOOL, True, "(DATALOG) rules that differ only in values of constants will be merged into a single rule"),
('similarity_compressor_threshold', UINT, 11, "(DATALOG) if similarity_compressor is on, this value determines how many similar rules there must be in order for them to be merged"),
('all_or_nothing_deltas', BOOL, False, "(DATALOG) compile rules so that it is enough for the delta relation in union and widening operations to determine only whether the updated relation was modified or not"),
('compile_with_widening', BOOL, False, "(DATALOG) widening will be used to compile recursive rules"),
('eager_emptiness_checking', BOOL, True, "(DATALOG) emptiness of affected relations will be checked after each instruction, so that we may ommit unnecessary instructions"),
('default_table_checked', BOOL, False, "if true, the detault table will be default_table inside a wrapper that checks that its results are the same as of default_table_checker table"),
('default_table_checker', SYMBOL, 'null', "see default_table_checked"),
('initial_restart_timeout', UINT, 0, "length of saturation run before the first restart (in ms), zero means no restarts"),
('output_profile', BOOL, False, "determines whether profile informations should be output when outputting Datalog rules or instructions"),
('inline_linear', BOOL, True, "try linear inlining method"),
('inline_eager', BOOL, True, "try eager inlining of rules"),
('inline_linear_branch', BOOL, False, "try linear inlining method with potential expansion"),
('fix_unbound_vars', BOOL, False, "fix unbound variables in tail"),
('output_tuples', BOOL, True, "determines whether tuples for output predicates should be output"),
('print_with_fixedpoint_extensions', BOOL, True, "use SMT-LIB2 fixedpoint extensions, instead of pure SMT2, when printing rules"),
('print_low_level_smt2', BOOL, False, "use (faster) low-level SMT2 printer (the printer is scalable but the result may not be as readable)"),
('print_with_variable_declarations', BOOL, True, "use variable declarations when displaying rules (instead of attempting to use original names)"),
('bfs_model_search', BOOL, True, "PDR: use BFS strategy for expanding model search"),
('use_farkas', BOOL, True, "PDR: use lemma generator based on Farkas (for linear real arithmetic)"),
('generate_proof_trace', BOOL, False, "PDR: trace for 'sat' answer as proof object"),
('flexible_trace', BOOL, False, "PDR: allow PDR generate long counter-examples "
"by extending candidate trace within search area"),
('unfold_rules', UINT, 0, "PDR: unfold rules statically using iterative squarring"),
('use_model_generalizer', BOOL, False, "PDR: use model for backwards propagation (instead of symbolic simulation)"),
('validate_result', BOOL, False, "PDR validate result (by proof checking or model checking)"),
('simplify_formulas_pre', BOOL, False, "PDR: simplify derived formulas before inductive propagation"),
('simplify_formulas_post', BOOL, False, "PDR: simplify derived formulas after inductive propagation"),
('slice', BOOL, True, "PDR: simplify clause set using slicing"),
('coalesce_rules', BOOL, False, "BMC: coalesce rules"),
('use_multicore_generalizer', BOOL, False, "PDR: extract multiple cores for blocking states"),
('use_inductive_generalizer', BOOL, True, "PDR: generalize lemmas using induction strengthening"),
('cache_mode', UINT, 0, "PDR: use no (0), symbolic (1) or explicit cache (2) for model search"),
('inductive_reachability_check', BOOL, False, "PDR: assume negation of the cube on the previous level when "
"checking for reachability (not only during cube weakening)"),
('max_num_contexts', UINT, 500, "PDR: maximal number of contexts to create"),
('try_minimize_core', BOOL, False, "PDR: try to reduce core size (before inductive minimization)"),
('profile_timeout_milliseconds', UINT, 0, "instructions and rules that took less than the threshold will not be printed when printed the instruction/rule list"),
('dbg_fpr_nonempty_relation_signature', BOOL, False,
"if true, finite_product_relation will attempt to avoid creating inner relation with empty signature "
"by putting in half of the table columns, if it would have been empty otherwise"),
('print_answer', BOOL, False, 'print answer instance(s) to query'),
('print_certificate', BOOL, False, 'print certificate for reacahbility or non-reachability'),
('print_statistics', BOOL, False, 'print statistics'),
))

4
src/muz_qe/horn_tactic.cpp
View file

@ -168,8 +168,8 @@ class horn_tactic : public tactic {
bool produce_proofs = g->proofs_enabled();
if (produce_proofs) {
if (!m_ctx.get_params().get_bool("generate_proof_trace", true)) {
params_ref params = m_ctx.get_params();
if (!m_ctx.get_params().generate_proof_trace()) {
params_ref params = m_ctx.get_params().p;
params.set_bool("generate_proof_trace", true);
updt_params(params);
}

55
src/muz_qe/pdr_context.cpp
View file

@ -1123,17 +1123,17 @@ namespace pdr {
context::context(
smt_params& fparams,
params_ref const& params,
fixedpoint_params const& params,
ast_manager& m
)
: m_fparams(fparams),
m_params(params),
m(m),
m_context(0),
m_pm(m_fparams, m_params, m),
m_pm(m_fparams, params, m),
m_query_pred(m),
m_query(0),
m_search(m_params.get_bool("bfs_model_search", true)),
m_search(m_params.bfs_model_search()),
m_last_result(l_undef),
m_inductive_lvl(0),
m_cancel(false)
@ -1358,7 +1358,7 @@ namespace pdr {
};
void context::validate() {
if (!m_params.get_bool("validate_result", false)) {
if (!m_params.validate_result()) {
return;
}
switch(m_last_result) {
@ -1387,7 +1387,7 @@ namespace pdr {
break;
}
case l_false: {
expr_ref_vector refs(m), fmls(m);
expr_ref_vector refs(m);
expr_ref tmp(m);
model_ref model;
vector<relation_info> rs;
@ -1402,6 +1402,7 @@ namespace pdr {
for (unsigned i = 0; i < rules.size(); ++i) {
datalog::rule& r = *rules[i];
model->eval(r.get_head(), tmp);
expr_ref_vector fmls(m);
fmls.push_back(m.mk_not(tmp));
unsigned utsz = r.get_uninterpreted_tail_size();
unsigned tsz = r.get_tail_size();
@ -1449,34 +1450,26 @@ namespace pdr {
void context::init_core_generalizers(datalog::rule_set& rules) {
reset_core_generalizers();
classifier_proc classify(m, rules);
bool use_mc = m_params.get_bool("use_multicore_generalizer", false);
bool use_mc = m_params.use_multicore_generalizer();
if (use_mc) {
m_core_generalizers.push_back(alloc(core_multi_generalizer, *this, 0));
}
if (m_params.get_bool("use_farkas", true) && !classify.is_bool()) {
if (m_params.get_bool("inline_proof_mode", true)) {
m.toggle_proof_mode(PGM_FINE);
m_fparams.m_proof_mode = PGM_FINE;
m_fparams.m_arith_bound_prop = BP_NONE;
m_fparams.m_arith_auto_config_simplex = true;
m_fparams.m_arith_propagate_eqs = false;
m_fparams.m_arith_eager_eq_axioms = false;
if (classify.is_dl()) {
m_fparams.m_arith_mode = AS_DIFF_LOGIC;
m_fparams.m_arith_expand_eqs = true;
}
}
else {
m_core_generalizers.push_back(alloc(core_farkas_generalizer, *this, m, m_fparams));
if (m_params.use_farkas() && !classify.is_bool()) {
m.toggle_proof_mode(PGM_FINE);
m_fparams.m_proof_mode = PGM_FINE;
m_fparams.m_arith_bound_prop = BP_NONE;
m_fparams.m_arith_auto_config_simplex = true;
m_fparams.m_arith_propagate_eqs = false;
m_fparams.m_arith_eager_eq_axioms = false;
if (classify.is_dl()) {
m_fparams.m_arith_mode = AS_DIFF_LOGIC;
m_fparams.m_arith_expand_eqs = true;
}
}
if (!use_mc && m_params.get_bool("use_inductive_generalizer", true)) {
if (!use_mc && m_params.use_inductive_generalizer()) {
m_core_generalizers.push_back(alloc(core_bool_inductive_generalizer, *this, 0));
}
if (m_params.get_bool("use_interpolants", false)) {
m_core_generalizers.push_back(alloc(core_interpolant_generalizer, *this));
}
if (m_params.get_bool("inductive_reachability_check", false)) {
if (m_params.inductive_reachability_check()) {
m_core_generalizers.push_back(alloc(core_induction_generalizer, *this));
}
}
@ -1588,7 +1581,7 @@ namespace pdr {
\brief Retrieve satisfying assignment with explanation.
*/
expr_ref context::mk_sat_answer() const {
if (m_params.get_bool("generate_proof_trace", false)) {
if (m_params.generate_proof_trace()) {
proof_ref pr = get_proof();
return expr_ref(pr.get(), m);
}
@ -1709,7 +1702,7 @@ namespace pdr {
n.pt().add_property(ncore, uses_level?n.level():infty_level);
}
CASSERT("pdr",n.level() == 0 || check_invariant(n.level()-1));
m_search.backtrack_level(!found_invariant && m_params.get_bool("flexible_trace", false), n);
m_search.backtrack_level(!found_invariant && m_params.flexible_trace(), n);
break;
}
case l_undef: {
@ -1731,7 +1724,7 @@ namespace pdr {
}
void context::propagate(unsigned max_prop_lvl) {
if (m_params.get_bool("simplify_formulas_pre", false)) {
if (m_params.simplify_formulas_pre()) {
simplify_formulas();
}
for (unsigned lvl = 0; lvl <= max_prop_lvl; lvl++) {
@ -1750,7 +1743,7 @@ namespace pdr {
throw inductive_exception();
}
}
if (m_params.get_bool("simplify_formulas_post", false)) {
if (m_params.simplify_formulas_post()) {
simplify_formulas();
}
}
@ -1798,7 +1791,7 @@ namespace pdr {
*/
void context::create_children(model_node& n) {
SASSERT(n.level() > 0);
bool use_model_generalizer = m_params.get_bool("use_model_generalizer", false);
bool use_model_generalizer = m_params.use_model_generalizer();
datalog::scoped_no_proof _sc(m);
pred_transformer& pt = n.pt();

7
src/muz_qe/pdr_context.h
View file

@ -30,6 +30,7 @@ Revision History:
#include "pdr_prop_solver.h"
#include "pdr_reachable_cache.h"
namespace datalog {
class rule_set;
class context;
@ -291,7 +292,7 @@ namespace pdr {
};
smt_params& m_fparams;
params_ref const& m_params;
fixedpoint_params const& m_params;
ast_manager& m;
datalog::context* m_context;
manager m_pm;
@ -349,13 +350,13 @@ namespace pdr {
*/
context(
smt_params& fparams,
params_ref const& params,
fixedpoint_params const& params,
ast_manager& m);
~context();
smt_params& get_fparams() const { return m_fparams; }
params_ref const& get_params() const { return m_params; }
fixedpoint_params const& get_params() const { return m_params; }
ast_manager& get_manager() const { return m; }
manager& get_pdr_manager() { return m_pm; }
decl2rel const& get_pred_transformers() const { return m_rels; }

42
src/muz_qe/pdr_dl_interface.cpp
View file

@ -83,7 +83,6 @@ lbool dl_interface::query(expr * query) {
m_pdr_rules.reset();
m_refs.reset();
m_pred2slice.reset();
m_ctx.get_rmanager().reset_relations();
ast_manager& m = m_ctx.get_manager();
datalog::rule_manager& rule_manager = m_ctx.get_rule_manager();
datalog::rule_set old_rules(m_ctx.get_rules());
@ -108,13 +107,13 @@ lbool dl_interface::query(expr * query) {
model_converter_ref mc = datalog::mk_skip_model_converter();
proof_converter_ref pc;
if (m_ctx.get_params().get_bool("generate_proof_trace", false)) {
if (m_ctx.get_params().generate_proof_trace()) {
pc = datalog::mk_skip_proof_converter();
}
m_ctx.set_output_predicate(query_pred);
m_ctx.apply_default_transformation(mc, pc);
if (m_ctx.get_params().get_bool("slice", true)) {
if (m_ctx.get_params().slice()) {
datalog::rule_transformer transformer(m_ctx);
datalog::mk_slice* slice = alloc(datalog::mk_slice, m_ctx);
transformer.register_plugin(slice);
@ -133,10 +132,10 @@ lbool dl_interface::query(expr * query) {
}
}
if (m_ctx.get_params().get_uint("unfold_rules",0) > 0) {
unsigned num_unfolds = m_ctx.get_params().get_uint("unfold_rules", 0);
if (m_ctx.get_params().unfold_rules() > 0) {
unsigned num_unfolds = m_ctx.get_params().unfold_rules();
datalog::rule_transformer transformer1(m_ctx), transformer2(m_ctx);
if (m_ctx.get_params().get_uint("coalesce_rules", false)) {
if (m_ctx.get_params().coalesce_rules()) {
transformer1.register_plugin(alloc(datalog::mk_coalesce, m_ctx));
m_ctx.transform_rules(transformer1, mc, pc);
}
@ -198,7 +197,7 @@ expr_ref dl_interface::get_cover_delta(int level, func_decl* pred_orig) {
}
void dl_interface::add_cover(int level, func_decl* pred, expr* property) {
if (m_ctx.get_params().get_bool("slice", true)) {
if (m_ctx.get_params().slice()) {
throw default_exception("Covers are incompatible with slicing. Disable slicing before using covers");
}
m_context->add_cover(level, pred, property);
@ -246,32 +245,3 @@ model_ref dl_interface::get_model() {
proof_ref dl_interface::get_proof() {
return m_context->get_proof();
}
void dl_interface::collect_params(param_descrs& p) {
p.insert("bfs_model_search", CPK_BOOL, "PDR: (default true) use BFS strategy for expanding model search");
p.insert("use_farkas", CPK_BOOL, "PDR: (default true) use lemma generator based on Farkas (for linear real arithmetic)");
p.insert("generate_proof_trace", CPK_BOOL, "PDR: (default false) trace for 'sat' answer as proof object");
p.insert("inline_proofs", CPK_BOOL, "PDR: (default true) run PDR with proof mode turned on and extract "
"Farkas coefficients directly (instead of creating a separate proof object when extracting coefficients)");
p.insert("flexible_trace", CPK_BOOL, "PDR: (default false) allow PDR generate long counter-examples "
"by extending candidate trace within search area");
p.insert("unfold_rules", CPK_UINT, "PDR: (default 0) unfold rules statically using iterative squarring");
p.insert("use_model_generalizer", CPK_BOOL, "PDR: (default false) use model for backwards propagation (instead of symbolic simulation)");
p.insert("validate_result", CPK_BOOL, "PDR (default false) validate result (by proof checking or model checking)");
#ifndef _EXTERNAL_RELEASE
p.insert("use_multicore_generalizer", CPK_BOOL, "PDR: (default false) extract multiple cores for blocking states");
p.insert("use_inductive_generalizer", CPK_BOOL, "PDR: (default true) generalize lemmas using induction strengthening");
p.insert("use_interpolants", CPK_BOOL, "PDR: (default false) use iZ3 interpolation for lemma generation");
p.insert("dump_interpolants", CPK_BOOL, "PDR: (default false) display interpolants");
p.insert("cache_mode", CPK_UINT, "PDR: use no (0 - default) symbolic (1) or explicit cache (2) for model search");
p.insert("inductive_reachability_check", CPK_BOOL,
"PDR: (default false) assume negation of the cube on the previous level when "
"checking for reachability (not only during cube weakening)");
p.insert("max_num_contexts", CPK_UINT, "PDR: (default 500) maximal number of contexts to create");
p.insert("try_minimize_core", CPK_BOOL, "PDR: (default false) try to reduce core size (before inductive minimization)");
#endif
p.insert("simplify_formulas_pre", CPK_BOOL, "PDR: (default false) simplify derived formulas before inductive propagation");
p.insert("simplify_formulas_post", CPK_BOOL, "PDR: (default false) simplify derived formulas after inductive propagation");
p.insert("slice", CPK_BOOL, "PDR: (default true) simplify clause set using slicing");
p.insert("coalesce_rules", CPK_BOOL, "BMC: (default false) coalesce rules");
}

2
src/muz_qe/pdr_dl_interface.h
View file

@ -66,8 +66,6 @@ namespace pdr {
expr_ref get_cover_delta(int level, func_decl* pred);
void add_cover(int level, func_decl* pred, expr* property);
static void collect_params(param_descrs& p);
void updt_params();

1
src/muz_qe/pdr_farkas_learner.cpp
View file

@ -29,7 +29,6 @@ Revision History:
#include "pdr_util.h"
#include "pdr_farkas_learner.h"
#include "th_rewriter.h"
#include "pdr_interpolant_provider.h"
#include "ast_ll_pp.h"
#include "arith_bounds_tactic.h"
#include "proof_utils.h"

74
src/muz_qe/pdr_generalizers.cpp
View file

@ -20,7 +20,6 @@ Revision History:
#include "pdr_context.h"
#include "pdr_farkas_learner.h"
#include "pdr_interpolant_provider.h"
#include "pdr_generalizers.h"
#include "expr_abstract.h"
#include "var_subst.h"
@ -143,77 +142,6 @@ namespace pdr {
}
/**
< F, phi, i + 1 >
/ \
< G, psi, i > < H, theta, i >
core
Given:
1. psi => core
2. Gi => not core
3. phi & psi & theta => F_{i+1}
Then, by weakening 2:
Gi => (F_{i+1} => not (phi & core & theta))
Find interpolant I, such that
Gi => I, I => (F_{i+1} => not (phi & core' & theta'))
where core => core', theta => theta'
This implementation checks if
Gi => (F_{i+1} => not (phi & theta))
*/
void core_interpolant_generalizer::operator()(model_node& n, expr_ref_vector& core, bool& uses_level) {
if (!n.parent()) {
return;
}
manager& pm = n.pt().get_pdr_manager();
ast_manager& m = n.pt().get_manager();
model_node& p = *n.parent();
// find index of node into parent.
unsigned index = 0;
for (; index < p.children().size() && (&n != p.children()[index]); ++index);
SASSERT(index < p.children().size());
expr_ref G(m), F(m), r(m), B(m), I(m), cube(m);
expr_ref_vector fmls(m);
F = p.pt().get_formulas(p.level(), true);
G = n.pt().get_formulas(n.level(), true);
pm.formula_n2o(index, false, G);
// get formulas from siblings.
for (unsigned i = 0; i < p.children().size(); ++i) {
if (i != index) {
pm.formula_n2o(p.children()[i]->state(), r, i, true);
fmls.push_back(r);
}
}
fmls.push_back(F);
fmls.push_back(p.state());
B = pm.mk_and(fmls);
// when G & B is unsat, find I such that G => I, I => not B
lbool res = pm.get_interpolator().get_interpolant(G, B, I);
TRACE("pdr",
tout << "Interpolating:\n" << mk_pp(G, m) << "\n" << mk_pp(B, m) << "\n";
if (res == l_true) tout << mk_pp(I, m) << "\n"; else tout << "failed\n";);
if(res == l_true) {
pm.formula_o2n(I, cube, index, true);
TRACE("pdr", tout << "After renaming: " << mk_pp(cube, m) << "\n";);
core.reset();
datalog::flatten_and(cube, core);
uses_level = true;
}
}
//
@ -463,7 +391,7 @@ namespace pdr {
imp imp(m_ctx);
ast_manager& m = core.get_manager();
expr_ref goal = imp.mk_induction_goal(p->pt(), p->level(), depth);
smt::kernel ctx(m, m_ctx.get_fparams(), m_ctx.get_params());
smt::kernel ctx(m, m_ctx.get_fparams(), m_ctx.get_params().p);
ctx.assert_expr(goal);
lbool r = ctx.check();
TRACE("pdr", tout << r << "\n";

7
src/muz_qe/pdr_generalizers.h
View file

@ -51,13 +51,6 @@ namespace pdr {
virtual void operator()(model_node& n, expr_ref_vector const& core, bool uses_level, cores& new_cores);
};
class core_interpolant_generalizer : public core_generalizer {
public:
core_interpolant_generalizer(context& ctx): core_generalizer(ctx) {}
virtual ~core_interpolant_generalizer() {}
virtual void operator()(model_node& n, expr_ref_vector& core, bool& uses_level);
};
class core_induction_generalizer : public core_generalizer {
class imp;
public:

381
src/muz_qe/pdr_interpolant_provider.cpp
View file

@ -1,381 +0,0 @@
/*++
Copyright (c) 2011 Microsoft Corporation
Module Name:
pdr_interpolant_provider.cpp
Abstract:
Interface for obtaining interpolants.
This file is Windows specific.
Author:
Krystof Hoder (t-khoder) 2011-10-19.
Revision History:
--*/
//disables the warning on deprecation of fgets function -- didn't really find by what it should be replaced
#ifdef _WINDOWS
#pragma warning(disable: 4995)
#endif
#include <sstream>
#include "ast_smt_pp.h"
#include "cmd_context.h"
#include "for_each_expr.h"
#include "obj_hashtable.h"
#include "smt2parser.h"
#include "rewriter.h"
#include "rewriter_def.h"
#include "pdr_util.h"
#include "pdr_interpolant_provider.h"
#include "expr_context_simplifier.h"
#ifdef _WINDOWS
#include <windows.h>
#include <cstdio>
#include <strsafe.h>
#include <process.h>
/**
Requirements for the use of this object:
The directory where the expcutable is must contain also executable
PdrInterpolator.exe.
This executable takes one argument with a file name that contains
two SMTLIB problem instances, each terminated by string "\n##next##\n".
The output of the executable is given to the standard output and
is also terminated by the "\n##next##\n" string.
If formulas in the two input problems are unsatisfiable, they problem
is printed at the output in the format
(assert FORM)
If the formulas are satisfiable, "0" is output and if the result cannot
be determined, the output is "?". (Both are still followed by "\n##next##\n").
*/
class interpolant_provider_impl : public interpolant_provider
{
static std::string s_terminator_str;
static std::string s_satisfiable_str;
static std::string s_unknown_str;
std::string m_exec_name;
params_ref const & m_params;
/**
If non-empty, contains name of a temporary file that is used for passing the
interpolation problem to the interpolating engine.
*/
std::string m_tmp_file_name;
simplifier m_simpl;
PROCESS_INFORMATION m_pi;
STARTUPINFOA m_si;
HANDLE m_in_rd;
HANDLE m_out_rd;
HANDLE m_in_wr;
HANDLE m_out_wr;
class used_symbol_inserter {
typedef obj_hashtable<func_decl> func_decl_set;
typedef obj_hashtable<sort> sort_set;
ast_manager& m;
cmd_context& m_cctx;
func_decl_set m_funcs;
sort_set m_sorts;
void handle_sort(sort * s) {
if(s->get_family_id()!=null_family_id || m_sorts.contains(s)) {
return;
}
m_sorts.insert(s);
NOT_IMPLEMENTED_YET();
//we should insert it into the context somehow, but now not sure how and
//we don't deal with user defined sorts (yet)...
//m_cctx.insert(s);
}
void handle_func_decl(func_decl * fn) {
if(fn->get_family_id()!=null_family_id || m_funcs.contains(fn)) {
return;
}
m_funcs.insert(fn);
m_cctx.insert(fn);
}
public:
used_symbol_inserter(cmd_context& cctx) : m(cctx.m()), m_cctx(cctx) {}
void operator()(var * n) {
handle_sort(n->get_sort());
}
void operator()(app * n) {
if (is_uninterp(n)) {
handle_func_decl(n->get_decl());
}
handle_sort(n->get_decl()->get_range());
}
void operator()(quantifier * n) {
unsigned sz = n->get_num_decls();
for(unsigned i=0; i<sz; ++i) {
handle_sort(n->get_decl_sort(i));
}
}
};
class form_fixer_cfg : public default_rewriter_cfg
{
ast_manager& m;
public:
form_fixer_cfg(ast_manager& m) : m(m) {}
br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result,
proof_ref & result_pr)
{
if(m.is_or(f) && num==0) {
result = m.mk_false();
return BR_DONE;
}
return BR_FAILED;
}
};
std::string get_tmp_file_name();
std::string execute_interpolator(std::string input);
void simplify_expr(expr* f, expr_ref& result);
void output_interpolant_problem(std::ostream& out, expr * f1, expr * f2);
public:
interpolant_provider_impl(ast_manager& m, params_ref const& params, std::string exec_name)
: interpolant_provider(m),
m_params(params),
m_exec_name(exec_name),
m_simpl(m) {
memset(&m_si, 0, sizeof(m_si));
memset(&m_pi, 0, sizeof(m_pi));
}
~interpolant_provider_impl();
/**
If (f1 /\ f2) is unsatisfiable, return true and into res assign a formula
I such that f1 --> I, I --> ~f2, and the language if I is in the intersection
of languages of f1 and f2.
If (f1 /\ f2) is satisfiable, return false.
*/
virtual lbool get_interpolant(expr * f1, expr * f2, expr_ref& res);
};
std::string interpolant_provider_impl::s_terminator_str = ";##next##";
std::string interpolant_provider_impl::s_satisfiable_str = ";#sat#";
std::string interpolant_provider_impl::s_unknown_str = ";#unknown#";
interpolant_provider_impl::~interpolant_provider_impl() {
if(m_tmp_file_name.size()!=0) {
DeleteFileA(m_tmp_file_name.c_str());
}
CloseHandle(m_pi.hProcess);
CloseHandle(m_pi.hThread);
CloseHandle(m_in_rd);
CloseHandle(m_in_wr);
CloseHandle(m_out_rd);
CloseHandle(m_out_wr);
}
void interpolant_provider_impl::simplify_expr(expr* f, expr_ref& result) {
expr_ref rwr_f(m);
form_fixer_cfg fixer(m);
rewriter_tpl<form_fixer_cfg> rwr(m, false, fixer);
rwr(f, rwr_f);
proof_ref pr(m);
m_simpl(rwr_f, result, pr);
}
std::string interpolant_provider_impl::get_tmp_file_name() {
//return "c:\\test.txt";
if(m_tmp_file_name.length()!=0) {
return m_tmp_file_name;
}
char path[MAX_PATH];
if(GetTempPathA(256, path)==0) {
throw default_exception("cannot get temp directory");
}
std::stringstream name_prefix_builder;
name_prefix_builder<<"pdr"<<GetCurrentProcessId();
char file[MAX_PATH];
if(GetTempFileNameA(path, name_prefix_builder.str().c_str(), 1, file)==0) {
throw default_exception("cannot get temp file");
}
m_tmp_file_name = file;
return m_tmp_file_name;
}
void interpolant_provider_impl::output_interpolant_problem(std::ostream& out, expr * f1, expr * f2) {
expr_ref t1(m), t2(m);
simplify_expr(f1, t1);
simplify_expr(f2, t2);
ast_smt_pp pp(m);
pp.add_assumption(t1);
pp.display(out, t2);
out << "\n" << s_terminator_str << "\n";
}
std::string interpolant_provider_impl::execute_interpolator(std::string input)
{
if (!m_pi.hProcess) {
SECURITY_ATTRIBUTES sa;
sa.nLength = sizeof(SECURITY_ATTRIBUTES);
sa.bInheritHandle = TRUE;
sa.lpSecurityDescriptor = NULL;
if (!CreatePipe(&m_out_rd, &m_out_wr, &sa, 0)) {
throw default_exception("Could not create pipe");
}
if (!CreatePipe(&m_in_rd, &m_in_wr, &sa, 0)) {
throw default_exception("Could not create pipe");
}
m_si.cb = sizeof(m_si);
m_si.hStdError = 0;
m_si.hStdOutput = m_out_wr;
m_si.hStdInput = m_in_rd;
m_si.dwFlags |= STARTF_USESTDHANDLES;
if(!CreateProcessA(
NULL,
(LPSTR)m_exec_name.c_str(), // command line
NULL, // process security attributes
NULL, // primary thread security attributes
TRUE, // handles are inherited
0, // creation flags
NULL, // use parent's environment
NULL, // use parent's current directory
&m_si, // STARTUPINFO pointer
&m_pi)) { // receives PROCESS_INFORMATION
throw default_exception("Could not create process");
}
}
DWORD wr = 0, rd = 0;
if (!WriteFile(m_in_wr, input.c_str(), static_cast<unsigned>(input.size()), &wr, 0)) {
throw default_exception("Cold not write to pipe");
}
std::string result;
char line[256];
while (true) {
memset(line, 0, sizeof(line));
if (!ReadFile(m_out_rd, line, sizeof(line)-1, &rd, 0)) {
throw default_exception("Cold not write to pipe");
}
result += line;
if (strstr(result.c_str(), s_terminator_str.c_str())) {
return result;
}
}
}
lbool interpolant_provider_impl::get_interpolant(expr * f1, expr * f2, expr_ref& res) {
std::ostringstream prb;
output_interpolant_problem(prb, f1, f2);
std::string res_text = execute_interpolator(prb.str());
if(strstr(res_text.c_str(), s_satisfiable_str.c_str())) {
return l_false;
}
if(strstr(res_text.c_str(), s_unknown_str.c_str())) {
return l_undef;
}
cmd_context cctx(false, &m);
for_each_expr(used_symbol_inserter(cctx), f1);
parse_smt2_commands(cctx, std::istringstream(res_text), false);
ptr_vector<expr>::const_iterator ait = cctx.begin_assertions();
ptr_vector<expr>::const_iterator aend = cctx.end_assertions();
if(ait+1!=aend) {
throw default_exception("invalid interpolator output");
}
res = *ait;
if (m_params.get_bool("dump_interpolants", false)) {
interpolant_provider::output_interpolant(m, f1, f2, res);
}
return l_true;
}
interpolant_provider * interpolant_provider::mk(ast_manager& m, params_ref const& p)
{
char self_name[MAX_PATH];
GetModuleFileNameA(NULL, self_name, MAX_PATH);
char * last_backslash = strrchr(self_name,'\\');
if(last_backslash==NULL) {
throw default_exception("GetModuleFileNameA did not return full path to the executable");
}
//we cut the string at the last backslash
*last_backslash = 0;
std::string exec_name = self_name + std::string(".\\PdrInterpolator.exe");
return alloc(interpolant_provider_impl, m, p, exec_name);
}
#else
interpolant_provider *
interpolant_provider::mk(ast_manager& m, params_ref const& p) {
// interpolations are windows specific and private.
return 0;
}
#endif
void interpolant_provider::output_interpolant(ast_manager& m, expr* A, expr* B, expr* I) {
static unsigned file_num = 0;
std::ostringstream filename;
filename << "interpolation_" << file_num++ << ".smt";
std::ofstream out(filename.str().c_str());
ast_smt_pp pp(m);
pp.add_assumption(A);
pp.display(out, B);
std::ostringstream strm;
strm << ";" << mk_pp(I, m) << "\n";
buffer<char> buff;
std::string s = strm.str();
char const* i_str = s.c_str();
while (*i_str) {
buff.push_back(*i_str);
if (*i_str == '\n') {
buff.push_back(';');
}
++i_str;
}
buff.push_back(0);
out << buff.c_ptr();
out << "##next##\n";
out.close();
}

54
src/muz_qe/pdr_interpolant_provider.h
View file

@ -1,54 +0,0 @@
/*++
Copyright (c) 2011 Microsoft Corporation
Module Name:
interpolant_provider.h
Abstract:
Interface for obtaining interpolants.
Author:
Krystof Hoder (t-khoder) 2011-10-19.
Revision History:
--*/
#include "ast.h"
#include "lbool.h"
#include "model.h"
#include "params.h"
#ifndef _PDR_INTERPOLANT_PROVIDER_H_
#define _PDR_INTERPOLANT_PROVIDER_H_
class interpolant_provider
{
protected:
ast_manager & m;
interpolant_provider(ast_manager& m) : m(m) {}
public:
virtual ~interpolant_provider() {}
/**
If (f1 /\ f2) is unsatisfiable, return true and into res assign a formula
I such that f1 --> I, I --> ~f2, and the language if I is in the intersection
of languages of f1 and f2.
If (f1 /\ f2) is satisfiable, return false.
*/
virtual lbool get_interpolant(expr * f1, expr * f2, expr_ref& res) = 0;
static interpolant_provider * mk(ast_manager& m, params_ref const& p);
static void output_interpolant(ast_manager& m, expr* A, expr* B, expr* I);
};
#endif

15
src/muz_qe/pdr_manager.cpp
View file

@ -166,7 +166,7 @@ namespace pdr {
return res;
}
manager::manager(smt_params& fparams, params_ref const& params, ast_manager& manager) :
manager::manager(smt_params& fparams, fixedpoint_params const& params, ast_manager& manager) :
m(manager),
m_fparams(fparams),
m_params(params),
@ -311,17 +311,8 @@ namespace pdr {
else {
return false;
}
}
interpolant_provider& manager::get_interpolator() {
if(!m_interpolator) {
m_interpolator = interpolant_provider::mk(m, get_params());
}
return *m_interpolator;
}
}
bool manager::implication_surely_holds(expr * lhs, expr * rhs, expr * bg) {
smt::kernel sctx(m, get_fparams());
if(bg) {

18
src/muz_qe/pdr_manager.h
View file

@ -32,7 +32,6 @@ Revision History:
#include "pdr_util.h"
#include "pdr_sym_mux.h"
#include "pdr_farkas_learner.h"
#include "pdr_interpolant_provider.h"
#include "pdr_smt_context_manager.h"
#include "dl_rule.h"
@ -79,7 +78,7 @@ namespace pdr {
{
ast_manager& m;
smt_params& m_fparams;
params_ref const& m_params;
fixedpoint_params const& m_params;
mutable bool_rewriter m_brwr;
@ -91,16 +90,6 @@ namespace pdr {
/** whenever we need an unique number, we get this one and increase */
unsigned m_next_unique_num;
/**
It would make more sense to have interpolantor inside the prop_solver,
however we have one prop_solver instance in each relation.
Each instance of interpolant_provider creates a temporary file and
interpolant_provider can be shared, so it makes more sence to have
it in pdr_manager which is created only once.
*/
scoped_ptr<interpolant_provider> m_interpolator;
static vector<std::string> get_state_suffixes();
@ -110,12 +99,12 @@ namespace pdr {
void add_new_state(func_decl * s);
public:
manager(smt_params& fparams, params_ref const& params,
manager(smt_params& fparams, fixedpoint_params const& params,
ast_manager & manager);
ast_manager& get_manager() const { return m; }
smt_params& get_fparams() const { return m_fparams; }
params_ref const& get_params() const { return m_params; }
fixedpoint_params const& get_params() const { return m_params; }
bool_rewriter& get_brwr() const { return m_brwr; }
expr_ref mk_and(unsigned sz, expr* const* exprs);
@ -298,7 +287,6 @@ namespace pdr {
expr* get_background() const { return m_background; }
interpolant_provider& get_interpolator();
/**
Return true if we can show that lhs => rhs. The function can have false negatives

2
src/muz_qe/pdr_prop_solver.cpp
View file

@ -212,7 +212,7 @@ namespace pdr {
m(pm.get_manager()),
m_pm(pm),
m_name(name),
m_try_minimize_core(pm.get_params().get_bool("try_minimize_core", false)),
m_try_minimize_core(pm.get_params().try_minimize_core()),
m_ctx(pm.mk_fresh()),
m_pos_level_atoms(m),
m_neg_level_atoms(m),

4
src/muz_qe/pdr_reachable_cache.cpp
View file

@ -21,13 +21,13 @@ Revision History:
namespace pdr {
reachable_cache::reachable_cache(pdr::manager & pm, params_ref const& params)
reachable_cache::reachable_cache(pdr::manager & pm, fixedpoint_params const& params)
: m(pm.get_manager()),
m_pm(pm),
m_ctx(0),
m_ref_holder(m),
m_disj_connector(m),
m_cache_mode((datalog::PDR_CACHE_MODE)params.get_uint("cache_mode",0)) {
m_cache_mode((datalog::PDR_CACHE_MODE)params.cache_mode()) {
if (m_cache_mode == datalog::CONSTRAINT_CACHE) {
m_ctx = pm.mk_fresh();
m_ctx->assert_expr(m_pm.get_background());

11
src/muz_qe/pdr_reachable_cache.h
View file

@ -17,14 +17,13 @@ Revision History:
--*/
#include "ast.h"
#include "params.h"
#include "ref_vector.h"
#include "pdr_manager.h"
#include "pdr_smt_context_manager.h"
#ifndef _REACHABLE_CACHE_H_
#define _REACHABLE_CACHE_H_
#include "ast.h"
#include "ref_vector.h"
#include "pdr_manager.h"
#include "pdr_smt_context_manager.h"
namespace pdr {
class reachable_cache {
@ -48,7 +47,7 @@ namespace pdr {
void add_disjuncted_formula(expr * f);
public:
reachable_cache(pdr::manager & pm, params_ref const& params);
reachable_cache(pdr::manager & pm, fixedpoint_params const& params);
void add_init(app * f) { add_disjuncted_formula(f); }

4
src/muz_qe/pdr_smt_context_manager.cpp
View file

@ -93,10 +93,10 @@ namespace pdr {
return m_context.get_proof();
}
smt_context_manager::smt_context_manager(smt_params& fp, params_ref const& p, ast_manager& m):
smt_context_manager::smt_context_manager(smt_params& fp, fixedpoint_params const& p, ast_manager& m):
m_fparams(fp),
m(m),
m_max_num_contexts(p.get_uint("max_num_contexts", 500)),
m_max_num_contexts(p.max_num_contexts()),
m_num_contexts(0),
m_predicate_list(m) {
}

3
src/muz_qe/pdr_smt_context_manager.h
View file

@ -23,6 +23,7 @@ Revision History:
#include "smt_kernel.h"
#include "sat_solver.h"
#include "func_decl_dependencies.h"
#include "dl_util.h"
namespace pdr {
@ -96,7 +97,7 @@ namespace pdr {
app_ref_vector m_predicate_list;
func_decl_set m_predicate_set;
public:
smt_context_manager(smt_params& fp, params_ref const& p, ast_manager& m);
smt_context_manager(smt_params& fp, fixedpoint_params const& p, ast_manager& m);
~smt_context_manager();
smt_context* mk_fresh();
void collect_statistics(statistics& st) const;

50
src/muz_qe/pdr_util.cpp
View file

@ -86,48 +86,6 @@ namespace pdr {
return res.str();
}
/////////////////////////
// select elimination rewriter
//
class select_elim {
ast_manager& m;
array_util a;
model_ref m_model;
public:
select_elim(ast_manager& m, model_ref& md): m(m), a(m), m_model(md) {}
br_status mk_app_core(func_decl* f, unsigned num_args, expr* const* args, expr_ref& result) {
if (a.is_select(f)) {
expr_ref tmp(m);
tmp = m.mk_app(f, num_args, args);
m_model->eval(tmp, result);
return BR_DONE;
}
else {
return BR_FAILED;
}
}
};
struct select_elim_cfg: public default_rewriter_cfg {
select_elim m_r;
bool rewrite_patterns() const { return false; }
br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) {
return m_r.mk_app_core(f, num, args, result);
}
select_elim_cfg(ast_manager & m, model_ref& md, params_ref const & p):m_r(m, md) {}
};
class select_elim_star : public rewriter_tpl<select_elim_cfg> {
select_elim_cfg m_cfg;
public:
select_elim_star(ast_manager & m, model_ref& md, params_ref const & p = params_ref()):
rewriter_tpl<select_elim_cfg>(m, false, m_cfg),
m_cfg(m, md, p) {}
};
/////////////////////////
@ -238,13 +196,6 @@ namespace pdr {
result.push_back(m.mk_not(e));
}
}
#if 0
select_elim_star select_elim(m, m_model);
for (unsigned i = 0; i < result.size(); ++i) {
select_elim(result[i].get(), tmp);
result[i] = tmp;
}
#endif
reset();
TRACE("pdr",
tout << "minimized model:\n";
@ -1266,6 +1217,5 @@ namespace pdr {
template class rewriter_tpl<pdr::ite_hoister_cfg>;
template class rewriter_tpl<pdr::select_elim_cfg>;

517
src/muz_qe/rel_context.cpp Normal file
View file

@ -0,0 +1,517 @@
/*++
Copyright (c) 2012 Microsoft Corporation
Module Name:
rel_context.cpp
Abstract:
context for relational datalog engine.
Author:
Nikolaj Bjorner (nbjorner) 2012-12-3.
Revision History:
Extracted from dl_context
--*/
#include"rel_context.h"
#include"dl_context.h"
#include"dl_compiler.h"
#include"dl_instruction.h"
#include"dl_mk_explanations.h"
#include"dl_mk_magic_sets.h"
#include"dl_product_relation.h"
#include"dl_bound_relation.h"
#include"dl_interval_relation.h"
#include"dl_finite_product_relation.h"
#include"dl_sparse_table.h"
#include"dl_table.h"
#include"dl_table_relation.h"
#ifndef _EXTERNAL_RELEASE
#include"dl_skip_table.h"
#endif
namespace datalog {
rel_context::rel_context(context& ctx)
: m_context(ctx),
m(ctx.get_manager()),
m_rmanager(ctx),
m_answer(m),
m_cancel(false),
m_last_result_relation(0) {
get_rmanager().register_plugin(alloc(sparse_table_plugin, get_rmanager()));
get_rmanager().register_plugin(alloc(hashtable_table_plugin, get_rmanager()));
get_rmanager().register_plugin(alloc(bitvector_table_plugin, get_rmanager()));
get_rmanager().register_plugin(alloc(equivalence_table_plugin, get_rmanager()));
#ifndef _EXTERNAL_RELEASE
get_rmanager().register_plugin(alloc(skip_table_plugin, get_rmanager()));
#endif
//register plugins for builtin relations
get_rmanager().register_plugin(alloc(bound_relation_plugin, get_rmanager()));
get_rmanager().register_plugin(alloc(interval_relation_plugin, get_rmanager()));
}
rel_context::~rel_context() {
if (m_last_result_relation) {
m_last_result_relation->deallocate();
m_last_result_relation = 0;
}
}
void rel_context::collect_predicates(decl_set & res) {
unsigned rule_cnt = m_context.get_rules().get_num_rules();
for (unsigned rindex=0; rindex<rule_cnt; rindex++) {
rule * r = m_context.get_rules().get_rule(rindex);
res.insert(r->get_head()->get_decl());
unsigned tail_len = r->get_uninterpreted_tail_size();
for (unsigned tindex=0; tindex<tail_len; tindex++) {
res.insert(r->get_tail(tindex)->get_decl());
}
}
decl_set::iterator oit = m_output_preds.begin();
decl_set::iterator oend = m_output_preds.end();
for (; oit!=oend; ++oit) {
res.insert(*oit);
}
get_rmanager().collect_predicates(res);
}
lbool rel_context::saturate() {
m_context.ensure_closed();
bool time_limit = m_context.soft_timeout()!=0;
unsigned remaining_time_limit = m_context.soft_timeout();
unsigned restart_time = m_context.initial_restart_timeout();
rule_set original_rules(m_context.get_rules());
decl_set original_predicates;
m_context.collect_predicates(original_predicates);
instruction_block rules_code;
instruction_block termination_code;
execution_context ex_ctx(m_context);
lbool result;
TRACE("dl", m_context.display(tout););
while (true) {
model_converter_ref mc; // Ignored in Datalog mode
proof_converter_ref pc; // Ignored in Datalog mode
m_context.transform_rules(mc, pc);
compiler::compile(m_context, m_context.get_rules(), rules_code, termination_code);
TRACE("dl", rules_code.display(*this, tout); );
bool timeout_after_this_round = time_limit && (restart_time==0 || remaining_time_limit<=restart_time);
if (time_limit || restart_time!=0) {
unsigned timeout = time_limit ? (restart_time!=0) ?
std::min(remaining_time_limit, restart_time)
: remaining_time_limit : restart_time;
ex_ctx.set_timelimit(timeout);
}
bool early_termination = !rules_code.perform(ex_ctx);
ex_ctx.reset_timelimit();
VERIFY( termination_code.perform(ex_ctx) );
rules_code.process_all_costs();
IF_VERBOSE(10, ex_ctx.report_big_relations(1000, verbose_stream()););
if (!early_termination) {
m_context.set_status(OK);
result = l_true;
break;
}
if (memory::above_high_watermark()) {
m_context.set_status(MEMOUT);
result = l_undef;
break;
}
if (timeout_after_this_round || m_cancel) {
m_context.set_status(TIMEOUT);
result = l_undef;
break;
}
SASSERT(restart_time != 0);
if (time_limit) {
SASSERT(remaining_time_limit>restart_time);
remaining_time_limit -= restart_time;
}
uint64 new_restart_time = static_cast<uint64>(restart_time)*m_context.initial_restart_timeout();
if (new_restart_time > UINT_MAX) {
restart_time = UINT_MAX;
}
else {
restart_time = static_cast<unsigned>(new_restart_time);
}
rules_code.reset();
termination_code.reset();
ex_ctx.reset();
m_context.reopen();
restrict_predicates(original_predicates);
m_context.replace_rules(original_rules);
m_context.close();
}
m_context.reopen();
restrict_predicates(original_predicates);
m_context.replace_rules(original_rules);
m_context.close();
TRACE("dl", ex_ctx.report_big_relations(100, tout););
m_cancel = false;
return result;
}
#define BEGIN_QUERY() \
rule_set original_rules(m_context.get_rules()); \
decl_set original_preds; \
m_context.collect_predicates(original_preds); \
bool was_closed = m_context.is_closed(); \
if (was_closed) { \
m_context.reopen(); \
} \
#define END_QUERY() \
m_context.reopen(); \
m_context.replace_rules(original_rules); \
restrict_predicates(original_preds); \
\
if (was_closed) { \
m_context.close(); \
} \
lbool rel_context::query(unsigned num_rels, func_decl * const* rels) {
get_rmanager().reset_saturated_marks();
BEGIN_QUERY();
for (unsigned i = 0; i < num_rels; ++i) {
set_output_predicate(rels[i]);
}
m_context.close();
reset_negated_tables();
lbool res = saturate();
switch(res) {
case l_true: {
expr_ref_vector ans(m);
expr_ref e(m);
bool some_non_empty = num_rels == 0;
for (unsigned i = 0; i < num_rels; ++i) {
relation_base& rel = get_relation(rels[i]);
if (!rel.empty()) {
some_non_empty = true;
}
rel.to_formula(e);
ans.push_back(e);
}
SASSERT(!m_last_result_relation);
if (some_non_empty) {
m_answer = m.mk_and(ans.size(), ans.c_ptr());
}
else {
m_answer = m.mk_false();
res = l_false;
}
break;
}
case l_false:
m_answer = m.mk_false();
break;
case l_undef:
break;
}
END_QUERY();
return res;
}
lbool rel_context::query(expr* query) {
get_rmanager().reset_saturated_marks();
BEGIN_QUERY();
rule_manager& rm = m_context.get_rule_manager();
rule_ref qrule(rm);
rule_ref_vector qrules(rm);
func_decl_ref query_pred(m);
try {
rm.mk_query(query, query_pred, qrules, qrule);
}
catch(default_exception& exn) {
m_context.close();
m_context.set_status(INPUT_ERROR);
throw exn;
}
try {
m_context.add_rules(qrules);
}
catch (default_exception& exn) {
m_context.close();
m_context.set_status(INPUT_ERROR);
throw exn;
}
set_output_predicate(qrule->get_head()->get_decl());
m_context.close();
reset_negated_tables();
if (m_context.generate_explanations()) {
model_converter_ref mc; // ignored in Datalog mode
proof_converter_ref pc; // ignored in Datalog mode
rule_transformer transformer(m_context);
//expl_plugin is deallocated when transformer goes out of scope
mk_explanations * expl_plugin =
alloc(mk_explanations, m_context, m_context.explanations_on_relation_level());
transformer.register_plugin(expl_plugin);
m_context.transform_rules(transformer, mc, pc);
//we will retrieve the predicate with explanations instead of the original query predicate
query_pred = expl_plugin->get_e_decl(query_pred);
const rule_vector & query_rules = m_context.get_rules().get_predicate_rules(query_pred);
SASSERT(query_rules.size()==1);
qrule = query_rules.back();
}
if (m_context.magic_sets_for_queries()) {
model_converter_ref mc; // Ignored in Datalog mode
proof_converter_ref pc; // Ignored in Datalog mode
rule_transformer transformer(m_context);
transformer.register_plugin(alloc(mk_magic_sets, m_context, qrule.get()));
m_context.transform_rules(transformer, mc, pc);
}
lbool res = saturate();
if (res != l_undef) {
m_last_result_relation = get_relation(query_pred).clone();
if (m_last_result_relation->empty()) {
res = l_false;
m_answer = m.mk_false();
}
else {
m_last_result_relation->to_formula(m_answer);
}
}
END_QUERY();
return res;
}
void rel_context::reset_negated_tables() {
rule_set::pred_set_vector const & pred_sets = m_context.get_rules().get_strats();
bool non_empty = false;
for (unsigned i = 1; i < pred_sets.size(); ++i) {
func_decl_set::iterator it = pred_sets[i]->begin(), end = pred_sets[i]->end();
for (; it != end; ++it) {
func_decl* pred = *it;
relation_base & rel = get_relation(pred);
if (!rel.empty()) {
non_empty = true;
break;
}
}
}
if (!non_empty) {
return;
}
// collect predicates that depend on negation.
func_decl_set depends_on_negation;
for (unsigned i = 1; i < pred_sets.size(); ++i) {
bool change = true;
while (change) {
change = false;
func_decl_set::iterator it = pred_sets[i]->begin(), end = pred_sets[i]->end();
for (; it != end; ++it) {
func_decl* pred = *it;
if (depends_on_negation.contains(pred)) {
continue;
}
rule_vector const& rules = m_context.get_rules().get_predicate_rules(pred);
bool inserted = false;
for (unsigned j = 0; !inserted && j < rules.size(); ++j) {
rule* r = rules[j];
unsigned psz = r->get_positive_tail_size();
unsigned tsz = r->get_uninterpreted_tail_size();
if (psz < tsz) {
depends_on_negation.insert(pred);
change = true;
inserted = true;
}
for (unsigned k = 0; !inserted && k < tsz; ++k) {
func_decl* tail_decl = r->get_tail(k)->get_decl();
if (depends_on_negation.contains(tail_decl)) {
depends_on_negation.insert(pred);
change = true;
inserted = true;
}
}
}
}
}
}
func_decl_set::iterator it = depends_on_negation.begin(), end = depends_on_negation.end();
for (; it != end; ++it) {
func_decl* pred = *it;
relation_base & rel = get_relation(pred);
if (!rel.empty()) {
TRACE("dl", tout << "Resetting: " << mk_ismt2_pp(pred, m) << "\n";);
rel.reset();
}
}
}
void rel_context::set_output_predicate(func_decl * pred) {
if (!m_output_preds.contains(pred)) {
m_output_preds.insert(pred);
}
}
void rel_context::restrict_predicates( const decl_set & res ) {
set_intersection(m_output_preds, res);
get_rmanager().restrict_predicates(res);
}
relation_base & rel_context::get_relation(func_decl * pred) { return get_rmanager().get_relation(pred); }
relation_base * rel_context::try_get_relation(func_decl * pred) const { return get_rmanager().try_get_relation(pred); }
relation_manager & rel_context::get_rmanager() { return m_rmanager; }
const relation_manager & rel_context::get_rmanager() const { return m_rmanager; }
bool rel_context::output_profile() const { return m_context.output_profile(); }
void rel_context::set_predicate_representation(func_decl * pred, unsigned relation_name_cnt,
symbol const * relation_names) {
relation_manager & rmgr = get_rmanager();
family_id target_kind = null_family_id;
switch (relation_name_cnt) {
case 0:
return;
case 1:
target_kind = get_ordinary_relation_plugin(relation_names[0]).get_kind();
break;
default: {
svector<family_id> rel_kinds; // kinds of plugins that are not table plugins
family_id rel_kind; // the aggregate kind of non-table plugins
for (unsigned i = 0; i < relation_name_cnt; i++) {
relation_plugin & p = get_ordinary_relation_plugin(relation_names[i]);
rel_kinds.push_back(p.get_kind());
}
if (rel_kinds.size() == 1) {
rel_kind = rel_kinds[0];
}
else {
relation_signature rel_sig;
//rmgr.from_predicate(pred, rel_sig);
product_relation_plugin & prod_plugin = product_relation_plugin::get_plugin(rmgr);
rel_kind = prod_plugin.get_relation_kind(rel_sig, rel_kinds);
}
target_kind = rel_kind;
break;
}
}
SASSERT(target_kind != null_family_id);
get_rmanager().set_predicate_kind(pred, target_kind);
}
relation_plugin & rel_context::get_ordinary_relation_plugin(symbol relation_name) {
relation_plugin * plugin = get_rmanager().get_relation_plugin(relation_name);
if (!plugin) {
std::stringstream sstm;
sstm << "relation plugin " << relation_name << " does not exist";
throw default_exception(sstm.str());
}
if (plugin->is_product_relation()) {
throw default_exception("cannot request product relation directly");
}
if (plugin->is_sieve_relation()) {
throw default_exception("cannot request sieve relation directly");
}
if (plugin->is_finite_product_relation()) {
throw default_exception("cannot request finite product relation directly");
}
return *plugin;
}
bool rel_context::result_contains_fact(relation_fact const& f) {
SASSERT(m_last_result_relation);
return m_last_result_relation->contains_fact(f);
}
void rel_context::reset_tables() {
get_rmanager().reset_saturated_marks();
rule_set::decl2rules::iterator it = m_context.get_rules().begin_grouped_rules();
rule_set::decl2rules::iterator end = m_context.get_rules().end_grouped_rules();
for (; it != end; ++it) {
func_decl* p = it->m_key;
relation_base & rel = get_relation(p);
rel.reset();
}
for (unsigned i = 0; i < m_table_facts.size(); ++i) {
func_decl* pred = m_table_facts[i].first;
relation_fact const& fact = m_table_facts[i].second;
get_relation(pred).add_fact(fact);
}
}
void rel_context::add_fact(func_decl* pred, relation_fact const& fact) {
get_rmanager().reset_saturated_marks();
get_relation(pred).add_fact(fact);
m_table_facts.push_back(std::make_pair(pred, fact));
}
void rel_context::add_fact(func_decl* pred, table_fact const& fact) {
get_rmanager().reset_saturated_marks();
relation_base & rel0 = get_relation(pred);
if (rel0.from_table()) {
table_relation & rel = static_cast<table_relation &>(rel0);
rel.add_table_fact(fact);
// TODO: table facts?
}
else {
relation_fact rfact(m);
for (unsigned i = 0; i < fact.size(); ++i) {
rfact.push_back(m_context.get_decl_util().mk_numeral(fact[i], pred->get_domain()[i]));
}
add_fact(pred, rfact);
}
}
void rel_context::store_relation(func_decl * pred, relation_base * rel) {
get_rmanager().store_relation(pred, rel);
}
void rel_context::inherit_predicate_kind(func_decl* new_pred, func_decl* orig_pred) {
if (orig_pred) {
family_id target_kind = get_rmanager().get_requested_predicate_kind(orig_pred);
if (target_kind != null_family_id) {
get_rmanager().set_predicate_kind(new_pred, target_kind);
}
}
}
void rel_context::display_output_facts(std::ostream & out) const {
get_rmanager().display_output_tables(out);
}
void rel_context::display_facts(std::ostream& out) const {
get_rmanager().display(out);
}
};

116
src/muz_qe/rel_context.h Normal file
View file

@ -0,0 +1,116 @@
/*++
Copyright (c) 2012 Microsoft Corporation
Module Name:
rel_context.h
Abstract:
context for relational datalog engine.
Author:
Nikolaj Bjorner (nbjorner) 2012-12-3.
Revision History:
Extracted from dl_context
--*/
#ifndef _REL_CONTEXT_H_
#define _REL_CONTEXT_H_
#include "ast.h"
#include "dl_relation_manager.h"
#include "lbool.h"
namespace datalog {
class context;
class rel_context {
typedef vector<std::pair<func_decl*,relation_fact> > fact_vector;
context& m_context;
ast_manager& m;
relation_manager m_rmanager;
expr_ref m_answer;
volatile bool m_cancel;
relation_base * m_last_result_relation;
decl_set m_output_preds;
fact_vector m_table_facts;
void reset_negated_tables();
lbool saturate();
relation_plugin & get_ordinary_relation_plugin(symbol relation_name);
void reset_tables();
public:
rel_context(context& ctx);
~rel_context();
relation_manager & get_rmanager();
const relation_manager & get_rmanager() const;
ast_manager& get_manager() { return m; }
context& get_context() { return m_context; }
relation_base & get_relation(func_decl * pred);
relation_base * try_get_relation(func_decl * pred) const;
expr_ref get_last_answer() { return m_answer; }
bool output_profile() const;
lbool query(expr* q);
lbool query(unsigned num_rels, func_decl * const* rels);
void set_predicate_representation(func_decl * pred, unsigned relation_name_cnt,
symbol const * relation_names);
void inherit_predicate_kind(func_decl* new_pred, func_decl* orig_pred);
void cancel() { m_cancel = true; }
void cleanup() { m_cancel = false; }
/**
\brief Restrict the set of used predicates to \c res.
The function deallocates unsused relations, it does not deal with rules.
*/
void restrict_predicates(const decl_set & res);
void collect_predicates(decl_set & res);
void set_output_predicate(func_decl * pred);
bool is_output_predicate(func_decl * pred) { return m_output_preds.contains(pred); }
const decl_set & get_output_predicates() const { return m_output_preds; }
/**
\brief query result if it contains fact.
*/
bool result_contains_fact(relation_fact const& f);
void add_fact(func_decl* pred, relation_fact const& fact);
void add_fact(func_decl* pred, table_fact const& fact);
/**
\brief Store the relation \c rel under the predicate \c pred. The \c context object
takes over the ownership of the relation object.
*/
void store_relation(func_decl * pred, relation_base * rel);
void display_output_facts(std::ostream & out) const;
void display_facts(std::ostream & out) const;
};
};
#endif /* _REL_CONTEXT_H_ */

20
src/shell/datalog_frontend.cpp
View file

@ -26,12 +26,12 @@ Revision History:
#undef max
#endif
#include"smt_params.h"
#include"datalog_parser.h"
#include"arith_decl_plugin.h"
#include"dl_compiler.h"
#include"dl_context.h"
#include"dl_mk_filter_rules.h"
#include"dl_finite_product_relation.h"
#include"dl_context.h"
#include"datalog_parser.h"
#include"datalog_frontend.h"
#include"timeout.h"
@ -71,7 +71,7 @@ static void display_statistics(
code.process_all_costs();
{
params_ref p(ctx.get_params());
params_ref p;
p.set_bool("output_profile", true);
p.set_uint("profile_milliseconds_threshold", 100);
ctx.updt_params(p);
@ -86,7 +86,7 @@ static void display_statistics(
out << "--------------\n";
out << "instructions \n";
code.display(ctx, out);
code.display(ctx.get_rel_context(), out);
out << "--------------\n";
out << "big relations \n";
@ -94,7 +94,7 @@ static void display_statistics(
}
out << "--------------\n";
out << "relation sizes\n";
ctx.get_rmanager().display_relation_sizes(out);
ctx.get_rel_context().get_rmanager().display_relation_sizes(out);
if (verbose) {
out << "--------------\n";
@ -139,7 +139,7 @@ unsigned read_datalog(char const * file) {
params.set_bool("default_table_checked", dl_params.m_default_table_checked);
datalog::context ctx(m, s_params, params);
datalog::relation_manager & rmgr = ctx.get_rmanager();
datalog::relation_manager & rmgr = ctx.get_rel_context().get_rmanager();
datalog::relation_plugin & inner_plg = *rmgr.get_relation_plugin(symbol("tr_hashtable"));
SASSERT(&inner_plg);
rmgr.register_plugin(alloc(datalog::finite_product_relation_plugin, inner_plg, rmgr));
@ -206,7 +206,7 @@ unsigned read_datalog(char const * file) {
datalog::compiler::compile(ctx, ctx.get_rules(), rules_code, termination_code);
TRACE("dl_compiler", rules_code.display(ctx, tout););
TRACE("dl_compiler", rules_code.display(ctx.get_rel_context(), tout););
rules_code.make_annotations(ex_ctx);
@ -248,10 +248,10 @@ unsigned read_datalog(char const * file) {
TRACE("dl_compiler", ctx.display(tout);
rules_code.display(ctx, tout););
rules_code.display(ctx.get_rel_context(), tout););
if (ctx.get_params().get_bool("output_tuples", true)) {
ctx.display_output_facts(std::cout);
if (ctx.get_params().output_tuples()) {
ctx.get_rel_context().display_output_facts(std::cout);
}
display_statistics(

234
src/test/dl_smt_relation.cpp
View file

@ -1,234 +0,0 @@
#include "dl_smt_relation.h"
#include "arith_decl_plugin.h"
#include "dl_context.h"
#include "z3.h"
#include "z3_private.h"
#include "reg_decl_plugins.h"
namespace datalog {
void test_smt_relation_unit() {
ast_manager m;
reg_decl_plugins(m);
arith_util a(m);
sort* int_sort = a.mk_int();
sort* real_sort = a.mk_real();
smt_params params;
context ctx(m, params);
relation_manager & rm = ctx.get_rmanager();
relation_signature sig1;
sig1.push_back(int_sort);
sig1.push_back(int_sort);
sig1.push_back(real_sort);
smt_relation_plugin plugin(rm);
scoped_rel<relation_base> r1 = plugin.mk_empty(sig1);
// add_fact
relation_fact fact1(m);
fact1.push_back(a.mk_numeral(rational(1), true));
fact1.push_back(a.mk_numeral(rational(2), true));
fact1.push_back(a.mk_numeral(rational(3), false));
relation_fact fact2(m);
fact2.push_back(a.mk_numeral(rational(2), true));
fact2.push_back(a.mk_numeral(rational(2), true));
fact2.push_back(a.mk_numeral(rational(3), false));
r1->add_fact(fact1);
r1->display(std::cout << "r1: ");
// contains_fact
SASSERT(r1->contains_fact(fact1));
SASSERT(!r1->contains_fact(fact2));
// empty
scoped_rel<relation_base> r2 = plugin.mk_empty(sig1);
SASSERT(!r1->empty());
SASSERT(r2->empty());
// clone
scoped_rel<relation_base> r3 = r1->clone();
// complement?
r2->add_fact(fact2);
scoped_rel<relation_base> r4 = dynamic_cast<smt_relation&>(*r2).complement(0);
r4->display(std::cout << "complement r4: " );
// join
unsigned col_cnt = 2;
unsigned cols1[2] = {1, 2};
unsigned cols2[2] = {0, 2};
scoped_ptr<relation_join_fn> joinfn = plugin.mk_join_fn(*r1, *r4, col_cnt, cols1, cols2);
scoped_rel<relation_base> r5 = (*joinfn)(*r1, *r4);
r5->display(std::cout<< "join r5: ");
relation_fact fact3(m);
fact3.push_back(a.mk_numeral(rational(1), true));
fact3.push_back(a.mk_numeral(rational(2), true));
fact3.push_back(a.mk_numeral(rational(3), false));
fact3.push_back(a.mk_numeral(rational(2), true));
fact3.push_back(a.mk_numeral(rational(2), true));
fact3.push_back(a.mk_numeral(rational(3), false));
SASSERT(!r5->contains_fact(fact3));
fact3[5] = a.mk_numeral(rational(4), false);
SASSERT(!r5->contains_fact(fact3));
fact3[5] = a.mk_numeral(rational(3), false);
fact3[4] = a.mk_numeral(rational(3), true);
SASSERT(r5->contains_fact(fact3));
// project
unsigned removed_cols[2] = { 1, 4 };
scoped_ptr<relation_transformer_fn> projfn = plugin.mk_project_fn(*r5, col_cnt, removed_cols);
scoped_rel<relation_base> r6 = (*projfn)(*r5);
r6->display(std::cout<< "project r6: ");
// rename
unsigned cycle[3] = { 0, 2, 4 };
unsigned cycle_len = 3;
scoped_rel<relation_transformer_fn> renamefn = plugin.mk_rename_fn(*r5, cycle_len, cycle);
scoped_rel<relation_base> r7 = (*renamefn)(*r5);
r7->display(std::cout << "rename r7: ");
// union
// widen
relation_base* delta = 0;
scoped_ptr<relation_union_fn> widenfn = plugin.mk_widen_fn(*r1, *r2, delta);
scoped_ptr<relation_union_fn> unionfn = plugin.mk_union_fn(*r1, *r2, delta);
scoped_rel<relation_base> r8 = r1->clone();
(*unionfn)(*r8,*r2,0);
r8->display(std::cout << "union r8: ");
// filter_identical
unsigned identical_cols[2] = { 1, 3 };
scoped_ptr<relation_mutator_fn> filti = plugin.mk_filter_identical_fn(*r5, col_cnt, identical_cols);
scoped_rel<relation_base> r9 = r1->clone();
(*filti)(*r9);
r9->display(std::cout << "filter identical r9: ");
// filter_equal
app_ref value(m);
value = m.mk_const(symbol("x"), int_sort);
scoped_rel<relation_mutator_fn> eqn = plugin.mk_filter_equal_fn(*r5, value.get(), 3);
scoped_rel<relation_base> r10 = r1->clone();
(*eqn)(*r10);
r10->display(std::cout << "filter equal r10: ");
// filter_interpreted
app_ref cond(m);
cond = a.mk_lt(m.mk_var(3, int_sort), m.mk_var(4, int_sort));
scoped_rel<relation_mutator_fn> filtint = plugin.mk_filter_interpreted_fn(*r5, cond);
scoped_rel<relation_base> r11 = r5->clone();
(*filtint)(*r11);
r11->display(std::cout << "filter interpreted r11: ");
}
void test_smt_relation_api() {
enable_trace("smt_relation");
enable_trace("smt_relation2");
enable_trace("quant_elim");
Z3_config cfg = Z3_mk_config();
Z3_set_param_value(cfg, "DL_DEFAULT_RELATION", "smt_relation2");
Z3_context ctx = Z3_mk_context(cfg);
Z3_fixedpoint dl = Z3_mk_fixedpoint(ctx);
Z3_fixedpoint_inc_ref(ctx,dl);
Z3_del_config(cfg);
Z3_sort int_sort = Z3_mk_int_sort(ctx);
Z3_sort bool_sort = Z3_mk_bool_sort(ctx);
Z3_func_decl nil_decl, is_nil_decl;
Z3_func_decl cons_decl, is_cons_decl, head_decl, tail_decl;
Z3_sort list = Z3_mk_list_sort(
ctx,
Z3_mk_string_symbol(ctx, "list"),
int_sort,
&nil_decl,
&is_nil_decl,
&cons_decl,
&is_cons_decl,
&head_decl,
&tail_decl);
Z3_sort listint[2] = { list, int_sort };
Z3_symbol p_sym = Z3_mk_string_symbol(ctx, "p");
Z3_symbol q_sym = Z3_mk_string_symbol(ctx, "q");
Z3_func_decl p = Z3_mk_func_decl(ctx, p_sym, 2, listint, bool_sort);
Z3_func_decl q = Z3_mk_func_decl(ctx, q_sym, 2, listint, bool_sort);
Z3_fixedpoint_register_relation(ctx, dl, p);
Z3_fixedpoint_register_relation(ctx, dl, q);
Z3_ast zero = Z3_mk_numeral(ctx, "0", int_sort);
Z3_ast one = Z3_mk_numeral(ctx, "1", int_sort);
Z3_ast two = Z3_mk_numeral(ctx, "2", int_sort);
Z3_ast x = Z3_mk_bound(ctx, 0, list);
Z3_ast y = Z3_mk_bound(ctx, 1, int_sort);
Z3_ast z = Z3_mk_bound(ctx, 2, list);
Z3_ast zero_x[2] = { zero, x };
Z3_ast fx = Z3_mk_app(ctx, cons_decl, 2, zero_x);
Z3_ast zero_fx[2] = { zero, fx };
Z3_ast ffx = Z3_mk_app(ctx, cons_decl, 2, zero_fx);
Z3_ast xy[2] = { x, y };
Z3_ast zy[2] = { z, y };
// Z3_ast ffxy[2] = { ffx, y };
// Z3_ast fxy[2] = { fx, y };
Z3_ast zero_nil[2] = { zero, Z3_mk_app(ctx, nil_decl, 0, 0) };
Z3_ast f0 = Z3_mk_app(ctx, cons_decl, 2, zero_nil);
Z3_ast zero_f0[2] = { zero, f0 };
Z3_ast f1 = Z3_mk_app(ctx, cons_decl, 2, zero_f0);
Z3_ast zero_f1[2] = { zero, f1 };
Z3_ast f2 = Z3_mk_app(ctx, cons_decl, 2, zero_f1);
Z3_ast zero_f2[2] = { zero, f2 };
Z3_ast f3 = Z3_mk_app(ctx, cons_decl, 2, zero_f2);
Z3_ast zero_f3[2] = { zero, f3 };
Z3_ast f4 = Z3_mk_app(ctx, cons_decl, 2, zero_f3);
Z3_ast zero_f4[2] = { zero, f4 };
Z3_ast f5 = Z3_mk_app(ctx, cons_decl, 2, zero_f4);
Z3_ast zero_z[2] = { zero, z };
Z3_ast fz = Z3_mk_app(ctx, cons_decl, 2, zero_z);
Z3_ast pxy = Z3_mk_app(ctx, p, 2, xy);
Z3_ast pzy = Z3_mk_app(ctx, p, 2, zy);
Z3_ast qxy = Z3_mk_app(ctx, q, 2, xy);
Z3_ast qzy = Z3_mk_app(ctx, q, 2, zy);
Z3_ast even_y = Z3_mk_eq(ctx, zero, Z3_mk_mod(ctx, y, two));
Z3_ast odd_y = Z3_mk_eq(ctx, one, Z3_mk_mod(ctx, y, two));
// p(x, y) :- odd(y), p(z,y), f(z) = x . // dead rule.
// q(x, y) :- p(f(f(x)), y).
// p(x, y) :- q(f(x), y) // x decreases
// p(x, y) :- even y, x = f^5(0) // initial condition.
Z3_ast body1[3] = { pzy, Z3_mk_eq(ctx, fz, x), odd_y };
Z3_ast body2[2] = { pzy, Z3_mk_eq(ctx, ffx, z) };
Z3_ast body3[2] = { qzy, Z3_mk_eq(ctx, fx, z) };
Z3_ast body4[2] = { even_y, Z3_mk_eq(ctx, x, f5) };
Z3_fixedpoint_add_rule(ctx, dl, Z3_mk_implies(ctx, Z3_mk_and(ctx, 3, body1), pxy), 0);
Z3_fixedpoint_add_rule(ctx, dl, Z3_mk_implies(ctx, Z3_mk_and(ctx, 2, body2), qxy), 0);
Z3_fixedpoint_add_rule(ctx, dl, Z3_mk_implies(ctx, Z3_mk_and(ctx, 2, body3), pxy), 0);
Z3_fixedpoint_add_rule(ctx, dl, Z3_mk_implies(ctx, Z3_mk_and(ctx, 2, body4), pxy), 0);
Z3_lbool r = Z3_fixedpoint_query(ctx, dl, pxy);
if (r != Z3_L_UNDEF) {
std::cout << Z3_ast_to_string(ctx, Z3_fixedpoint_get_answer(ctx, dl)) << "\n";
}
Z3_del_context(ctx);
}
};
void tst_dl_smt_relation() {
datalog::test_smt_relation_api();
datalog::test_smt_relation_unit();
}

1
src/test/main.cpp
View file

@ -166,7 +166,6 @@ int main(int argc, char ** argv) {
TST(total_order);
TST(dl_table);
TST(dl_context);
TST(dl_smt_relation);
TST(dl_query);
TST(dl_util);
TST(dl_product_relation);