mirror of
https://github.com/Z3Prover/z3
synced 2025-04-10 19:27:06 +00:00
port to new parameter infrastructure
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner
parent
67485b8af7
commit
5c11f394cd
src
muz_qe
datalog_parser.cppdl_bmc_engine.cppdl_bmc_engine.hdl_cmds.cppdl_context.cppdl_context.hdl_mk_bit_blast.cppdl_mk_rule_inliner.cppdl_smt_relation.cppdl_smt_relation.hdl_util.hfixedpoint_params.pyghorn_tactic.cpppdr_context.cpppdr_context.hpdr_dl_interface.cpppdr_dl_interface.hpdr_farkas_learner.cpppdr_generalizers.cpppdr_generalizers.hpdr_interpolant_provider.cpppdr_interpolant_provider.hpdr_manager.cpppdr_manager.hpdr_prop_solver.cpppdr_reachable_cache.cpppdr_reachable_cache.hpdr_smt_context_manager.cpppdr_smt_context_manager.h
shell
test
|
|
@ -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);
|
||||
|
|
|
|||
|
|
@ -71,7 +71,7 @@ namespace datalog {
|
|||
m_ctx.set_output_predicate(m_query_pred);
|
||||
m_ctx.apply_default_transformation(mc, m_pc);
|
||||
|
||||
if (m_ctx.get_params().get_bool("slice", true)) {
|
||||
if (m_ctx.get_params().slice()) {
|
||||
datalog::rule_transformer transformer(m_ctx);
|
||||
datalog::mk_slice* slice = alloc(datalog::mk_slice, m_ctx);
|
||||
transformer.register_plugin(slice);
|
||||
|
|
@ -1100,9 +1100,6 @@ namespace datalog {
|
|||
m_solver.reset_statistics();
|
||||
}
|
||||
|
||||
void bmc::collect_params(param_descrs& p) {
|
||||
}
|
||||
|
||||
expr_ref bmc::get_answer() {
|
||||
return m_answer;
|
||||
}
|
||||
|
|
|
|||
|
|
@ -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);
|
||||
};
|
||||
};
|
||||
|
||||
|
|
|
|||
|
|
@ -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,8 @@ class dl_context {
|
|||
scoped_ptr<datalog::context> m_context;
|
||||
trail_stack<dl_context> m_trail;
|
||||
|
||||
public:
|
||||
dl_context(cmd_context & ctx, dl_collected_cmds* collected_cmds):
|
||||
m_params(m_params_ref),
|
||||
m_cmd(ctx),
|
||||
m_collected_cmds(collected_cmds),
|
||||
m_ref_count(0),
|
||||
|
|
@ -64,7 +66,7 @@ public:
|
|||
void init() {
|
||||
ast_manager& m = m_cmd.m();
|
||||
if (!m_context) {
|
||||
m_context = alloc(datalog::context, m, m_params);
|
||||
m_context = alloc(datalog::context, m, m_fparams, m_params_ref);
|
||||
}
|
||||
if (!m_decl_plugin) {
|
||||
symbol name("datalog_relation");
|
||||
|
|
@ -212,7 +214,7 @@ public:
|
|||
datalog::context& dlctx = m_dl_ctx->dlctx();
|
||||
set_background(ctx);
|
||||
dlctx.updt_params(m_params);
|
||||
unsigned timeout = m_params.get_uint("timeout", UINT_MAX);
|
||||
unsigned timeout = m_dl_ctx->m_params.timeout();
|
||||
cancel_eh<datalog::context> eh(dlctx);
|
||||
lbool status = l_undef;
|
||||
{
|
||||
|
|
@ -267,10 +269,6 @@ public:
|
|||
|
||||
virtual void init_pdescrs(cmd_context & ctx, param_descrs & p) {
|
||||
m_dl_ctx->dlctx().collect_params(p);
|
||||
insert_timeout(p);
|
||||
p.insert("print_answer", CPK_BOOL, "(default: false) print answer instance(s) to query.");
|
||||
p.insert("print_certificate", CPK_BOOL, "(default: false) print certificate for reachability or non-reachability.");
|
||||
p.insert("print_statistics", CPK_BOOL, "(default: false) print statistics.");
|
||||
}
|
||||
|
||||
|
||||
|
|
@ -285,7 +283,7 @@ private:
|
|||
}
|
||||
|
||||
void print_answer(cmd_context& ctx) {
|
||||
if (m_params.get_bool("print_answer", false)) {
|
||||
if (m_dl_ctx->m_params.print_answer()) {
|
||||
datalog::context& dlctx = m_dl_ctx->dlctx();
|
||||
ast_manager& m = ctx.m();
|
||||
expr_ref query_result(dlctx.get_answer_as_formula(), m);
|
||||
|
|
@ -300,7 +298,7 @@ private:
|
|||
}
|
||||
|
||||
void print_statistics(cmd_context& ctx) {
|
||||
if (m_params.get_bool("print_statistics", false)) {
|
||||
if (m_dl_ctx->m_params.print_statistics()) {
|
||||
statistics st;
|
||||
datalog::context& dlctx = m_dl_ctx->dlctx();
|
||||
unsigned long long max_mem = memory::get_max_used_memory();
|
||||
|
|
@ -314,7 +312,7 @@ private:
|
|||
}
|
||||
|
||||
void print_certificate(cmd_context& ctx) {
|
||||
if (m_params.get_bool("print_certificate", false)) {
|
||||
if (m_dl_ctx->m_params.print_certificate()) {
|
||||
datalog::context& dlctx = m_dl_ctx->dlctx();
|
||||
if (!dlctx.display_certificate(ctx.regular_stream())) {
|
||||
throw cmd_exception("certificates are not supported for the selected engine");
|
||||
|
|
|
|||
|
|
@ -44,7 +44,6 @@ Revision History:
|
|||
#include"dl_compiler.h"
|
||||
#include"dl_instruction.h"
|
||||
#include"dl_context.h"
|
||||
#include"dl_smt_relation.h"
|
||||
#ifndef _EXTERNAL_RELEASE
|
||||
#include"dl_skip_table.h"
|
||||
#endif
|
||||
|
|
@ -229,7 +228,8 @@ namespace datalog {
|
|||
context::context(ast_manager & m, smt_params& fp, params_ref const& pa):
|
||||
m(m),
|
||||
m_fparams(fp),
|
||||
m_params(pa),
|
||||
m_params_ref(pa),
|
||||
m_params(m_params_ref),
|
||||
m_decl_util(m),
|
||||
m_rewriter(m),
|
||||
m_var_subst(m),
|
||||
|
|
@ -259,7 +259,6 @@ namespace datalog {
|
|||
#endif
|
||||
|
||||
//register plugins for builtin relations
|
||||
get_rmanager().register_plugin(alloc(smt_relation_plugin, get_rmanager()));
|
||||
|
||||
get_rmanager().register_plugin(alloc(bound_relation_plugin, get_rmanager()));
|
||||
get_rmanager().register_plugin(alloc(interval_relation_plugin, get_rmanager()));
|
||||
|
|
@ -960,66 +959,13 @@ namespace datalog {
|
|||
}
|
||||
|
||||
void context::collect_params(param_descrs& p) {
|
||||
p.insert("engine", CPK_SYMBOL, "(default: automatically configured) select 'datalog', PDR 'pdr' engine.");
|
||||
p.insert("bit_blast", CPK_BOOL, "(default: false) bit-blast bit-vectors (for PDR engine).");
|
||||
p.insert("default_table", CPK_SYMBOL, "default table implementation: 'sparse' (default), 'hashtable', 'bitvector', 'interval'");
|
||||
p.insert("default_relation", CPK_SYMBOL, "default relation implementation: 'external_relation', 'pentagon'");
|
||||
|
||||
p.insert("generate_explanations", CPK_BOOL, "if true, signature of relations will be extended to contain explanations for facts");
|
||||
p.insert("explanations_on_relation_level", CPK_BOOL, "if true, explanations are generated as history of each relation, "
|
||||
"rather than per fact (generate_explanations must be set to true for this option to have any effect)");
|
||||
|
||||
p.insert("magic_sets_for_queries", CPK_BOOL, "magic set transformation will be used for queries");
|
||||
p.insert("unbound_compressor", CPK_BOOL, "auxiliary relations will be introduced to avoid unbound variables in rule heads");
|
||||
p.insert("similarity_compressor", CPK_BOOL, "rules that differ only in values of constants will be merged into a single rule");
|
||||
p.insert("similarity_compressor_threshold", CPK_UINT, "if dl_similiaryt_compressor is on, this value determines how many "
|
||||
"similar rules there must be in order for them to be merged");
|
||||
|
||||
p.insert("all_or_nothing_deltas", CPK_BOOL, "compile rules so that it is enough for the delta relation in union and widening "
|
||||
"operations to determine only whether the updated relation was modified or not");
|
||||
p.insert("compile_with_widening", CPK_BOOL, "widening will be used to compile recursive rules");
|
||||
p.insert("eager_emptiness_checking", CPK_BOOL, "emptiness of affected relations will be checked after each instruction, "
|
||||
"so that we may ommit unnecessary instructions");
|
||||
p.insert("default_table_checked", CPK_BOOL,
|
||||
"if true, the detault table will be default_table inside a wrapper that checks that "
|
||||
"its results are the same as of default_table_checker table");
|
||||
|
||||
|
||||
p.insert("initial_restart_timeout", CPK_UINT, "length of saturation run before the first restart (in ms); zero means no restarts");
|
||||
p.insert("restart_timeout_quotient", CPK_UINT, "restart timeout will be multiplied by this number after each restart");
|
||||
p.insert("use_map_names", CPK_BOOL, "use names from map files when displaying tuples");
|
||||
|
||||
p.insert("output_profile", CPK_BOOL, "determines whether profile informations should be output when outputting Datalog rules or instructions");
|
||||
p.insert("output_tuples", CPK_BOOL, "determines whether tuples for output predicates should be output");
|
||||
p.insert("profile_timeout_milliseconds", CPK_UINT, "instructions and rules that took less than the threshold will not be printed when printed the instruction/rule list");
|
||||
|
||||
p.insert("print_with_fixedpoint_extensions", CPK_BOOL, "(default true) use SMT-LIB2 fixedpoint extensions, instead of pure SMT2, when printing rules");
|
||||
p.insert("print_low_level_smt2", CPK_BOOL, "(default false) use (faster) low-level SMT2 printer (the printer is scalable but the result may not be as readable)");
|
||||
p.insert("print_with_variable_declarations", CPK_BOOL, "(default true) use variable declarations when displaying rules (instead of attempting to use original names)");
|
||||
|
||||
#ifndef _EXTERNAL_RELEASE
|
||||
p.insert("dbg_fpr_nonempty_relation_signature", CPK_BOOL,
|
||||
"if true, finite_product_relation will attempt to avoid creating inner relation with empty signature "
|
||||
"by putting in half of the table columns, if it would have been empty otherwise");
|
||||
|
||||
p.insert("smt_relation_ground_recursive", CPK_BOOL, "Ensure recursive relation is ground in union");
|
||||
p.insert("inline_linear_branch", CPK_BOOL, "try linear inlining method with potential expansion");
|
||||
#endif
|
||||
p.insert("fix_unbound_vars", CPK_BOOL, "fix unbound variables in tail");
|
||||
p.insert("default_table_checker", CPK_SYMBOL, "see default_table_checked");
|
||||
p.insert("inline_linear", CPK_BOOL, "(default true) try linear inlining method");
|
||||
p.insert("inline_eager", CPK_BOOL, "(default true) try eager inlining of rules");
|
||||
|
||||
|
||||
pdr::dl_interface::collect_params(p);
|
||||
bmc::collect_params(p);
|
||||
fixedpoint_params::collect_param_descrs(p);
|
||||
insert_timeout(p);
|
||||
}
|
||||
|
||||
void context::updt_params(params_ref const& p) {
|
||||
m_params.copy(p);
|
||||
if (m_pdr.get()) m_pdr->updt_params();
|
||||
|
||||
m_params_ref.copy(p);
|
||||
if (m_pdr.get()) m_pdr->updt_params();
|
||||
}
|
||||
|
||||
void context::collect_predicates(decl_set & res) {
|
||||
|
|
@ -1190,7 +1136,7 @@ namespace datalog {
|
|||
};
|
||||
|
||||
void context::configure_engine() {
|
||||
symbol e = m_params.get_sym("engine", symbol());
|
||||
symbol e = m_params.engine();
|
||||
|
||||
if (e == symbol("datalog")) {
|
||||
m_engine = DATALOG_ENGINE;
|
||||
|
|
@ -1668,9 +1614,9 @@ namespace datalog {
|
|||
expr_ref fml(m);
|
||||
expr_ref_vector rules(m);
|
||||
svector<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);
|
||||
|
||||
|
|
|
|||
|
|
@ -24,7 +24,6 @@ Revision History:
|
|||
#undef max
|
||||
#endif
|
||||
#include"arith_decl_plugin.h"
|
||||
#include"smt_params.h"
|
||||
#include"map.h"
|
||||
#include"th_rewriter.h"
|
||||
#include"str_hashtable.h"
|
||||
|
|
@ -44,6 +43,7 @@ Revision History:
|
|||
#include"model_converter.h"
|
||||
#include"proof_converter.h"
|
||||
#include"model2expr.h"
|
||||
#include"smt_params.h"
|
||||
|
||||
namespace datalog {
|
||||
|
||||
|
|
@ -78,8 +78,9 @@ namespace datalog {
|
|||
typedef vector<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;
|
||||
|
|
@ -122,7 +123,7 @@ namespace datalog {
|
|||
|
||||
|
||||
public:
|
||||
context(ast_manager & m, smt_params& params, params_ref const& p = params_ref());
|
||||
context(ast_manager & m, smt_params& fp, params_ref const& p = params_ref());
|
||||
~context();
|
||||
void reset();
|
||||
|
||||
|
|
@ -150,31 +151,31 @@ namespace datalog {
|
|||
const relation_manager & get_rmanager() const { return m_rmanager; }
|
||||
rule_manager & get_rule_manager() { return m_rule_manager; }
|
||||
smt_params & get_fparams() const { return m_fparams; }
|
||||
params_ref const& get_params() const { return m_params; }
|
||||
fixedpoint_params const& get_params() const { return m_params; }
|
||||
DL_ENGINE get_engine() { configure_engine(); return m_engine; }
|
||||
th_rewriter& get_rewriter() { return m_rewriter; }
|
||||
var_subst & get_var_subst() { return m_var_subst; }
|
||||
dl_decl_util & get_decl_util() { return m_decl_util; }
|
||||
|
||||
bool output_profile() const { return m_params.get_bool("output_profile", false); }
|
||||
bool fix_unbound_vars() const { return m_params.get_bool("fix_unbound_vars", false); }
|
||||
symbol default_table() const { return m_params.get_sym("default_table", symbol("sparse")); }
|
||||
symbol default_relation() const { return m_params.get_sym("default_relation", external_relation_plugin::get_name()); }
|
||||
symbol default_table_checker() const { return m_params.get_sym("default_table_checker", symbol("sparse")); }
|
||||
bool default_table_checked() const { return m_params.get_bool("default_table_checked", false); }
|
||||
bool dbg_fpr_nonempty_relation_signature() const { return m_params.get_bool("dbg_fpr_nonempty_relation_signatures", false); }
|
||||
unsigned dl_profile_milliseconds_threshold() const { return m_params.get_uint("profile_milliseconds_threshold", 0); }
|
||||
bool all_or_nothing_deltas() const { return m_params.get_bool("all_or_nothing_deltas", false); }
|
||||
bool compile_with_widening() const { return m_params.get_bool("compile_with_widening", false); }
|
||||
bool unbound_compressor() const { return m_params.get_bool("unbound_compressor", true); }
|
||||
bool similarity_compressor() const { return m_params.get_bool("similarity_compressor", true); }
|
||||
unsigned similarity_compressor_threshold() const { return m_params.get_uint("similarity_compressor_threshold", 11); }
|
||||
bool output_profile() const { return m_params.output_profile(); }
|
||||
bool fix_unbound_vars() const { return m_params.fix_unbound_vars(); }
|
||||
symbol default_table() const { return m_params.default_table(); }
|
||||
symbol default_relation() const { return m_params.default_relation(); } // external_relation_plugin::get_name());
|
||||
symbol default_table_checker() const { return m_params.default_table_checker(); }
|
||||
bool default_table_checked() const { return m_params.default_table_checked(); }
|
||||
bool dbg_fpr_nonempty_relation_signature() const { return m_params.dbg_fpr_nonempty_relation_signature(); }
|
||||
unsigned dl_profile_milliseconds_threshold() const { return m_params.profile_timeout_milliseconds(); }
|
||||
bool all_or_nothing_deltas() const { return m_params.all_or_nothing_deltas(); }
|
||||
bool compile_with_widening() const { return m_params.compile_with_widening(); }
|
||||
bool unbound_compressor() const { return m_params.unbound_compressor(); }
|
||||
bool similarity_compressor() const { return m_params.similarity_compressor(); }
|
||||
unsigned similarity_compressor_threshold() const { return m_params.similarity_compressor_threshold(); }
|
||||
unsigned soft_timeout() const { return m_fparams.m_soft_timeout; }
|
||||
unsigned initial_restart_timeout() const { return m_params.get_uint("initial_restart_timeout", 0); }
|
||||
bool generate_explanations() const { return m_params.get_bool("generate_explanations", false); }
|
||||
bool explanations_on_relation_level() const { return m_params.get_bool("explanations_on_relation_level", false); }
|
||||
bool magic_sets_for_queries() const { return m_params.get_bool("magic_sets_for_queries", false); }
|
||||
bool eager_emptiness_checking() const { return m_params.get_bool("eager_emptiness_checking", true); }
|
||||
unsigned initial_restart_timeout() const { return m_params.initial_restart_timeout(); }
|
||||
bool generate_explanations() const { return m_params.generate_explanations(); }
|
||||
bool explanations_on_relation_level() const { return m_params.explanations_on_relation_level(); }
|
||||
bool magic_sets_for_queries() const { return m_params.magic_sets_for_queries(); }
|
||||
bool eager_emptiness_checking() const { return m_params.eager_emptiness_checking(); }
|
||||
|
||||
void register_finite_sort(sort * s, sort_kind k);
|
||||
|
||||
|
|
|
|||
|
|
@ -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) {
|
||||
|
|
|
|||
|
|
@ -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;
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -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;
|
||||
}
|
||||
};
|
||||
|
||||
|
|
@ -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
|
||||
|
|
@ -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
62
src/muz_qe/fixedpoint_params.pyg
Normal 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: (default true) use BFS strategy for expanding model search"),
|
||||
('use_farkas', BOOL, True, "PDR: (default true) use lemma generator based on Farkas (for linear real arithmetic)"),
|
||||
('generate_proof_trace', BOOL, False, "PDR: (default false) trace for 'sat' answer as proof object"),
|
||||
('flexible_trace', BOOL, False, "PDR: (default false) allow PDR generate long counter-examples "
|
||||
"by extending candidate trace within search area"),
|
||||
('unfold_rules', UINT, 0, "PDR: (default 0) unfold rules statically using iterative squarring"),
|
||||
('use_model_generalizer', BOOL, False, "PDR: (default false) use model for backwards propagation (instead of symbolic simulation)"),
|
||||
('validate_result', BOOL, False, "PDR (default false) validate result (by proof checking or model checking)"),
|
||||
('simplify_formulas_pre', BOOL, False, "PDR: (default false) simplify derived formulas before inductive propagation"),
|
||||
('simplify_formulas_post', BOOL, False, "PDR: (default false) simplify derived formulas after inductive propagation"),
|
||||
('slice', BOOL, True, "PDR: (default true) simplify clause set using slicing"),
|
||||
('coalesce_rules', BOOL, False, "BMC: (default false) coalesce rules"),
|
||||
('use_multicore_generalizer', BOOL, False, "PDR: (default false) extract multiple cores for blocking states"),
|
||||
('use_inductive_generalizer', BOOL, True, "PDR: (default true) generalize lemmas using induction strengthening"),
|
||||
('cache_mode', UINT, 0, "PDR: use no (0 - default) symbolic (1) or explicit cache (2) for model search"),
|
||||
('inductive_reachability_check', BOOL, False, "PDR: (default false) assume negation of the cube on the previous level when "
|
||||
"checking for reachability (not only during cube weakening)"),
|
||||
('max_num_contexts', UINT, 500, "PDR: (default 500) maximal number of contexts to create"),
|
||||
('try_minimize_core', BOOL, False, "PDR: (default false) try to reduce core size (before inductive minimization)"),
|
||||
('profile_timeout_milliseconds', UINT, 0, "instructions and rules that took less than the threshold will not be printed when printed the instruction/rule list"),
|
||||
('dbg_fpr_nonempty_relation_signature', BOOL, False,
|
||||
"if true, finite_product_relation will attempt to avoid creating inner relation with empty signature "
|
||||
"by putting in half of the table columns, if it would have been empty otherwise"),
|
||||
('print_answer', BOOL, False, 'print answer instance(s) to query'),
|
||||
('print_certificate', BOOL, False, 'print certificate for reacahbility or non-reachability'),
|
||||
('print_statistics', BOOL, False, 'print statistics'),
|
||||
))
|
||||
|
||||
|
||||
|
||||
|
|
@ -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);
|
||||
}
|
||||
|
|
|
|||
|
|
@ -1123,17 +1123,17 @@ namespace pdr {
|
|||
|
||||
context::context(
|
||||
smt_params& fparams,
|
||||
params_ref const& params,
|
||||
fixedpoint_params const& params,
|
||||
ast_manager& m
|
||||
)
|
||||
: m_fparams(fparams),
|
||||
m_params(params),
|
||||
m(m),
|
||||
m_context(0),
|
||||
m_pm(m_fparams, m_params, m),
|
||||
m_pm(m_fparams, params, m),
|
||||
m_query_pred(m),
|
||||
m_query(0),
|
||||
m_search(m_params.get_bool("bfs_model_search", true)),
|
||||
m_search(m_params.bfs_model_search()),
|
||||
m_last_result(l_undef),
|
||||
m_inductive_lvl(0),
|
||||
m_cancel(false)
|
||||
|
|
@ -1358,7 +1358,7 @@ namespace pdr {
|
|||
};
|
||||
|
||||
void context::validate() {
|
||||
if (!m_params.get_bool("validate_result", false)) {
|
||||
if (!m_params.validate_result()) {
|
||||
return;
|
||||
}
|
||||
switch(m_last_result) {
|
||||
|
|
@ -1449,34 +1449,26 @@ namespace pdr {
|
|||
void context::init_core_generalizers(datalog::rule_set& rules) {
|
||||
reset_core_generalizers();
|
||||
classifier_proc classify(m, rules);
|
||||
bool use_mc = m_params.get_bool("use_multicore_generalizer", false);
|
||||
bool use_mc = m_params.use_multicore_generalizer();
|
||||
if (use_mc) {
|
||||
m_core_generalizers.push_back(alloc(core_multi_generalizer, *this, 0));
|
||||
}
|
||||
if (m_params.get_bool("use_farkas", true) && !classify.is_bool()) {
|
||||
if (m_params.get_bool("inline_proof_mode", true)) {
|
||||
m.toggle_proof_mode(PGM_FINE);
|
||||
m_fparams.m_proof_mode = PGM_FINE;
|
||||
m_fparams.m_arith_bound_prop = BP_NONE;
|
||||
m_fparams.m_arith_auto_config_simplex = true;
|
||||
m_fparams.m_arith_propagate_eqs = false;
|
||||
m_fparams.m_arith_eager_eq_axioms = false;
|
||||
if (classify.is_dl()) {
|
||||
m_fparams.m_arith_mode = AS_DIFF_LOGIC;
|
||||
m_fparams.m_arith_expand_eqs = true;
|
||||
}
|
||||
}
|
||||
else {
|
||||
m_core_generalizers.push_back(alloc(core_farkas_generalizer, *this, m, m_fparams));
|
||||
if (m_params.use_farkas() && !classify.is_bool()) {
|
||||
m.toggle_proof_mode(PGM_FINE);
|
||||
m_fparams.m_proof_mode = PGM_FINE;
|
||||
m_fparams.m_arith_bound_prop = BP_NONE;
|
||||
m_fparams.m_arith_auto_config_simplex = true;
|
||||
m_fparams.m_arith_propagate_eqs = false;
|
||||
m_fparams.m_arith_eager_eq_axioms = false;
|
||||
if (classify.is_dl()) {
|
||||
m_fparams.m_arith_mode = AS_DIFF_LOGIC;
|
||||
m_fparams.m_arith_expand_eqs = true;
|
||||
}
|
||||
}
|
||||
if (!use_mc && m_params.get_bool("use_inductive_generalizer", true)) {
|
||||
if (!use_mc && m_params.use_inductive_generalizer()) {
|
||||
m_core_generalizers.push_back(alloc(core_bool_inductive_generalizer, *this, 0));
|
||||
}
|
||||
if (m_params.get_bool("use_interpolants", false)) {
|
||||
m_core_generalizers.push_back(alloc(core_interpolant_generalizer, *this));
|
||||
}
|
||||
if (m_params.get_bool("inductive_reachability_check", false)) {
|
||||
if (m_params.inductive_reachability_check()) {
|
||||
m_core_generalizers.push_back(alloc(core_induction_generalizer, *this));
|
||||
}
|
||||
}
|
||||
|
|
@ -1588,7 +1580,7 @@ namespace pdr {
|
|||
\brief Retrieve satisfying assignment with explanation.
|
||||
*/
|
||||
expr_ref context::mk_sat_answer() const {
|
||||
if (m_params.get_bool("generate_proof_trace", false)) {
|
||||
if (m_params.generate_proof_trace()) {
|
||||
proof_ref pr = get_proof();
|
||||
return expr_ref(pr.get(), m);
|
||||
}
|
||||
|
|
@ -1709,7 +1701,7 @@ namespace pdr {
|
|||
n.pt().add_property(ncore, uses_level?n.level():infty_level);
|
||||
}
|
||||
CASSERT("pdr",n.level() == 0 || check_invariant(n.level()-1));
|
||||
m_search.backtrack_level(!found_invariant && m_params.get_bool("flexible_trace", false), n);
|
||||
m_search.backtrack_level(!found_invariant && m_params.flexible_trace(), n);
|
||||
break;
|
||||
}
|
||||
case l_undef: {
|
||||
|
|
@ -1731,7 +1723,7 @@ namespace pdr {
|
|||
}
|
||||
|
||||
void context::propagate(unsigned max_prop_lvl) {
|
||||
if (m_params.get_bool("simplify_formulas_pre", false)) {
|
||||
if (m_params.simplify_formulas_pre()) {
|
||||
simplify_formulas();
|
||||
}
|
||||
for (unsigned lvl = 0; lvl <= max_prop_lvl; lvl++) {
|
||||
|
|
@ -1750,7 +1742,7 @@ namespace pdr {
|
|||
throw inductive_exception();
|
||||
}
|
||||
}
|
||||
if (m_params.get_bool("simplify_formulas_post", false)) {
|
||||
if (m_params.simplify_formulas_post()) {
|
||||
simplify_formulas();
|
||||
}
|
||||
}
|
||||
|
|
@ -1798,7 +1790,7 @@ namespace pdr {
|
|||
*/
|
||||
void context::create_children(model_node& n) {
|
||||
SASSERT(n.level() > 0);
|
||||
bool use_model_generalizer = m_params.get_bool("use_model_generalizer", false);
|
||||
bool use_model_generalizer = m_params.use_model_generalizer();
|
||||
datalog::scoped_no_proof _sc(m);
|
||||
|
||||
pred_transformer& pt = n.pt();
|
||||
|
|
|
|||
|
|
@ -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; }
|
||||
|
|
|
|||
|
|
@ -108,13 +108,13 @@ lbool dl_interface::query(expr * query) {
|
|||
|
||||
model_converter_ref mc = datalog::mk_skip_model_converter();
|
||||
proof_converter_ref pc;
|
||||
if (m_ctx.get_params().get_bool("generate_proof_trace", false)) {
|
||||
if (m_ctx.get_params().generate_proof_trace()) {
|
||||
pc = datalog::mk_skip_proof_converter();
|
||||
}
|
||||
m_ctx.set_output_predicate(query_pred);
|
||||
m_ctx.apply_default_transformation(mc, pc);
|
||||
|
||||
if (m_ctx.get_params().get_bool("slice", true)) {
|
||||
if (m_ctx.get_params().slice()) {
|
||||
datalog::rule_transformer transformer(m_ctx);
|
||||
datalog::mk_slice* slice = alloc(datalog::mk_slice, m_ctx);
|
||||
transformer.register_plugin(slice);
|
||||
|
|
@ -133,10 +133,10 @@ lbool dl_interface::query(expr * query) {
|
|||
}
|
||||
}
|
||||
|
||||
if (m_ctx.get_params().get_uint("unfold_rules",0) > 0) {
|
||||
unsigned num_unfolds = m_ctx.get_params().get_uint("unfold_rules", 0);
|
||||
if (m_ctx.get_params().unfold_rules() > 0) {
|
||||
unsigned num_unfolds = m_ctx.get_params().unfold_rules();
|
||||
datalog::rule_transformer transformer1(m_ctx), transformer2(m_ctx);
|
||||
if (m_ctx.get_params().get_uint("coalesce_rules", false)) {
|
||||
if (m_ctx.get_params().coalesce_rules()) {
|
||||
transformer1.register_plugin(alloc(datalog::mk_coalesce, m_ctx));
|
||||
m_ctx.transform_rules(transformer1, mc, pc);
|
||||
}
|
||||
|
|
@ -198,7 +198,7 @@ expr_ref dl_interface::get_cover_delta(int level, func_decl* pred_orig) {
|
|||
}
|
||||
|
||||
void dl_interface::add_cover(int level, func_decl* pred, expr* property) {
|
||||
if (m_ctx.get_params().get_bool("slice", true)) {
|
||||
if (m_ctx.get_params().slice()) {
|
||||
throw default_exception("Covers are incompatible with slicing. Disable slicing before using covers");
|
||||
}
|
||||
m_context->add_cover(level, pred, property);
|
||||
|
|
@ -246,32 +246,3 @@ model_ref dl_interface::get_model() {
|
|||
proof_ref dl_interface::get_proof() {
|
||||
return m_context->get_proof();
|
||||
}
|
||||
|
||||
void dl_interface::collect_params(param_descrs& p) {
|
||||
p.insert("bfs_model_search", CPK_BOOL, "PDR: (default true) use BFS strategy for expanding model search");
|
||||
p.insert("use_farkas", CPK_BOOL, "PDR: (default true) use lemma generator based on Farkas (for linear real arithmetic)");
|
||||
p.insert("generate_proof_trace", CPK_BOOL, "PDR: (default false) trace for 'sat' answer as proof object");
|
||||
p.insert("inline_proofs", CPK_BOOL, "PDR: (default true) run PDR with proof mode turned on and extract "
|
||||
"Farkas coefficients directly (instead of creating a separate proof object when extracting coefficients)");
|
||||
p.insert("flexible_trace", CPK_BOOL, "PDR: (default false) allow PDR generate long counter-examples "
|
||||
"by extending candidate trace within search area");
|
||||
p.insert("unfold_rules", CPK_UINT, "PDR: (default 0) unfold rules statically using iterative squarring");
|
||||
p.insert("use_model_generalizer", CPK_BOOL, "PDR: (default false) use model for backwards propagation (instead of symbolic simulation)");
|
||||
p.insert("validate_result", CPK_BOOL, "PDR (default false) validate result (by proof checking or model checking)");
|
||||
#ifndef _EXTERNAL_RELEASE
|
||||
p.insert("use_multicore_generalizer", CPK_BOOL, "PDR: (default false) extract multiple cores for blocking states");
|
||||
p.insert("use_inductive_generalizer", CPK_BOOL, "PDR: (default true) generalize lemmas using induction strengthening");
|
||||
p.insert("use_interpolants", CPK_BOOL, "PDR: (default false) use iZ3 interpolation for lemma generation");
|
||||
p.insert("dump_interpolants", CPK_BOOL, "PDR: (default false) display interpolants");
|
||||
p.insert("cache_mode", CPK_UINT, "PDR: use no (0 - default) symbolic (1) or explicit cache (2) for model search");
|
||||
p.insert("inductive_reachability_check", CPK_BOOL,
|
||||
"PDR: (default false) assume negation of the cube on the previous level when "
|
||||
"checking for reachability (not only during cube weakening)");
|
||||
p.insert("max_num_contexts", CPK_UINT, "PDR: (default 500) maximal number of contexts to create");
|
||||
p.insert("try_minimize_core", CPK_BOOL, "PDR: (default false) try to reduce core size (before inductive minimization)");
|
||||
#endif
|
||||
p.insert("simplify_formulas_pre", CPK_BOOL, "PDR: (default false) simplify derived formulas before inductive propagation");
|
||||
p.insert("simplify_formulas_post", CPK_BOOL, "PDR: (default false) simplify derived formulas after inductive propagation");
|
||||
p.insert("slice", CPK_BOOL, "PDR: (default true) simplify clause set using slicing");
|
||||
p.insert("coalesce_rules", CPK_BOOL, "BMC: (default false) coalesce rules");
|
||||
}
|
||||
|
|
|
|||
|
|
@ -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();
|
||||
|
||||
|
|
|
|||
|
|
@ -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"
|
||||
|
|
|
|||
|
|
@ -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";
|
||||
|
|
|
|||
|
|
@ -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:
|
||||
|
|
|
|||
|
|
@ -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();
|
||||
}
|
||||
|
|
@ -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
|
||||
|
|
@ -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) {
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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),
|
||||
|
|
|
|||
|
|
@ -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());
|
||||
|
|
|
|||
|
|
@ -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); }
|
||||
|
||||
|
|
|
|||
|
|
@ -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) {
|
||||
}
|
||||
|
|
|
|||
|
|
@ -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;
|
||||
|
|
|
|||
|
|
@ -26,12 +26,12 @@ Revision History:
|
|||
#undef max
|
||||
#endif
|
||||
#include"smt_params.h"
|
||||
#include"datalog_parser.h"
|
||||
#include"arith_decl_plugin.h"
|
||||
#include"dl_compiler.h"
|
||||
#include"dl_context.h"
|
||||
#include"dl_mk_filter_rules.h"
|
||||
#include"dl_finite_product_relation.h"
|
||||
#include"dl_context.h"
|
||||
#include"datalog_parser.h"
|
||||
#include"datalog_frontend.h"
|
||||
#include"timeout.h"
|
||||
|
||||
|
|
@ -71,7 +71,7 @@ static void display_statistics(
|
|||
|
||||
code.process_all_costs();
|
||||
{
|
||||
params_ref p(ctx.get_params());
|
||||
params_ref p;
|
||||
p.set_bool("output_profile", true);
|
||||
p.set_uint("profile_milliseconds_threshold", 100);
|
||||
ctx.updt_params(p);
|
||||
|
|
@ -250,7 +250,7 @@ unsigned read_datalog(char const * file) {
|
|||
TRACE("dl_compiler", ctx.display(tout);
|
||||
rules_code.display(ctx, tout););
|
||||
|
||||
if (ctx.get_params().get_bool("output_tuples", true)) {
|
||||
if (ctx.get_params().output_tuples()) {
|
||||
ctx.display_output_facts(std::cout);
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -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();
|
||||
}
|
||||
|
|
@ -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);
|
||||
|
|
|
|||
Loading…
Reference in a new issue