mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-31 11:42:28 +00:00
Code Activity

revamp configuration parameter names for fixedpoint

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2014-08-18 01:03:11 -07:00
parent f748a03ac7
commit ddbff6f77b
12 changed files with 358 additions and 246 deletions
Download patch file Download diff file Expand all files Collapse all files

54
src/muz/base/dl_context.cpp
View file

@ -272,34 +272,34 @@ namespace datalog {
bool context::generate_proof_trace() const { return m_params->generate_proof_trace(); }
bool context::output_profile() const { return m_params->output_profile(); }
bool context::output_tuples() const { return m_params->output_tuples(); }
bool context::use_map_names() const { return m_params->use_map_names(); }
bool context::fix_unbound_vars() const { return m_params->fix_unbound_vars(); }
symbol context::default_table() const { return m_params->default_table(); }
symbol context::default_relation() const { return m_params->default_relation(); } // external_relation_plugin::get_name());
symbol context::default_table_checker() const { return m_params->default_table_checker(); }
bool context::default_table_checked() const { return m_params->default_table_checked(); }
bool context::dbg_fpr_nonempty_relation_signature() const { return m_params->dbg_fpr_nonempty_relation_signature(); }
unsigned context::dl_profile_milliseconds_threshold() const { return m_params->profile_timeout_milliseconds(); }
bool context::all_or_nothing_deltas() const { return m_params->all_or_nothing_deltas(); }
bool context::compile_with_widening() const { return m_params->compile_with_widening(); }
bool context::unbound_compressor() const { return m_params->unbound_compressor(); }
bool context::similarity_compressor() const { return m_params->similarity_compressor(); }
unsigned context::similarity_compressor_threshold() const { return m_params->similarity_compressor_threshold(); }
bool context::output_profile() const { return m_params->datalog_output_profile(); }
bool context::output_tuples() const { return m_params->datalog_print_tuples(); }
bool context::use_map_names() const { return m_params->datalog_use_map_names(); }
bool context::fix_unbound_vars() const { return m_params->xform_fix_unbound_vars(); }
symbol context::default_table() const { return m_params->datalog_default_table(); }
symbol context::default_relation() const { return m_params->datalog_default_relation(); } // external_relation_plugin::get_name());
symbol context::default_table_checker() const { return m_params->datalog_default_table_checker(); }
bool context::default_table_checked() const { return m_params->datalog_default_table_checked(); }
bool context::dbg_fpr_nonempty_relation_signature() const { return m_params->datalog_dbg_fpr_nonempty_relation_signature(); }
unsigned context::dl_profile_milliseconds_threshold() const { return m_params->datalog_profile_timeout_milliseconds(); }
bool context::all_or_nothing_deltas() const { return m_params->datalog_all_or_nothing_deltas(); }
bool context::compile_with_widening() const { return m_params->datalog_compile_with_widening(); }
bool context::unbound_compressor() const { return m_params->datalog_unbound_compressor(); }
bool context::similarity_compressor() const { return m_params->datalog_similarity_compressor(); }
unsigned context::similarity_compressor_threshold() const { return m_params->datalog_similarity_compressor_threshold(); }
unsigned context::soft_timeout() const { return m_fparams.m_soft_timeout; }
unsigned context::initial_restart_timeout() const { return m_params->initial_restart_timeout(); }
bool context::generate_explanations() const { return m_params->generate_explanations(); }
bool context::explanations_on_relation_level() const { return m_params->explanations_on_relation_level(); }
bool context::magic_sets_for_queries() const { return m_params->magic_sets_for_queries(); }
bool context::eager_emptiness_checking() const { return m_params->eager_emptiness_checking(); }
unsigned context::initial_restart_timeout() const { return m_params->datalog_initial_restart_timeout(); }
bool context::generate_explanations() const { return m_params->datalog_generate_explanations(); }
bool context::explanations_on_relation_level() const { return m_params->datalog_explanations_on_relation_level(); }
bool context::magic_sets_for_queries() const { return m_params->datalog_magic_sets_for_queries(); }
bool context::eager_emptiness_checking() const { return m_params->datalog_eager_emptiness_checking(); }
bool context::bit_blast() const { return m_params->bit_blast(); }
bool context::karr() const { return m_params->karr(); }
bool context::scale() const { return m_params->scale(); }
bool context::magic() const { return m_params->magic(); }
bool context::quantify_arrays() const { return m_params->quantify_arrays(); }
bool context::instantiate_quantifiers() const { return m_params->instantiate_quantifiers(); }
bool context::bit_blast() const { return m_params->xform_bit_blast(); }
bool context::karr() const { return m_params->xform_karr(); }
bool context::scale() const { return m_params->xform_scale(); }
bool context::magic() const { return m_params->xform_magic(); }
bool context::quantify_arrays() const { return m_params->xform_quantify_arrays(); }
bool context::instantiate_quantifiers() const { return m_params->xform_instantiate_quantifiers(); }
void context::register_finite_sort(sort * s, sort_kind k) {
@ -1153,7 +1153,7 @@ namespace datalog {
expr_ref fml(m);
expr_ref_vector rules(m);
svector<symbol> names;
bool use_fixedpoint_extensions = m_params->print_with_fixedpoint_extensions();
bool use_fixedpoint_extensions = m_params->print_fixedpoint_extensions();
bool print_low_level = m_params->print_low_level_smt2();
bool do_declare_vars = m_params->print_with_variable_declarations();

217
src/muz/base/fixedpoint_params.pyg
View file

@ -2,82 +2,147 @@ 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"),
('magic', BOOL, False, "perform symbolic magic set transformation"),
('scale', BOOL, False, "add scaling variable to linear real arithemtic clauses"),
('unbound_compressor', BOOL, True, "auxiliary relations will be introduced to avoid unbound variables in rule heads"),
('similarity_compressor', BOOL, True, "(DATALOG) rules that differ only in values of constants will be merged into a single rule"),
('similarity_compressor_threshold', UINT, 11, "(DATALOG) if similarity_compressor is on, this value determines how many similar rules there must be in order for them to be merged"),
('all_or_nothing_deltas', BOOL, False, "(DATALOG) compile rules so that it is enough for the delta relation in union and widening operations to determine only whether the updated relation was modified or not"),
('compile_with_widening', BOOL, False, "(DATALOG) widening will be used to compile recursive rules"),
('eager_emptiness_checking', BOOL, True, "(DATALOG) emptiness of affected relations will be checked after each instruction, so that we may ommit unnecessary instructions"),
('default_table_checked', BOOL, False, "if true, the detault table will be default_table inside a wrapper that checks that its results are the same as of default_table_checker table"),
('default_table_checker', SYMBOL, 'null', "see default_table_checked"),
('initial_restart_timeout', UINT, 0, "length of saturation run before the first restart (in ms), zero means no restarts"),
('output_profile', BOOL, False, "determines whether profile informations should be output when outputting Datalog rules or instructions"),
('inline_linear', BOOL, True, "try linear inlining method"),
('inline_eager', BOOL, True, "try eager inlining of rules"),
('inline_linear_branch', BOOL, False, "try linear inlining method with potential expansion"),
('fix_unbound_vars', BOOL, False, "fix unbound variables in tail"),
('output_tuples', BOOL, True, "determines whether tuples for output predicates should be output"),
('print_with_fixedpoint_extensions', BOOL, True, "use SMT-LIB2 fixedpoint extensions, instead of pure SMT2, when printing rules"),
('print_low_level_smt2', BOOL, False, "use (faster) low-level SMT2 printer (the printer is scalable but the result may not be as readable)"),
('print_with_variable_declarations', BOOL, True, "use variable declarations when displaying rules (instead of attempting to use original names)"),
('bfs_model_search', BOOL, True, "PDR: use BFS strategy for expanding model search"),
('use_farkas', BOOL, True, "PDR: use lemma generator based on Farkas (for linear real arithmetic)"),
('generate_proof_trace', BOOL, False, "PDR: trace for 'sat' answer as proof object"),
('flexible_trace', BOOL, False, "PDR: allow PDR generate long counter-examples "
"by extending candidate trace within search area"),
('unfold_rules', UINT, 0, "PDR: unfold rules statically using iterative squarring"),
('use_model_generalizer', BOOL, False, "PDR: use model for backwards propagation (instead of symbolic simulation)"),
('validate_result', BOOL, False, "PDR validate result (by proof checking or model checking)"),
('simplify_formulas_pre', BOOL, False, "PDR: simplify derived formulas before inductive propagation"),
('simplify_formulas_post', BOOL, False, "PDR: simplify derived formulas after inductive propagation"),
('slice', BOOL, True, "PDR: simplify clause set using slicing"),
('karr', BOOL, False, "Add linear invariants to clauses using Karr's method"),
('quantify_arrays', BOOL, False, "create quantified Horn clauses from clauses with arrays"),
('instantiate_quantifiers', BOOL, False, "instantiate quantified Horn clauses using E-matching heuristic"),
('coalesce_rules', BOOL, False, "BMC: coalesce rules"),
('use_multicore_generalizer', BOOL, False, "PDR: extract multiple cores for blocking states"),
('use_inductive_generalizer', BOOL, True, "PDR: generalize lemmas using induction strengthening"),
('use_arith_inductive_generalizer', BOOL, False, "PDR: generalize lemmas using arithmetic heuristics for induction strengthening"),
('use_convex_closure_generalizer', BOOL, False, "PDR: generalize using convex closures of lemmas"),
('use_convex_interior_generalizer', BOOL, False, "PDR: generalize using convex interiors of lemmas"),
('cache_mode', UINT, 0, "PDR: use no (0), symbolic (1) or explicit cache (2) for model search"),
('inductive_reachability_check', BOOL, False, "PDR: assume negation of the cube on the previous level when "
"checking for reachability (not only during cube weakening)"),
('max_num_contexts', UINT, 500, "PDR: maximal number of contexts to create"),
('try_minimize_core', BOOL, False, "PDR: try to reduce core size (before inductive minimization)"),
('profile_timeout_milliseconds', UINT, 0, "instructions and rules that took less than the threshold will not be printed when printed the instruction/rule list"),
('dbg_fpr_nonempty_relation_signature', BOOL, False,
"if true, finite_product_relation will attempt to avoid creating inner relation with empty signature "
"by putting in half of the table columns, if it would have been empty otherwise"),
('print_answer', BOOL, False, 'print answer instance(s) to query'),
('print_certificate', BOOL, False, 'print certificate for reachability or non-reachability'),
('print_boogie_certificate', BOOL, False, 'print certificate for reachability or non-reachability using a format understood by Boogie'),
('print_statistics', BOOL, False, 'print statistics'),
('use_utvpi', BOOL, True, 'PDR: Enable UTVPI strategy'),
('tab_selection', SYMBOL, 'weight', 'selection method for tabular strategy: weight (default), first, var-use'),
('full_expand', BOOL, False, 'DUALITY: Fully expand derivation trees'),
('no_conj', BOOL, False, 'DUALITY: No forced covering (conjectures)'),
('feasible_edges', BOOL, True, 'DUALITY: Don\'t expand definitley infeasible edges'),
('use_underapprox', BOOL, False, 'DUALITY: Use underapproximations'),
('stratified_inlining', BOOL, False, 'DUALITY: Use stratified inlining'),
('recursion_bound', UINT, UINT_MAX, 'DUALITY: Recursion bound for stratified inlining'),
('profile', BOOL, False, 'DUALITY: profile run time'),
('mbqi', BOOL, True, 'DUALITY: use model-based quantifier instantion'),
('batch_expand', BOOL, False, 'DUALITY: use batch expansion'),
('dump_aig', SYMBOL, '', 'Dump clauses in AIG text format (AAG) to the given file name'),
('conjecture_file', STRING, '', 'DUALITY: save conjectures to file'),
('engine', SYMBOL, 'auto-config',
'Select: auto-config, datalog, duality, pdr, bmc'),
('datalog.default_table', SYMBOL, 'sparse',
'default table implementation: sparse, hashtable, bitvector, interval'),
('datalog.default_relation', SYMBOL, 'pentagon',
'default relation implementation: external_relation, pentagon'),
('datalog.generate_explanations', BOOL, False,
'produce explanations for produced facts when using the datalog engine'),
('datalog.use_map_names', BOOL, True,
"use names from map files when displaying tuples"),
('datalog.magic_sets_for_queries', BOOL, False,
"magic set transformation will be used for queries"),
('datalog.explanations_on_relation_level', BOOL, False,
'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)'),
('datalog.unbound_compressor', BOOL, True,
"auxiliary relations will be introduced to avoid unbound variables " +
"in rule heads"),
('datalog.similarity_compressor', BOOL, True,
"rules that differ only in values of constants will be merged into " +
"a single rule"),
('datalog.similarity_compressor_threshold', UINT, 11,
"if similarity_compressor is on, this value determines how many " +
"similar rules there must be in order for them to be merged"),
('datalog.all_or_nothing_deltas', BOOL, False,
"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"),
('datalog.compile_with_widening', BOOL, False,
"widening will be used to compile recursive rules"),
('datalog.eager_emptiness_checking', BOOL, True,
"emptiness of affected relations will be checked after each instruction, " +
"so that we may ommit unnecessary instructions"),
('datalog.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'),
('datalog.default_table_checker', SYMBOL, 'null', "see default_table_checked"),
('datalog.initial_restart_timeout', UINT, 0,
"length of saturation run before the first restart (in ms), " +
"zero means no restarts"),
('datalog.output_profile', BOOL, False,
"determines whether profile information should be " +
"output when outputting Datalog rules or instructions"),
('datalog.print.tuples', BOOL, True,
"determines whether tuples for output predicates should be output"),
('datalog.profile_timeout_milliseconds', UINT, 0,
"instructions and rules that took less than the threshold " +
"will not be printed when printed the instruction/rule list"),
('datalog.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"),
('duality.full_expand', BOOL, False, 'Fully expand derivation trees'),
('duality.no_conj', BOOL, False, 'No forced covering (conjectures)'),
('duality.feasible_edges', BOOL, True,
'Don\'t expand definitley infeasible edges'),
('duality.use_underapprox', BOOL, False, 'Use underapproximations'),
('duality.stratified_inlining', BOOL, False, 'Use stratified inlining'),
('duality.recursion_bound', UINT, UINT_MAX,
'Recursion bound for stratified inlining'),
('duality.profile', BOOL, False, 'profile run time'),
('duality.mbqi', BOOL, True, 'use model-based quantifier instantion'),
('duality.batch_expand', BOOL, False, 'use batch expansion'),
('duality.conjecture_file', STRING, '', 'save conjectures to file'),
('pdr.bfs_model_search', BOOL, True,
"use BFS strategy for expanding model search"),
('pdr.farkas', BOOL, True,
"use lemma generator based on Farkas (for linear real arithmetic)"),
('generate_proof_trace', BOOL, False, "trace for 'sat' answer as proof object"),
('pdr.flexible_trace', BOOL, False,
"allow PDR generate long counter-examples " +
"by extending candidate trace within search area"),
('pdr.use_model_generalizer', BOOL, False,
"use model for backwards propagation (instead of symbolic simulation)"),
('pdr.validate_result', BOOL, False,
"validate result (by proof checking or model checking)"),
('pdr.simplify_formulas_pre', BOOL, False,
"simplify derived formulas before inductive propagation"),
('pdr.simplify_formulas_post', BOOL, False,
"simplify derived formulas after inductive propagation"),
('pdr.use_multicore_generalizer', BOOL, False,
"extract multiple cores for blocking states"),
('pdr.use_inductive_generalizer', BOOL, True,
"generalize lemmas using induction strengthening"),
('pdr.use_arith_inductive_generalizer', BOOL, False,
"generalize lemmas using arithmetic heuristics for induction strengthening"),
('pdr.use_convex_closure_generalizer', BOOL, False,
"generalize using convex closures of lemmas"),
('pdr.use_convex_interior_generalizer', BOOL, False,
"generalize using convex interiors of lemmas"),
('pdr.cache_mode', UINT, 0, "use no (0), symbolic (1) or explicit " +
"cache (2) for model search"),
('pdr.inductive_reachability_check', BOOL, False,
"assume negation of the cube on the previous level when " +
"checking for reachability (not only during cube weakening)"),
('pdr.max_num_contexts', UINT, 500, "maximal number of contexts to create"),
('pdr.try_minimize_core', BOOL, False,
"try to reduce core size (before inductive minimization)"),
('pdr.utvpi', BOOL, True, 'Enable UTVPI strategy'),
('print.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)"),
('print.answer', BOOL, False, 'print answer instance(s) to query'),
('print.certificate', BOOL, False,
'print certificate for reachability or non-reachability'),
('print.boogie_certificate', BOOL, False,
'print certificate for reachability or non-reachability using a ' +
'format understood by Boogie'),
('print.statistics', BOOL, False, 'print statistics'),
('print.aig', SYMBOL, '',
'Dump clauses in AIG text format (AAG) to the given file name'),
('tab.selection', SYMBOL, 'weight',
'selection method for tabular strategy: weight (default), first, var-use'),
('xform.bit_blast', BOOL, False,
'bit-blast bit-vectors'),
('xform.magic', BOOL, False,
"perform symbolic magic set transformation"),
('xform.scale', BOOL, False,
"add scaling variable to linear real arithemtic clauses"),
('xform.inline_linear', BOOL, True, "try linear inlining method"),
('xform.inline_eager', BOOL, True, "try eager inlining of rules"),
('xform.inline_linear_branch', BOOL, False,
"try linear inlining method with potential expansion"),
('xform.fix_unbound_vars', BOOL, False, "fix unbound variables in tail"),
('xform.unfold_rules', UINT, 0,
"unfold rules statically using iterative squarring"),
('xform.slice', BOOL, True, "simplify clause set using slicing"),
('xform.karr', BOOL, False,
"Add linear invariants to clauses using Karr's method"),
('xform.quantify_arrays', BOOL, False,
"create quantified Horn clauses from clauses with arrays"),
('xform.instantiate_quantifiers', BOOL, False,
"instantiate quantified Horn clauses using E-matching heuristic"),
('xform.coalesce_rules', BOOL, False, "coalesce rules"),
))

2
src/muz/bmc/dl_bmc_engine.cpp
View file

@ -1442,7 +1442,7 @@ namespace datalog {
expr_ref bg_assertion = m_ctx.get_background_assertion();
apply_default_transformation(m_ctx);
if (m_ctx.get_params().slice()) {
if (m_ctx.get_params().xform_slice()) {
datalog::rule_transformer transformer(m_ctx);
datalog::mk_slice* slice = alloc(datalog::mk_slice, m_ctx);
transformer.register_plugin(slice);

20
src/muz/duality/duality_dl_interface.cpp
View file

@ -146,7 +146,7 @@ lbool dl_interface::query(::expr * query) {
// make a new problem and solver
_d = alloc(duality_data,m_ctx.get_manager());
_d->ctx.set("mbqi",m_ctx.get_params().mbqi());
_d->ctx.set("mbqi",m_ctx.get_params().duality_mbqi());
_d->ls = alloc(RPFP::iZ3LogicSolver,_d->ctx);
_d->rpfp = alloc(RPFP,_d->ls);
@ -223,14 +223,14 @@ lbool dl_interface::query(::expr * query) {
// set its options
IF_VERBOSE(1, rs->SetOption("report","1"););
rs->SetOption("full_expand",m_ctx.get_params().full_expand() ? "1" : "0");
rs->SetOption("no_conj",m_ctx.get_params().no_conj() ? "1" : "0");
rs->SetOption("feasible_edges",m_ctx.get_params().feasible_edges() ? "1" : "0");
rs->SetOption("use_underapprox",m_ctx.get_params().use_underapprox() ? "1" : "0");
rs->SetOption("stratified_inlining",m_ctx.get_params().stratified_inlining() ? "1" : "0");
rs->SetOption("batch_expand",m_ctx.get_params().batch_expand() ? "1" : "0");
rs->SetOption("conjecture_file",m_ctx.get_params().conjecture_file());
unsigned rb = m_ctx.get_params().recursion_bound();
rs->SetOption("full_expand",m_ctx.get_params().duality_full_expand() ? "1" : "0");
rs->SetOption("no_conj",m_ctx.get_params().duality_no_conj() ? "1" : "0");
rs->SetOption("feasible_edges",m_ctx.get_params().duality_feasible_edges() ? "1" : "0");
rs->SetOption("use_underapprox",m_ctx.get_params().duality_use_underapprox() ? "1" : "0");
rs->SetOption("stratified_inlining",m_ctx.get_params().duality_stratified_inlining() ? "1" : "0");
rs->SetOption("batch_expand",m_ctx.get_params().duality_batch_expand() ? "1" : "0");
rs->SetOption("conjecture_file",m_ctx.get_params().duality_conjecture_file());
unsigned rb = m_ctx.get_params().duality_recursion_bound();
if(rb != UINT_MAX){
std::ostringstream os; os << rb;
rs->SetOption("recursion_bound", os.str());
@ -250,7 +250,7 @@ lbool dl_interface::query(::expr * query) {
// profile!
if(m_ctx.get_params().profile())
if(m_ctx.get_params().duality_profile())
print_profile(std::cout);
// save the result and counterexample if there is one

2
src/muz/fp/horn_tactic.cpp
View file

@ -316,7 +316,7 @@ class horn_tactic : public tactic {
m_ctx.get_rules(); // flush adding rules.
apply_default_transformation(m_ctx);
if (m_ctx.get_params().slice()) {
if (m_ctx.get_params().xform_slice()) {
datalog::rule_transformer transformer(m_ctx);
datalog::mk_slice* slice = alloc(datalog::mk_slice, m_ctx);
transformer.register_plugin(slice);

258
src/muz/pdr/pdr_context.cpp
View file

@ -81,7 +81,7 @@ namespace pdr {
ctx(ctx), m_head(head, m),
m_sig(m), m_solver(pm, ctx.get_params(), head->get_name()),
m_invariants(m), m_transition(m), m_initial_state(m),
m_reachable(pm, (datalog::PDR_CACHE_MODE)ctx.get_params().cache_mode()) {}
m_reachable(pm, (datalog::PDR_CACHE_MODE)ctx.get_params().pdr_cache_mode()) {}
pred_transformer::~pred_transformer() {
rule2inst::iterator it2 = m_rule2inst.begin(), end2 = m_rule2inst.end();
@ -738,6 +738,11 @@ namespace pdr {
m_closed = true;
}
void model_node::reopen() {
SASSERT(m_closed);
m_closed = false;
}
static bool is_ini(datalog::rule const& r) {
return r.get_uninterpreted_tail_size() == 0;
}
@ -747,6 +752,7 @@ namespace pdr {
return const_cast<datalog::rule*>(m_rule);
}
// only initial states are not set by the PDR search.
SASSERT(m_model.get());
datalog::rule const& rl1 = pt().find_rule(*m_model);
if (is_ini(rl1)) {
set_rule(&rl1);
@ -866,9 +872,10 @@ namespace pdr {
}
void model_search::add_leaf(model_node& n) {
unsigned& count = cache(n).insert_if_not_there2(n.state(), 0)->get_data().m_value;
++count;
if (count == 1 || is_repeated(n)) {
model_nodes ns;
model_nodes& nodes = cache(n).insert_if_not_there2(n.state(), ns)->get_data().m_value;
nodes.push_back(&n);
if (nodes.size() == 1 || is_repeated(n)) {
set_leaf(n);
}
else {
@ -877,7 +884,7 @@ namespace pdr {
}
void model_search::set_leaf(model_node& n) {
erase_children(n);
erase_children(n, true);
SASSERT(n.is_open());
enqueue_leaf(n);
}
@ -899,7 +906,7 @@ namespace pdr {
set_leaf(*root);
}
obj_map<expr, unsigned>& model_search::cache(model_node const& n) {
obj_map<expr, ptr_vector<model_node> >& model_search::cache(model_node const& n) {
unsigned l = n.orig_level();
if (l >= m_cache.size()) {
m_cache.resize(l + 1);
@ -907,7 +914,7 @@ namespace pdr {
return m_cache[l];
}
void model_search::erase_children(model_node& n) {
void model_search::erase_children(model_node& n, bool backtrack) {
ptr_vector<model_node> todo, nodes;
todo.append(n.children());
erase_leaf(n);
@ -918,13 +925,20 @@ namespace pdr {
nodes.push_back(m);
todo.append(m->children());
erase_leaf(*m);
remove_node(*m);
remove_node(*m, backtrack);
}
std::for_each(nodes.begin(), nodes.end(), delete_proc<model_node>());
}
void model_search::remove_node(model_node& n) {
if (0 == --cache(n).find(n.state())) {
void model_search::remove_node(model_node& n, bool backtrack) {
model_nodes& nodes = cache(n).find(n.state());
nodes.erase(&n);
if (nodes.size() > 0 && n.is_open() && backtrack) {
for (unsigned i = 0; i < nodes.size(); ++i) {
nodes[i]->reopen();
}
}
if (nodes.empty()) {
cache(n).remove(n.state());
}
}
@ -971,6 +985,9 @@ namespace pdr {
if (n->get_model_ptr()) {
models.insert(n->state(), n->get_model_ptr());
rules.insert(n->state(), n->get_rule());
pred_transformer& pt = n->pt();
context& ctx = pt.get_context();
datalog::context& dctx = ctx.get_context();
}
todo.pop_back();
todo.append(n->children().size(), n->children().c_ptr());
@ -981,12 +998,18 @@ namespace pdr {
model_node* n = todo.back();
model* md = 0;
ast_manager& m = n->pt().get_manager();
if (!n->get_model_ptr() && models.find(n->state(), md)) {
TRACE("pdr", tout << mk_pp(n->state(), m) << "\n";);
model_ref mr(md);
n->set_model(mr);
datalog::rule const* rule = rules.find(n->state());
n->set_rule(rule);
if (!n->get_model_ptr()) {
if (models.find(n->state(), md)) {
TRACE("pdr", tout << mk_pp(n->state(), m) << "\n";);
model_ref mr(md);
n->set_model(mr);
datalog::rule const* rule = rules.find(n->state());
n->set_rule(rule);
}
else {
IF_VERBOSE(1, n->display(verbose_stream() << "no model:\n", 0);
verbose_stream() << mk_pp(n->state(), m) << "\n";);
}
}
todo.pop_back();
todo.append(n->children().size(), n->children().c_ptr());
@ -1205,8 +1228,8 @@ namespace pdr {
void model_search::reset() {
if (m_root) {
erase_children(*m_root);
remove_node(*m_root);
erase_children(*m_root, false);
remove_node(*m_root, false);
dealloc(m_root);
m_root = 0;
}
@ -1239,10 +1262,10 @@ namespace pdr {
m_params(params),
m(m),
m_context(0),
m_pm(m_fparams, params.max_num_contexts(), m),
m_pm(m_fparams, params.pdr_max_num_contexts(), m),
m_query_pred(m),
m_query(0),
m_search(m_params.bfs_model_search()),
m_search(m_params.pdr_bfs_model_search(), m),
m_last_result(l_undef),
m_inductive_lvl(0),
m_expanded_lvl(0),
@ -1470,93 +1493,108 @@ namespace pdr {
}
}
};
void context::validate() {
if (!m_params.validate_result()) {
return;
}
void context::validate_proof() {
std::stringstream msg;
switch(m_last_result) {
case l_true: {
proof_ref pr = get_proof();
proof_checker checker(m);
expr_ref_vector side_conditions(m);
bool ok = checker.check(pr, side_conditions);
if (!ok) {
msg << "proof validation failed";
proof_ref pr = get_proof();
proof_checker checker(m);
expr_ref_vector side_conditions(m);
bool ok = checker.check(pr, side_conditions);
if (!ok) {
msg << "proof validation failed";
IF_VERBOSE(0, verbose_stream() << msg.str() << "\n";);
throw default_exception(msg.str());
}
for (unsigned i = 0; i < side_conditions.size(); ++i) {
expr* cond = side_conditions[i].get();
expr_ref tmp(m);
tmp = m.mk_not(cond);
IF_VERBOSE(2, verbose_stream() << "checking side-condition:\n" << mk_pp(cond, m) << "\n";);
smt::kernel solver(m, get_fparams());
solver.assert_expr(tmp);
lbool res = solver.check();
if (res != l_false) {
msg << "rule validation failed when checking: " << mk_pp(cond, m);
IF_VERBOSE(0, verbose_stream() << msg.str() << "\n";);
throw default_exception(msg.str());
}
for (unsigned i = 0; i < side_conditions.size(); ++i) {
expr* cond = side_conditions[i].get();
expr_ref tmp(m);
tmp = m.mk_not(cond);
IF_VERBOSE(2, verbose_stream() << "checking side-condition:\n" << mk_pp(cond, m) << "\n";);
}
}
}
void context::validate_search() {
expr_ref tr = m_search.get_trace(*this);
// TBD: tr << "\n";
}
void context::validate_model() {
std::stringstream msg;
expr_ref_vector refs(m);
expr_ref tmp(m);
model_ref model;
vector<relation_info> rs;
model_converter_ref mc;
get_level_property(m_inductive_lvl, refs, rs);
inductive_property ex(m, mc, rs);
ex.to_model(model);
decl2rel::iterator it = m_rels.begin(), end = m_rels.end();
var_subst vs(m, false);
for (; it != end; ++it) {
ptr_vector<datalog::rule> const& rules = it->m_value->rules();
for (unsigned i = 0; i < rules.size(); ++i) {
datalog::rule& r = *rules[i];
model->eval(r.get_head(), tmp);
expr_ref_vector fmls(m);
fmls.push_back(m.mk_not(tmp));
unsigned utsz = r.get_uninterpreted_tail_size();
unsigned tsz = r.get_tail_size();
for (unsigned j = 0; j < utsz; ++j) {
model->eval(r.get_tail(j), tmp);
fmls.push_back(tmp);
}
for (unsigned j = utsz; j < tsz; ++j) {
fmls.push_back(r.get_tail(j));
}
tmp = m.mk_and(fmls.size(), fmls.c_ptr());
ptr_vector<sort> sorts;
svector<symbol> names;
get_free_vars(tmp, sorts);
for (unsigned i = 0; i < sorts.size(); ++i) {
if (!sorts[i]) {
sorts[i] = m.mk_bool_sort();
}
names.push_back(symbol(i));
}
sorts.reverse();
if (!sorts.empty()) {
tmp = m.mk_exists(sorts.size(), sorts.c_ptr(), names.c_ptr(), tmp);
}
smt::kernel solver(m, get_fparams());
solver.assert_expr(tmp);
lbool res = solver.check();
if (res != l_false) {
msg << "rule validation failed when checking: " << mk_pp(cond, m);
msg << "rule validation failed when checking: " << mk_pp(tmp, m);
IF_VERBOSE(0, verbose_stream() << msg.str() << "\n";);
throw default_exception(msg.str());
}
}
break;
}
case l_false: {
expr_ref_vector refs(m);
expr_ref tmp(m);
model_ref model;
vector<relation_info> rs;
model_converter_ref mc;
get_level_property(m_inductive_lvl, refs, rs);
inductive_property ex(m, mc, rs);
ex.to_model(model);
decl2rel::iterator it = m_rels.begin(), end = m_rels.end();
var_subst vs(m, false);
for (; it != end; ++it) {
ptr_vector<datalog::rule> const& rules = it->m_value->rules();
for (unsigned i = 0; i < rules.size(); ++i) {
datalog::rule& r = *rules[i];
model->eval(r.get_head(), tmp);
expr_ref_vector fmls(m);
fmls.push_back(m.mk_not(tmp));
unsigned utsz = r.get_uninterpreted_tail_size();
unsigned tsz = r.get_tail_size();
for (unsigned j = 0; j < utsz; ++j) {
model->eval(r.get_tail(j), tmp);
fmls.push_back(tmp);
}
for (unsigned j = utsz; j < tsz; ++j) {
fmls.push_back(r.get_tail(j));
}
tmp = m.mk_and(fmls.size(), fmls.c_ptr());
ptr_vector<sort> sorts;
svector<symbol> names;
get_free_vars(tmp, sorts);
for (unsigned i = 0; i < sorts.size(); ++i) {
if (!sorts[i]) {
sorts[i] = m.mk_bool_sort();
}
names.push_back(symbol(i));
}
sorts.reverse();
if (!sorts.empty()) {
tmp = m.mk_exists(sorts.size(), sorts.c_ptr(), names.c_ptr(), tmp);
}
smt::kernel solver(m, get_fparams());
solver.assert_expr(tmp);
lbool res = solver.check();
if (res != l_false) {
msg << "rule validation failed when checking: " << mk_pp(tmp, m);
IF_VERBOSE(0, verbose_stream() << msg.str() << "\n";);
throw default_exception(msg.str());
}
}
}
break;
}
}
void context::validate() {
if (!m_params.pdr_validate_result()) {
return;
}
switch(m_last_result) {
case l_true:
if (m_params.generate_proof_trace()) {
validate_proof();
}
validate_search();
break;
case l_false:
validate_model();
break;
default:
break;
}
@ -1570,7 +1608,7 @@ namespace pdr {
void context::init_core_generalizers(datalog::rule_set& rules) {
reset_core_generalizers();
classifier_proc classify(m, rules);
bool use_mc = m_params.use_multicore_generalizer();
bool use_mc = m_params.pdr_use_multicore_generalizer();
if (use_mc) {
m_core_generalizers.push_back(alloc(core_multi_generalizer, *this, 0));
}
@ -1580,9 +1618,9 @@ namespace pdr {
m_fparams.m_arith_auto_config_simplex = true;
m_fparams.m_arith_propagate_eqs = false;
m_fparams.m_arith_eager_eq_axioms = false;
if (m_params.use_utvpi() &&
!m_params.use_convex_closure_generalizer() &&
!m_params.use_convex_interior_generalizer()) {
if (m_params.pdr_utvpi() &&
!m_params.pdr_use_convex_closure_generalizer() &&
!m_params.pdr_use_convex_interior_generalizer()) {
if (classify.is_dl()) {
m_fparams.m_arith_mode = AS_DIFF_LOGIC;
m_fparams.m_arith_expand_eqs = true;
@ -1594,19 +1632,19 @@ namespace pdr {
}
}
}
if (m_params.use_convex_closure_generalizer()) {
if (m_params.pdr_use_convex_closure_generalizer()) {
m_core_generalizers.push_back(alloc(core_convex_hull_generalizer, *this, true));
}
if (m_params.use_convex_interior_generalizer()) {
if (m_params.pdr_use_convex_interior_generalizer()) {
m_core_generalizers.push_back(alloc(core_convex_hull_generalizer, *this, false));
}
if (!use_mc && m_params.use_inductive_generalizer()) {
if (!use_mc && m_params.pdr_use_inductive_generalizer()) {
m_core_generalizers.push_back(alloc(core_bool_inductive_generalizer, *this, 0));
}
if (m_params.inductive_reachability_check()) {
if (m_params.pdr_inductive_reachability_check()) {
m_core_generalizers.push_back(alloc(core_induction_generalizer, *this));
}
if (m_params.use_arith_inductive_generalizer()) {
if (m_params.pdr_use_arith_inductive_generalizer()) {
m_core_generalizers.push_back(alloc(core_arith_inductive_generalizer, *this));
}
@ -1824,7 +1862,7 @@ namespace pdr {
m_expanded_lvl = n.level();
}
pred_transformer::scoped_farkas sf (n.pt(), m_params.use_farkas());
pred_transformer::scoped_farkas sf (n.pt(), m_params.pdr_farkas());
if (n.pt().is_reachable(n.state())) {
TRACE("pdr", tout << "reachable\n";);
close_node(n);
@ -1865,7 +1903,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.flexible_trace(), n);
m_search.backtrack_level(!found_invariant && m_params.pdr_flexible_trace(), n);
break;
}
case l_undef: {
@ -1892,7 +1930,7 @@ namespace pdr {
}
void context::propagate(unsigned max_prop_lvl) {
if (m_params.simplify_formulas_pre()) {
if (m_params.pdr_simplify_formulas_pre()) {
simplify_formulas();
}
for (unsigned lvl = m_expanded_lvl; lvl <= max_prop_lvl; lvl++) {
@ -1911,7 +1949,7 @@ namespace pdr {
throw inductive_exception();
}
}
if (m_params.simplify_formulas_post()) {
if (m_params.pdr_simplify_formulas_post()) {
simplify_formulas();
}
}
@ -1959,16 +1997,18 @@ namespace pdr {
*/
void context::create_children(model_node& n) {
SASSERT(n.level() > 0);
bool use_model_generalizer = m_params.use_model_generalizer();
bool use_model_generalizer = m_params.pdr_use_model_generalizer();
scoped_no_proof _sc(m);
pred_transformer& pt = n.pt();
model_ref M = n.get_model_ptr();
SASSERT(M.get());
datalog::rule const& r = pt.find_rule(*M);
expr* T = pt.get_transition(r);
expr* phi = n.state();
n.set_rule(&r);
TRACE("pdr",
tout << "Model:\n";

21
src/muz/pdr/pdr_context.h
View file

@ -124,6 +124,7 @@ namespace pdr {
unsigned get_num_levels() { return m_levels.size(); }
expr_ref get_cover_delta(func_decl* p_orig, int level);
void add_cover(unsigned level, expr* property);
context& get_context() { return ctx; }
std::ostream& display(std::ostream& strm) const;
@ -231,6 +232,7 @@ namespace pdr {
}
void set_closed();
void reopen();
void set_pre_closed() { m_closed = true; }
void reset() { m_children.reset(); }
@ -243,19 +245,21 @@ namespace pdr {
};
class model_search {
typedef ptr_vector<model_node> model_nodes;
ast_manager& m;
bool m_bfs;
model_node* m_root;
std::deque<model_node*> m_leaves;
vector<obj_map<expr, unsigned> > m_cache;
obj_map<expr, unsigned>& cache(model_node const& n);
void erase_children(model_node& n);
vector<obj_map<expr, model_nodes > > m_cache;
obj_map<expr, model_nodes>& cache(model_node const& n);
void erase_children(model_node& n, bool backtrack);
void erase_leaf(model_node& n);
void remove_node(model_node& n);
void remove_node(model_node& n, bool backtrack);
void enqueue_leaf(model_node& n); // add leaf to priority queue.
void update_models();
public:
model_search(bool bfs): m_bfs(bfs), m_root(0) {}
model_search(bool bfs, ast_manager& m): m(m), m_bfs(bfs), m_root(0) {}
~model_search();
void reset();
@ -267,7 +271,7 @@ namespace pdr {
void set_root(model_node* n);
model_node& get_root() const { return *m_root; }
std::ostream& display(std::ostream& out) const;
expr_ref get_trace(context const& ctx);
expr_ref get_trace(context const& ctx);
proof_ref get_proof_trace(context const& ctx);
void backtrack_level(bool uses_level, model_node& n);
};
@ -355,6 +359,9 @@ namespace pdr {
void reset_core_generalizers();
void validate();
void validate_proof();
void validate_search();
void validate_model();
public:

10
src/muz/pdr/pdr_dl_interface.cpp
View file

@ -105,7 +105,7 @@ lbool dl_interface::query(expr * query) {
apply_default_transformation(m_ctx);
if (m_ctx.get_params().slice()) {
if (m_ctx.get_params().xform_slice()) {
datalog::rule_transformer transformer(m_ctx);
datalog::mk_slice* slice = alloc(datalog::mk_slice, m_ctx);
transformer.register_plugin(slice);
@ -122,12 +122,12 @@ lbool dl_interface::query(expr * query) {
}
}
if (m_ctx.get_params().unfold_rules() > 0) {
unsigned num_unfolds = m_ctx.get_params().unfold_rules();
if (m_ctx.get_params().xform_unfold_rules() > 0) {
unsigned num_unfolds = m_ctx.get_params().xform_unfold_rules();
datalog::rule_transformer transf1(m_ctx), transf2(m_ctx);
transf1.register_plugin(alloc(datalog::mk_coalesce, m_ctx));
transf2.register_plugin(alloc(datalog::mk_unfold, m_ctx));
if (m_ctx.get_params().coalesce_rules()) {
if (m_ctx.get_params().xform_coalesce_rules()) {
m_ctx.transform_rules(transf1);
}
while (num_unfolds > 0) {
@ -176,7 +176,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().slice()) {
if (m_ctx.get_params().xform_slice()) {
throw default_exception("Covers are incompatible with slicing. Disable slicing before using covers");
}
m_context->add_cover(level, pred, property);

2
src/muz/pdr/pdr_prop_solver.cpp
View file

@ -231,7 +231,7 @@ namespace pdr {
m(pm.get_manager()),
m_pm(pm),
m_name(name),
m_try_minimize_core(p.try_minimize_core()),
m_try_minimize_core(p.pdr_try_minimize_core()),
m_ctx(pm.mk_fresh()),
m_pos_level_atoms(m),
m_neg_level_atoms(m),

8
src/muz/rel/rel_context.cpp
View file

@ -150,8 +150,8 @@ namespace datalog {
}
TRACE("dl", m_context.display(tout););
if (m_context.get_params().dump_aig().size()) {
const char *filename = static_cast<const char*>(m_context.get_params().dump_aig().c_ptr());
if (m_context.get_params().print_aig().size()) {
const char *filename = static_cast<const char*>(m_context.get_params().print_aig().c_ptr());
aig_exporter aig(m_context.get_rules(), get_context(), &m_table_facts);
std::ofstream strm(filename, std::ios_base::binary);
aig(strm);
@ -284,7 +284,7 @@ namespace datalog {
transf.register_plugin(alloc(mk_interp_tail_simplifier, m_context));
transf.register_plugin(alloc(mk_separate_negated_tails, m_context));
if (m_context.get_params().bit_blast()) {
if (m_context.get_params().xform_bit_blast()) {
transf.register_plugin(alloc(mk_bit_blast, m_context, 22000));
transf.register_plugin(alloc(mk_interp_tail_simplifier, m_context, 21000));
}
@ -518,7 +518,7 @@ namespace datalog {
void rel_context::add_fact(func_decl* pred, relation_fact const& fact) {
get_rmanager().reset_saturated_marks();
get_relation(pred).add_fact(fact);
if (m_context.get_params().dump_aig().size()) {
if (m_context.get_params().print_aig().size()) {
m_table_facts.push_back(std::make_pair(pred, fact));
}
}

6
src/muz/transforms/dl_mk_rule_inliner.cpp
View file

@ -754,7 +754,7 @@ namespace datalog {
valid.reset();
valid.resize(sz, true);
bool allow_branching = m_context.get_params().inline_linear_branch();
bool allow_branching = m_context.get_params().xform_inline_linear_branch();
for (unsigned i = 0; i < sz; ++i) {
@ -866,7 +866,7 @@ namespace datalog {
scoped_ptr<rule_set> res = alloc(rule_set, m_context);
if (m_context.get_params().inline_eager()) {
if (m_context.get_params().xform_inline_eager()) {
TRACE("dl", source.display(tout << "before eager inlining\n"););
plan_inlining(source);
something_done = transform_rules(source, *res);
@ -884,7 +884,7 @@ namespace datalog {
res = alloc(rule_set, source);
}
if (m_context.get_params().inline_linear() && inline_linear(res)) {
if (m_context.get_params().xform_inline_linear() && inline_linear(res)) {
something_done = true;
}

4
src/muz/transforms/dl_transforms.cpp
View file

@ -44,12 +44,12 @@ namespace datalog {
transf.register_plugin(alloc(datalog::mk_coi_filter, ctx));
transf.register_plugin(alloc(datalog::mk_interp_tail_simplifier, ctx));
if (ctx.get_params().quantify_arrays()) {
if (ctx.get_params().xform_quantify_arrays()) {
transf.register_plugin(alloc(datalog::mk_quantifier_abstraction, ctx, 38000));
}
transf.register_plugin(alloc(datalog::mk_quantifier_instantiation, ctx, 37000));
transf.register_plugin(alloc(datalog::mk_scale, ctx, 36030));
if (ctx.get_params().magic()) {
if (ctx.get_params().xform_magic()) {
transf.register_plugin(alloc(datalog::mk_magic_symbolic, ctx, 36020));
}
transf.register_plugin(alloc(datalog::mk_karr_invariants, ctx, 36010));