diff --git a/src/muz/base/dl_context.cpp b/src/muz/base/dl_context.cpp index fbef46ae3..859d4419f 100644 --- a/src/muz/base/dl_context.cpp +++ b/src/muz/base/dl_context.cpp @@ -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 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(); diff --git a/src/muz/base/fixedpoint_params.pyg b/src/muz/base/fixedpoint_params.pyg index 5bfbba6b2..d61c442d3 100644 --- a/src/muz/base/fixedpoint_params.pyg +++ b/src/muz/base/fixedpoint_params.pyg @@ -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"), )) diff --git a/src/muz/bmc/dl_bmc_engine.cpp b/src/muz/bmc/dl_bmc_engine.cpp index 51b1a5295..2ad5b3b94 100644 --- a/src/muz/bmc/dl_bmc_engine.cpp +++ b/src/muz/bmc/dl_bmc_engine.cpp @@ -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); diff --git a/src/muz/duality/duality_dl_interface.cpp b/src/muz/duality/duality_dl_interface.cpp index 0584e6b58..3f035b453 100755 --- a/src/muz/duality/duality_dl_interface.cpp +++ b/src/muz/duality/duality_dl_interface.cpp @@ -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 diff --git a/src/muz/fp/horn_tactic.cpp b/src/muz/fp/horn_tactic.cpp index 0c094c277..1e7a6e617 100644 --- a/src/muz/fp/horn_tactic.cpp +++ b/src/muz/fp/horn_tactic.cpp @@ -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); diff --git a/src/muz/pdr/pdr_context.cpp b/src/muz/pdr/pdr_context.cpp index e55806243..2ddfd1c01 100644 --- a/src/muz/pdr/pdr_context.cpp +++ b/src/muz/pdr/pdr_context.cpp @@ -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(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& model_search::cache(model_node const& n) { + obj_map >& 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 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()); } - 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 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 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 sorts; + svector 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 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 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 sorts; - svector 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"; diff --git a/src/muz/pdr/pdr_context.h b/src/muz/pdr/pdr_context.h index 8a4f3e438..63adfa1f6 100644 --- a/src/muz/pdr/pdr_context.h +++ b/src/muz/pdr/pdr_context.h @@ -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_nodes; + ast_manager& m; bool m_bfs; model_node* m_root; std::deque m_leaves; - vector > m_cache; - - obj_map& cache(model_node const& n); - void erase_children(model_node& n); + vector > m_cache; + + obj_map& 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: diff --git a/src/muz/pdr/pdr_dl_interface.cpp b/src/muz/pdr/pdr_dl_interface.cpp index 45872fe99..b75be70c1 100644 --- a/src/muz/pdr/pdr_dl_interface.cpp +++ b/src/muz/pdr/pdr_dl_interface.cpp @@ -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); diff --git a/src/muz/pdr/pdr_prop_solver.cpp b/src/muz/pdr/pdr_prop_solver.cpp index 8fe8c0e0e..06f858608 100644 --- a/src/muz/pdr/pdr_prop_solver.cpp +++ b/src/muz/pdr/pdr_prop_solver.cpp @@ -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), diff --git a/src/muz/rel/rel_context.cpp b/src/muz/rel/rel_context.cpp index 3b5e07c41..1a3d2cdae 100644 --- a/src/muz/rel/rel_context.cpp +++ b/src/muz/rel/rel_context.cpp @@ -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(m_context.get_params().dump_aig().c_ptr()); + if (m_context.get_params().print_aig().size()) { + const char *filename = static_cast(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)); } } diff --git a/src/muz/transforms/dl_mk_rule_inliner.cpp b/src/muz/transforms/dl_mk_rule_inliner.cpp index 522bd2e86..366547575 100644 --- a/src/muz/transforms/dl_mk_rule_inliner.cpp +++ b/src/muz/transforms/dl_mk_rule_inliner.cpp @@ -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 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; } diff --git a/src/muz/transforms/dl_transforms.cpp b/src/muz/transforms/dl_transforms.cpp index 80634c676..9cdc1ab01 100644 --- a/src/muz/transforms/dl_transforms.cpp +++ b/src/muz/transforms/dl_transforms.cpp @@ -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));