From 6adaed718f52a5f8a8d819453f6dcff91402e43d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 6 Jun 2018 13:11:48 -0700 Subject: [PATCH] remove pdr Signed-off-by: Nikolaj Bjorner --- src/CMakeLists.txt | 1 - src/muz/base/dl_context.cpp | 31 +- src/muz/base/dl_engine_base.h | 2 - src/muz/base/fixedpoint_params.pyg | 132 +- src/muz/fp/CMakeLists.txt | 1 - src/muz/fp/dl_register_engine.cpp | 4 - src/muz/pdr/CMakeLists.txt | 20 - src/muz/pdr/pdr_closure.cpp | 177 -- src/muz/pdr/pdr_closure.h | 67 - src/muz/pdr/pdr_context.cpp | 2431 ----------------------- src/muz/pdr/pdr_context.h | 448 ----- src/muz/pdr/pdr_dl_interface.cpp | 225 --- src/muz/pdr/pdr_dl_interface.h | 78 - src/muz/pdr/pdr_farkas_learner.cpp | 1012 ---------- src/muz/pdr/pdr_farkas_learner.h | 128 -- src/muz/pdr/pdr_generalizers.cpp | 777 -------- src/muz/pdr/pdr_generalizers.h | 110 - src/muz/pdr/pdr_manager.cpp | 321 --- src/muz/pdr/pdr_manager.h | 304 --- src/muz/pdr/pdr_prop_solver.cpp | 459 ----- src/muz/pdr/pdr_prop_solver.h | 139 -- src/muz/pdr/pdr_reachable_cache.cpp | 132 -- src/muz/pdr/pdr_reachable_cache.h | 66 - src/muz/pdr/pdr_smt_context_manager.cpp | 167 -- src/muz/pdr/pdr_smt_context_manager.h | 92 - src/muz/pdr/pdr_sym_mux.cpp | 601 ------ src/muz/pdr/pdr_sym_mux.h | 247 --- src/muz/pdr/pdr_util.cpp | 508 ----- src/muz/pdr/pdr_util.h | 81 - 29 files changed, 70 insertions(+), 8691 deletions(-) delete mode 100644 src/muz/pdr/CMakeLists.txt delete mode 100644 src/muz/pdr/pdr_closure.cpp delete mode 100644 src/muz/pdr/pdr_closure.h delete mode 100644 src/muz/pdr/pdr_context.cpp delete mode 100644 src/muz/pdr/pdr_context.h delete mode 100644 src/muz/pdr/pdr_dl_interface.cpp delete mode 100644 src/muz/pdr/pdr_dl_interface.h delete mode 100644 src/muz/pdr/pdr_farkas_learner.cpp delete mode 100644 src/muz/pdr/pdr_farkas_learner.h delete mode 100644 src/muz/pdr/pdr_generalizers.cpp delete mode 100644 src/muz/pdr/pdr_generalizers.h delete mode 100644 src/muz/pdr/pdr_manager.cpp delete mode 100644 src/muz/pdr/pdr_manager.h delete mode 100644 src/muz/pdr/pdr_prop_solver.cpp delete mode 100644 src/muz/pdr/pdr_prop_solver.h delete mode 100644 src/muz/pdr/pdr_reachable_cache.cpp delete mode 100644 src/muz/pdr/pdr_reachable_cache.h delete mode 100644 src/muz/pdr/pdr_smt_context_manager.cpp delete mode 100644 src/muz/pdr/pdr_smt_context_manager.h delete mode 100644 src/muz/pdr/pdr_sym_mux.cpp delete mode 100644 src/muz/pdr/pdr_sym_mux.h delete mode 100644 src/muz/pdr/pdr_util.cpp delete mode 100644 src/muz/pdr/pdr_util.h diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 9020c9e4b..7dee4039a 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -81,7 +81,6 @@ add_subdirectory(muz/base) add_subdirectory(muz/dataflow) add_subdirectory(muz/transforms) add_subdirectory(muz/rel) -add_subdirectory(muz/pdr) add_subdirectory(muz/clp) add_subdirectory(muz/tab) add_subdirectory(muz/bmc) diff --git a/src/muz/base/dl_context.cpp b/src/muz/base/dl_context.cpp index cc14de5ce..2b0987be7 100644 --- a/src/muz/base/dl_context.cpp +++ b/src/muz/base/dl_context.cpp @@ -188,9 +188,7 @@ namespace datalog { if (m_trail.get_num_scopes() == 0) { throw default_exception("there are no backtracking points to pop to"); } - if (m_engine.get()) { - throw default_exception("pop operation is only supported by duality engine"); - } + throw default_exception("pop operation is not supported"); m_trail.pop_scope(1); } @@ -576,17 +574,11 @@ namespace datalog { m_rule_properties.check_infinite_sorts(); break; case SPACER_ENGINE: - case PDR_ENGINE: m_rule_properties.collect(r); m_rule_properties.check_existential_tail(); m_rule_properties.check_for_negated_predicates(); m_rule_properties.check_uninterpreted_free(); break; - case QPDR_ENGINE: - m_rule_properties.collect(r); - m_rule_properties.check_for_negated_predicates(); - m_rule_properties.check_uninterpreted_free(); - break; case BMC_ENGINE: m_rule_properties.collect(r); m_rule_properties.check_for_negated_predicates(); @@ -776,19 +768,14 @@ namespace datalog { DL_ENGINE get_engine() const { return m_engine_type; } void operator()(expr* e) { - if (is_quantifier(e)) { - m_engine_type = QPDR_ENGINE; - } - else if (m_engine_type != QPDR_ENGINE) { if (a.is_int_real(e)) { - m_engine_type = PDR_ENGINE; + m_engine_type = SPACER_ENGINE; } else if (is_var(e) && m.is_bool(e)) { - m_engine_type = PDR_ENGINE; + m_engine_type = SPACER_ENGINE; } else if (dt.is_datatype(m.get_sort(e))) { - m_engine_type = PDR_ENGINE; - } + m_engine_type = SPACER_ENGINE; } } }; @@ -805,12 +792,6 @@ namespace datalog { else if (e == symbol("spacer")) { m_engine_type = SPACER_ENGINE; } - else if (e == symbol("pdr")) { - m_engine_type = PDR_ENGINE; - } - else if (e == symbol("qpdr")) { - m_engine_type = QPDR_ENGINE; - } else if (e == symbol("bmc")) { m_engine_type = BMC_ENGINE; } @@ -858,8 +839,6 @@ namespace datalog { switch (get_engine()) { case DATALOG_ENGINE: case SPACER_ENGINE: - case PDR_ENGINE: - case QPDR_ENGINE: case BMC_ENGINE: case QBMC_ENGINE: case TAB_ENGINE: @@ -882,8 +861,6 @@ namespace datalog { switch (get_engine()) { case DATALOG_ENGINE: case SPACER_ENGINE: - case PDR_ENGINE: - case QPDR_ENGINE: case BMC_ENGINE: case QBMC_ENGINE: case TAB_ENGINE: diff --git a/src/muz/base/dl_engine_base.h b/src/muz/base/dl_engine_base.h index 9fc90ab1d..d6099e04c 100644 --- a/src/muz/base/dl_engine_base.h +++ b/src/muz/base/dl_engine_base.h @@ -25,9 +25,7 @@ Revision History: namespace datalog { enum DL_ENGINE { DATALOG_ENGINE, - PDR_ENGINE, SPACER_ENGINE, - QPDR_ENGINE, BMC_ENGINE, QBMC_ENGINE, TAB_ENGINE, diff --git a/src/muz/base/fixedpoint_params.pyg b/src/muz/base/fixedpoint_params.pyg index b5231c27b..f11e2faf9 100644 --- a/src/muz/base/fixedpoint_params.pyg +++ b/src/muz/base/fixedpoint_params.pyg @@ -1,37 +1,37 @@ -def_module_params('fixedpoint', +def_module_params('fixedpoint', description='fixedpoint parameters', export=True, params=(('timeout', UINT, UINT_MAX, 'set timeout'), - ('engine', SYMBOL, 'auto-config', - 'Select: auto-config, datalog, spacer, pdr, bmc'), - ('datalog.default_table', SYMBOL, 'sparse', + ('engine', SYMBOL, 'auto-config', + 'Select: auto-config, datalog, bmc, spacer'), + ('datalog.default_table', SYMBOL, 'sparse', 'default table implementation: sparse, hashtable, bitvector, interval'), - ('datalog.default_relation', SYMBOL, 'pentagon', + ('datalog.default_relation', SYMBOL, 'pentagon', 'default relation implementation: external_relation, pentagon'), - ('datalog.generate_explanations', BOOL, False, + ('datalog.generate_explanations', BOOL, False, 'produce explanations for produced facts when using the datalog engine'), - ('datalog.use_map_names', BOOL, True, + ('datalog.use_map_names', BOOL, True, "use names from map files when displaying tuples"), - ('datalog.magic_sets_for_queries', BOOL, False, + ('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 ' + + ('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 " + + ('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 " + + ('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 " + + ('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, + ('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 " + + "union and widening operations to determine only whether the " + "updated relation was modified or not"), - ('datalog.compile_with_widening', BOOL, False, + ('datalog.compile_with_widening', BOOL, False, "widening will be used to compile recursive rules"), ('datalog.default_table_checked', BOOL, False, "if true, the default " + 'table will be default_table inside a wrapper that checks that its results ' + @@ -39,15 +39,15 @@ def_module_params('fixedpoint', ('datalog.default_table_checker', SYMBOL, 'null', "see default_table_checked"), ('datalog.check_relation',SYMBOL,'null', "name of default relation to check. " + "operations on the default relation will be verified using SMT solving"), - ('datalog.initial_restart_timeout', UINT, 0, - "length of saturation run before the first restart (in ms), " + + ('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 " + + ('datalog.output_profile', BOOL, False, + "determines whether profile information should be " + "output when outputting Datalog rules or instructions"), - ('datalog.print.tuples', BOOL, True, + ('datalog.print.tuples', BOOL, True, "determines whether tuples for output predicates should be output"), - ('datalog.profile_timeout_milliseconds', UINT, 0, + ('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, @@ -56,94 +56,94 @@ def_module_params('fixedpoint', "table columns, if it would have been empty otherwise"), ('datalog.subsumption', BOOL, True, "if true, removes/filters predicates with total transitions"), - ('pdr.bfs_model_search', BOOL, True, - "use BFS strategy for expanding model search"), - ('pdr.farkas', BOOL, True, + ('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, + ('pdr.flexible_trace', BOOL, False, "allow PDR generate long counter-examples " + "by extending candidate trace within search area"), - ('pdr.flexible_trace_depth', UINT, UINT_MAX, + ('pdr.flexible_trace_depth', UINT, UINT_MAX, 'Controls the depth (below the current level) at which flexible trace can be applied'), - ('pdr.use_model_generalizer', BOOL, False, + ('pdr.use_model_generalizer', BOOL, False, "use model for backwards propagation (instead of symbolic simulation)"), - ('pdr.validate_result', BOOL, False, + ('pdr.validate_result', BOOL, False, "validate result (by proof checking or model checking)"), - ('pdr.simplify_formulas_pre', BOOL, False, + ('pdr.simplify_formulas_pre', BOOL, False, "simplify derived formulas before inductive propagation"), - ('pdr.simplify_formulas_post', BOOL, False, + ('pdr.simplify_formulas_post', BOOL, False, "simplify derived formulas after inductive propagation"), - ('pdr.use_multicore_generalizer', BOOL, False, + ('pdr.use_multicore_generalizer', BOOL, False, "extract multiple cores for blocking states"), - ('pdr.use_inductive_generalizer', BOOL, True, + ('pdr.use_inductive_generalizer', BOOL, True, "generalize lemmas using induction strengthening"), - ('pdr.use_arith_inductive_generalizer', BOOL, False, + ('pdr.use_arith_inductive_generalizer', BOOL, False, "generalize lemmas using arithmetic heuristics for induction strengthening"), - ('pdr.use_convex_closure_generalizer', BOOL, False, + ('pdr.use_convex_closure_generalizer', BOOL, False, "generalize using convex closures of lemmas"), - ('pdr.use_convex_interior_generalizer', BOOL, False, + ('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 " + + ('pdr.cache_mode', UINT, 0, "use no (0), symbolic (1) or explicit " + "cache (2) for model search"), - ('pdr.inductive_reachability_check', BOOL, False, + ('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, + ('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, " + + ('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 " + + ('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, + ('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', BOOL, False, 'print certificate for reachability or non-reachability'), - ('print_boogie_certificate', BOOL, False, + ('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, '', + ('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, + ('xform.bit_blast', BOOL, False, 'bit-blast bit-vectors'), - ('xform.magic', BOOL, False, + ('xform.magic', BOOL, False, "perform symbolic magic set transformation"), - ('xform.scale', BOOL, False, + ('xform.scale', BOOL, False, "add scaling variable to linear real arithmetic 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, + ('xform.inline_linear_branch', BOOL, False, "try linear inlining method with potential expansion"), ('xform.compress_unbound', BOOL, True, "compress tails with unbound variables"), ('xform.fix_unbound_vars', BOOL, False, "fix unbound variables in tail"), - ('xform.unfold_rules', UINT, 0, + ('xform.unfold_rules', UINT, 0, "unfold rules statically using iterative squarring"), ('xform.slice', BOOL, True, "simplify clause set using slicing"), - ('xform.karr', BOOL, False, + ('xform.karr', BOOL, False, "Add linear invariants to clauses using Karr's method"), ('spacer.use_eqclass', BOOL, False, "Generalizes equalities to equivalence classes"), - ('xform.transform_arrays', BOOL, False, + ('xform.transform_arrays', BOOL, False, "Rewrites arrays equalities and applies select over store"), - ('xform.instantiate_arrays', BOOL, False, + ('xform.instantiate_arrays', BOOL, False, "Transforms P(a) into P(i, a[i] a)"), - ('xform.instantiate_arrays.enforce', BOOL, False, + ('xform.instantiate_arrays.enforce', BOOL, False, "Transforms P(a) into P(i, a[i]), discards a from predicate"), - ('xform.instantiate_arrays.nb_quantifier', UINT, 1, + ('xform.instantiate_arrays.nb_quantifier', UINT, 1, "Gives the number of quantifiers per array"), - ('xform.instantiate_arrays.slice_technique', SYMBOL, "no-slicing", + ('xform.instantiate_arrays.slice_technique', SYMBOL, "no-slicing", "=> GetId(i) = i, => GetId(i) = true"), - ('xform.quantify_arrays', BOOL, False, + ('xform.quantify_arrays', BOOL, False, "create quantified Horn clauses from clauses with arrays"), - ('xform.instantiate_quantifiers', BOOL, False, + ('xform.instantiate_quantifiers', BOOL, False, "instantiate quantified Horn clauses using E-matching heuristic"), ('xform.coalesce_rules', BOOL, False, "coalesce rules"), ('xform.tail_simplifier_pve', BOOL, True, "propagate_variable_equivalences"), @@ -154,8 +154,8 @@ def_module_params('fixedpoint', ('spacer.use_lemma_as_cti', BOOL, False, 'SPACER: use a lemma instead of a CTI in flexible_trace'), ('spacer.reset_obligation_queue', BOOL, True, 'SPACER: reset obligation queue when entering a new level'), ('spacer.use_array_eq_generalizer', BOOL, True, 'SPACER: attempt to generalize lemmas with array equalities'), - ('spacer.use_derivations', BOOL, True, 'SPACER: using derivation mechanism to cache intermediate results for non-linear rules'), - ('xform.array_blast', BOOL, False, "try to eliminate local array terms using Ackermannization -- some array terms may remain"), + ('spacer.use_derivations', BOOL, True, 'SPACER: using derivation mechanism to cache intermediate results for non-linear rules'), + ('xform.array_blast', BOOL, False, "try to eliminate local array terms using Ackermannization -- some array terms may remain"), ('xform.array_blast_full', BOOL, False, "eliminate all local array variables by QE"), ('spacer.skip_propagate', BOOL, False, "Skip propagate/pushing phase. Turns PDR into a BMC that returns either reachable or unknown"), ('spacer.max_level', UINT, UINT_MAX, "Maximum level to explore"), diff --git a/src/muz/fp/CMakeLists.txt b/src/muz/fp/CMakeLists.txt index 41262813a..4837df81b 100644 --- a/src/muz/fp/CMakeLists.txt +++ b/src/muz/fp/CMakeLists.txt @@ -9,7 +9,6 @@ z3_add_component(fp clp ddnf muz - pdr rel spacer tab diff --git a/src/muz/fp/dl_register_engine.cpp b/src/muz/fp/dl_register_engine.cpp index a2270d774..28a2a1c5e 100644 --- a/src/muz/fp/dl_register_engine.cpp +++ b/src/muz/fp/dl_register_engine.cpp @@ -21,7 +21,6 @@ Revision History: #include "muz/clp/clp_context.h" #include "muz/tab/tab_context.h" #include "muz/rel/rel_context.h" -#include "muz/pdr/pdr_dl_interface.h" #include "muz/ddnf/ddnf.h" #include "muz/spacer/spacer_dl_interface.h" @@ -30,9 +29,6 @@ namespace datalog { engine_base* register_engine::mk_engine(DL_ENGINE engine_type) { switch(engine_type) { - case PDR_ENGINE: - case QPDR_ENGINE: - return alloc(pdr::dl_interface, *m_ctx); case SPACER_ENGINE: return alloc(spacer::dl_interface, *m_ctx); case DATALOG_ENGINE: diff --git a/src/muz/pdr/CMakeLists.txt b/src/muz/pdr/CMakeLists.txt deleted file mode 100644 index ca2992b97..000000000 --- a/src/muz/pdr/CMakeLists.txt +++ /dev/null @@ -1,20 +0,0 @@ -z3_add_component(pdr - SOURCES - pdr_closure.cpp - pdr_context.cpp - pdr_dl_interface.cpp - pdr_farkas_learner.cpp - pdr_generalizers.cpp - pdr_manager.cpp - pdr_prop_solver.cpp - pdr_reachable_cache.cpp - pdr_smt_context_manager.cpp - pdr_sym_mux.cpp - pdr_util.cpp - COMPONENT_DEPENDENCIES - arith_tactics - core_tactics - muz - smt_tactic - transforms -) diff --git a/src/muz/pdr/pdr_closure.cpp b/src/muz/pdr/pdr_closure.cpp deleted file mode 100644 index 82caf285b..000000000 --- a/src/muz/pdr/pdr_closure.cpp +++ /dev/null @@ -1,177 +0,0 @@ -/*++ -Copyright (c) 2013 Microsoft Corporation - -Module Name: - - pdr_closure.cpp - -Abstract: - - Utility functions for computing closures. - -Author: - - Nikolaj Bjorner (nbjorner) 2013-9-1. - -Revision History: - ---*/ - -#include "muz/pdr/pdr_closure.h" -#include "muz/pdr/pdr_context.h" -#include "ast/rewriter/expr_safe_replace.h" -#include "ast/ast_util.h" - -namespace pdr { - - expr_ref scaler::operator()(expr* e, expr* k, obj_map* translate) { - m_cache[0].reset(); - m_cache[1].reset(); - m_translate = translate; - m_k = k; - return scale(e, false); - } - - expr_ref scaler::scale(expr* e, bool is_mul) { - expr* r; - if (m_cache[is_mul].find(e, r)) { - return expr_ref(r, m); - } - if (!is_app(e)) { - return expr_ref(e, m); - } - app* ap = to_app(e); - if (m_translate && m_translate->find(ap->get_decl(), r)) { - return expr_ref(r, m); - } - if (!is_mul && a.is_numeral(e)) { - return expr_ref(a.mk_mul(m_k, e), m); - } - expr_ref_vector args(m); - bool is_mul_rec = is_mul || a.is_mul(e); - for (unsigned i = 0; i < ap->get_num_args(); ++i) { - args.push_back(scale(ap->get_arg(i), is_mul_rec)); - } - expr_ref result(m); - result = m.mk_app(ap->get_decl(), args.size(), args.c_ptr()); - m_cache[is_mul].insert(e, result); - return result; - } - - expr_ref scaler::undo_k(expr* e, expr* k) { - expr_safe_replace sub(m); - th_rewriter rw(m); - expr_ref result(e, m); - sub.insert(k, a.mk_numeral(rational(1), false)); - sub(result); - rw(result); - return result; - } - - - closure::closure(pred_transformer& p, bool is_closure): - m(p.get_manager()), m_pt(p), a(m), - m_is_closure(is_closure), m_sigma(m), m_trail(m) {} - - - void closure::add_variables(unsigned num_vars, expr_ref_vector& fmls) { - manager& pm = m_pt.get_pdr_manager(); - SASSERT(num_vars > 0); - while (m_vars.size() < num_vars) { - m_vars.resize(m_vars.size()+1); - m_sigma.push_back(m.mk_fresh_const("sigma", a.mk_real())); - } - - unsigned sz = m_pt.sig_size(); - - for (unsigned i = 0; i < sz; ++i) { - expr* var; - ptr_vector vars; - func_decl* fn0 = m_pt.sig(i); - func_decl* fn1 = pm.o2n(fn0, 0); - sort* srt = fn0->get_range(); - if (a.is_int_real(srt)) { - for (unsigned j = 0; j < num_vars; ++j) { - if (!m_vars[j].find(fn1, var)) { - var = m.mk_fresh_const(fn1->get_name().str().c_str(), srt); - m_trail.push_back(var); - m_vars[j].insert(fn1, var); - } - vars.push_back(var); - } - fmls.push_back(m.mk_eq(m.mk_const(fn1), a.mk_add(num_vars, vars.c_ptr()))); - } - } - if (m_is_closure) { - for (unsigned i = 0; i < num_vars; ++i) { - fmls.push_back(a.mk_ge(m_sigma[i].get(), a.mk_numeral(rational(0), a.mk_real()))); - } - } - else { - // is interior: - for (unsigned i = 0; i < num_vars; ++i) { - fmls.push_back(a.mk_gt(m_sigma[i].get(), a.mk_numeral(rational(0), a.mk_real()))); - } - } - fmls.push_back(m.mk_eq(a.mk_numeral(rational(1), a.mk_real()), a.mk_add(num_vars, m_sigma.c_ptr()))); - } - - expr_ref closure::close_fml(expr* e) { - expr* e0, *e1, *e2; - expr_ref result(m); - if (a.is_lt(e, e1, e2)) { - result = a.mk_le(e1, e2); - } - else if (a.is_gt(e, e1, e2)) { - result = a.mk_ge(e1, e2); - } - else if (m.is_not(e, e0) && a.is_ge(e0, e1, e2)) { - result = a.mk_le(e1, e2); - } - else if (m.is_not(e, e0) && a.is_le(e0, e1, e2)) { - result = a.mk_ge(e1, e2); - } - else if (a.is_ge(e) || a.is_le(e) || m.is_eq(e) || - (m.is_not(e, e0) && (a.is_gt(e0) || a.is_lt(e0)))) { - result = e; - } - else { - IF_VERBOSE(1, verbose_stream() << "Cannot close: " << mk_pp(e, m) << "\n";); - result = m.mk_true(); - } - return result; - } - - expr_ref closure::close_conjunction(expr* fml) { - expr_ref_vector fmls(m); - flatten_and(fml, fmls); - for (unsigned i = 0; i < fmls.size(); ++i) { - fmls[i] = close_fml(fmls[i].get()); - } - return expr_ref(mk_and(fmls), m); - } - - expr_ref closure::relax(unsigned i, expr* fml) { - scaler sc(m); - expr_ref result = sc(fml, m_sigma[i].get(), &m_vars[i]); - return close_conjunction(result); - } - - expr_ref closure::operator()(expr_ref_vector const& As) { - if (As.empty()) { - return expr_ref(m.mk_false(), m); - } - if (As.size() == 1) { - return expr_ref(As[0], m); - } - expr_ref_vector fmls(m); - expr_ref B(m); - add_variables(As.size(), fmls); - for (unsigned i = 0; i < As.size(); ++i) { - fmls.push_back(relax(i, As[i])); - } - B = mk_and(fmls); - return B; - } - -} diff --git a/src/muz/pdr/pdr_closure.h b/src/muz/pdr/pdr_closure.h deleted file mode 100644 index c41e83389..000000000 --- a/src/muz/pdr/pdr_closure.h +++ /dev/null @@ -1,67 +0,0 @@ -/*++ -Copyright (c) 2013 Microsoft Corporation - -Module Name: - - pdr_closure.h - -Abstract: - - Utility functions for computing closures. - -Author: - - Nikolaj Bjorner (nbjorner) 2013-9-1. - -Revision History: - ---*/ - -#ifndef PDR_CLOSURE_H_ -#define PDR_CLOSURE_H_ - -#include "ast/arith_decl_plugin.h" - -namespace pdr { - - // Arithmetic scaling functor. - // Variables are replaced using - // m_translate. Constants are replaced by - // multiplication with a variable 'k' (scale factor). - class scaler { - ast_manager& m; - arith_util a; - obj_map m_cache[2]; - expr* m_k; - obj_map* m_translate; - public: - scaler(ast_manager& m): m(m), a(m), m_translate(nullptr) {} - expr_ref operator()(expr* e, expr* k, obj_map* translate = nullptr); - expr_ref undo_k(expr* e, expr* k); - private: - expr_ref scale(expr* e, bool is_mul); - }; - - class pred_transformer; - - class closure { - ast_manager& m; - pred_transformer& m_pt; - arith_util a; - bool m_is_closure; - expr_ref_vector m_sigma; - expr_ref_vector m_trail; - vector > m_vars; - - expr_ref relax(unsigned i, expr* fml); - expr_ref close_conjunction(expr* fml); - expr_ref close_fml(expr* fml); - void add_variables(unsigned num_vars, expr_ref_vector& fmls); - public: - closure(pred_transformer& pt, bool is_closure); - expr_ref operator()(expr_ref_vector const& As); - - }; -} - -#endif diff --git a/src/muz/pdr/pdr_context.cpp b/src/muz/pdr/pdr_context.cpp deleted file mode 100644 index 1b1350617..000000000 --- a/src/muz/pdr/pdr_context.cpp +++ /dev/null @@ -1,2431 +0,0 @@ -/*++ -Copyright (c) 2011 Microsoft Corporation - -Module Name: - - pdr_context.cpp - -Abstract: - - PDR predicate transformers and search context. - -Author: - - Nikolaj Bjorner (nbjorner) 2011-11-20. - -Revision History: - - Based on pdr_dl.cpp by - Krystof Hoder (t-khoder) 2011-9-19. - -Notes: - - ---*/ - - -#include -#include "muz/base/dl_util.h" -#include "ast/rewriter/rewriter.h" -#include "ast/rewriter/rewriter_def.h" -#include "ast/rewriter/var_subst.h" -#include "util/util.h" -#include "muz/pdr/pdr_prop_solver.h" -#include "muz/pdr/pdr_context.h" -#include "muz/pdr/pdr_generalizers.h" -#include "ast/for_each_expr.h" -#include "muz/base/dl_rule_set.h" -#include "smt/tactic/unit_subsumption_tactic.h" -#include "model/model_smt2_pp.h" -#include "muz/transforms/dl_mk_rule_inliner.h" -#include "ast/ast_smt2_pp.h" -#include "qe/qe_lite.h" -#include "ast/ast_ll_pp.h" -#include "ast/proofs/proof_checker.h" -#include "smt/smt_value_sort.h" -#include "muz/base/dl_boogie_proof.h" -#include "ast/scoped_proof.h" -#include "tactic/core/blast_term_ite_tactic.h" -#include "model/model_implicant.h" -#include "ast/rewriter/expr_safe_replace.h" -#include "ast/ast_util.h" - -namespace pdr { - - - static const unsigned infty_level = UINT_MAX; - - static bool is_infty_level(unsigned lvl) { return lvl == infty_level; } - - static unsigned next_level(unsigned lvl) { return is_infty_level(lvl)?lvl:(lvl+1); } - - struct pp_level { - unsigned m_level; - pp_level(unsigned l): m_level(l) {} - }; - - static std::ostream& operator<<(std::ostream& out, pp_level const& p) { - if (is_infty_level(p.m_level)) { - return out << "oo"; - } - else { - return out << p.m_level; - } - } - - // ---------------- - // pred_tansformer - - pred_transformer::pred_transformer(context& ctx, manager& pm, func_decl* head): - pm(pm), m(pm.get_manager()), - ctx(ctx), m_head(head, m), - m_sig(m), m_solver(pm, head->get_name()), - m_invariants(m), m_transition(m), m_initial_state(m), - 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(); - for (; it2 != end2; ++it2) { - dealloc(it2->m_value); - } - rule2expr::iterator it3 = m_rule2transition.begin(), end3 = m_rule2transition.end(); - for (; it3 != end3; ++it3) { - m.dec_ref(it3->m_value); - } - } - - std::ostream& pred_transformer::display(std::ostream& out) const { - if (!rules().empty()) out << "rules\n"; - datalog::rule_manager& rm = ctx.get_context().get_rule_manager(); - for (unsigned i = 0; i < rules().size(); ++i) { - rm.display_smt2(*rules()[i], out) << "\n"; - } - out << "transition\n" << mk_pp(transition(), m) << "\n"; - return out; - } - - void pred_transformer::collect_statistics(statistics& st) const { - m_solver.collect_statistics(st); - m_reachable.collect_statistics(st); - st.update("PDR num propagations", m_stats.m_num_propagations); - unsigned np = m_invariants.size(); - for (unsigned i = 0; i < m_levels.size(); ++i) { - np += m_levels[i].size(); - } - st.update("PDR num properties", np); - } - - void pred_transformer::reset_statistics() { - m_solver.reset_statistics(); - m_reachable.reset_statistics(); - m_stats.reset(); - } - - void pred_transformer::init_sig() { - if (m_sig.empty()) { - for (unsigned i = 0; i < m_head->get_arity(); ++i) { - sort * arg_sort = m_head->get_domain(i); - std::stringstream name_stm; - name_stm << m_head->get_name() << '_' << i; - func_decl_ref stm(m); - stm = m.mk_func_decl(symbol(name_stm.str().c_str()), 0, (sort*const*)nullptr, arg_sort); - m_sig.push_back(pm.get_o_pred(stm, 0)); - } - } - } - - void pred_transformer::ensure_level(unsigned level) { - if (is_infty_level(level)) { - return; - } - while (m_levels.size() <= level) { - m_solver.add_level(); - m_levels.push_back(expr_ref_vector(m)); - } - } - - bool pred_transformer::is_reachable(expr* state) { - return m_reachable.is_reachable(state); - } - - datalog::rule const& pred_transformer::find_rule(model_core const& model) const { - TRACE("pdr_verbose", - datalog::rule_manager& rm = ctx.get_context().get_rule_manager(); - for (auto const& kv : m_tag2rule) { - expr* pred = kv.m_key; - tout << mk_pp(pred, m) << ":\n"; - if (kv.m_value) rm.display_smt2(*kv.m_value, tout) << "\n"; - } - ); - - if (m_tag2rule.size() == 1) { - return *m_tag2rule.begin()->m_value; - } - - expr_ref vl(m); - for (auto const& kv : m_tag2rule) { - expr* pred = kv.m_key; - if (model.eval(to_app(pred)->get_decl(), vl) && m.is_true(vl)) { - return *kv.m_value; - } - } - throw default_exception("could not find rule"); - } - - void pred_transformer::find_predecessors(datalog::rule const& r, ptr_vector& preds) const { - preds.reset(); - unsigned tail_sz = r.get_uninterpreted_tail_size(); - for (unsigned ti = 0; ti < tail_sz; ti++) { - preds.push_back(r.get_tail(ti)->get_decl()); - } - } - - - void pred_transformer::remove_predecessors(expr_ref_vector& literals) { - // remove tags - for (unsigned i = 0; i < literals.size(); ) { - expr* l = literals[i].get(); - m.is_not(l, l); - if (m_tag2rule.contains(l)) { - literals[i] = literals.back(); - literals.pop_back(); - } - else { - ++i; - } - } - } - - void pred_transformer::simplify_formulas(tactic& tac, expr_ref_vector& v) { - goal_ref g(alloc(goal, m, false, false, false)); - for (expr* e : v) g->assert_expr(e); - goal_ref_buffer result; - tac(g, result); - SASSERT(result.size() == 1); - goal* r = result[0]; - v.reset(); - for (unsigned j = 0; j < r->size(); ++j) v.push_back(r->form(j)); - } - - void pred_transformer::simplify_formulas() { - tactic_ref us = mk_unit_subsumption_tactic(m); - simplify_formulas(*us, m_invariants); - for (auto & fmls : m_levels) - simplify_formulas(*us, fmls); - } - - expr_ref pred_transformer::get_formulas(unsigned level, bool add_axioms) { - expr_ref_vector res(m); - if (add_axioms) { - res.push_back(pm.get_background()); - res.push_back((level == 0)?initial_state():transition()); - } - res.append(m_invariants); - for (unsigned i = level; i < m_levels.size(); ++i) { - res.append(m_levels[i]); - } - return pm.mk_and(res); - } - - expr_ref pred_transformer::get_propagation_formula(decl2rel const& pts, unsigned level) { - expr_ref result(m), tmp1(m), tmp2(m); - expr_ref_vector conj(m); - if (level == 0) { - conj.push_back(initial_state()); - } - else { - conj.push_back(transition()); - } - conj.push_back(get_formulas(level, true)); - obj_map::iterator it = m_tag2rule.begin(), end = m_tag2rule.end(); - for (; level > 0 && it != end; ++it) { - expr* tag = it->m_key; - datalog::rule const* r = it->m_value; - if (!r) continue; - find_predecessors(*r, m_predicates); - for (unsigned i = 0; i < m_predicates.size(); ++i) { - func_decl* d = m_predicates[i]; - pred_transformer & pt = *pts.find(d); - tmp1 = pt.get_formulas(level-1, false); - TRACE("pdr", tout << mk_pp(tmp1, m) << "\n";); - pm.formula_n2o(tmp1, tmp2, i, false); - conj.push_back(m.mk_implies(tag, tmp2)); - } - } - return pm.mk_and(conj); - } - - bool pred_transformer::propagate_to_next_level(unsigned src_level) { - unsigned tgt_level = next_level(src_level); - ensure_level(next_level(tgt_level)); - expr_ref_vector& src = m_levels[src_level]; - - CTRACE("pdr", !src.empty(), - tout << "propagating " << src_level << " to " << tgt_level; - tout << " for relation " << head()->get_name() << "\n";); - - for (unsigned i = 0; i < src.size(); ) { - expr * curr = src[i].get(); - unsigned stored_lvl = 0; - VERIFY(m_prop2level.find(curr, stored_lvl)); - SASSERT(stored_lvl >= src_level); - bool assumes_level; - if (stored_lvl > src_level) { - TRACE("pdr", tout << "at level: "<< stored_lvl << " " << mk_pp(curr, m) << "\n";); - src[i] = src.back(); - src.pop_back(); - } - else if (is_invariant(tgt_level, curr, false, assumes_level)) { - - add_property(curr, assumes_level?tgt_level:infty_level); - TRACE("pdr", tout << "is invariant: "<< pp_level(tgt_level) << " " << mk_pp(curr, m) << "\n";); - src[i] = src.back(); - src.pop_back(); - ++m_stats.m_num_propagations; - } - else { - TRACE("pdr", tout << "not propagated: " << mk_pp(curr, m) << "\n";); - ++i; - } - } - IF_VERBOSE(3, verbose_stream() << "propagate: " << pp_level(src_level) << "\n"; - for (unsigned i = 0; i < src.size(); ++i) { - verbose_stream() << mk_pp(src[i].get(), m) << "\n"; - }); - return src.empty(); - } - - bool pred_transformer::add_property1(expr * lemma, unsigned lvl) { - if (is_infty_level(lvl)) { - if (!m_invariants.contains(lemma)) { - TRACE("pdr", tout << "property1: " << head()->get_name() << " " << mk_pp(lemma, m) << "\n";); - m_invariants.push_back(lemma); - m_prop2level.insert(lemma, lvl); - m_solver.add_formula(lemma); - return true; - } - else { - TRACE("pdr", tout << "already contained: " << head()->get_name() << " " << mk_pp(lemma, m) << "\n";); - return false; - } - } - ensure_level(lvl); - unsigned old_level; - if (!m_prop2level.find(lemma, old_level) || old_level < lvl) { - TRACE("pdr", tout << "property1: " << pp_level(lvl) << " " << head()->get_name() << " " << mk_pp(lemma, m) << "\n";); - m_levels[lvl].push_back(lemma); - m_prop2level.insert(lemma, lvl); - m_solver.add_level_formula(lemma, lvl); - return true; - } - else { - TRACE("pdr", tout << "old-level: " << pp_level(old_level) << " " << head()->get_name() << " " << mk_pp(lemma, m) << "\n";); - return false; - } - } - - void pred_transformer::add_child_property(pred_transformer& child, expr* lemma, unsigned lvl) { - ensure_level(lvl); - expr_ref_vector fmls(m); - mk_assumptions(child.head(), lemma, fmls); - for (unsigned i = 0; i < fmls.size(); ++i) { - TRACE("pdr", tout << "child property: " << mk_pp(fmls[i].get(), m) << "\n";); - if (is_infty_level(lvl)) { - m_solver.add_formula(fmls[i].get()); - } - else { - m_solver.add_level_formula(fmls[i].get(), lvl); - } - } - } - - void pred_transformer::add_property(expr* lemma, unsigned lvl) { - expr_ref_vector lemmas(m); - flatten_and(lemma, lemmas); - for (unsigned i = 0; i < lemmas.size(); ++i) { - expr* lemma_i = lemmas[i].get(); - if (add_property1(lemma_i, lvl)) { - IF_VERBOSE(2, verbose_stream() << pp_level(lvl) << " " << mk_pp(lemma_i, m) << "\n";); - for (unsigned j = 0; j < m_use.size(); ++j) { - m_use[j]->add_child_property(*this, lemma_i, next_level(lvl)); - } - } - } - } - - expr_ref pred_transformer::get_cover_delta(func_decl* p_orig, int level) { - expr_ref result(m.mk_true(), m), v(m), c(m); - if (level == -1) { - result = pm.mk_and(m_invariants); - } - else if ((unsigned)level < m_levels.size()) { - result = pm.mk_and(m_levels[level]); - } - // replace local constants by bound variables. - expr_substitution sub(m); - for (unsigned i = 0; i < sig_size(); ++i) { - c = m.mk_const(pm.o2n(sig(i), 0)); - v = m.mk_var(i, sig(i)->get_range()); - sub.insert(c, v); - } - scoped_ptr rep = mk_default_expr_replacer(m); - rep->set_substitution(&sub); - (*rep)(result); - - // adjust result according to model converter. - unsigned arity = m_head->get_arity(); - model_ref md = alloc(model, m); - if (arity == 0) { - md->register_decl(m_head, result); - } - else { - func_interp* fi = alloc(func_interp, m, arity); - fi->set_else(result); - md->register_decl(m_head, fi); - } - model_converter_ref mc = ctx.get_model_converter(); - apply(mc, md); - if (p_orig->get_arity() == 0) { - result = md->get_const_interp(p_orig); - } - else { - result = md->get_func_interp(p_orig)->get_interp(); - } - return result; - } - - void pred_transformer::add_cover(unsigned level, expr* property) { - // replace bound variables by local constants. - expr_ref result(property, m), v(m), c(m); - expr_substitution sub(m); - for (unsigned i = 0; i < sig_size(); ++i) { - c = m.mk_const(pm.o2n(sig(i), 0)); - v = m.mk_var(i, sig(i)->get_range()); - sub.insert(v, c); - } - scoped_ptr rep = mk_default_expr_replacer(m); - rep->set_substitution(&sub); - (*rep)(result); - TRACE("pdr", tout << "cover:\n" << mk_pp(result, m) << "\n";); - // add the property. - add_property(result, level); - } - - void pred_transformer::propagate_to_infinity(unsigned invariant_level) { - expr_ref inv = get_formulas(invariant_level, false); - add_property(inv, infty_level); - // cleanup - for (unsigned i = invariant_level; i < m_levels.size(); ++i) { - m_levels[i].reset(); - } - } - - lbool pred_transformer::is_reachable(model_node& n, expr_ref_vector* core, bool& uses_level) { - TRACE("pdr", - tout << "is-reachable: " << head()->get_name() << " level: " << n.level() << "\n"; - tout << mk_pp(n.state(), m) << "\n";); - ensure_level(n.level()); - model_ref model; - prop_solver::scoped_level _sl(m_solver, n.level()); - m_solver.set_core(core); - m_solver.set_model(&model); - lbool is_sat = m_solver.check_conjunction_as_assumptions(n.state()); - if (is_sat == l_true && core) { - core->reset(); - TRACE("pdr", tout << "updating model\n"; - model_smt2_pp(tout, m, *model, 0); - tout << mk_pp(n.state(), m) << "\n";); - n.set_model(model); - } - else if (is_sat == l_false) { - uses_level = m_solver.assumes_level(); - } - m_solver.set_model(nullptr); - return is_sat; - } - - bool pred_transformer::is_invariant(unsigned level, expr* states, bool inductive, bool& assumes_level, expr_ref_vector* core) { - expr_ref_vector conj(m); - expr_ref tmp(m); - - conj.push_back(m.mk_not(states)); - - if (inductive) { - mk_assumptions(head(), states, conj); - } - tmp = pm.mk_and(conj); - prop_solver::scoped_level _sl(m_solver, level); - m_solver.set_core(core); - m_solver.set_model(nullptr); - lbool r = m_solver.check_conjunction_as_assumptions(tmp); - if (r == l_false) { - assumes_level = m_solver.assumes_level(); - } - return r == l_false; - } - - bool pred_transformer::check_inductive(unsigned level, expr_ref_vector& lits, bool& assumes_level) { - manager& pm = get_pdr_manager(); - expr_ref_vector conj(m), core(m); - expr_ref fml(m), states(m); - states = m.mk_not(pm.mk_and(lits)); - mk_assumptions(head(), states, conj); - fml = pm.mk_and(conj); - prop_solver::scoped_level _sl(m_solver, level); - m_solver.set_core(&core); - m_solver.set_subset_based_core(true); - m_solver.set_model(nullptr); - lbool res = m_solver.check_assumptions_and_formula(lits, fml); - if (res == l_false) { - lits.reset(); - lits.append(core); - assumes_level = m_solver.assumes_level(); - } - return res == l_false; - } - - void pred_transformer::mk_assumptions(func_decl* head, expr* fml, expr_ref_vector& result) { - expr_ref tmp1(m), tmp2(m); - obj_map::iterator it = m_tag2rule.begin(), end = m_tag2rule.end(); - for (; it != end; ++it) { - expr* pred = it->m_key; - datalog::rule const* r = it->m_value; - if (!r) continue; - find_predecessors(*r, m_predicates); - for (unsigned i = 0; i < m_predicates.size(); i++) { - func_decl* d = m_predicates[i]; - if (d == head) { - tmp1 = m.mk_implies(pred, fml); - pm.formula_n2o(tmp1, tmp2, i); - result.push_back(tmp2); - } - } - } - } - - void pred_transformer::initialize(decl2rel const& pts) { - m_initial_state = m.mk_false(); - m_transition = m.mk_true(); - init_rules(pts, m_initial_state, m_transition); - th_rewriter rw(m); - rw(m_transition); - rw(m_initial_state); - - m_solver.add_formula(m_transition); - m_solver.add_level_formula(m_initial_state, 0); - TRACE("pdr", - tout << "Initial state: " << mk_pp(m_initial_state, m) << "\n"; - tout << "Transition: " << mk_pp(m_transition, m) << "\n";); - SASSERT(is_app(m_initial_state)); - m_reachable.add_init(to_app(m_initial_state)); - } - - void pred_transformer::init_rules(decl2rel const& pts, expr_ref& init, expr_ref& transition) { - expr_ref_vector transitions(m); - ptr_vector tr_rules; - datalog::rule const* rule; - expr_ref_vector disj(m); - app_ref pred(m); - for (unsigned i = 0; i < rules().size(); ++i) { - init_rule(pts, *rules()[i], init, tr_rules, transitions); - } - switch(transitions.size()) { - case 0: - transition = m.mk_false(); - break; - case 1: - // create a dummy tag. - pred = m.mk_fresh_const(head()->get_name().str().c_str(), m.mk_bool_sort()); - rule = tr_rules[0]; - m_tag2rule.insert(pred, rule); - m_rule2tag.insert(rule, pred.get()); - transitions.push_back(pred); - transition = pm.mk_and(transitions); - break; - default: - for (unsigned i = 0; i < transitions.size(); ++i) { - pred = m.mk_fresh_const(head()->get_name().str().c_str(), m.mk_bool_sort()); - rule = tr_rules[i]; - m_tag2rule.insert(pred, rule); - m_rule2tag.insert(rule, pred); - disj.push_back(pred); - transitions[i] = m.mk_implies(pred, transitions[i].get()); - } - transitions.push_back(m.mk_or(disj.size(), disj.c_ptr())); - transition = pm.mk_and(transitions); - break; - } - } - - void pred_transformer::init_rule( - decl2rel const& pts, - datalog::rule const& rule, - expr_ref& init, - ptr_vector& rules, - expr_ref_vector& transitions) - { - // Predicates that are variable representatives. Other predicates at - // positions the variables occur are made equivalent with these. - expr_ref_vector conj(m); - app_ref_vector var_reprs(m); - ptr_vector aux_vars; - - unsigned ut_size = rule.get_uninterpreted_tail_size(); - unsigned t_size = rule.get_tail_size(); - SASSERT(ut_size <= t_size); - init_atom(pts, rule.get_head(), var_reprs, conj, UINT_MAX); - for (unsigned i = 0; i < ut_size; ++i) { - if (rule.is_neg_tail(i)) { - char const* msg = "PDR does not supported negated predicates in rule tails"; - IF_VERBOSE(0, verbose_stream() << msg << "\n";); - throw default_exception(msg); - } - init_atom(pts, rule.get_tail(i), var_reprs, conj, i); - } - for (unsigned i = ut_size; i < t_size; ++i) { - ground_free_vars(rule.get_tail(i), var_reprs, aux_vars); - } - SASSERT(check_filled(var_reprs)); - expr_ref_vector tail(m); - for (unsigned i = ut_size; i < t_size; ++i) { - tail.push_back(rule.get_tail(i)); - } - flatten_and(tail); - for (unsigned i = 0; i < tail.size(); ++i) { - expr_ref tmp(m); - var_subst vs(m, false); - vs(tail[i].get(), var_reprs.size(), (expr*const*)var_reprs.c_ptr(), tmp); - conj.push_back(tmp); - TRACE("pdr", tout << mk_pp(tail[i].get(), m) << "\n" << mk_pp(tmp, m) << "\n";); - if (!is_ground(tmp)) { - std::stringstream msg; - msg << "PDR cannot solve non-ground tails: " << tmp; - IF_VERBOSE(0, verbose_stream() << msg.str() << "\n";); - throw default_exception(msg.str()); - } - } - expr_ref fml = pm.mk_and(conj); - th_rewriter rw(m); - rw(fml); - if (ctx.is_dl() || ctx.is_utvpi()) { - blast_term_ite(fml); - } - TRACE("pdr", tout << mk_pp(fml, m) << "\n";); - SASSERT(is_ground(fml)); - if (m.is_false(fml)) { - // no-op. - } - else { - if (ut_size == 0) { - init = m.mk_or(init, fml); - } - transitions.push_back(fml); - m.inc_ref(fml); - m_rule2transition.insert(&rule, fml.get()); - rules.push_back(&rule); - } - m_rule2inst.insert(&rule, alloc(app_ref_vector, var_reprs)); - m_rule2vars.insert(&rule, aux_vars); - TRACE("pdr", - tout << rule.get_decl()->get_name() << "\n"; - for (unsigned i = 0; i < var_reprs.size(); ++i) { - tout << mk_pp(var_reprs[i].get(), m) << " "; - } - if (!var_reprs.empty()) tout << "\n";); - } - - bool pred_transformer::check_filled(app_ref_vector const& v) const { - for (unsigned i = 0; i < v.size(); ++i) { - if (!v[i]) return false; - } - return true; - } - - // create constants for free variables in tail. - void pred_transformer::ground_free_vars(expr* e, app_ref_vector& vars, ptr_vector& aux_vars) { - expr_free_vars fv; - fv(e); - while (vars.size() < fv.size()) { - vars.push_back(nullptr); - } - for (unsigned i = 0; i < fv.size(); ++i) { - if (fv[i] && !vars[i].get()) { - vars[i] = m.mk_fresh_const("aux", fv[i]); - aux_vars.push_back(vars[i].get()); - } - } - } - - // create names for variables used in relations. - void pred_transformer::init_atom( - decl2rel const& pts, - app * atom, - app_ref_vector& var_reprs, - expr_ref_vector& conj, - unsigned tail_idx - ) - { - unsigned arity = atom->get_num_args(); - func_decl* head = atom->get_decl(); - pred_transformer& pt = *pts.find(head); - for (unsigned i = 0; i < arity; i++) { - app_ref rep(m); - - if (tail_idx == UINT_MAX) { - rep = m.mk_const(pm.o2n(pt.sig(i), 0)); - } - else { - rep = m.mk_const(pm.o2o(pt.sig(i), 0, tail_idx)); - } - - expr * arg = atom->get_arg(i); - if (is_var(arg)) { - var * v = to_var(arg); - unsigned var_idx = v->get_idx(); - if (var_idx >= var_reprs.size()) { - var_reprs.resize(var_idx+1); - } - expr * repr = var_reprs[var_idx].get(); - if (repr) { - conj.push_back(m.mk_eq(rep, repr)); - } - else { - var_reprs[var_idx] = rep; - } - } - else { - SASSERT(is_app(arg)); - conj.push_back(m.mk_eq(rep, arg)); - } - } - } - - void pred_transformer::add_premises(decl2rel const& pts, unsigned lvl, expr_ref_vector& r) { - r.push_back(pm.get_background()); - r.push_back((lvl == 0)?initial_state():transition()); - for (unsigned i = 0; i < rules().size(); ++i) { - add_premises(pts, lvl, *rules()[i], r); - } - } - - void pred_transformer::close(expr* e) { - m_reachable.add_reachable(e); - } - - void pred_transformer::add_premises(decl2rel const& pts, unsigned lvl, datalog::rule& rule, expr_ref_vector& r) { - find_predecessors(rule, m_predicates); - for (unsigned i = 0; i < m_predicates.size(); ++i) { - expr_ref tmp(m); - func_decl* head = m_predicates[i]; - pred_transformer& pt = *pts.find(head); - expr_ref inv = pt.get_formulas(lvl, false); - if (!m.is_true(inv)) { - pm.formula_n2o(inv, tmp, i, true); - r.push_back(tmp); - } - } - } - - void pred_transformer::inherit_properties(pred_transformer& other) { - SASSERT(m_head == other.m_head); - obj_map::iterator it = other.m_prop2level.begin(); - obj_map::iterator end = other.m_prop2level.end(); - for (; it != end; ++it) { - IF_VERBOSE(2, verbose_stream() << "(pdr-inherit: " << mk_pp(it->m_key, m) << ")\n";); - add_property(it->m_key, it->m_value); - } - } - - // ---------------- - // model_node - - void model_node::set_closed() { - TRACE("pdr", tout << state() << "\n";); - pt().close(state()); - m_closed = true; - } - - void model_node::set_open() { - SASSERT(m_closed); - m_closed = false; - model_node* p = parent(); - while (p && p->is_closed()) { - p->m_closed = false; - p = p->parent(); - } - } - - void model_node::check_pre_closed() { - for (unsigned i = 0; i < children().size(); ++i) { - if (children()[i]->is_open()) return; - } - set_pre_closed(); - model_node* p = parent(); - while (p && p->is_1closed()) { - p->set_pre_closed(); - p = p->parent(); - } - } - - static bool is_ini(datalog::rule const& r) { - return r.get_uninterpreted_tail_size() == 0; - } - - datalog::rule* model_node::get_rule() { - if (m_rule) { - return const_cast(m_rule); - } - // only initial states are not set by the PDR search. - SASSERT(m_model.get()); - if (!m_model.get()) { - std::stringstream msg; - msg << "no model for node " << state(); - IF_VERBOSE(0, verbose_stream() << msg.str() << "\n";); - throw default_exception(msg.str()); - } - - datalog::rule const& rl1 = pt().find_rule(*m_model); - if (is_ini(rl1)) { - set_rule(&rl1); - return const_cast(m_rule); - } - ast_manager& m = pt().get_manager(); - // otherwise, the initial state is reachable. - ptr_vector const& rules = pt().rules(); - ptr_vector ini_rules; - expr_ref_vector tags(m); - expr_ref ini_tags(m), ini_state(m); - for (unsigned i = 0; i < rules.size(); ++i) { - datalog::rule* rl = rules[i]; - if (is_ini(*rl)) { - tags.push_back(pt().rule2tag(rl)); - } - } - SASSERT(!tags.empty()); - ini_tags = ::mk_or(tags); - ini_state = m.mk_and(ini_tags, pt().initial_state(), state()); - model_ref mdl; - pt().get_solver().set_model(&mdl); - TRACE("pdr", tout << ini_state << "\n";); - if (l_true != pt().get_solver().check_conjunction_as_assumptions(ini_state)) { - std::stringstream msg; - msg << "Unsatisfiable initial state: " << ini_state << "\n"; - display(msg, 2); - IF_VERBOSE(0, verbose_stream() << msg.str() << "\n";); - throw default_exception(msg.str()); - } - SASSERT(mdl.get()); - datalog::rule const& rl2 = pt().find_rule(*mdl); - SASSERT(is_ini(rl2)); - set_rule(&rl2); - pt().get_solver().set_model(nullptr); - return const_cast(m_rule); - } - - - void model_node::mk_instantiate(datalog::rule_ref& r0, datalog::rule_ref& r1, expr_ref_vector& binding) { - ast_manager& m = pt().get_manager(); - expr_ref_vector conjs(m); - obj_map model; - flatten_and(state(), conjs); - for (unsigned i = 0; i < conjs.size(); ++i) { - expr* e = conjs[i].get(), *e1, *e2; - if (m.is_eq(e, e1, e2)) { - if (m.is_value(e2)) { - model.insert(e1, e2); - } - else if (m.is_value(e1)) { - model.insert(e2, e1); - } - } - else if (m.is_not(e, e1)) { - model.insert(e1, m.mk_false()); - } - else { - model.insert(e, m.mk_true()); - } - } - r0 = get_rule(); - app_ref_vector& inst = pt().get_inst(r0); - TRACE("pdr", tout << state() << " instance: " << inst.size() << "\n";); - for (unsigned i = 0; i < inst.size(); ++i) { - expr* v; - if (model.find(inst[i].get(), v)) { - binding.push_back(v); - } - else { - binding.push_back(m.mk_var(i, m.get_sort(inst[i].get()))); - } - } - r1 = r0; - if (!inst.empty()) { - r1.get_manager().substitute(r1, binding.size(), binding.c_ptr()); - } - } - - - - std::ostream& model_node::display(std::ostream& out, unsigned indent) { - for (unsigned i = 0; i < indent; ++i) out << " "; - out << m_level << " " << m_pt.head()->get_name() << " " << (m_closed?"closed":"open") << "\n"; - for (unsigned i = 0; i < indent; ++i) out << " "; - out << " " << mk_pp(m_state, m_state.get_manager(), indent) << " " << m_state->get_id() << "\n"; - for (unsigned i = 0; i < children().size(); ++i) { - children()[i]->display(out, indent + 1); - } - return out; - } - - // return order of this node in the children of its parent - unsigned model_node::index() const { - model_node* p = parent(); - if (!p) return 0; - for (unsigned i = 0; i < p->children().size(); ++i) { - if (this == p->children()[i]) return i; - } - UNREACHABLE(); - return 0; - } - - // detach this node from a queue with the head root - // requires: root is a head of a queue - void model_node::dequeue(model_node*& root) { - TRACE("pdr", tout << this << " root: " << root << " " << state() << "\n";); - if (!m_next && !m_prev) return; - SASSERT(m_next); - SASSERT(m_prev); - SASSERT(children().empty()); - if (this == m_next) { - SASSERT(m_prev == this); - if (root == this) { - root = nullptr; - } - } - else { - m_next->m_prev = m_prev; - m_prev->m_next = m_next; - if (this == root) { - root = m_next; - } - } - TRACE("pdr", tout << "new root: " << root << "\n";); - m_prev = nullptr; - m_next = nullptr; - } - - - // insert node n after this in the queue - // requires: this is in a queue or this == n - void model_node::enqueue(model_node* n) { - TRACE("pdr", tout << n << " " << n->state() << "\n";); - SASSERT(!n->m_next); - SASSERT(!n->m_prev); - if (this == n) { - m_next = n; - m_prev = n; - } - else { - n->m_next = m_next; - m_next->m_prev = n; - m_next = n; - n->m_prev = this; - } - } - // ---------------- - // model_search - - /** - \brief Dequeue the next goal. - */ - model_node* model_search::next() { - if (!m_goal) { - return nullptr; - } - else { - model_node* result = m_goal; - result->dequeue(m_goal); - return result; - } - } - - - void model_search::add_leaf(model_node& n) { - SASSERT(n.children().empty()); - model_nodes ns; - model_nodes& nodes = cache(n).insert_if_not_there2(n.state(), ns)->get_data().m_value; - if (nodes.contains(&n)) { - return; - } - nodes.push_back(&n); - TRACE("pdr_verbose", tout << "add: " << n.level() << ": " << &n << " " << n.state() << "\n";); - if (nodes.size() == 1) { - set_leaf(n); - } - else { - n.set_pre_closed(); - } - } - - void model_search::set_leaf(model_node& n) { - // remove all children that n might have - erase_children(n, true); - SASSERT(n.is_open()); - enqueue_leaf(&n); - } - - void model_search::enqueue_leaf(model_node* n) { - TRACE("pdr_verbose", tout << "node: " << n << " " << n->state() << " goal: " << m_goal << "\n";); - SASSERT(n->is_open()); - // queue is empty, initialize it with n - if (!m_goal) { - m_goal = n; - m_goal->enqueue(n); - } - // insert n after m_goal - else if (m_bfs) { - m_goal->enqueue(n); - } - // insert n after m_goal()->next() - else { - m_goal->next()->enqueue(n); - } - } - - void model_search::set_root(model_node* root) { - reset(); - m_root = root; - SASSERT(cache(*root).empty()); - cache(*root).insert(root->state(), 1); - set_leaf(*root); - } - - obj_map >& model_search::cache(model_node const& n) { - unsigned l = n.orig_level(); - if (l >= m_cache.size()) { - m_cache.resize(l + 1); - } - return m_cache[l]; - } - - void model_search::erase_children(model_node& n, bool backtrack) { - ptr_vector todo, nodes; - todo.append(n.children()); - // detach n from queue - remove_goal(n); - // removes children - n.reset(); - while (!todo.empty()) { - model_node* m = todo.back(); - todo.pop_back(); - nodes.push_back(m); - todo.append(m->children()); - remove_node(*m, backtrack); - } - std::for_each(nodes.begin(), nodes.end(), delete_proc()); - } - - // removes node from the search tree and from the cache - void model_search::remove_node(model_node& n, bool backtrack) { - TRACE("pdr_verbose", tout << "remove: " << n.level() << ": " << &n << " " << n.state() << "\n";); - model_nodes& nodes = cache(n).find(n.state()); - nodes.erase(&n); - // detach n from m_goals - remove_goal(n); - // TBD: siblings would also fail if n is not a goal. - if (!nodes.empty() && backtrack && nodes[0]->children().empty() && nodes[0]->is_closed()) { - TRACE("pdr_verbose", for (unsigned i = 0; i < nodes.size(); ++i) n.display(tout << &n << "\n", 2);); - model_node* n1 = nodes[0]; - n1->set_open(); - enqueue_leaf(n1); - } - - if (!nodes.empty() && n.get_model_ptr() && backtrack) { - model_ref mr(n.get_model_ptr()); - nodes[0]->set_model(mr); - } - if (nodes.empty()) { - cache(n).remove(n.state()); - } - } - - // detach node n from the queue m_goal - void model_search::remove_goal(model_node& n) { - n.dequeue(m_goal); - } - - void model_search::well_formed() { - // each open leaf is in the set of m_goal. - ptr_vector nodes; - nodes.push_back(&get_root()); - for (unsigned i = 0; i < nodes.size(); ++i) { - model_node* n = nodes[i]; - if (!n->children().empty()) { - nodes.append(n->children()); - } - else if (n->is_open() && !n->is_goal() && n->parent()) { - TRACE("pdr", n->display(tout << "node " << n << " not found among leaves\n", 0); display(tout);); - UNREACHABLE(); - return; - } - } - if (m_goal) { - model_node* n = m_goal; - do { - if (!n->is_open() || !n->children().empty()) { - TRACE("pdr", n->display(tout << "invalid leaf\n", 0); - display(tout);); - UNREACHABLE(); - return; - } - n = n->next(); - } - while (m_goal != n); - } - - // each state appears in at most one goal per level. - bool found = true; - for (unsigned l = 0; m_goal && found; ++l) { - found = false; - obj_hashtable open_states; - model_node* n = m_goal; - do { - if (n->level() == l) { - found = true; - if (n->is_open()) { - if (open_states.contains(n->state())) { - TRACE("pdr", n->display(tout << "repeated leaf\n", 0); display(tout);); - UNREACHABLE(); - } - open_states.insert(n->state()); - } - } - n = n->next(); - } - while (m_goal != n); - } - // a node is open if and only if it contains an - // open child which is a goal. - for (unsigned i = 0; i < nodes.size(); ++i) { - model_node* n = nodes[i]; - if (!n->children().empty() && n->parent()) { - found = false; - for (unsigned j = 0; !found && j < n->children().size(); ++j) { - found = n->children()[j]->is_open(); - } - if (n->is_open() != found) { - TRACE("pdr", n->display(tout << "node in inconsistent state\n", 0); display(tout);); - UNREACHABLE(); - } - } - } - } - - unsigned model_search::num_goals() const { - model_node* n = m_goal; - unsigned num = 0; - if (n) { - do { - ++num; - n = n->next(); - } - while (n != m_goal); - } - return num; - } - - std::ostream& model_search::display(std::ostream& out) const { - if (m_root) { - m_root->display(out, 0); - } - out << "goals " << num_goals() << "\n"; - model_node* n = m_goal; - if (n) { - do { - n->display(out, 1); - n = n->next(); - } - while (n != m_goal); - } - return out; - } - - /** - \brief Ensure that all nodes in the tree have associated models. - get_trace and get_proof_trace rely on models to extract rules. - */ - void model_search::update_models() { - obj_map models; - obj_map rules; - ptr_vector todo; - todo.push_back(m_root); - while (!todo.empty()) { - model_node* n = todo.back(); - if (n->get_model_ptr()) { - models.insert(n->state(), n->get_model_ptr()); - rules.insert(n->state(), n->get_rule()); - } - todo.pop_back(); - todo.append(n->children().size(), n->children().c_ptr()); - } - - todo.push_back(m_root); - while (!todo.empty()) { - model_node* n = todo.back(); - model* md = nullptr; - if (!n->get_model_ptr()) { - if (models.find(n->state(), md)) { - TRACE("pdr", tout << n->state() << "\n";); - model_ref mr(md); - n->set_model(mr); - datalog::rule const* rule = rules.find(n->state()); - n->set_rule(rule); - } - else { - TRACE("pdr", tout << "no model for " << n->state() << "\n";); - IF_VERBOSE(1, n->display(verbose_stream() << "no model:\n", 0); - verbose_stream() << n->state() << "\n";); - } - } - else { - TRACE("pdr", tout << n->state() << "\n";); - } - todo.pop_back(); - todo.append(n->children().size(), n->children().c_ptr()); - } - } - - /** - Extract trace comprising of constraints - and predicates that are satisfied from facts to the query. - The resulting trace - */ - expr_ref model_search::get_trace(context const& ctx) { - pred_transformer& pt = get_root().pt(); - ast_manager& m = pt.get_manager(); - manager& pm = pt.get_pdr_manager(); - datalog::context& dctx = ctx.get_context(); - datalog::rule_manager& rm = dctx.get_rule_manager(); - expr_ref_vector constraints(m), predicates(m); - expr_ref tmp(m); - ptr_vector children; - unsigned deltas[2]; - datalog::rule_ref rule(rm), r0(rm); - model_node* n = m_root; - datalog::rule_counter& vc = rm.get_counter(); - substitution subst(m); - unifier unif(m); - rule = n->get_rule(); - unsigned max_var = vc.get_max_rule_var(*rule); - predicates.push_back(rule->get_head()); - children.push_back(n); - bool first = true; - update_models(); - while (!children.empty()) { - SASSERT(children.size() == predicates.size()); - expr_ref_vector binding(m); - n = children.back(); - children.pop_back(); - TRACE("pdr", n->display(tout, 0);); - n->mk_instantiate(r0, rule, binding); - - max_var = std::max(max_var, vc.get_max_rule_var(*rule)); - subst.reset(); - subst.reserve(2, max_var+1); - deltas[0] = 0; - deltas[1] = max_var+1; - - VERIFY(unif(predicates.back(), rule->get_head(), subst)); - for (unsigned i = 0; i < constraints.size(); ++i) { - subst.apply(2, deltas, expr_offset(constraints[i].get(), 0), tmp); - dctx.get_rewriter()(tmp); - constraints[i] = tmp; - } - for (unsigned i = 0; i < predicates.size(); ++i) { - subst.apply(2, deltas, expr_offset(predicates[i].get(), 0), tmp); - predicates[i] = tmp; - } - if (!first) { - constraints.push_back(predicates.back()); - } - first = false; - predicates.pop_back(); - for (unsigned i = rule->get_uninterpreted_tail_size(); i < rule->get_tail_size(); ++i) { - subst.apply(2, deltas, expr_offset(rule->get_tail(i), 1), tmp); - constraints.push_back(tmp); - } - for (unsigned i = 0; i < constraints.size(); ++i) { - max_var = std::max(vc.get_max_var(constraints[i].get()), max_var); - } - if (n->children().empty()) { - // nodes whose states are repeated - // in the search tree do not have children. - continue; - } - - SASSERT(n->children().size() == rule->get_uninterpreted_tail_size()); - - for (unsigned i = 0; i < rule->get_uninterpreted_tail_size(); ++i) { - subst.apply(2, deltas, expr_offset(rule->get_tail(i), 1), tmp); - predicates.push_back(tmp); - } - for (unsigned i = 0; i < predicates.size(); ++i) { - max_var = std::max(vc.get_max_var(predicates[i].get()), max_var); - } - - children.append(n->children()); - } - expr_safe_replace repl(m); - for (unsigned i = 0; i < constraints.size(); ++i) { - expr* e = constraints[i].get(), *e1, *e2; - if (m.is_eq(e, e1, e2) && is_var(e1) && is_ground(e2)) { - repl.insert(e1, e2); - } - else if (m.is_eq(e, e1, e2) && is_var(e2) && is_ground(e1)) { - repl.insert(e2, e1); - } - } - expr_ref_vector result(m); - for (unsigned i = 0; i < constraints.size(); ++i) { - expr_ref tmp(m); - tmp = constraints[i].get(); - repl(tmp); - dctx.get_rewriter()(tmp); - if (!m.is_true(tmp)) { - result.push_back(tmp); - } - } - return pm.mk_and(result); - } - - proof_ref model_search::get_proof_trace(context const& ctx) { - pred_transformer& pt = get_root().pt(); - ast_manager& m = pt.get_manager(); - datalog::context& dctx = ctx.get_context(); - datalog::rule_manager& rm = dctx.get_rule_manager(); - datalog::rule_unifier unif(dctx); - datalog::dl_decl_util util(m); - datalog::rule_ref r0(rm), r1(rm); - obj_map cache; - obj_map rules; - ptr_vector todo; - proof_ref_vector trail(m); - datalog::rule_ref_vector rules_trail(rm); - proof* pr = nullptr; - unif.set_normalize(true); - todo.push_back(m_root); - update_models(); - while (!todo.empty()) { - model_node* n = todo.back(); - TRACE("pdr", n->display(tout, 0);); - if (cache.find(n->state(), pr)) { - todo.pop_back(); - continue; - } - ptr_vector pfs; - ptr_vector rls; - ptr_vector const& chs = n->children(); - pfs.push_back(0); - rls.push_back(0); - for (unsigned i = 0; i < chs.size(); ++i) { - if (cache.find(chs[i]->state(), pr)) { - pfs.push_back(pr); - rls.push_back(rules.find(chs[i]->state())); - } - else { - todo.push_back(chs[i]); - } - } - if (pfs.size() != 1 + chs.size()) { - continue; - } - proof_ref rl(m); - expr_ref_vector binding(m); - n->mk_instantiate(r0, r1, binding); - proof_ref p1(m), p2(m); - p1 = r0->get_proof(); - IF_VERBOSE(0, if (!p1) r0->display(dctx, verbose_stream());); - SASSERT(p1); - pfs[0] = p1; - rls[0] = r1; - TRACE("pdr", - tout << "root: " << mk_pp(p1.get(), m) << "\n"; - for (unsigned i = 0; i < binding.size(); ++i) { - tout << mk_pp(binding[i].get(), m) << "\n"; - } - for (unsigned i = 1; i < pfs.size(); ++i) { - tout << mk_pp(pfs[i], m) << "\n"; - } - ); - datalog::rule_ref reduced_rule(rm), r3(rm); - reduced_rule = rls[0]; - // check if binding is identity. - bool binding_is_id = true; - for (unsigned i = 0; binding_is_id && i < binding.size(); ++i) { - expr* v = binding[i].get(); - binding_is_id = is_var(v) && to_var(v)->get_idx() == i; - } - if (rls.size() > 1 || !binding_is_id) { - expr_ref tmp(m); - vector substs; - svector > positions; - substs.push_back(binding); // TODO base substitution. - for (unsigned i = 1; i < rls.size(); ++i) { - datalog::rule& src = *rls[i]; - bool unified = unif.unify_rules(*reduced_rule, 0, src); - if (!unified) { - IF_VERBOSE(0, - verbose_stream() << "Could not unify rules: "; - reduced_rule->display(dctx, verbose_stream()); - src.display(dctx, verbose_stream());); - } - expr_ref_vector sub1 = unif.get_rule_subst(*reduced_rule, true); - TRACE("pdr", - for (unsigned k = 0; k < sub1.size(); ++k) { - tout << mk_pp(sub1[k].get(), m) << " "; - } - tout << "\n"; - ); - - for (unsigned j = 0; j < substs.size(); ++j) { - for (unsigned k = 0; k < substs[j].size(); ++k) { - var_subst(m, false)(substs[j][k].get(), sub1.size(), sub1.c_ptr(), tmp); - substs[j][k] = tmp; - } - while (substs[j].size() < sub1.size()) { - substs[j].push_back(sub1[substs[j].size()].get()); - } - } - - positions.push_back(std::make_pair(i,0)); - substs.push_back(unif.get_rule_subst(src, false)); - VERIFY(unif.apply(*reduced_rule.get(), 0, src, r3)); - reduced_rule = r3; - } - - expr_ref fml_concl(m); - rm.to_formula(*reduced_rule.get(), fml_concl); - p1 = m.mk_hyper_resolve(pfs.size(), pfs.c_ptr(), fml_concl, positions, substs); - - } - cache.insert(n->state(), p1); - rules.insert(n->state(), reduced_rule); - trail.push_back(p1); - rules_trail.push_back(reduced_rule); - todo.pop_back(); - } - return proof_ref(cache.find(m_root->state()), m); - } - - model_search::~model_search() { - TRACE("pdr", tout << "\n";); - reset(); - } - - void model_search::reset() { - if (m_root) { - erase_children(*m_root, false); - remove_node(*m_root, false); - dealloc(m_root); - m_root = nullptr; - } - m_cache.reset(); - } - - void model_search::backtrack_level(bool uses_level, model_node& n) { - SASSERT(m_root); - if (uses_level && m_root->level() > n.level()) { - IF_VERBOSE(2, verbose_stream() << "Increase level " << n.level() << "\n";); - n.increase_level(); - enqueue_leaf(&n); - } - else { - model_node* p = n.parent(); - if (p) { - set_leaf(*p); - } - } - DEBUG_CODE(well_formed();); - } - - // ---------------- - // context - - context::context( - smt_params& fparams, - fixedpoint_params const& params, - ast_manager& m - ) - : m_fparams(fparams), - m_params(params), - m(m), - m_context(nullptr), - m_pm(m_fparams, params.pdr_max_num_contexts(), m), - m_query_pred(m), - m_query(nullptr), - m_search(m_params.pdr_bfs_model_search()), - m_last_result(l_undef), - m_inductive_lvl(0), - m_expanded_lvl(0) - { - } - - context::~context() { - reset_core_generalizers(); - reset(); - } - - void context::reset(decl2rel& rels) { - decl2rel::iterator it = rels.begin(), end = rels.end(); - for (; it != end; ++it) { - dealloc(it->m_value); - } - rels.reset(); - } - - void context::reset(bool full) { - TRACE("pdr", tout << "reset\n";); - reset(m_rels); - if (full) { - reset(m_rels_tmp); - } - m_search.reset(); - m_query = nullptr; - m_last_result = l_undef; - m_inductive_lvl = 0; - } - - void context::init_rules(datalog::rule_set& rules, decl2rel& rels) { - m_context = &rules.get_context(); - // Allocate collection of predicate transformers - datalog::rule_set::decl2rules::iterator dit = rules.begin_grouped_rules(), dend = rules.end_grouped_rules(); - decl2rel::obj_map_entry* e; - for (; dit != dend; ++dit) { - func_decl* pred = dit->m_key; - TRACE("pdr", tout << mk_pp(pred, m) << "\n";); - SASSERT(!rels.contains(pred)); - e = rels.insert_if_not_there2(pred, alloc(pred_transformer, *this, get_pdr_manager(), pred)); - datalog::rule_vector const& pred_rules = *dit->m_value; - for (unsigned i = 0; i < pred_rules.size(); ++i) { - e->get_data().m_value->add_rule(pred_rules[i]); - } - } - TRACE("pdr", tout << "adding rules\n";); - datalog::rule_set::iterator rit = rules.begin(), rend = rules.end(); - for (; rit != rend; ++rit) { - datalog::rule* r = *rit; - pred_transformer* pt; - unsigned utz = r->get_uninterpreted_tail_size(); - for (unsigned i = 0; i < utz; ++i) { - func_decl* pred = r->get_decl(i); - if (!rels.find(pred, pt)) { - pt = alloc(pred_transformer, *this, get_pdr_manager(), pred); - rels.insert(pred, pt); - } - } - } - // Initialize use list dependencies - TRACE("pdr", tout << "initialize use list dependencies\n";); - decl2rel::iterator it = rels.begin(), end = rels.end(); - for (; it != end; ++it) { - func_decl* pred = it->m_key; - pred_transformer* pt = it->m_value, *pt_user; - obj_hashtable const& deps = rules.get_dependencies().get_deps(pred); - obj_hashtable::iterator itf = deps.begin(), endf = deps.end(); - for (; itf != endf; ++itf) { - TRACE("pdr", tout << mk_pp(pred, m) << " " << mk_pp(*itf, m) << "\n";); - pt_user = rels.find(*itf); - pt_user->add_use(pt); - } - } - - TRACE("pdr", tout << "initialize predicate transformers\n";); - // Initialize the predicate transformers. - it = rels.begin(), end = rels.end(); - for (; it != end; ++it) { - SASSERT(it->m_value); - pred_transformer& rel = *it->m_value; - rel.initialize(rels); - TRACE("pdr", rel.display(tout); ); - } - } - - void context::update_rules(datalog::rule_set& rules) { - TRACE("pdr", tout << "update rules\n";); - reset(m_rels_tmp); - init_core_generalizers(rules); - init_rules(rules, m_rels_tmp); - decl2rel::iterator it = m_rels_tmp.begin(), end = m_rels_tmp.end(); - for (; it != end; ++it) { - pred_transformer* pt = nullptr; - if (m_rels.find(it->m_key, pt)) { - it->m_value->inherit_properties(*pt); - } - } - reset(false); - it = m_rels_tmp.begin(), end = m_rels_tmp.end(); - for (; it != end; ++it) { - m_rels.insert(it->m_key, it->m_value); - } - m_rels_tmp.reset(); - TRACE("pdr", tout << "done update rules\n";); - } - - unsigned context::get_num_levels(func_decl* p) { - pred_transformer* pt = nullptr; - if (m_rels.find(p, pt)) { - return pt->get_num_levels(); - } - else { - IF_VERBOSE(10, verbose_stream() << "did not find predicate " << p->get_name() << "\n";); - return 0; - } - } - - expr_ref context::get_cover_delta(int level, func_decl* p_orig, func_decl* p) { - pred_transformer* pt = nullptr; - if (m_rels.find(p, pt)) { - return pt->get_cover_delta(p_orig, level); - } - else { - IF_VERBOSE(10, verbose_stream() << "did not find predicate " << p->get_name() << "\n";); - return expr_ref(m.mk_true(), m); - } - } - - void context::add_cover(int level, func_decl* p, expr* property) { - pred_transformer* pt = nullptr; - if (!m_rels.find(p, pt)) { - pt = alloc(pred_transformer, *this, get_pdr_manager(), p); - m_rels.insert(p, pt); - IF_VERBOSE(10, verbose_stream() << "did not find predicate " << p->get_name() << "\n";); - } - unsigned lvl = (level == -1)?infty_level:((unsigned)level); - pt->add_cover(lvl, property); - } - - class context::classifier_proc { - ast_manager& m; - arith_util a; - bool m_is_bool; - bool m_is_bool_arith; - bool m_has_arith; - bool m_is_dl; - bool m_is_utvpi; - public: - classifier_proc(ast_manager& m, datalog::rule_set& rules): - m(m), a(m), m_is_bool(true), m_is_bool_arith(true), m_has_arith(false), m_is_dl(false), m_is_utvpi(false) { - classify(rules); - } - void operator()(expr* e) { - if (m_is_bool) { - if (!m.is_bool(e)) { - m_is_bool = false; - } - else if (is_var(e)) { - // no-op. - } - else if (!is_app(e)) { - m_is_bool = false; - } - else if (to_app(e)->get_num_args() > 0 && - to_app(e)->get_family_id() != m.get_basic_family_id()) { - m_is_bool = false; - } - } - - m_has_arith = m_has_arith || a.is_int_real(e); - - if (m_is_bool_arith) { - if (!m.is_bool(e) && !a.is_int_real(e)) { - m_is_bool_arith = false; - } - else if (is_var(e)) { - // no-op - } - else if (!is_app(e)) { - m_is_bool_arith = false; - } - else if (to_app(e)->get_num_args() > 0 && - to_app(e)->get_family_id() != m.get_basic_family_id() && - to_app(e)->get_family_id() != a.get_family_id()) { - m_is_bool_arith = false; - } - } - } - - bool is_bool() const { return m_is_bool; } - - bool is_bool_arith() const { return m_is_bool_arith; } - - bool is_dl() const { return m_is_dl; } - - bool is_utvpi() const { return m_is_utvpi; } - - private: - - void classify(datalog::rule_set& rules) { - expr_fast_mark1 mark; - datalog::rule_set::iterator it = rules.begin(), end = rules.end(); - for (; it != end; ++it) { - datalog::rule& r = *(*it); - classify_pred(mark, r.get_head()); - unsigned utsz = r.get_uninterpreted_tail_size(); - for (unsigned i = 0; i < utsz; ++i) { - classify_pred(mark, r.get_tail(i)); - } - for (unsigned i = utsz; i < r.get_tail_size(); ++i) { - quick_for_each_expr(*this, mark, r.get_tail(i)); - } - } - mark.reset(); - - m_is_dl = false; - m_is_utvpi = false; - if (m_has_arith) { - ptr_vector forms; - for (it = rules.begin(); it != end; ++it) { - datalog::rule& r = *(*it); - unsigned utsz = r.get_uninterpreted_tail_size(); - forms.push_back(r.get_head()); - for (unsigned i = utsz; i < r.get_tail_size(); ++i) { - forms.push_back(r.get_tail(i)); - } - } - m_is_dl = is_difference_logic(m, forms.size(), forms.c_ptr()); - m_is_utvpi = m_is_dl || is_utvpi_logic(m, forms.size(), forms.c_ptr()); - } - } - - void classify_pred(expr_fast_mark1& mark, app* pred) { - for (unsigned i = 0; i < pred->get_num_args(); ++i) { - quick_for_each_expr(*this, mark, pred->get_arg(i)); - } - } - }; - - void context::validate_proof() { - std::stringstream msg; - 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()); - } - } - } - - void context::validate_search() { - expr_ref tr = m_search.get_trace(*this); - TRACE("pdr", tout << tr << "\n";); - smt::kernel solver(m, get_fparams()); - solver.assert_expr(tr); - lbool res = solver.check(); - if (res != l_true) { - std::stringstream msg; - msg << "rule validation failed when checking: " << tr; - IF_VERBOSE(0, verbose_stream() << msg.str() << "\n";); - throw default_exception(msg.str()); - } - } - - void context::validate_model() { - IF_VERBOSE(1, verbose_stream() << "(pdr.validate_model)\n";); - 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); - var_subst vs(m, false); - expr_free_vars fv; - for (auto const& kv : m_rels) { - ptr_vector const& rules = kv.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()); - svector names; - fv(tmp); - fv.set_default_sort(m.mk_bool_sort()); - for (unsigned i = 0; i < fv.size(); ++i) { - names.push_back(symbol(i)); - } - fv.reverse(); - if (!fv.empty()) { - tmp = m.mk_exists(fv.size(), fv.c_ptr(), names.c_ptr(), tmp); - } - smt::kernel solver(m, get_fparams()); - solver.assert_expr(tmp); - lbool res = solver.check(); - TRACE("pdr", tout << tmp << " " << res << "\n";); - 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()); - } - } - } - } - - 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; - } - } - - void context::reset_core_generalizers() { - std::for_each(m_core_generalizers.begin(), m_core_generalizers.end(), delete_proc()); - m_core_generalizers.reset(); - } - - void context::init_core_generalizers(datalog::rule_set& rules) { - reset_core_generalizers(); - classifier_proc classify(m, rules); - bool use_mc = m_params.pdr_use_multicore_generalizer(); - if (use_mc) { - m_core_generalizers.push_back(alloc(core_multi_generalizer, *this, 0)); - } - if (!classify.is_bool()) { - m.toggle_proof_mode(PGM_ENABLED); - 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 (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_eq2ineq = true; - } - else if (classify.is_utvpi()) { - IF_VERBOSE(1, verbose_stream() << "UTVPI\n";); - m_fparams.m_arith_mode = AS_UTVPI; - m_fparams.m_arith_eq2ineq = true; - } - else { - m_fparams.m_arith_mode = AS_ARITH; - m_fparams.m_arith_eq2ineq = false; - } - } - } - if (m_params.pdr_use_convex_closure_generalizer()) { - m_core_generalizers.push_back(alloc(core_convex_hull_generalizer, *this, true)); - } - 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.pdr_use_inductive_generalizer()) { - m_core_generalizers.push_back(alloc(core_bool_inductive_generalizer, *this, 0)); - } - if (m_params.pdr_inductive_reachability_check()) { - m_core_generalizers.push_back(alloc(core_induction_generalizer, *this)); - } - if (m_params.pdr_use_arith_inductive_generalizer()) { - m_core_generalizers.push_back(alloc(core_arith_inductive_generalizer, *this)); - } - - } - - void context::get_level_property(unsigned lvl, expr_ref_vector& res, vector& rs) { - decl2rel::iterator it = m_rels.begin(), end = m_rels.end(); - for (; it != end; ++it) { - pred_transformer* r = it->m_value; - if (r->head() == m_query_pred) { - continue; - } - expr_ref conj = r->get_formulas(lvl, false); - m_pm.formula_n2o(0, false, conj); - res.push_back(conj); - ptr_vector sig(r->head()->get_arity(), r->sig()); - rs.push_back(relation_info(m, r->head(), sig, conj)); - } - } - - void context::simplify_formulas() { - decl2rel::iterator it = m_rels.begin(), end = m_rels.end(); - for (; it != end; ++it) { - pred_transformer* r = it->m_value; - r->simplify_formulas(); - } - } - - lbool context::solve() { - TRACE("pdr", tout << "solve\n";); - m_last_result = l_undef; - try { - solve_impl(); - UNREACHABLE(); - } - catch (model_exception) { - IF_VERBOSE(1, verbose_stream() << "\n"; m_search.display(verbose_stream());); - m_last_result = l_true; - validate(); - - IF_VERBOSE(1, - if (m_params.print_boogie_certificate()) { - display_certificate(verbose_stream()); - }); - - return l_true; - } - catch (inductive_exception) { - simplify_formulas(); - m_last_result = l_false; - TRACE("pdr", display_certificate(tout);); - IF_VERBOSE(1, { - expr_ref_vector refs(m); - vector rs; - get_level_property(m_inductive_lvl, refs, rs); - model_converter_ref mc; - inductive_property ex(m, mc, rs); - verbose_stream() << ex.to_string(); - }); - - // upgrade invariants that are known to be inductive. - decl2rel::iterator it = m_rels.begin (), end = m_rels.end (); - for (; m_inductive_lvl > 0 && it != end; ++it) { - if (it->m_value->head() != m_query_pred) { - it->m_value->propagate_to_infinity (m_inductive_lvl); - } - } - validate(); - return l_false; - } - catch (unknown_exception) { - return l_undef; - } - UNREACHABLE(); - return l_undef; - } - - void context::checkpoint() { - if (m.canceled()) { - throw default_exception(Z3_CANCELED_MSG); - } - } - - /** - \brief retrieve answer. - */ - expr_ref context::get_answer() { - switch(m_last_result) { - case l_true: return mk_sat_answer(); - case l_false: return mk_unsat_answer(); - default: return expr_ref(m.mk_true(), m); - } - } - - model_ref context::get_model() { - SASSERT(m_last_result == l_false); - expr_ref_vector refs(m); - vector rs; - model_ref md; - get_level_property(m_inductive_lvl, refs, rs); - inductive_property ex(m, m_mc, rs); - ex.to_model(md); - return md; - } - - proof_ref context::get_proof() const { - scoped_proof _sc(m); - proof_ref proof(m); - SASSERT(m_last_result == l_true); - proof = m_search.get_proof_trace(*this); - TRACE("pdr", tout << "PDR trace: " << proof << "\n";); - apply(m, m_pc.get(), proof); - TRACE("pdr", tout << "PDR trace: " << proof << "\n";); - // proof_utils::push_instantiations_up(proof); - // TRACE("pdr", tout << "PDR up: " << proof << "\n";); - return proof; - } - - - /** - \brief Retrieve satisfying assignment with explanation. - */ - expr_ref context::mk_sat_answer() const { - if (m_params.generate_proof_trace()) { - proof_ref pr = get_proof(); - return expr_ref(pr.get(), m); - } - return m_search.get_trace(*this); - } - - expr_ref context::mk_unsat_answer() { - expr_ref_vector refs(m); - vector rs; - get_level_property(m_inductive_lvl, refs, rs); - inductive_property ex(m, const_cast(m_mc), rs); - return ex.to_expr(); - } - - void context::solve_impl() { - if (!m_rels.find(m_query_pred, m_query)) { - throw inductive_exception(); - } - unsigned lvl = 0; - bool reachable; - while (true) { - checkpoint(); - m_expanded_lvl = lvl; - reachable = check_reachability(lvl); - if (reachable) { - throw model_exception(); - } - if (lvl != 0) { - propagate(lvl); - } - lvl++; - m_stats.m_max_depth = std::max(m_stats.m_max_depth, lvl); - IF_VERBOSE(1,verbose_stream() << "Entering level "<level() << "\n";); - checkpoint(); - expand_node(*node); - } - return root->is_closed(); - } - - void context::close_node(model_node& n) { - n.set_closed(); - model_node* p = n.parent(); - while (p && p->is_1closed()) { - p->set_closed(); - p = p->parent(); - } - } - - - void context::expand_node(model_node& n) { - SASSERT(n.is_open()); - expr_ref_vector cube(m); - - if (n.level() < m_expanded_lvl) { - m_expanded_lvl = n.level(); - } - - 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); - } - else { - bool uses_level = true; - switch (expand_state(n, cube, uses_level)) { - case l_true: - if (n.level() == 0) { - TRACE("pdr", n.display(tout << "reachable at level 0\n", 0);); - close_node(n); - } - else { - TRACE("pdr", n.display(tout, 0);); - create_children(n); - } - break; - case l_false: { - core_generalizer::cores cores; - cores.push_back(std::make_pair(cube, uses_level)); - TRACE("pdr", tout << "cube:\n"; - for (unsigned j = 0; j < cube.size(); ++j) tout << mk_pp(cube[j].get(), m) << "\n";); - for (unsigned i = 0; !cores.empty() && i < m_core_generalizers.size(); ++i) { - core_generalizer::cores new_cores; - for (unsigned j = 0; j < cores.size(); ++j) { - (*m_core_generalizers[i])(n, cores[j].first, cores[j].second, new_cores); - } - cores.reset(); - cores.append(new_cores); - } - bool found_invariant = false; - for (unsigned i = 0; i < cores.size(); ++i) { - expr_ref_vector const& core = cores[i].first; - uses_level = cores[i].second; - found_invariant = !uses_level || found_invariant; - expr_ref ncore(m_pm.mk_not_and(core), m); - TRACE("pdr", tout << "invariant state: " << (uses_level?"":"(inductive) ") << mk_pp(ncore, m) << "\n";); - 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.pdr_flexible_trace(), n); - break; - } - case l_undef: { - TRACE("pdr", tout << "unknown state: " << mk_pp(m_pm.mk_and(cube), m) << "\n";); - IF_VERBOSE(1, verbose_stream() << "unknown state\n";); - throw unknown_exception(); - } - } - } - } - - // - // check if predicate transformer has a satisfiable predecessor state. - // returns either a satisfiable predecessor state or - // return a property that blocks state and is implied by the - // predicate transformer (or some unfolding of it). - // - lbool context::expand_state(model_node& n, expr_ref_vector& result, bool& uses_level) { - TRACE("pdr", - tout << "expand_state: " << n.pt().head()->get_name(); - tout << " level: " << n.level() << "\n"; - tout << mk_pp(n.state(), m) << "\n";); - - return n.pt().is_reachable(n, &result, uses_level); - } - - void context::propagate(unsigned max_prop_lvl) { - if (m_params.pdr_simplify_formulas_pre()) { - simplify_formulas(); - } - for (unsigned lvl = m_expanded_lvl; lvl <= max_prop_lvl; lvl++) { - checkpoint(); - bool all_propagated = true; - decl2rel::iterator it = m_rels.begin(), end = m_rels.end(); - for (; it != end; ++it) { - checkpoint(); - pred_transformer& r = *it->m_value; - all_propagated = r.propagate_to_next_level(lvl) && all_propagated; - } - CASSERT("pdr", check_invariant(lvl)); - - if (all_propagated && lvl == max_prop_lvl) { - m_inductive_lvl = lvl; - throw inductive_exception(); - } - } - if (m_params.pdr_simplify_formulas_post()) { - simplify_formulas(); - } - } - - - /** - \brief create children states from model cube. - - Introduce the shorthands: - - - T(x0,x1,x) for transition - - phi(x) for n.state() - - M(x0,x1,x) for n.model() - - Assumptions: - M => phi & T - - In other words, - 1. phi & T is implied by M - - Goal is to find phi0(x0), phi1(x1) such that: - - phi(x) & phi0(x0) & phi1(x1) => T(x0, x1, x) - - Strategy: - - - Extract literals from T & phi using ternary simulation with M. - - resulting formula is Phi. - - - perform cheap existential quantifier elimination on - Phi <- exists x . Phi(x0,x1,x) - (e.g., destructive equality resolution) - - - Sub-strategy 1: rename remaining x to fresh variables. - - Sub-strategy 2: replace remaining x to M(x). - - - For each literal L in result: - - - if L is x0 pure, add L to L0 - - if L is x1 pure, add L to L1 - - if L mixes x0, x1, add x1 = M(x1) to L1, add L(x1 |-> M(x1)) to L0 - - - Create sub-goals for L0 and L1. - - */ - void context::create_children(model_node& n) { - SASSERT(n.level() > 0); - 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"; - model_smt2_pp(tout, m, *M, 0); - tout << "\n"; - tout << "Transition:\n" << mk_pp(T, m) << "\n"; - tout << "Phi:\n" << mk_pp(phi, m) << "\n";); - - model_implicant mev(m); - expr_ref_vector mdl(m), forms(m), Phi(m); - forms.push_back(T); - forms.push_back(phi); - flatten_and(forms); - ptr_vector forms1(forms.size(), forms.c_ptr()); - if (use_model_generalizer) { - Phi.append(mev.minimize_model(forms1, M)); - } - else { - Phi.append(mev.minimize_literals(forms1, M)); - } - ptr_vector preds; - pt.find_predecessors(r, preds); - pt.remove_predecessors(Phi); - - app_ref_vector vars(m); - unsigned sig_size = pt.head()->get_arity(); - for (unsigned i = 0; i < sig_size; ++i) { - vars.push_back(m.mk_const(m_pm.o2n(pt.sig(i), 0))); - } - ptr_vector& aux_vars = pt.get_aux_vars(r); - vars.append(aux_vars.size(), aux_vars.c_ptr()); - - scoped_ptr rep; - qe_lite qe(m, m_params.p); - expr_ref phi1 = m_pm.mk_and(Phi); - qe(vars, phi1); - TRACE("pdr", tout << "Eliminated\n" << mk_pp(phi1, m) << "\n";); - if (!use_model_generalizer) { - reduce_disequalities(*M, 3, phi1); - TRACE("pdr", tout << "Reduced-eq\n" << mk_pp(phi1, m) << "\n";); - } - get_context().get_rewriter()(phi1); - - TRACE("pdr", - tout << "Vars:\n"; - for (unsigned i = 0; i < vars.size(); ++i) { - tout << mk_pp(vars[i].get(), m) << "\n"; - } - tout << "Literals\n"; - tout << mk_pp(m_pm.mk_and(Phi), m) << "\n"; - tout << "Reduced\n" << mk_pp(phi1, m) << "\n";); - - if (!vars.empty()) { - // also fresh names for auxiliary variables in body? - expr_substitution sub(m); - expr_ref tmp(m); - proof_ref pr(m); - pr = m.mk_asserted(m.mk_true()); - for (unsigned i = 0; i < vars.size(); ++i) { - tmp = mev.eval(M, vars[i].get()); - sub.insert(vars[i].get(), tmp, pr); - } - if (!rep) rep = mk_expr_simp_replacer(m); - rep->set_substitution(&sub); - (*rep)(phi1); - TRACE("pdr", tout << "Projected:\n" << mk_pp(phi1, m) << "\n";); - } - Phi.reset(); - flatten_and(phi1, Phi); - unsigned_vector indices; - vector child_states; - child_states.resize(preds.size(), expr_ref_vector(m)); - for (unsigned i = 0; i < Phi.size(); ++i) { - m_pm.collect_indices(Phi[i].get(), indices); - if (indices.size() == 0) { - IF_VERBOSE(3, verbose_stream() << "Skipping " << mk_pp(Phi[i].get(), m) << "\n";); - } - else if (indices.size() == 1) { - child_states[indices.back()].push_back(Phi[i].get()); - } - else { - expr_substitution sub(m); - expr_ref tmp(m); - proof_ref pr(m); - pr = m.mk_asserted(m.mk_true()); - vector > vars; - m_pm.collect_variables(Phi[i].get(), vars); - SASSERT(vars.size() == indices.back()+1); - for (unsigned j = 1; j < indices.size(); ++j) { - ptr_vector const& vs = vars[indices[j]]; - for (unsigned k = 0; k < vs.size(); ++k) { - tmp = mev.eval(M, vs[k]); - sub.insert(vs[k], tmp, pr); - child_states[indices[j]].push_back(m.mk_eq(vs[k], tmp)); - } - } - tmp = Phi[i].get(); - if (!rep) rep = mk_expr_simp_replacer(m); - rep->set_substitution(&sub); - (*rep)(tmp); - child_states[indices[0]].push_back(tmp); - } - - } - - expr_ref n_cube(m); - for (unsigned i = 0; i < preds.size(); ++i) { - pred_transformer& pt = *m_rels.find(preds[i]); - SASSERT(pt.head() == preds[i]); - expr_ref o_cube = m_pm.mk_and(child_states[i]); - m_pm.formula_o2n(o_cube, n_cube, i); - model_node* child = alloc(model_node, &n, n_cube, pt, n.level()-1); - ++m_stats.m_num_nodes; - m_search.add_leaf(*child); - IF_VERBOSE(2, verbose_stream() << "Predecessor: " << mk_pp(n_cube, m) << " " << (child->is_closed()?"closed":"open") << "\n";); - m_stats.m_max_depth = std::max(m_stats.m_max_depth, child->depth()); - } - n.check_pre_closed(); - TRACE("pdr", m_search.display(tout);); - } - - void context::collect_statistics(statistics& st) const { - decl2rel::iterator it = m_rels.begin(), end = m_rels.end(); - for (it = m_rels.begin(); it != end; ++it) { - it->m_value->collect_statistics(st); - } - st.update("PDR num unfoldings", m_stats.m_num_nodes); - st.update("PDR max depth", m_stats.m_max_depth); - st.update("PDR inductive level", m_inductive_lvl); - m_pm.collect_statistics(st); - - for (unsigned i = 0; i < m_core_generalizers.size(); ++i) { - m_core_generalizers[i]->collect_statistics(st); - } - } - - void context::reset_statistics() { - decl2rel::iterator it = m_rels.begin(), end = m_rels.end(); - for (it = m_rels.begin(); it != end; ++it) { - it->m_value->reset_statistics(); - } - m_stats.reset(); - m_pm.reset_statistics(); - - for (unsigned i = 0; i < m_core_generalizers.size(); ++i) { - m_core_generalizers[i]->reset_statistics(); - } - - } - - - std::ostream& context::display(std::ostream& out) const { - decl2rel::iterator it = m_rels.begin(), end = m_rels.end(); - for (; it != end; ++it) { - it->m_value->display(out); - } - m_search.display(out); - return out; - } - - bool context::check_invariant(unsigned lvl) { - decl2rel::iterator it = m_rels.begin(), end = m_rels.end(); - for (; it != end; ++it) { - checkpoint(); - if (!check_invariant(lvl, it->m_key)) { - return false; - } - } - return true; - } - - bool context::check_invariant(unsigned lvl, func_decl* fn) { - smt::kernel ctx(m, m_fparams); - pred_transformer& pt = *m_rels.find(fn); - expr_ref_vector conj(m); - expr_ref inv = pt.get_formulas(next_level(lvl), false); - if (m.is_true(inv)) return true; - pt.add_premises(m_rels, lvl, conj); - conj.push_back(m.mk_not(inv)); - expr_ref fml(m.mk_and(conj.size(), conj.c_ptr()), m); - ctx.assert_expr(fml); - lbool result = ctx.check(); - TRACE("pdr", tout << "Check invariant level: " << lvl << " " << result << "\n" << mk_pp(fml, m) << "\n";); - return result == l_false; - } - - void context::display_certificate(std::ostream& strm) { - switch(m_last_result) { - case l_false: { - expr_ref_vector refs(m); - vector rs; - get_level_property(m_inductive_lvl, refs, rs); - inductive_property ex(m, const_cast(m_mc), rs); - strm << ex.to_string(); - break; - } - case l_true: { - if (m_params.print_boogie_certificate()) { - datalog::boogie_proof bp(m); - bp.set_proof(get_proof()); - bp.set_model(nullptr); - bp.pp(strm); - } - else { - strm << mk_pp(mk_sat_answer(), m); - } - break; - } - case l_undef: { - strm << "unknown"; - break; - } - } - } - -} diff --git a/src/muz/pdr/pdr_context.h b/src/muz/pdr/pdr_context.h deleted file mode 100644 index ebaa3f257..000000000 --- a/src/muz/pdr/pdr_context.h +++ /dev/null @@ -1,448 +0,0 @@ -/*++ -Copyright (c) 2011 Microsoft Corporation - -Module Name: - - pdr_context.h - -Abstract: - - PDR for datalog - -Author: - - Nikolaj Bjorner (nbjorner) 2011-11-20. - -Revision History: - ---*/ - -#ifndef PDR_CONTEXT_H_ -#define PDR_CONTEXT_H_ - -#ifdef _CYGWIN -#undef min -#undef max -#endif -#include -#include "muz/pdr/pdr_manager.h" -#include "muz/pdr/pdr_prop_solver.h" -#include "muz/pdr/pdr_reachable_cache.h" -#include "muz/base/fixedpoint_params.hpp" - - -namespace datalog { - class rule_set; - class context; -}; - -namespace pdr { - - class pred_transformer; - class model_node; - class context; - - typedef obj_map rule2inst; - typedef obj_map decl2rel; - - - // - // Predicate transformer state. - // A predicate transformer corresponds to the - // set of rules that have the same head predicates. - // - - class pred_transformer { - - struct stats { - unsigned m_num_propagations; - stats() { reset(); } - void reset() { memset(this, 0, sizeof(*this)); } - }; - - typedef obj_map rule2expr; - typedef obj_map > rule2apps; - - manager& pm; // pdr-manager - ast_manager& m; // manager - context& ctx; - - func_decl_ref m_head; // predicate - func_decl_ref_vector m_sig; // signature - ptr_vector m_use; // places where 'this' is referenced. - ptr_vector m_rules; // rules used to derive transformer - prop_solver m_solver; // solver context - vector m_levels; // level formulas - expr_ref_vector m_invariants; // properties that are invariant. - obj_map m_prop2level; // map property to level where it occurs. - obj_map m_tag2rule; // map tag predicate to rule. - rule2expr m_rule2tag; // map rule to predicate tag. - rule2inst m_rule2inst; // map rules to instantiations of indices - rule2expr m_rule2transition; // map rules to transition - rule2apps m_rule2vars; // map rule to auxiliary variables - expr_ref m_transition; // transition relation. - expr_ref m_initial_state; // initial state. - reachable_cache m_reachable; - ptr_vector m_predicates; - stats m_stats; - - void init_sig(); - void ensure_level(unsigned level); - bool add_property1(expr * lemma, unsigned lvl); // add property 'p' to state at level lvl. - void add_child_property(pred_transformer& child, expr* lemma, unsigned lvl); - void mk_assumptions(func_decl* head, expr* fml, expr_ref_vector& result); - - // Initialization - void init_rules(decl2rel const& pts, expr_ref& init, expr_ref& transition); - void init_rule(decl2rel const& pts, datalog::rule const& rule, expr_ref& init, - ptr_vector& rules, expr_ref_vector& transition); - void init_atom(decl2rel const& pts, app * atom, app_ref_vector& var_reprs, expr_ref_vector& conj, unsigned tail_idx); - - void simplify_formulas(tactic& tac, expr_ref_vector& fmls); - - // Debugging - bool check_filled(app_ref_vector const& v) const; - - void add_premises(decl2rel const& pts, unsigned lvl, datalog::rule& rule, expr_ref_vector& r); - - public: - pred_transformer(context& ctx, manager& pm, func_decl* head); - ~pred_transformer(); - - void add_rule(datalog::rule* r) { m_rules.push_back(r); } - void add_use(pred_transformer* pt) { if (!m_use.contains(pt)) m_use.insert(pt); } - void initialize(decl2rel const& pts); - - func_decl* head() const { return m_head; } - ptr_vector const& rules() const { return m_rules; } - func_decl* sig(unsigned i) { init_sig(); return m_sig[i].get(); } // signature - func_decl* const* sig() { init_sig(); return m_sig.c_ptr(); } - unsigned sig_size() { init_sig(); return m_sig.size(); } - expr* transition() const { return m_transition; } - expr* initial_state() const { return m_initial_state; } - expr* rule2tag(datalog::rule const* r) { return m_rule2tag.find(r); } - 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; - - void collect_statistics(statistics& st) const; - void reset_statistics(); - - bool is_reachable(expr* state); - void remove_predecessors(expr_ref_vector& literals); - void find_predecessors(datalog::rule const& r, ptr_vector& predicates) const; - datalog::rule const& find_rule(model_core const& model) const; - expr* get_transition(datalog::rule const& r) { return m_rule2transition.find(&r); } - ptr_vector& get_aux_vars(datalog::rule const& r) { return m_rule2vars.find(&r); } - - bool propagate_to_next_level(unsigned level); - void propagate_to_infinity(unsigned level); - void add_property(expr * lemma, unsigned lvl); // add property 'p' to state at level. - - lbool is_reachable(model_node& n, expr_ref_vector* core, bool& uses_level); - bool is_invariant(unsigned level, expr* co_state, bool inductive, bool& assumes_level, expr_ref_vector* core = nullptr); - bool check_inductive(unsigned level, expr_ref_vector& state, bool& assumes_level); - - expr_ref get_formulas(unsigned level, bool add_axioms); - - void simplify_formulas(); - - expr_ref get_propagation_formula(decl2rel const& pts, unsigned level); - - manager& get_pdr_manager() const { return pm; } - ast_manager& get_manager() const { return m; } - - void add_premises(decl2rel const& pts, unsigned lvl, expr_ref_vector& r); - - void close(expr* e); - - app_ref_vector& get_inst(datalog::rule const* r) { return *m_rule2inst.find(r);} - - void inherit_properties(pred_transformer& other); - - void ground_free_vars(expr* e, app_ref_vector& vars, ptr_vector& aux_vars); - - prop_solver& get_solver() { return m_solver; } - prop_solver const& get_solver() const { return m_solver; } - - void set_use_farkas(bool f) { get_solver().set_use_farkas(f); } - bool get_use_farkas() const { return get_solver().get_use_farkas(); } - class scoped_farkas { - bool m_old; - pred_transformer& m_p; - public: - scoped_farkas(pred_transformer& p, bool v): m_old(p.get_use_farkas()), m_p(p) { - p.set_use_farkas(v); - } - ~scoped_farkas() { m_p.set_use_farkas(m_old); } - }; - - }; - - - // structure for counter-example search. - class model_node { - model_node* m_parent; - model_node* m_next; - model_node* m_prev; - pred_transformer& m_pt; - expr_ref m_state; - model_ref m_model; - ptr_vector m_children; - unsigned m_level; - unsigned m_orig_level; - unsigned m_depth; - bool m_closed; - datalog::rule const* m_rule; - public: - model_node(model_node* parent, expr_ref& state, pred_transformer& pt, unsigned level): - m_parent(parent), m_next(nullptr), m_prev(nullptr), m_pt(pt), m_state(state), m_model(nullptr), - m_level(level), m_orig_level(level), m_depth(0), m_closed(false), m_rule(nullptr) { - model_node* p = m_parent; - if (p) { - p->m_children.push_back(this); - SASSERT(p->m_level == level+1); - SASSERT(p->m_level > 0); - m_depth = p->m_depth+1; - if (p && p->is_closed()) { - p->set_open(); - } - } - } - void set_model(model_ref& m) { m_model = m; } - unsigned level() const { return m_level; } - unsigned orig_level() const { return m_orig_level; } - unsigned depth() const { return m_depth; } - void increase_level() { ++m_level; } - expr_ref const& state() const { return m_state; } - ptr_vector const& children() { return m_children; } - pred_transformer& pt() const { return m_pt; } - model_node* parent() const { return m_parent; } - model* get_model_ptr() const { return m_model.get(); } - model const& get_model() const { return *m_model; } - unsigned index() const; - - bool is_closed() const { return m_closed; } - bool is_open() const { return !is_closed(); } - - bool is_1closed() { - if (is_closed()) return true; - if (m_children.empty()) return false; - for (unsigned i = 0; i < m_children.size(); ++i) { - if (m_children[i]->is_open()) return false; - } - return true; - } - - void check_pre_closed(); - void set_closed(); - void set_open(); - void set_pre_closed() { TRACE("pdr", tout << state() << "\n";); m_closed = true; } - void reset() { m_children.reset(); } - - void set_rule(datalog::rule const* r) { m_rule = r; } - datalog::rule* get_rule(); - - void mk_instantiate(datalog::rule_ref& r0, datalog::rule_ref& r1, expr_ref_vector& binding); - - std::ostream& display(std::ostream& out, unsigned indent); - - void dequeue(model_node*& root); - void enqueue(model_node* n); - model_node* next() const { return m_next; } - bool is_goal() const { return nullptr != next(); } - }; - - class model_search { - typedef ptr_vector model_nodes; - bool m_bfs; - model_node* m_root; - model_node* m_goal; - vector > m_cache; - obj_map& cache(model_node const& n); - void erase_children(model_node& n, bool backtrack); - void remove_node(model_node& n, bool backtrack); - void enqueue_leaf(model_node* n); // add leaf to priority queue. - void update_models(); - void set_leaf(model_node& n); // Set node as leaf, remove children. - unsigned num_goals() const; - - public: - model_search(bool bfs): m_bfs(bfs), m_root(nullptr), m_goal(nullptr) {} - ~model_search(); - - void reset(); - model_node* next(); - void add_leaf(model_node& n); // add fresh node. - - 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); - proof_ref get_proof_trace(context const& ctx); - void backtrack_level(bool uses_level, model_node& n); - void remove_goal(model_node& n); - - void well_formed(); - }; - - struct model_exception { }; - struct inductive_exception {}; - - - // 'state' is unsatisfiable at 'level' with 'core'. - // Minimize or weaken core. - class core_generalizer { - protected: - context& m_ctx; - public: - typedef vector > cores; - core_generalizer(context& ctx): m_ctx(ctx) {} - virtual ~core_generalizer() {} - virtual void operator()(model_node& n, expr_ref_vector& core, bool& uses_level) = 0; - virtual void operator()(model_node& n, expr_ref_vector const& core, bool uses_level, cores& new_cores) { - new_cores.push_back(std::make_pair(core, uses_level)); - if (!core.empty()) { - (*this)(n, new_cores.back().first, new_cores.back().second); - } - } - virtual void collect_statistics(statistics& st) const {} - virtual void reset_statistics() {} - }; - - class context { - - struct stats { - unsigned m_num_nodes; - unsigned m_max_depth; - stats() { reset(); } - void reset() { memset(this, 0, sizeof(*this)); } - }; - - smt_params& m_fparams; - fixedpoint_params const& m_params; - ast_manager& m; - datalog::context* m_context; - manager m_pm; - decl2rel m_rels; // Map from relation predicate to fp-operator. - decl2rel m_rels_tmp; - func_decl_ref m_query_pred; - pred_transformer* m_query; - mutable model_search m_search; - lbool m_last_result; - unsigned m_inductive_lvl; - unsigned m_expanded_lvl; - ptr_vector m_core_generalizers; - stats m_stats; - model_converter_ref m_mc; - proof_converter_ref m_pc; - - // Functions used by search. - void solve_impl(); - bool check_reachability(unsigned level); - void propagate(unsigned max_prop_lvl); - void close_node(model_node& n); - void check_pre_closed(model_node& n); - void expand_node(model_node& n); - lbool expand_state(model_node& n, expr_ref_vector& cube, bool& uses_level); - void create_children(model_node& n); - expr_ref mk_sat_answer() const; - expr_ref mk_unsat_answer(); - - // Generate inductive property - void get_level_property(unsigned lvl, expr_ref_vector& res, vector & rs); - - - // Initialization - class classifier_proc; - void init_core_generalizers(datalog::rule_set& rules); - - bool check_invariant(unsigned lvl); - bool check_invariant(unsigned lvl, func_decl* fn); - - void checkpoint(); - - void init_rules(datalog::rule_set& rules, decl2rel& transformers); - - void simplify_formulas(); - - void reset_core_generalizers(); - - void reset(decl2rel& rels); - - void validate(); - void validate_proof(); - void validate_search(); - void validate_model(); - - public: - - /** - Initial values of predicates are stored in corresponding relations in dctx. - - We check whether there is some reachable state of the relation checked_relation. - */ - context( - smt_params& fparams, - fixedpoint_params const& params, - ast_manager& m); - - ~context(); - - smt_params& get_fparams() const { return m_fparams; } - 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; } - pred_transformer& get_pred_transformer(func_decl* p) const { return *m_rels.find(p); } - datalog::context& get_context() const { SASSERT(m_context); return *m_context; } - expr_ref get_answer(); - - bool is_dl() const { return m_fparams.m_arith_mode == AS_DIFF_LOGIC; } - bool is_utvpi() const { return m_fparams.m_arith_mode == AS_UTVPI; } - - void collect_statistics(statistics& st) const; - void reset_statistics(); - - std::ostream& display(std::ostream& strm) const; - - void display_certificate(std::ostream& strm); - - lbool solve(); - - void reset(bool full = true); - - void set_query(func_decl* q) { m_query_pred = q; } - - void set_unsat() { m_last_result = l_false; } - - void set_model_converter(model_converter_ref& mc) { m_mc = mc; } - - model_converter_ref get_model_converter() { return m_mc; } - - void set_proof_converter(proof_converter_ref& pc) { m_pc = pc; } - - void update_rules(datalog::rule_set& rules); - - void set_axioms(expr* axioms) { m_pm.set_background(axioms); } - - unsigned get_num_levels(func_decl* p); - - expr_ref get_cover_delta(int level, func_decl* p_orig, func_decl* p); - - void add_cover(int level, func_decl* pred, expr* property); - - model_ref get_model(); - - proof_ref get_proof() const; - - model_node& get_root() const { return m_search.get_root(); } - - }; - -}; - -#endif diff --git a/src/muz/pdr/pdr_dl_interface.cpp b/src/muz/pdr/pdr_dl_interface.cpp deleted file mode 100644 index 27ce0500c..000000000 --- a/src/muz/pdr/pdr_dl_interface.cpp +++ /dev/null @@ -1,225 +0,0 @@ -/*++ -Copyright (c) 2011 Microsoft Corporation - -Module Name: - - pdr_dl.cpp - -Abstract: - - SMT2 interface for the datalog PDR - -Author: - - Krystof Hoder (t-khoder) 2011-9-22. - -Revision History: - ---*/ - -#include "muz/base/dl_context.h" -#include "muz/transforms/dl_mk_coi_filter.h" -#include "muz/base/dl_rule.h" -#include "muz/base/dl_rule_transformer.h" -#include "muz/pdr/pdr_context.h" -#include "muz/pdr/pdr_dl_interface.h" -#include "muz/base/dl_rule_set.h" -#include "muz/transforms/dl_mk_slice.h" -#include "muz/transforms/dl_mk_unfold.h" -#include "muz/transforms/dl_mk_coalesce.h" -#include "muz/transforms/dl_transforms.h" -#include "ast/scoped_proof.h" -#include "model/model_smt2_pp.h" - -using namespace pdr; - -dl_interface::dl_interface(datalog::context& ctx) : - engine_base(ctx.get_manager(), "pdr"), - m_ctx(ctx), - m_pdr_rules(ctx), - m_old_rules(ctx), - m_context(nullptr), - m_refs(ctx.get_manager()) { - m_context = alloc(pdr::context, ctx.get_fparams(), ctx.get_params(), ctx.get_manager()); -} - - -dl_interface::~dl_interface() { - dealloc(m_context); -} - - -// -// Check if the new rules are weaker so that we can -// re-use existing context. -// -void dl_interface::check_reset() { - datalog::rule_set const& new_rules = m_ctx.get_rules(); - datalog::rule_ref_vector const& old_rules = m_old_rules.get_rules(); - bool is_subsumed = !old_rules.empty(); - for (unsigned i = 0; is_subsumed && i < new_rules.get_num_rules(); ++i) { - is_subsumed = false; - for (unsigned j = 0; !is_subsumed && j < old_rules.size(); ++j) { - if (m_ctx.check_subsumes(*old_rules[j], *new_rules.get_rule(i))) { - is_subsumed = true; - } - } - if (!is_subsumed) { - TRACE("pdr", new_rules.get_rule(i)->display(m_ctx, tout << "Fresh rule ");); - m_context->reset(); - } - } - m_old_rules.replace_rules(new_rules); -} - - -lbool dl_interface::query(expr * query) { - //we restore the initial state in the datalog context - m_ctx.ensure_opened(); - m_refs.reset(); - m_pred2slice.reset(); - ast_manager& m = m_ctx.get_manager(); - datalog::rule_manager& rm = m_ctx.get_rule_manager(); - datalog::rule_set& rules0 = m_ctx.get_rules(); - - datalog::rule_set old_rules(rules0); - func_decl_ref query_pred(m); - rm.mk_query(query, rules0); - expr_ref bg_assertion = m_ctx.get_background_assertion(); - - check_reset(); - - TRACE("pdr", - if (!m.is_true(bg_assertion)) { - tout << "axioms:\n"; - tout << mk_pp(bg_assertion, m) << "\n"; - } - tout << "query: " << mk_pp(query, m) << "\n"; - tout << "rules:\n"; - m_ctx.display_rules(tout); - ); - - - apply_default_transformation(m_ctx); - - 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); - m_ctx.transform_rules(transformer); - - // track sliced predicates. - obj_map const& preds = slice->get_predicates(); - obj_map::iterator it = preds.begin(); - obj_map::iterator end = preds.end(); - for (; it != end; ++it) { - m_pred2slice.insert(it->m_key, it->m_value); - m_refs.push_back(it->m_key); - m_refs.push_back(it->m_value); - } - } - - 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().xform_coalesce_rules()) { - m_ctx.transform_rules(transf1); - } - while (num_unfolds > 0) { - m_ctx.transform_rules(transf2); - --num_unfolds; - } - } - - const datalog::rule_set& rules = m_ctx.get_rules(); - if (rules.get_output_predicates().empty()) { - m_context->set_unsat(); - return l_false; - } - - query_pred = rules.get_output_predicate(); - - TRACE("pdr", - tout << "rules:\n"; - m_ctx.display_rules(tout); - m_ctx.display_smt2(0, 0, tout); - ); - - IF_VERBOSE(2, m_ctx.display_rules(verbose_stream());); - m_pdr_rules.replace_rules(rules); - m_pdr_rules.close(); - m_ctx.record_transformed_rules(); - m_ctx.reopen(); - m_ctx.replace_rules(old_rules); - - - scoped_restore_proof _sc(m); // update_rules may overwrite the proof mode. - - m_context->set_proof_converter(m_ctx.get_proof_converter()); - m_context->set_model_converter(m_ctx.get_model_converter()); - m_context->set_query(query_pred); - m_context->set_axioms(bg_assertion); - m_context->update_rules(m_pdr_rules); - - if (m_pdr_rules.get_rules().empty()) { - m_context->set_unsat(); - IF_VERBOSE(1, model_smt2_pp(verbose_stream(), m, *m_context->get_model(),0);); - return l_false; - } - - return m_context->solve(); - -} - -expr_ref dl_interface::get_cover_delta(int level, func_decl* pred_orig) { - func_decl* pred = pred_orig; - m_pred2slice.find(pred_orig, pred); - SASSERT(pred); - return m_context->get_cover_delta(level, pred_orig, pred); -} - -void dl_interface::add_cover(int level, func_decl* pred, expr* property) { - 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); -} - -unsigned dl_interface::get_num_levels(func_decl* pred) { - m_pred2slice.find(pred, pred); - SASSERT(pred); - return m_context->get_num_levels(pred); -} - -void dl_interface::collect_statistics(statistics& st) const { - m_context->collect_statistics(st); -} - -void dl_interface::reset_statistics() { - m_context->reset_statistics(); -} - -void dl_interface::display_certificate(std::ostream& out) const { - m_context->display_certificate(out); -} - -expr_ref dl_interface::get_answer() { - return m_context->get_answer(); -} - - - -void dl_interface::updt_params() { - dealloc(m_context); - m_context = alloc(pdr::context, m_ctx.get_fparams(), m_ctx.get_params(), m_ctx.get_manager()); -} - -model_ref dl_interface::get_model() { - return m_context->get_model(); -} - -proof_ref dl_interface::get_proof() { - return m_context->get_proof(); -} diff --git a/src/muz/pdr/pdr_dl_interface.h b/src/muz/pdr/pdr_dl_interface.h deleted file mode 100644 index 1a0b04635..000000000 --- a/src/muz/pdr/pdr_dl_interface.h +++ /dev/null @@ -1,78 +0,0 @@ -/*++ -Copyright (c) 2011 Microsoft Corporation - -Module Name: - - pdr_dl_interface.h - -Abstract: - - SMT2 interface for the datalog PDR - -Author: - - Krystof Hoder (t-khoder) 2011-9-22. - -Revision History: - ---*/ - -#ifndef PDR_DL_INTERFACE_H_ -#define PDR_DL_INTERFACE_H_ - -#include "util/lbool.h" -#include "muz/base/dl_rule.h" -#include "muz/base/dl_rule_set.h" -#include "muz/base/dl_util.h" -#include "muz/base/dl_engine_base.h" -#include "util/statistics.h" - -namespace datalog { - class context; -} - -namespace pdr { - - class context; - - class dl_interface : public datalog::engine_base { - datalog::context& m_ctx; - datalog::rule_set m_pdr_rules; - datalog::rule_set m_old_rules; - context* m_context; - obj_map m_pred2slice; - ast_ref_vector m_refs; - - void check_reset(); - - public: - dl_interface(datalog::context& ctx); - ~dl_interface() override; - - lbool query(expr* query) override; - - void display_certificate(std::ostream& out) const override; - - void collect_statistics(statistics& st) const override; - - void reset_statistics() override; - - expr_ref get_answer() override; - - unsigned get_num_levels(func_decl* pred) override; - - expr_ref get_cover_delta(int level, func_decl* pred) override; - - void add_cover(int level, func_decl* pred, expr* property) override; - - void updt_params() override; - - model_ref get_model() override; - - proof_ref get_proof() override; - - }; -} - - -#endif diff --git a/src/muz/pdr/pdr_farkas_learner.cpp b/src/muz/pdr/pdr_farkas_learner.cpp deleted file mode 100644 index 6695788c2..000000000 --- a/src/muz/pdr/pdr_farkas_learner.cpp +++ /dev/null @@ -1,1012 +0,0 @@ -/*++ -Copyright (c) 2011 Microsoft Corporation - -Module Name: - - pdr_farkas_learner.cpp - -Abstract: - - Proviced abstract interface and some inplementations of algorithms - for strenghtning lemmas - -Author: - - Krystof Hoder (t-khoder) 2011-11-1. - -Revision History: - ---*/ - -#include "ast/ast_smt2_pp.h" -#include "ast/array_decl_plugin.h" -#include "ast/rewriter/bool_rewriter.h" -#include "ast/dl_decl_plugin.h" -#include "ast/for_each_expr.h" -#include "muz/base/dl_util.h" -#include "ast/rewriter/rewriter.h" -#include "ast/rewriter/rewriter_def.h" -#include "muz/pdr/pdr_util.h" -#include "muz/pdr/pdr_farkas_learner.h" -#include "ast/rewriter/th_rewriter.h" -#include "ast/ast_ll_pp.h" -#include "tactic/arith/arith_bounds_tactic.h" -#include "ast/proofs/proof_utils.h" -#include "ast/reg_decl_plugins.h" - - -namespace pdr { - - class farkas_learner::constr { - - ast_manager& m; - arith_util a; - app_ref_vector m_ineqs; - vector m_coeffs; - - unsigned m_time; - unsigned_vector m_roots, m_size, m_his, m_reps, m_ts; - - void mk_coerce(expr*& e1, expr*& e2) { - if (a.is_int(e1) && a.is_real(e2)) { - e1 = a.mk_to_real(e1); - } - else if (a.is_int(e2) && a.is_real(e1)) { - e2 = a.mk_to_real(e2); - } - } - - app* mk_add(expr* e1, expr* e2) { - mk_coerce(e1, e2); - return a.mk_add(e1, e2); - } - - app* mk_mul(expr* e1, expr* e2) { - mk_coerce(e1, e2); - return a.mk_mul(e1, e2); - } - - app* mk_le(expr* e1, expr* e2) { - mk_coerce(e1, e2); - return a.mk_le(e1, e2); - } - - app* mk_ge(expr* e1, expr* e2) { - mk_coerce(e1, e2); - return a.mk_ge(e1, e2); - } - - app* mk_gt(expr* e1, expr* e2) { - mk_coerce(e1, e2); - return a.mk_gt(e1, e2); - } - - app* mk_lt(expr* e1, expr* e2) { - mk_coerce(e1, e2); - return a.mk_lt(e1, e2); - } - - void mul(rational const& c, expr* e, expr_ref& res) { - expr_ref tmp(m); - if (c.is_one()) { - tmp = e; - } - else { - tmp = mk_mul(a.mk_numeral(c, c.is_int() && a.is_int(e)), e); - } - res = mk_add(res, tmp); - } - - bool is_int_sort(app* c) { - SASSERT(m.is_eq(c) || a.is_le(c) || a.is_lt(c) || a.is_gt(c) || a.is_ge(c)); - SASSERT(a.is_int(c->get_arg(0)) || a.is_real(c->get_arg(0))); - return a.is_int(c->get_arg(0)); - } - - bool is_int_sort() { - SASSERT(!m_ineqs.empty()); - return is_int_sort(m_ineqs[0].get()); - } - - void normalize_coeffs() { - rational l(1); - for (unsigned i = 0; i < m_coeffs.size(); ++i) { - l = lcm(l, denominator(m_coeffs[i])); - } - if (!l.is_one()) { - for (unsigned i = 0; i < m_coeffs.size(); ++i) { - m_coeffs[i] *= l; - } - } - } - - app* mk_one() { - return a.mk_numeral(rational(1), true); - } - - app* fix_sign(bool is_pos, app* c) { - expr* x, *y; - SASSERT(m.is_eq(c) || a.is_le(c) || a.is_lt(c) || a.is_gt(c) || a.is_ge(c)); - bool is_int = is_int_sort(c); - if (is_int && is_pos && (a.is_lt(c, x, y) || a.is_gt(c, y, x))) { - return mk_le(mk_add(x, mk_one()), y); - } - if (is_int && !is_pos && (a.is_le(c, x, y) || a.is_ge(c, y, x))) { - // !(x <= y) <=> x > y <=> x >= y + 1 - return mk_ge(x, mk_add(y, mk_one())); - } - if (is_pos) { - return c; - } - if (a.is_le(c, x, y)) return mk_gt(x, y); - if (a.is_lt(c, x, y)) return mk_ge(x, y); - if (a.is_ge(c, x, y)) return mk_lt(x, y); - if (a.is_gt(c, x, y)) return mk_le(x, y); - UNREACHABLE(); - return c; - } - - public: - constr(ast_manager& m) : m(m), a(m), m_ineqs(m), m_time(0) {} - - void reset() { - m_ineqs.reset(); - m_coeffs.reset(); - } - - /** add a multiple of constraint c to the current constr */ - void add(rational const & coef, app * c) { - bool is_pos = true; - expr* e; - while (m.is_not(c, e)) { - is_pos = !is_pos; - c = to_app(e); - } - - if (!coef.is_zero() && !m.is_true(c)) { - m_coeffs.push_back(coef); - m_ineqs.push_back(fix_sign(is_pos, c)); - } - } - - // - // Extract the complement of premises multiplied by Farkas coefficients. - // - void get(expr_ref& res) { - if (m_coeffs.empty()) { - res = m.mk_false(); - return; - } - bool is_int = is_int_sort(); - if (is_int) { - normalize_coeffs(); - } - TRACE("pdr", - for (unsigned i = 0; i < m_coeffs.size(); ++i) { - tout << m_coeffs[i] << ": " << mk_pp(m_ineqs[i].get(), m) << "\n"; - } - ); - - res = extract_consequence(0, m_coeffs.size()); - -#if 1 - // partition equalities into variable disjoint sets. - // take the conjunction of these instead of the - // linear combination. - partition_ineqs(); - expr_ref_vector lits(m); - unsigned lo = 0; - for (unsigned i = 0; i < m_his.size(); ++i) { - unsigned hi = m_his[i]; - lits.push_back(extract_consequence(lo, hi)); - lo = hi; - } - res = mk_or(lits); - IF_VERBOSE(2, { if (lits.size() > 1) { verbose_stream() << "combined lemma: " << mk_pp(res, m) << "\n"; } }); -#endif - } - - private: - - // partition inequalities into variable disjoint sets. - void partition_ineqs() { - m_reps.reset(); - m_his.reset(); - ++m_time; - for (unsigned i = 0; i < m_ineqs.size(); ++i) { - m_reps.push_back(process_term(m_ineqs[i].get())); - } - unsigned head = 0; - while (head < m_ineqs.size()) { - unsigned r = find(m_reps[head]); - unsigned tail = head; - for (unsigned i = head+1; i < m_ineqs.size(); ++i) { - if (find(m_reps[i]) == r) { - ++tail; - if (tail != i) { - SASSERT(tail < i); - std::swap(m_reps[tail], m_reps[i]); - app_ref tmp(m); - tmp = m_ineqs[i].get(); - m_ineqs[i] = m_ineqs[tail].get(); - m_ineqs[tail] = tmp; - std::swap(m_coeffs[tail], m_coeffs[i]); - } - } - } - head = tail + 1; - m_his.push_back(head); - } - } - - unsigned find(unsigned idx) { - if (m_ts.size() <= idx) { - m_roots.resize(idx+1); - m_size.resize(idx+1); - m_ts.resize(idx+1); - m_roots[idx] = idx; - m_ts[idx] = m_time; - m_size[idx] = 1; - return idx; - } - if (m_ts[idx] != m_time) { - m_size[idx] = 1; - m_ts[idx] = m_time; - m_roots[idx] = idx; - return idx; - } - while (true) { - if (m_roots[idx] == idx) { - return idx; - } - idx = m_roots[idx]; - } - } - - void merge(unsigned i, unsigned j) { - i = find(i); - j = find(j); - if (i == j) { - return; - } - if (m_size[i] > m_size[j]) { - std::swap(i, j); - } - m_roots[i] = j; - m_size[j] += m_size[i]; - } - - unsigned process_term(expr* e) { - unsigned r = e->get_id(); - ptr_vector todo; - ast_mark mark; - todo.push_back(e); - while (!todo.empty()) { - e = todo.back(); - todo.pop_back(); - if (mark.is_marked(e)) { - continue; - } - mark.mark(e, true); - if (is_uninterp(e)) { - merge(r, e->get_id()); - } - if (is_app(e)) { - app* a = to_app(e); - for (unsigned i = 0; i < a->get_num_args(); ++i) { - todo.push_back(a->get_arg(i)); - } - } - } - return r; - } - - expr_ref extract_consequence(unsigned lo, unsigned hi) { - bool is_int = is_int_sort(); - app_ref zero(a.mk_numeral(rational::zero(), is_int), m); - expr_ref res(m); - res = zero; - bool is_strict = false; - bool is_eq = true; - expr* x, *y; - for (unsigned i = lo; i < hi; ++i) { - app* c = m_ineqs[i].get(); - if (m.is_eq(c, x, y)) { - mul(m_coeffs[i], x, res); - mul(-m_coeffs[i], y, res); - } - if (a.is_lt(c, x, y) || a.is_gt(c, y, x)) { - mul(m_coeffs[i], x, res); - mul(-m_coeffs[i], y, res); - is_strict = true; - is_eq = false; - } - if (a.is_le(c, x, y) || a.is_ge(c, y, x)) { - mul(m_coeffs[i], x, res); - mul(-m_coeffs[i], y, res); - is_eq = false; - } - } - - zero = a.mk_numeral(rational::zero(), a.is_int(res)); - if (is_eq) { - res = m.mk_eq(res, zero); - } - else if (is_strict) { - res = mk_lt(res, zero); - } - else { - res = mk_le(res, zero); - } - res = m.mk_not(res); - th_rewriter rw(m); - params_ref params; - params.set_bool("gcd_rounding", true); - rw.updt_params(params); - proof_ref pr(m); - expr_ref result(m); - rw(res, result, pr); - fix_dl(result); - return result; - } - - // patch: swap addends to make static - // features recognize difference constraint. - void fix_dl(expr_ref& r) { - expr* e; - if (m.is_not(r, e)) { - r = e; - fix_dl(r); - r = m.mk_not(r); - return; - } - expr* e1, *e2, *e3, *e4; - if ((m.is_eq(r, e1, e2) || a.is_lt(r, e1, e2) || a.is_gt(r, e1, e2) || - a.is_le(r, e1, e2) || a.is_ge(r, e1, e2))) { - if (a.is_add(e1, e3, e4) && a.is_mul(e3)) { - r = m.mk_app(to_app(r)->get_decl(), a.mk_add(e4,e3), e2); - } - } - } - }; - - farkas_learner::farkas_learner(smt_params& params, ast_manager& outer_mgr) - : m_proof_params(get_proof_params(params)), - m_pr(PGM_ENABLED), - m_constr(nullptr), - m_combine_farkas_coefficients(true), - p2o(m_pr, outer_mgr), - o2p(outer_mgr, m_pr) - { - reg_decl_plugins(m_pr); - m_ctx = alloc(smt::kernel, m_pr, m_proof_params); - } - - farkas_learner::~farkas_learner() { - dealloc(m_constr); - } - - smt_params farkas_learner::get_proof_params(smt_params& orig_params) { - smt_params res(orig_params); - res.m_arith_bound_prop = BP_NONE; - // temp hack to fix the build - // res.m_conflict_resolution_strategy = CR_ALL_DECIDED; - res.m_arith_auto_config_simplex = true; - res.m_arith_propagate_eqs = false; - res.m_arith_eager_eq_axioms = false; - res.m_arith_eq_bounds = false; - return res; - } - - class farkas_learner::equality_expander_cfg : public default_rewriter_cfg - { - ast_manager& m; - arith_util m_ar; - public: - equality_expander_cfg(ast_manager& m) : m(m), m_ar(m) {} - - bool get_subst(expr * s, expr * & t, proof * & t_pr) { - expr * x, *y; - if (m.is_eq(s, x, y) && (m_ar.is_int(x) || m_ar.is_real(x))) { - t = m.mk_and(m_ar.mk_ge(x, y), m_ar.mk_le(x, y)); - return true; - } - else { - return false; - } - } - - }; - - class collect_pure_proc { - func_decl_set& m_symbs; - public: - collect_pure_proc(func_decl_set& s):m_symbs(s) {} - - void operator()(app* a) { - if (a->get_family_id() == null_family_id) { - m_symbs.insert(a->get_decl()); - } - } - void operator()(var*) {} - void operator()(quantifier*) {} - }; - - - bool farkas_learner::get_lemma_guesses(expr * A_ext, expr * B_ext, expr_ref_vector& lemmas) - { - expr_ref A(o2p(A_ext), m_pr); - expr_ref B(o2p(B_ext), m_pr); - proof_ref pr(m_pr); - expr_ref tmp(m_pr); - expr_ref_vector ilemmas(m_pr); - equality_expander_cfg ee_rwr_cfg(m_pr); - rewriter_tpl ee_rwr(m_pr, false, ee_rwr_cfg); - - lemmas.reset(); - - ee_rwr(A, A); - ee_rwr(B, B); - - expr_set bs; - expr_ref_vector blist(m_pr); - flatten_and(B, blist); - for (unsigned i = 0; i < blist.size(); ++i) { - bs.insert(blist[i].get()); - } - - - if (!m_ctx) { - m_ctx = alloc(smt::kernel, m_pr, m_proof_params); - } - - m_ctx->push(); - m_ctx->assert_expr(A); - expr_set::iterator it = bs.begin(), end = bs.end(); - for (; it != end; ++it) { - m_ctx->assert_expr(*it); - } - lbool res = m_ctx->check(); - bool is_unsat = res == l_false; - if (is_unsat) { - pr = m_ctx->get_proof(); - get_lemmas(m_ctx->get_proof(), bs, ilemmas); - for (unsigned i = 0; i < ilemmas.size(); ++i) { - lemmas.push_back(p2o(ilemmas[i].get())); - } - } - m_ctx->pop(1); - - IF_VERBOSE(3, { - for (unsigned i = 0; i < ilemmas.size(); ++i) { - verbose_stream() << "B': " << mk_pp(ilemmas[i].get(), m_pr) << "\n"; - } - }); - - TRACE("farkas_learner", - tout << (is_unsat?"unsat":"sat") << "\n"; - tout << "A: " << mk_pp(A_ext, m_ctx->m()) << "\n"; - tout << "B: " << mk_pp(B_ext, m_ctx->m()) << "\n"; - for (unsigned i = 0; i < lemmas.size(); ++i) { - tout << "B': " << mk_pp(ilemmas[i].get(), m_pr) << "\n"; - }); - DEBUG_CODE( - if (is_unsat) { - m_ctx->push(); - m_ctx->assert_expr(A); - for (unsigned i = 0; i < ilemmas.size(); ++i) { - m_ctx->assert_expr(ilemmas[i].get()); - } - lbool res2 = m_ctx->check(); - SASSERT(l_false == res2); - m_ctx->pop(1); - } - ); - return is_unsat; - } - - // - // Perform simple subsumption check of lemmas. - // - void farkas_learner::simplify_lemmas(expr_ref_vector& lemmas) { - ast_manager& m = lemmas.get_manager(); - goal_ref g(alloc(goal, m, false, false, false)); - TRACE("farkas_simplify_lemmas", - for (unsigned i = 0; i < lemmas.size(); ++i) { - tout << mk_pp(lemmas[i].get(), m) << "\n"; - }); - - for (unsigned i = 0; i < lemmas.size(); ++i) { - g->assert_expr(lemmas[i].get()); - } - expr_ref tmp(m); - goal_ref_buffer result; - tactic_ref simplifier = mk_arith_bounds_tactic(m); - (*simplifier)(g, result); - lemmas.reset(); - SASSERT(result.size() == 1); - goal* r = result[0]; - for (unsigned i = 0; i < r->size(); ++i) { - lemmas.push_back(r->form(i)); - } - TRACE("farkas_simplify_lemmas", - tout << "simplified:\n"; - for (unsigned i = 0; i < lemmas.size(); ++i) { - tout << mk_pp(lemmas[i].get(), m) << "\n"; - }); - } - - - void farkas_learner::combine_constraints(unsigned n, app * const * lits, rational const * coeffs, expr_ref& res) - { - ast_manager& m = res.get_manager(); - if (m_combine_farkas_coefficients) { - if (!m_constr) { - m_constr = alloc(constr, m); - } - m_constr->reset(); - for (unsigned i = 0; i < n; ++i) { - m_constr->add(coeffs[i], lits[i]); - } - m_constr->get(res); - } - else { - bool_rewriter rw(m); - rw.mk_or(n, (expr*const*)(lits), res); - res = m.mk_not(res); - } - } - - class farkas_learner::constant_replacer_cfg : public default_rewriter_cfg - { - const obj_map& m_translation; - public: - constant_replacer_cfg(const obj_map& translation) - : m_translation(translation) - { } - - bool get_subst(expr * s, expr * & t, proof * & t_pr) { - return m_translation.find(s, t); - } - }; - - // every uninterpreted symbol is in symbs - class is_pure_expr_proc { - func_decl_set const& m_symbs; - public: - struct non_pure {}; - - is_pure_expr_proc(func_decl_set const& s):m_symbs(s) {} - - void operator()(app* a) { - if (a->get_family_id() == null_family_id) { - if (!m_symbs.contains(a->get_decl())) { - throw non_pure(); - } - } - } - void operator()(var*) {} - void operator()(quantifier*) {} - }; - - bool farkas_learner::is_pure_expr(func_decl_set const& symbs, expr* e) const { - is_pure_expr_proc proc(symbs); - try { - for_each_expr(proc, e); - } - catch (is_pure_expr_proc::non_pure) { - return false; - } - return true; - }; - - - /** - Revised version of Farkas strengthener. - 1. Mark B-pure nodes as derivations that depend only on B. - 2. Collect B-influenced nodes - 3. (optional) Permute B-pure units over resolution steps to narrow dependencies on B. - 4. Weaken B-pure units for resolution with Farkas Clauses. - 5. Add B-pure units elsewhere. - - Rules: - - hypothesis h |- h - - H |- false - - lemma ---------- - |- not H - - Th |- L \/ C H |- not L - - th-lemma ------------------------- - H |- C - - Note: C is false for theory axioms, C is unit literal for propagation. - - - rewrite |- t = s - - H |- t = s - - monotonicity ---------------- - H |- f(t) = f(s) - - H |- t = s H' |- s = u - - trans ---------------------- - H, H' |- t = u - - H |- C \/ L H' |- not L - - unit_resolve ------------------------ - H, H' |- C - - H |- a ~ b H' |- a - - mp -------------------- - H, H' |- b - - - def-axiom |- C - - - asserted |- f - - Mark nodes by: - - Hypotheses - - Dependency on bs - - Dependency on A - - A node is unit derivable from bs if: - - It has no hypotheses. - - It depends on bs. - - It does not depend on A. - - NB: currently unit derivable is not symmetric: A clause can be - unit derivable, but a unit literal with hypotheses is not. - This is clearly wrong, because hypotheses are just additional literals - in a clausal version. - - NB: the routine is not interpolating, though an interpolating variant would - be preferrable because then we can also use it for model propagation. - - We collect the unit derivable nodes from bs. - These are the weakenings of bs, besides the - units under Farkas. - - */ - -#define INSERT(_x_) if (!lemma_set.contains(_x_)) { lemma_set.insert(_x_); lemmas.push_back(_x_); } - - void farkas_learner::get_lemmas(proof* root, expr_set const& bs, expr_ref_vector& lemmas) { - ast_manager& m = lemmas.get_manager(); - bool_rewriter brwr(m); - func_decl_set Bsymbs; - collect_pure_proc collect_proc(Bsymbs); - expr_set::iterator it = bs.begin(), end = bs.end(); - for (; it != end; ++it) { - for_each_expr(collect_proc, *it); - } - - proof_ref pr(root, m); - proof_utils::reduce_hypotheses(pr); - proof_utils::permute_unit_resolution(pr); - IF_VERBOSE(3, verbose_stream() << "Reduced proof:\n" << mk_ismt2_pp(pr, m) << "\n";); - - ptr_vector hyprefs; - obj_map hypmap; - obj_hashtable lemma_set; - ast_mark b_depend, a_depend, visited, b_closed; - expr_set* empty_set = alloc(expr_set); - hyprefs.push_back(empty_set); - ptr_vector todo; - TRACE("pdr_verbose", tout << mk_pp(pr, m) << "\n";); - todo.push_back(pr); - while (!todo.empty()) { - proof* p = todo.back(); - SASSERT(m.is_proof(p)); - if (visited.is_marked(p)) { - todo.pop_back(); - continue; - } - bool all_visit = true; - for (unsigned i = 0; i < m.get_num_parents(p); ++i) { - expr* arg = p->get_arg(i); - SASSERT(m.is_proof(arg)); - if (!visited.is_marked(arg)) { - all_visit = false; - todo.push_back(to_app(arg)); - } - } - if (!all_visit) { - continue; - } - visited.mark(p, true); - todo.pop_back(); - - // retrieve hypotheses and dependencies on A, bs. - bool b_dep = false, a_dep = false; - expr_set* hyps = empty_set; - for (unsigned i = 0; i < m.get_num_parents(p); ++i) { - expr* arg = p->get_arg(i); - a_dep = a_dep || a_depend.is_marked(arg); - b_dep = b_dep || b_depend.is_marked(arg); - expr_set* hyps2 = hypmap.find(arg); - if (hyps != hyps2 && !hyps2->empty()) { - if (hyps->empty()) { - hyps = hyps2; - } - else { - expr_set* hyps3 = alloc(expr_set); - set_union(*hyps3, *hyps); - set_union(*hyps3, *hyps2); - hyps = hyps3; - hyprefs.push_back(hyps); - } - } - } - hypmap.insert(p, hyps); - a_depend.mark(p, a_dep); - b_depend.mark(p, b_dep); - -#define IS_B_PURE(_p) (b_depend.is_marked(_p) && !a_depend.is_marked(_p) && hypmap.find(_p)->empty()) - - - // Add lemmas that depend on bs, have no hypotheses, don't depend on A. - if ((!hyps->empty() || a_depend.is_marked(p)) && - b_depend.is_marked(p) && !is_farkas_lemma(m, p)) { - for (unsigned i = 0; i < m.get_num_parents(p); ++i) { - app* arg = to_app(p->get_arg(i)); - if (IS_B_PURE(arg)) { - expr* fact = m.get_fact(arg); - if (is_pure_expr(Bsymbs, fact)) { - TRACE("farkas_learner", - tout << "Add: " << mk_pp(m.get_fact(arg), m) << "\n"; - tout << mk_pp(arg, m) << "\n"; - ); - INSERT(fact); - } - else { - get_asserted(p, bs, b_closed, lemma_set, lemmas); - b_closed.mark(p, true); - } - } - } - } - - switch(p->get_decl_kind()) { - case PR_ASSERTED: - if (bs.contains(m.get_fact(p))) { - b_depend.mark(p, true); - } - else { - a_depend.mark(p, true); - } - break; - case PR_HYPOTHESIS: { - SASSERT(hyps == empty_set); - hyps = alloc(expr_set); - hyps->insert(m.get_fact(p)); - hyprefs.push_back(hyps); - hypmap.insert(p, hyps); - break; - } - case PR_DEF_AXIOM: { - if (!is_pure_expr(Bsymbs, m.get_fact(p))) { - a_depend.mark(p, true); - } - break; - } - case PR_LEMMA: { - expr_set* hyps2 = alloc(expr_set); - hyprefs.push_back(hyps2); - set_union(*hyps2, *hyps); - hyps = hyps2; - expr* fml = m.get_fact(p); - hyps->remove(fml); - if (m.is_or(fml)) { - for (unsigned i = 0; i < to_app(fml)->get_num_args(); ++i) { - expr* f = to_app(fml)->get_arg(i); - expr_ref hyp(m); - brwr.mk_not(f, hyp); - hyps->remove(hyp); - } - } - hypmap.insert(p, hyps); - break; - } - case PR_TH_LEMMA: { - if (!is_farkas_lemma(m, p)) break; - - SASSERT(m.has_fact(p)); - unsigned prem_cnt = m.get_num_parents(p); - func_decl * d = p->get_decl(); - SASSERT(d->get_num_parameters() >= prem_cnt+2); - SASSERT(d->get_parameter(0).get_symbol() == "arith"); - SASSERT(d->get_parameter(1).get_symbol() == "farkas"); - parameter const* params = d->get_parameters() + 2; - - app_ref_vector lits(m); - expr_ref tmp(m); - unsigned num_b_pures = 0; - rational coef; - vector coeffs; - - TRACE("farkas_learner", - for (unsigned i = 0; i < prem_cnt; ++i) { - VERIFY(params[i].is_rational(coef)); - proof* prem = to_app(p->get_arg(i)); - bool b_pure = IS_B_PURE(prem); - tout << (b_pure?"B":"A") << " " << coef << " " << mk_pp(m.get_fact(prem), m) << "\n"; - } - tout << mk_pp(m.get_fact(p), m) << "\n"; - ); - - // NB. Taking 'abs' of coefficients is a workaround. - // The Farkas coefficient extraction in arith_core must be wrong. - // The coefficients would be always positive relative to the theory lemma. - - for(unsigned i = 0; i < prem_cnt; ++i) { - expr * prem_e = p->get_arg(i); - SASSERT(is_app(prem_e)); - proof * prem = to_app(prem_e); - - if(IS_B_PURE(prem)) { - ++num_b_pures; - } - else { - VERIFY(params[i].is_rational(coef)); - lits.push_back(to_app(m.get_fact(prem))); - coeffs.push_back(abs(coef)); - } - } - params += prem_cnt; - if (prem_cnt + 2 < d->get_num_parameters()) { - unsigned num_args = 1; - expr* fact = m.get_fact(p); - expr* const* args = &fact; - if (m.is_or(fact)) { - app* _or = to_app(fact); - num_args = _or->get_num_args(); - args = _or->get_args(); - } - SASSERT(prem_cnt + 2 + num_args == d->get_num_parameters()); - for (unsigned i = 0; i < num_args; ++i) { - expr* prem_e = args[i]; - brwr.mk_not(prem_e, tmp); - VERIFY(params[i].is_rational(coef)); - SASSERT(is_app(tmp)); - lits.push_back(to_app(tmp)); - coeffs.push_back(abs(coef)); - } - - } - SASSERT(coeffs.size() == lits.size()); - if (num_b_pures > 0) { - expr_ref res(m); - combine_constraints(coeffs.size(), lits.c_ptr(), coeffs.c_ptr(), res); - TRACE("farkas_learner", tout << "Add: " << mk_pp(res, m) << "\n";); - INSERT(res); - b_closed.mark(p, true); - } - } - default: - break; - } - } - - std::for_each(hyprefs.begin(), hyprefs.end(), delete_proc()); - simplify_lemmas(lemmas); - } - - void farkas_learner::get_consequences(proof* root, expr_set const& bs, expr_ref_vector& consequences) { - TRACE("farkas_learner", tout << "get consequences\n";); - m_combine_farkas_coefficients = false; - get_lemmas(root, bs, consequences); - m_combine_farkas_coefficients = true; - } - - void farkas_learner::get_asserted(proof* p, expr_set const& bs, ast_mark& b_closed, obj_hashtable& lemma_set, expr_ref_vector& lemmas) { - ast_manager& m = lemmas.get_manager(); - ast_mark visited; - proof* p0 = p; - ptr_vector todo; - todo.push_back(p); - - while (!todo.empty()) { - p = todo.back(); - todo.pop_back(); - if (visited.is_marked(p) || b_closed.is_marked(p)) { - continue; - } - visited.mark(p, true); - for (unsigned i = 0; i < m.get_num_parents(p); ++i) { - expr* arg = p->get_arg(i); - SASSERT(m.is_proof(arg)); - todo.push_back(to_app(arg)); - } - if (p->get_decl_kind() == PR_ASSERTED && - bs.contains(m.get_fact(p))) { - expr* fact = m.get_fact(p); - (void)p0; - TRACE("farkas_learner", - tout << mk_ll_pp(p0,m) << "\n"; - tout << "Add: " << mk_pp(p,m) << "\n";); - INSERT(fact); - b_closed.mark(p, true); - } - } - } - - - bool farkas_learner::is_farkas_lemma(ast_manager& m, expr* e) { - app * a; - func_decl* d; - symbol sym; - return - is_app(e) && - (a = to_app(e), d = a->get_decl(), true) && - PR_TH_LEMMA == a->get_decl_kind() && - d->get_num_parameters() >= 2 && - d->get_parameter(0).is_symbol(sym) && sym == "arith" && - d->get_parameter(1).is_symbol(sym) && sym == "farkas" && - d->get_num_parameters() >= m.get_num_parents(to_app(e)) + 2; - }; - - - void farkas_learner::test() { - smt_params params; - enable_trace("farkas_learner"); - - bool res; - ast_manager m; - reg_decl_plugins(m); - arith_util a(m); - pdr::farkas_learner fl(params, m); - expr_ref_vector lemmas(m); - - sort_ref int_s(a.mk_int(), m); - expr_ref x(m.mk_const(symbol("x"), int_s), m); - expr_ref y(m.mk_const(symbol("y"), int_s), m); - expr_ref z(m.mk_const(symbol("z"), int_s), m); - expr_ref u(m.mk_const(symbol("u"), int_s), m); - expr_ref v(m.mk_const(symbol("v"), int_s), m); - - // A: x > y >= z - // B: x < z - // Farkas: x <= z - expr_ref A(m.mk_and(a.mk_gt(x,y), a.mk_ge(y,z)),m); - expr_ref B(a.mk_gt(z,x),m); - res = fl.get_lemma_guesses(A, B, lemmas); - std::cout << "\nres: " << res << "\nlemmas: " << pp_cube(lemmas, m) << "\n"; - - // A: x > y >= z + 2 - // B: x = 1, z = 8 - // Farkas: x <= z + 2 - expr_ref one(a.mk_numeral(rational(1), true), m); - expr_ref two(a.mk_numeral(rational(2), true), m); - expr_ref eight(a.mk_numeral(rational(8), true), m); - A = m.mk_and(a.mk_gt(x,y),a.mk_ge(y,a.mk_add(z,two))); - B = m.mk_and(m.mk_eq(x,one), m.mk_eq(z, eight)); - res = fl.get_lemma_guesses(A, B, lemmas); - std::cout << "\nres: " << res << "\nlemmas: " << pp_cube(lemmas, m) << "\n"; - - // A: x > y >= z \/ x >= u > z - // B: z > x + 1 - // Farkas: z >= x - A = m.mk_or(m.mk_and(a.mk_gt(x,y),a.mk_ge(y,z)),m.mk_and(a.mk_ge(x,u),a.mk_gt(u,z))); - B = a.mk_gt(z, a.mk_add(x,one)); - res = fl.get_lemma_guesses(A, B, lemmas); - std::cout << "\nres: " << res << "\nlemmas: " << pp_cube(lemmas, m) << "\n"; - - // A: (x > y >= z \/ x >= u > z \/ u > v) - // B: z > x + 1 & not (u > v) - // Farkas: z >= x & not (u > v) - A = m.mk_or(m.mk_and(a.mk_gt(x,y),a.mk_ge(y,z)),m.mk_and(a.mk_ge(x,u),a.mk_gt(u,z)), a.mk_gt(u, v)); - B = m.mk_and(a.mk_gt(z, a.mk_add(x,one)), m.mk_not(a.mk_gt(u, v))); - res = fl.get_lemma_guesses(A, B, lemmas); - std::cout << "\nres: " << res << "\nlemmas: " << pp_cube(lemmas, m) << "\n"; - - } - - void farkas_learner::collect_statistics(statistics& st) const { - if (m_ctx) { - m_ctx->collect_statistics(st); - } - } - - -}; - diff --git a/src/muz/pdr/pdr_farkas_learner.h b/src/muz/pdr/pdr_farkas_learner.h deleted file mode 100644 index a5f3482e6..000000000 --- a/src/muz/pdr/pdr_farkas_learner.h +++ /dev/null @@ -1,128 +0,0 @@ -/*++ -Copyright (c) 2011 Microsoft Corporation - -Module Name: - - pdr_farkas_learner.h - -Abstract: - - SMT2 interface for the datalog PDR - -Author: - - Krystof Hoder (t-khoder) 2011-11-1. - -Revision History: - ---*/ - -#ifndef PDR_FARKAS_LEARNER_H_ -#define PDR_FARKAS_LEARNER_H_ - -#include "ast/arith_decl_plugin.h" -#include "ast/ast_translation.h" -#include "ast/bv_decl_plugin.h" -#include "smt/smt_kernel.h" -#include "ast/rewriter/bool_rewriter.h" -#include "muz/pdr/pdr_util.h" -#include "smt/params/smt_params.h" -#include "tactic/tactic.h" - -namespace pdr { - -class farkas_learner { - class farkas_collector; - class constant_replacer_cfg; - class equality_expander_cfg; - class constr; - - typedef obj_hashtable expr_set; - - smt_params m_proof_params; - ast_manager m_pr; - scoped_ptr m_ctx; - constr* m_constr; - - // - // true: produce a combined constraint by applying Farkas coefficients. - // false: produce a conjunction of the negated literals from the theory lemmas. - // - bool m_combine_farkas_coefficients; - - - static smt_params get_proof_params(smt_params& orig_params); - - // - // all ast objects passed to private functions have m_proof_mgs as their ast_manager - // - - ast_translation p2o; /** Translate expression from inner ast_manager to outer one */ - ast_translation o2p; /** Translate expression from outer ast_manager to inner one */ - - - /** All ast opbjects here are in the m_proof_mgs */ - void get_lemma_guesses_internal(proof * p, expr* A, expr * B, expr_ref_vector& lemmas); - - bool farkas2lemma(proof * fstep, expr* A, expr * B, expr_ref& res); - - void combine_constraints(unsigned cnt, app * const * constrs, rational const * coeffs, expr_ref& res); - - bool try_ensure_lemma_in_language(expr_ref& lemma, expr* A, const func_decl_set& lang); - - bool is_farkas_lemma(ast_manager& m, expr* e); - - void get_asserted(proof* p, expr_set const& bs, ast_mark& b_closed, obj_hashtable& lemma_set, expr_ref_vector& lemmas); - - bool is_pure_expr(func_decl_set const& symbs, expr* e) const; - - static void test(); - -public: - farkas_learner(smt_params& params, ast_manager& m); - - ~farkas_learner(); - - /** - All ast objects have the ast_manager which was passed as - an argument to the constructor (i.e. m_outer_mgr) - - B is a conjunction of literals. - A && B is unsat, equivalently A => ~B is valid - Find a weakened B' such that - A && B' is unsat and B' uses vocabulary (and constants) in common with A. - return lemmas to weaken B. - */ - - bool get_lemma_guesses(expr * A, expr * B, expr_ref_vector& lemmas); - - /** - Traverse a proof and retrieve lemmas using the vocabulary from bs. - */ - void get_lemmas(proof* root, expr_set const& bs, expr_ref_vector& lemmas); - - /** - Traverse a proof and retrieve consequences of A that are used to establish ~B. - The assumption is that: - - A => \/ ~consequences[i] and \/ ~consequences[i] => ~B - - e.g., the second implication can be rewritten as: - - B => /\ consequences[i] - */ - void get_consequences(proof* root, expr_set const& bs, expr_ref_vector& consequences); - - /** - \brief Simplify lemmas using subsumption. - */ - void simplify_lemmas(expr_ref_vector& lemmas); - - void collect_statistics(statistics& st) const; - -}; - - -} - -#endif diff --git a/src/muz/pdr/pdr_generalizers.cpp b/src/muz/pdr/pdr_generalizers.cpp deleted file mode 100644 index 8e52cb6f4..000000000 --- a/src/muz/pdr/pdr_generalizers.cpp +++ /dev/null @@ -1,777 +0,0 @@ -/*++ -Copyright (c) 2011 Microsoft Corporation - -Module Name: - - pdr_generalizers.cpp - -Abstract: - - Generalizers of satisfiable states and unsat cores. - -Author: - - Nikolaj Bjorner (nbjorner) 2011-11-20. - -Revision History: - ---*/ - - -#include "muz/pdr/pdr_context.h" -#include "muz/pdr/pdr_farkas_learner.h" -#include "muz/pdr/pdr_generalizers.h" -#include "ast/expr_abstract.h" -#include "ast/rewriter/var_subst.h" -#include "ast/rewriter/expr_safe_replace.h" -#include "model/model_smt2_pp.h" - - -namespace pdr { - - - // ------------------------ - // core_bool_inductive_generalizer - - // main propositional induction generalizer. - // drop literals one by one from the core and check if the core is still inductive. - // - void core_bool_inductive_generalizer::operator()(model_node& n, expr_ref_vector& core, bool& uses_level) { - if (core.size() <= 1) { - return; - } - ast_manager& m = core.get_manager(); - TRACE("pdr", for (unsigned i = 0; i < core.size(); ++i) { tout << mk_pp(core[i].get(), m) << "\n"; }); - unsigned num_failures = 0, i = 0, old_core_size = core.size(); - ptr_vector processed; - - while (i < core.size() && 1 < core.size() && (!m_failure_limit || num_failures <= m_failure_limit)) { - expr_ref lit(m); - lit = core[i].get(); - core[i] = m.mk_true(); - if (n.pt().check_inductive(n.level(), core, uses_level)) { - num_failures = 0; - for (i = 0; i < core.size() && processed.contains(core[i].get()); ++i); - } - else { - core[i] = lit; - processed.push_back(lit); - ++num_failures; - ++i; - } - } - IF_VERBOSE(2, verbose_stream() << "old size: " << old_core_size << " new size: " << core.size() << "\n";); - TRACE("pdr", tout << "old size: " << old_core_size << " new size: " << core.size() << "\n";); - } - - - void core_multi_generalizer::operator()(model_node& n, expr_ref_vector& core, bool& uses_level) { - UNREACHABLE(); - } - - /** - \brief Find minimal cores. - Apply a simple heuristic: find a minimal core, then find minimal cores that exclude at least one - literal from each of the literals in the minimal cores. - */ - void core_multi_generalizer::operator()(model_node& n, expr_ref_vector const& core, bool uses_level, cores& new_cores) { - ast_manager& m = core.get_manager(); - expr_ref_vector old_core(m), core0(core); - bool uses_level1 = uses_level; - m_gen(n, core0, uses_level1); - new_cores.push_back(std::make_pair(core0, uses_level1)); - obj_hashtable core_exprs, core1_exprs; - set_union(core_exprs, core0); - for (unsigned i = 0; i < old_core.size(); ++i) { - expr* lit = old_core[i].get(); - if (core_exprs.contains(lit)) { - expr_ref_vector core1(old_core); - core1[i] = core1.back(); - core1.pop_back(); - uses_level1 = uses_level; - m_gen(n, core1, uses_level1); - SASSERT(core1.size() <= old_core.size()); - if (core1.size() < old_core.size()) { - new_cores.push_back(std::make_pair(core1, uses_level1)); - core1_exprs.reset(); - set_union(core1_exprs, core1); - set_intersection(core_exprs, core1_exprs); - } - } - } - } - - // ------------------------ - // core_farkas_generalizer - - // - // for each disjunct of core: - // weaken predecessor. - // - - core_farkas_generalizer::core_farkas_generalizer(context& ctx, ast_manager& m, smt_params& p): - core_generalizer(ctx), - m_farkas_learner(p, m) - {} - - void core_farkas_generalizer::operator()(model_node& n, expr_ref_vector& core, bool& uses_level) { - ast_manager& m = n.pt().get_manager(); - if (core.empty()) return; - expr_ref A(m), B(mk_and(core)), C(m); - expr_ref_vector Bs(m); - flatten_or(B, Bs); - A = n.pt().get_propagation_formula(m_ctx.get_pred_transformers(), n.level()); - - bool change = false; - for (unsigned i = 0; i < Bs.size(); ++i) { - expr_ref_vector lemmas(m); - C = Bs[i].get(); - if (m_farkas_learner.get_lemma_guesses(A, B, lemmas)) { - TRACE("pdr", - tout << "Old core:\n" << mk_pp(B, m) << "\n"; - tout << "New core:\n" << mk_and(lemmas) << "\n";); - Bs[i] = mk_and(lemmas); - change = true; - } - } - if (change) { - C = mk_or(Bs); - TRACE("pdr", tout << "prop:\n" << mk_pp(A,m) << "\ngen:" << mk_pp(B, m) << "\nto: " << mk_pp(C, m) << "\n";); - core.reset(); - flatten_and(C, core); - uses_level = true; - } - } - - void core_farkas_generalizer::collect_statistics(statistics& st) const { - m_farkas_learner.collect_statistics(st); - } - - - core_convex_hull_generalizer::core_convex_hull_generalizer(context& ctx, bool is_closure): - core_generalizer(ctx), - m(ctx.get_manager()), - m_is_closure(is_closure) { - } - - void core_convex_hull_generalizer::operator()(model_node& n, expr_ref_vector const& core, bool uses_level, cores& new_cores) { - // method3(n, core, uses_level, new_cores); - method1(n, core, uses_level, new_cores); - } - - void core_convex_hull_generalizer::operator()(model_node& n, expr_ref_vector& core, bool& uses_level) { - UNREACHABLE(); - } - - // use the entire region as starting point for generalization. - // - // Constraints: - // add_variables: y = y1 + y2 - // core: Ay <= b -> conv1: A*y1 <= b*sigma1 - // sigma1 > 0 - // sigma2 > 0 - // 1 = sigma1 + sigma2 - // A'y <= b' -> conv2: A'*y2 <= b'*sigma2 - // - // If Constraints & Transition(y0, y) is unsat, then - // update with new core. - // - void core_convex_hull_generalizer::method1(model_node& n, expr_ref_vector const& core, bool uses_level, cores& new_cores) { - expr_ref_vector conv2(m), fmls(m), fml1_2(m); - bool change = false; - - if (core.empty()) { - new_cores.push_back(std::make_pair(core, uses_level)); - return; - } - closure cl(n.pt(), m_is_closure); - - expr_ref fml1 = mk_and(core); - expr_ref fml2 = n.pt().get_formulas(n.level(), false); - fml1_2.push_back(fml1); - fml1_2.push_back(nullptr); - flatten_and(fml2, fmls); - for (unsigned i = 0; i < fmls.size(); ++i) { - fml2 = m.mk_not(fmls[i].get()); - fml1_2[1] = fml2; - expr_ref state = cl(fml1_2); - TRACE("pdr", - tout << "Check states:\n" << mk_pp(state, m) << "\n"; - tout << "Old states:\n" << mk_pp(fml2, m) << "\n"; - ); - model_node nd(nullptr, state, n.pt(), n.level()); - pred_transformer::scoped_farkas sf(n.pt(), true); - bool uses_level1 = uses_level; - if (l_false == n.pt().is_reachable(nd, &conv2, uses_level1)) { - new_cores.push_back(std::make_pair(conv2, uses_level1)); - change = true; - expr_ref state1 = mk_and(conv2); - TRACE("pdr", - tout << mk_pp(state, m) << "\n"; - tout << "Generalized to:\n" << mk_pp(state1, m) << "\n";); - IF_VERBOSE(0, - verbose_stream() << mk_pp(state, m) << "\n"; - verbose_stream() << "Generalized to:\n" << mk_pp(state1, m) << "\n";); - } - } - if (!m_is_closure || !change) { - new_cores.push_back(std::make_pair(core, uses_level)); - } - } - - /* - Extract the lemmas from the transition relation that were used to establish unsatisfiability. - Take convex closures of conbinations of these lemmas. - */ - void core_convex_hull_generalizer::method3(model_node& n, expr_ref_vector const& core, bool uses_level, cores& new_cores) { - TRACE("dl", tout << "method: generalize consequences of F(R)\n"; - for (unsigned i = 0; i < core.size(); ++i) { - tout << "B:" << mk_pp(core[i], m) << "\n"; - }); - bool uses_level1; - expr_ref_vector core1(m); - core1.append(core); - expr_ref_vector consequences(m); - { - n.pt().get_solver().set_consequences(&consequences); - pred_transformer::scoped_farkas sf (n.pt(), true); - VERIFY(l_false == n.pt().is_reachable(n, &core1, uses_level1)); - n.pt().get_solver().set_consequences(nullptr); - } - IF_VERBOSE(0, - verbose_stream() << "Consequences: " << consequences.size() << "\n"; - for (unsigned i = 0; i < consequences.size(); ++i) { - verbose_stream() << mk_pp(consequences[i].get(), m) << "\n"; - } - verbose_stream() << "core: " << core1.size() << "\n"; - for (unsigned i = 0; i < core1.size(); ++i) { - verbose_stream() << mk_pp(core1[i].get(), m) << "\n"; - }); - - expr_ref tmp(m); - - // Check that F(R) => \/ consequences - { - expr_ref_vector cstate(m); - for (unsigned i = 0; i < consequences.size(); ++i) { - cstate.push_back(m.mk_not(consequences[i].get())); - } - tmp = m.mk_and(cstate.size(), cstate.c_ptr()); - model_node nd(nullptr, tmp, n.pt(), n.level()); - pred_transformer::scoped_farkas sf (n.pt(), false); - VERIFY(l_false == n.pt().is_reachable(nd, &core1, uses_level1)); - } - - // Create disjunction. - tmp = m.mk_and(core.size(), core.c_ptr()); - - // Check that \/ consequences => not (core) - if (!is_unsat(consequences, tmp)) { - IF_VERBOSE(0, verbose_stream() << "Consequences don't contradict the core\n";); - return; - } - IF_VERBOSE(0, verbose_stream() << "Consequences contradict core\n";); - - if (!strengthen_consequences(n, consequences, tmp)) { - return; - } - - IF_VERBOSE(0, verbose_stream() << "consequences strengthened\n";); - // Use the resulting formula to find Farkas lemmas from core. - } - - bool core_convex_hull_generalizer::strengthen_consequences(model_node& n, expr_ref_vector& As, expr* B) { - expr_ref A(m), tmp(m), convA(m); - unsigned sz = As.size(); - closure cl(n.pt(), m_is_closure); - for (unsigned i = 0; i < As.size(); ++i) { - expr_ref_vector Hs(m); - Hs.push_back(As[i].get()); - for (unsigned j = i + 1; j < As.size(); ++j) { - Hs.push_back(As[j].get()); - bool unsat = false; - A = cl(Hs); - tmp = As[i].get(); - As[i] = A; - unsat = is_unsat(As, B); - As[i] = tmp; - if (unsat) { - IF_VERBOSE(0, verbose_stream() << "New convex: " << mk_pp(convA, m) << "\n";); - convA = A; - As[j] = As.back(); - As.pop_back(); - --j; - } - else { - Hs.pop_back(); - } - } - if (Hs.size() > 1) { - As[i] = convA; - } - } - return sz > As.size(); - } - - - bool core_convex_hull_generalizer::is_unsat(expr_ref_vector const& As, expr* B) { - smt::kernel ctx(m, m_ctx.get_fparams(), m_ctx.get_params().p); - expr_ref disj(m); - disj = m.mk_or(As.size(), As.c_ptr()); - ctx.assert_expr(disj); - ctx.assert_expr(B); - std::cout << "Checking\n" << mk_pp(disj, m) << "\n" << mk_pp(B, m) << "\n"; - return l_false == ctx.check(); - } - - - // --------------------------------- - // core_arith_inductive_generalizer - // NB. this is trying out some ideas for generalization in - // an ad hoc specialized way. arith_inductive_generalizer should - // not be used by default. It is a place-holder for a general purpose - // extrapolator of a lattice basis. - - core_arith_inductive_generalizer::core_arith_inductive_generalizer(context& ctx): - core_generalizer(ctx), - m(ctx.get_manager()), - a(m), - m_refs(m) {} - - void core_arith_inductive_generalizer::operator()(model_node& n, expr_ref_vector& core, bool& uses_level) { - if (core.size() <= 1) { - return; - } - reset(); - expr_ref e(m), t1(m), t2(m), t3(m); - rational r; - - TRACE("pdr", for (unsigned i = 0; i < core.size(); ++i) { tout << mk_pp(core[i].get(), m) << "\n"; }); - - svector eqs; - get_eqs(core, eqs); - - if (eqs.empty()) { - return; - } - - expr_ref_vector new_core(m); - new_core.append(core); - - for (unsigned eq = 0; eq < eqs.size(); ++eq) { - rational r = eqs[eq].m_value; - expr* x = eqs[eq].m_term; - unsigned k = eqs[eq].m_i; - unsigned l = eqs[eq].m_j; - - new_core[l] = m.mk_true(); - new_core[k] = m.mk_true(); - - for (unsigned i = 0; i < new_core.size(); ++i) { - if (substitute_alias(r, x, new_core[i].get(), e)) { - new_core[i] = e; - } - } - if (abs(r) >= rational(2) && a.is_int(x)) { - new_core[k] = m.mk_eq(a.mk_mod(x, a.mk_numeral(rational(2), true)), a.mk_numeral(rational(0), true)); - new_core[l] = a.mk_le(x, a.mk_numeral(rational(0), true)); - } - } - - bool inductive = n.pt().check_inductive(n.level(), new_core, uses_level); - - IF_VERBOSE(1, - verbose_stream() << (inductive?"":"non") << "inductive\n"; - verbose_stream() << "old\n"; - for (unsigned j = 0; j < core.size(); ++j) { - verbose_stream() << mk_pp(core[j].get(), m) << "\n"; - } - verbose_stream() << "new\n"; - for (unsigned j = 0; j < new_core.size(); ++j) { - verbose_stream() << mk_pp(new_core[j].get(), m) << "\n"; - }); - - if (inductive) { - core.reset(); - core.append(new_core); - } - } - - void core_arith_inductive_generalizer::insert_bound(bool is_lower, expr* x, rational const& r, unsigned i) { - if (r.is_neg()) { - expr_ref e(m); - e = a.mk_uminus(x); - m_refs.push_back(e); - x = e; - is_lower = !is_lower; - } - - vector bound; - bound.push_back(std::make_pair(x, i)); - if (is_lower) { - m_lb.insert(abs(r), bound); - } - else { - m_ub.insert(abs(r), bound); - } - } - - void core_arith_inductive_generalizer::reset() { - m_refs.reset(); - m_lb.reset(); - m_ub.reset(); - } - - void core_arith_inductive_generalizer::get_eqs(expr_ref_vector const& core, svector& eqs) { - expr* e1, *x, *y; - expr_ref e(m); - rational r; - - for (unsigned i = 0; i < core.size(); ++i) { - e = core[i]; - if (m.is_not(e, e1) && a.is_le(e1, x, y) && a.is_numeral(y, r) && a.is_int(x)) { - // not (<= x r) <=> x >= r + 1 - insert_bound(true, x, r + rational(1), i); - } - else if (m.is_not(e, e1) && a.is_ge(e1, x, y) && a.is_numeral(y, r) && a.is_int(x)) { - // not (>= x r) <=> x <= r - 1 - insert_bound(false, x, r - rational(1), i); - } - else if (a.is_le(e, x, y) && a.is_numeral(y, r)) { - insert_bound(false, x, r, i); - } - else if (a.is_ge(e, x, y) && a.is_numeral(y, r)) { - insert_bound(true, x, r, i); - } - } - bounds_t::iterator it = m_lb.begin(), end = m_lb.end(); - for (; it != end; ++it) { - rational r = it->m_key; - vector & terms1 = it->m_value; - vector terms2; - if (r >= rational(2) && m_ub.find(r, terms2)) { - for (unsigned i = 0; i < terms1.size(); ++i) { - bool done = false; - for (unsigned j = 0; !done && j < terms2.size(); ++j) { - expr* t1 = terms1[i].first; - expr* t2 = terms2[j].first; - if (t1 == t2) { - eqs.push_back(eq(t1, r, terms1[i].second, terms2[j].second)); - done = true; - } - else { - e = m.mk_eq(t1, t2); - th_rewriter rw(m); - rw(e); - if (m.is_true(e)) { - eqs.push_back(eq(t1, r, terms1[i].second, terms2[j].second)); - done = true; - } - } - } - } - } - } - } - - bool core_arith_inductive_generalizer::substitute_alias(rational const& r, expr* x, expr* e, expr_ref& result) { - rational r2; - expr* y, *z, *e1; - if (m.is_not(e, e1) && substitute_alias(r, x, e1, result)) { - result = m.mk_not(result); - return true; - } - if (a.is_le(e, y, z) && a.is_numeral(z, r2)) { - if (r == r2) { - result = a.mk_le(y, x); - return true; - } - if (r == r2 + rational(1)) { - result = a.mk_lt(y, x); - return true; - } - if (r == r2 - rational(1)) { - result = a.mk_le(y, a.mk_sub(x, a.mk_numeral(rational(1), a.is_int(x)))); - return true; - } - - } - if (a.is_ge(e, y, z) && a.is_numeral(z, r2)) { - if (r == r2) { - result = a.mk_ge(y, x); - return true; - } - if (r2 == r + rational(1)) { - result = a.mk_gt(y, x); - return true; - } - if (r2 == r - rational(1)) { - result = a.mk_ge(y, a.mk_sub(x, a.mk_numeral(rational(1), a.is_int(x)))); - return true; - } - } - return false; - } - - - // - // < F, phi, i + 1> - // | - // < G, psi, i > - // - // where: - // - // p(x) <- F(x,y,p,q) - // q(x) <- G(x,y) - // - // Hyp: - // Q_k(x) => phi(x) j <= k <= i - // Q_k(x) => R_k(x) j <= k <= i + 1 - // Q_k(x) <=> Trans(Q_{k-1}) j < k <= i + 1 - // Conclusion: - // Q_{i+1}(x) => phi(x) - // - class core_induction_generalizer::imp { - context& m_ctx; - manager& pm; - ast_manager& m; - - // - // Create predicate Q_level - // - func_decl_ref mk_pred(unsigned level, func_decl* f) { - func_decl_ref result(m); - std::ostringstream name; - name << f->get_name() << "_" << level; - symbol sname(name.str().c_str()); - result = m.mk_func_decl(sname, f->get_arity(), f->get_domain(), f->get_range()); - return result; - } - - // - // Create formula exists y . z . F[Q_{level-1}, x, y, z] - // - expr_ref mk_transition_rule( - expr_ref_vector const& reps, - unsigned level, - datalog::rule const& rule) - { - expr_ref_vector conj(m), sub(m); - expr_ref result(m); - svector names; - unsigned ut_size = rule.get_uninterpreted_tail_size(); - unsigned t_size = rule.get_tail_size(); - if (0 == level && 0 < ut_size) { - result = m.mk_false(); - return result; - } - app* atom = rule.get_head(); - SASSERT(atom->get_num_args() == reps.size()); - - for (unsigned i = 0; i < reps.size(); ++i) { - expr* arg = atom->get_arg(i); - if (is_var(arg)) { - unsigned idx = to_var(arg)->get_idx(); - if (idx >= sub.size()) sub.resize(idx+1); - if (sub[idx].get()) { - conj.push_back(m.mk_eq(sub[idx].get(), reps[i])); - } - else { - sub[idx] = reps[i]; - } - } - else { - conj.push_back(m.mk_eq(arg, reps[i])); - } - } - for (unsigned i = 0; 0 < level && i < ut_size; i++) { - app* atom = rule.get_tail(i); - func_decl* head = atom->get_decl(); - func_decl_ref fn = mk_pred(level-1, head); - conj.push_back(m.mk_app(fn, atom->get_num_args(), atom->get_args())); - } - for (unsigned i = ut_size; i < t_size; i++) { - conj.push_back(rule.get_tail(i)); - } - result = mk_and(conj); - if (!sub.empty()) { - expr_ref tmp = result; - var_subst(m, false)(tmp, sub.size(), sub.c_ptr(), result); - } - expr_free_vars fv; - fv(result); - fv.set_default_sort(m.mk_bool_sort()); - for (unsigned i = 0; i < fv.size(); ++i) { - names.push_back(symbol(fv.size() - i - 1)); - } - if (!fv.empty()) { - fv.reverse(); - result = m.mk_exists(fv.size(), fv.c_ptr(), names.c_ptr(), result); - } - return result; - } - - expr_ref bind_head(expr_ref_vector const& reps, expr* fml) { - expr_ref result(m); - expr_abstract(m, 0, reps.size(), reps.c_ptr(), fml, result); - ptr_vector sorts; - svector names; - unsigned sz = reps.size(); - for (unsigned i = 0; i < sz; ++i) { - sorts.push_back(m.get_sort(reps[sz-i-1])); - names.push_back(symbol(sz-i-1)); - } - if (sz > 0) { - result = m.mk_forall(sorts.size(), sorts.c_ptr(), names.c_ptr(), result); - } - return result; - } - - expr_ref_vector mk_reps(pred_transformer& pt) { - expr_ref_vector reps(m); - expr_ref rep(m); - for (unsigned i = 0; i < pt.head()->get_arity(); ++i) { - rep = m.mk_const(pm.o2n(pt.sig(i), 0)); - reps.push_back(rep); - } - return reps; - } - - // - // extract transition axiom: - // - // forall x . p_lvl(x) <=> exists y z . F[p_{lvl-1}(y), q_{lvl-1}(z), x] - // - expr_ref mk_transition_axiom(pred_transformer& pt, unsigned level) { - expr_ref fml(m.mk_false(), m), tr(m); - expr_ref_vector reps = mk_reps(pt); - ptr_vector const& rules = pt.rules(); - for (unsigned i = 0; i < rules.size(); ++i) { - tr = mk_transition_rule(reps, level, *rules[i]); - fml = (i == 0)?tr.get():m.mk_or(fml, tr); - } - func_decl_ref fn = mk_pred(level, pt.head()); - fml = m.mk_iff(m.mk_app(fn, reps.size(), reps.c_ptr()), fml); - fml = bind_head(reps, fml); - return fml; - } - - // - // Create implication: - // Q_level(x) => phi(x) - // - expr_ref mk_predicate_property(unsigned level, pred_transformer& pt, expr* phi) { - expr_ref_vector reps = mk_reps(pt); - func_decl_ref fn = mk_pred(level, pt.head()); - expr_ref fml(m); - fml = m.mk_implies(m.mk_app(fn, reps.size(), reps.c_ptr()), phi); - fml = bind_head(reps, fml); - return fml; - } - - - - public: - imp(context& ctx): m_ctx(ctx), pm(ctx.get_pdr_manager()), m(ctx.get_manager()) {} - - // - // not exists y . F(x,y) - // - expr_ref mk_blocked_transition(pred_transformer& pt, unsigned level) { - SASSERT(level > 0); - expr_ref fml(m.mk_true(), m); - expr_ref_vector reps = mk_reps(pt), fmls(m); - ptr_vector const& rules = pt.rules(); - for (unsigned i = 0; i < rules.size(); ++i) { - fmls.push_back(m.mk_not(mk_transition_rule(reps, level, *rules[i]))); - } - fml = mk_and(fmls); - TRACE("pdr", tout << mk_pp(fml, m) << "\n";); - return fml; - } - - expr_ref mk_induction_goal(pred_transformer& pt, unsigned level, unsigned depth) { - SASSERT(level >= depth); - expr_ref_vector conjs(m); - ptr_vector pts; - unsigned_vector levels; - // negated goal - expr_ref phi = mk_blocked_transition(pt, level); - conjs.push_back(m.mk_not(mk_predicate_property(level, pt, phi))); - pts.push_back(&pt); - levels.push_back(level); - // Add I.H. - for (unsigned lvl = level-depth; lvl < level; ++lvl) { - if (lvl > 0) { - expr_ref psi = mk_blocked_transition(pt, lvl); - conjs.push_back(mk_predicate_property(lvl, pt, psi)); - pts.push_back(&pt); - levels.push_back(lvl); - } - } - // Transitions: - for (unsigned qhead = 0; qhead < pts.size(); ++qhead) { - pred_transformer& qt = *pts[qhead]; - unsigned lvl = levels[qhead]; - - // Add transition definition and properties at level. - conjs.push_back(mk_transition_axiom(qt, lvl)); - conjs.push_back(mk_predicate_property(lvl, qt, qt.get_formulas(lvl, true))); - - // Enqueue additional hypotheses - ptr_vector const& rules = qt.rules(); - if (lvl + depth < level || lvl == 0) { - continue; - } - for (unsigned i = 0; i < rules.size(); ++i) { - datalog::rule& r = *rules[i]; - unsigned ut_size = r.get_uninterpreted_tail_size(); - for (unsigned j = 0; j < ut_size; ++j) { - func_decl* f = r.get_tail(j)->get_decl(); - pred_transformer* rt = m_ctx.get_pred_transformers().find(f); - bool found = false; - for (unsigned k = 0; !found && k < levels.size(); ++k) { - found = (rt == pts[k] && levels[k] + 1 == lvl); - } - if (!found) { - levels.push_back(lvl-1); - pts.push_back(rt); - } - } - } - } - - expr_ref result = mk_and(conjs); - TRACE("pdr", tout << mk_pp(result, m) << "\n";); - return result; - } - }; - - // - // Instantiate Peano induction schema. - // - void core_induction_generalizer::operator()(model_node& n, expr_ref_vector& core, bool& uses_level) { - model_node* p = n.parent(); - if (p == nullptr) { - return; - } - unsigned depth = 2; - 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().p); - ctx.assert_expr(goal); - lbool r = ctx.check(); - TRACE("pdr", tout << r << "\n"; - for (unsigned i = 0; i < core.size(); ++i) { - tout << mk_pp(core[i].get(), m) << "\n"; - }); - if (r == l_false) { - core.reset(); - expr_ref phi = imp.mk_blocked_transition(p->pt(), p->level()); - core.push_back(m.mk_not(phi)); - uses_level = true; - } - } -}; - diff --git a/src/muz/pdr/pdr_generalizers.h b/src/muz/pdr/pdr_generalizers.h deleted file mode 100644 index a75b347a4..000000000 --- a/src/muz/pdr/pdr_generalizers.h +++ /dev/null @@ -1,110 +0,0 @@ -/*++ -Copyright (c) 2011 Microsoft Corporation - -Module Name: - - pdr_generalizers.h - -Abstract: - - Generalizer plugins. - -Author: - - Nikolaj Bjorner (nbjorner) 2011-11-22. - -Revision History: - ---*/ - -#ifndef PDR_GENERALIZERS_H_ -#define PDR_GENERALIZERS_H_ - -#include "muz/pdr/pdr_context.h" -#include "muz/pdr/pdr_closure.h" -#include "ast/arith_decl_plugin.h" - -namespace pdr { - - class core_bool_inductive_generalizer : public core_generalizer { - unsigned m_failure_limit; - public: - core_bool_inductive_generalizer(context& ctx, unsigned failure_limit) : core_generalizer(ctx), m_failure_limit(failure_limit) {} - ~core_bool_inductive_generalizer() override {} - void operator()(model_node& n, expr_ref_vector& core, bool& uses_level) override; - }; - - template - class r_map : public map { - }; - - class core_arith_inductive_generalizer : public core_generalizer { - typedef std::pair term_loc_t; - typedef r_map > bounds_t; - - ast_manager& m; - arith_util a; - expr_ref_vector m_refs; - bounds_t m_lb; - bounds_t m_ub; - - struct eq { - expr* m_term; - rational m_value; - unsigned m_i; - unsigned m_j; - eq(expr* t, rational const& r, unsigned i, unsigned j): m_term(t), m_value(r), m_i(i), m_j(j) {} - }; - void reset(); - void insert_bound(bool is_lower, expr* x, rational const& r, unsigned i); - void get_eqs(expr_ref_vector const& core, svector& eqs); - bool substitute_alias(rational const&r, expr* x, expr* e, expr_ref& result); - public: - core_arith_inductive_generalizer(context& ctx); - ~core_arith_inductive_generalizer() override {} - void operator()(model_node& n, expr_ref_vector& core, bool& uses_level) override; - }; - - class core_farkas_generalizer : public core_generalizer { - farkas_learner m_farkas_learner; - public: - core_farkas_generalizer(context& ctx, ast_manager& m, smt_params& p); - ~core_farkas_generalizer() override {} - void operator()(model_node& n, expr_ref_vector& core, bool& uses_level) override; - void collect_statistics(statistics& st) const override; - }; - - - class core_convex_hull_generalizer : public core_generalizer { - ast_manager& m; - obj_map m_models; - bool m_is_closure; - void method1(model_node& n, expr_ref_vector const& core, bool uses_level, cores& new_cores); - void method3(model_node& n, expr_ref_vector const& core, bool uses_level, cores& new_cores); - bool strengthen_consequences(model_node& n, expr_ref_vector& As, expr* B); - bool is_unsat(expr_ref_vector const& As, expr* B); - public: - core_convex_hull_generalizer(context& ctx, bool is_closure); - ~core_convex_hull_generalizer() override {} - void operator()(model_node& n, expr_ref_vector const& core, bool uses_level, cores& new_cores) override; - void operator()(model_node& n, expr_ref_vector& core, bool& uses_level) override; - }; - - class core_multi_generalizer : public core_generalizer { - core_bool_inductive_generalizer m_gen; - public: - core_multi_generalizer(context& ctx, unsigned max_failures): core_generalizer(ctx), m_gen(ctx, max_failures) {} - ~core_multi_generalizer() override {} - void operator()(model_node& n, expr_ref_vector& core, bool& uses_level) override; - void operator()(model_node& n, expr_ref_vector const& core, bool uses_level, cores& new_cores) override; - }; - - class core_induction_generalizer : public core_generalizer { - class imp; - public: - core_induction_generalizer(context& ctx): core_generalizer(ctx) {} - ~core_induction_generalizer() override {} - void operator()(model_node& n, expr_ref_vector& core, bool& uses_level) override; - }; -}; -#endif diff --git a/src/muz/pdr/pdr_manager.cpp b/src/muz/pdr/pdr_manager.cpp deleted file mode 100644 index da15bf094..000000000 --- a/src/muz/pdr/pdr_manager.cpp +++ /dev/null @@ -1,321 +0,0 @@ -/*++ -Copyright (c) 2011 Microsoft Corporation - -Module Name: - - pdr_manager.cpp - -Abstract: - - A manager class for PDR, taking care of creating of AST - objects and conversions between them. - -Author: - - Krystof Hoder (t-khoder) 2011-8-25. - -Revision History: - ---*/ - -#include -#include "muz/pdr/pdr_manager.h" -#include "ast/ast_smt2_pp.h" -#include "ast/for_each_expr.h" -#include "ast/has_free_vars.h" -#include "ast/rewriter/expr_replacer.h" -#include "ast/expr_abstract.h" -#include "model/model2expr.h" -#include "model/model_smt2_pp.h" -#include "tactic/model_converter.h" - -namespace pdr { - - class collect_decls_proc { - func_decl_set& m_bound_decls; - func_decl_set& m_aux_decls; - public: - collect_decls_proc(func_decl_set& bound_decls, func_decl_set& aux_decls): - m_bound_decls(bound_decls), - m_aux_decls(aux_decls) { - } - - void operator()(app* a) { - if (a->get_family_id() == null_family_id) { - func_decl* f = a->get_decl(); - if (!m_bound_decls.contains(f)) { - m_aux_decls.insert(f); - } - } - } - void operator()(var* v) {} - void operator()(quantifier* q) {} - }; - - typedef hashtable symbol_set; - - expr_ref inductive_property::fixup_clause(expr* fml) const { - expr_ref_vector disjs(m); - flatten_or(fml, disjs); - expr_ref result(m); - bool_rewriter(m).mk_or(disjs.size(), disjs.c_ptr(), result); - return result; - } - - expr_ref inductive_property::fixup_clauses(expr* fml) const { - expr_ref_vector conjs(m); - expr_ref result(m); - flatten_and(fml, conjs); - for (unsigned i = 0; i < conjs.size(); ++i) { - conjs[i] = fixup_clause(conjs[i].get()); - } - bool_rewriter(m).mk_and(conjs.size(), conjs.c_ptr(), result); - return result; - } - - std::string inductive_property::to_string() const { - std::stringstream stm; - model_ref md; - expr_ref result(m); - to_model(md); - model_smt2_pp(stm, m, *md.get(), 0); - return stm.str(); - } - - void inductive_property::to_model(model_ref& md) const { - md = alloc(model, m); - vector const& rs = m_relation_info; - expr_ref_vector conjs(m); - for (unsigned i = 0; i < rs.size(); ++i) { - relation_info ri(rs[i]); - func_decl * pred = ri.m_pred; - expr_ref prop = fixup_clauses(ri.m_body); - func_decl_ref_vector const& sig = ri.m_vars; - expr_ref q(m); - expr_ref_vector sig_vars(m); - for (unsigned j = 0; j < sig.size(); ++j) { - sig_vars.push_back(m.mk_const(sig[sig.size()-j-1])); - } - expr_abstract(m, 0, sig_vars.size(), sig_vars.c_ptr(), prop, q); - if (sig.empty()) { - md->register_decl(pred, q); - } - else { - func_interp* fi = alloc(func_interp, m, sig.size()); - fi->set_else(q); - md->register_decl(pred, fi); - } - } - TRACE("pdr", model_smt2_pp(tout, m, *md, 0);); - apply(const_cast(m_mc), md); - } - - expr_ref inductive_property::to_expr() const { - model_ref md; - expr_ref result(m); - to_model(md); - model2expr(md, result); - return result; - } - - - void inductive_property::display(datalog::rule_manager& rm, ptr_vector const& rules, std::ostream& out) const { - func_decl_set bound_decls, aux_decls; - collect_decls_proc collect_decls(bound_decls, aux_decls); - - for (unsigned i = 0; i < m_relation_info.size(); ++i) { - bound_decls.insert(m_relation_info[i].m_pred); - func_decl_ref_vector const& sig = m_relation_info[i].m_vars; - for (unsigned j = 0; j < sig.size(); ++j) { - bound_decls.insert(sig[j]); - } - for_each_expr(collect_decls, m_relation_info[i].m_body); - } - for (unsigned i = 0; i < rules.size(); ++i) { - bound_decls.insert(rules[i]->get_decl()); - } - for (unsigned i = 0; i < rules.size(); ++i) { - unsigned u_sz = rules[i]->get_uninterpreted_tail_size(); - unsigned t_sz = rules[i]->get_tail_size(); - for (unsigned j = u_sz; j < t_sz; ++j) { - for_each_expr(collect_decls, rules[i]->get_tail(j)); - } - } - smt2_pp_environment_dbg env(m); - func_decl_set::iterator it = aux_decls.begin(), end = aux_decls.end(); - for (; it != end; ++it) { - func_decl* f = *it; - ast_smt2_pp(out, f, env); - out << "\n"; - } - - out << to_string() << "\n"; - for (unsigned i = 0; i < rules.size(); ++i) { - out << "(push)\n"; - out << "(assert (not\n"; - rm.display_smt2(*rules[i], out); - out << "))\n"; - out << "(check-sat)\n"; - out << "(pop)\n"; - } - } - - manager::manager(smt_params& fparams, unsigned max_num_contexts, ast_manager& manager) : - m(manager), - m_fparams(fparams), - m_brwr(m), - m_mux(m), - m_background(m.mk_true(), m), - m_contexts(fparams, max_num_contexts, m), - m_next_unique_num(0) - { - } - - - void manager::add_new_state(func_decl * s) { - SASSERT(s->get_arity()==0); //we currently don't support non-constant states - decl_vector vect; - SASSERT(o_index(0)==1); //we assume this in the number of retrieved symbols - m_mux.create_tuple(s, s->get_arity(), s->get_domain(), s->get_range(), 2, vect); - m_o0_preds.push_back(vect[o_index(0)]); - } - - func_decl * manager::get_o_pred(func_decl* s, unsigned idx) - { - func_decl * res = m_mux.try_get_by_prefix(s, o_index(idx)); - if(res) { return res; } - add_new_state(s); - res = m_mux.try_get_by_prefix(s, o_index(idx)); - SASSERT(res); - return res; - } - - func_decl * manager::get_n_pred(func_decl* s) - { - func_decl * res = m_mux.try_get_by_prefix(s, n_index()); - if(res) { return res; } - add_new_state(s); - res = m_mux.try_get_by_prefix(s, n_index()); - SASSERT(res); - return res; - } - - void manager::mk_model_into_cube(const expr_ref_vector & mdl, expr_ref & res) { - m_brwr.mk_and(mdl.size(), mdl.c_ptr(), res); - } - - void manager::mk_core_into_cube(const expr_ref_vector & core, expr_ref & res) { - m_brwr.mk_and(core.size(), core.c_ptr(), res); - } - - void manager::mk_cube_into_lemma(expr * cube, expr_ref & res) { - m_brwr.mk_not(cube, res); - } - - void manager::mk_lemma_into_cube(expr * lemma, expr_ref & res) { - m_brwr.mk_not(lemma, res); - } - - expr_ref manager::mk_and(unsigned sz, expr* const* exprs) { - expr_ref result(m); - m_brwr.mk_and(sz, exprs, result); - return result; - } - - expr_ref manager::mk_or(unsigned sz, expr* const* exprs) { - expr_ref result(m); - m_brwr.mk_or(sz, exprs, result); - return result; - } - - expr_ref manager::mk_not_and(expr_ref_vector const& conjs) { - expr_ref result(m), e(m); - expr_ref_vector es(conjs); - flatten_and(es); - for (unsigned i = 0; i < es.size(); ++i) { - m_brwr.mk_not(es[i].get(), e); - es[i] = e; - } - m_brwr.mk_or(es.size(), es.c_ptr(), result); - return result; - } - - void manager::get_or(expr* e, expr_ref_vector& result) { - result.push_back(e); - for (unsigned i = 0; i < result.size(); ) { - e = result[i].get(); - if (m.is_or(e)) { - result.append(to_app(e)->get_num_args(), to_app(e)->get_args()); - result[i] = result.back(); - result.pop_back(); - } - else { - ++i; - } - } - } - - bool manager::try_get_state_and_value_from_atom(expr * atom0, app *& state, app_ref& value) - { - if(!is_app(atom0)) { - return false; - } - app * atom = to_app(atom0); - expr * arg1; - expr * arg2; - app * candidate_state; - app_ref candidate_value(m); - if(m.is_not(atom, arg1)) { - if(!is_app(arg1)) { - return false; - } - candidate_state = to_app(arg1); - candidate_value = m.mk_false(); - } - else if(m.is_eq(atom, arg1, arg2)) { - if(!is_app(arg1) || !is_app(arg2)) { - return false; - } - if(!m_mux.is_muxed(to_app(arg1)->get_decl())) { - std::swap(arg1, arg2); - } - candidate_state = to_app(arg1); - candidate_value = to_app(arg2); - } - else { - candidate_state = atom; - candidate_value = m.mk_true(); - } - if(!m_mux.is_muxed(candidate_state->get_decl())) { - return false; - } - state = candidate_state; - value = candidate_value; - return true; - } - - bool manager::try_get_state_decl_from_atom(expr * atom, func_decl *& state) { - app_ref dummy_value_holder(m); - app * s; - if(try_get_state_and_value_from_atom(atom, s, dummy_value_holder)) { - state = s->get_decl(); - return true; - } - else { - return false; - } - } - - bool manager::implication_surely_holds(expr * lhs, expr * rhs, expr * bg) { - smt::kernel sctx(m, get_fparams()); - if(bg) { - sctx.assert_expr(bg); - } - sctx.assert_expr(lhs); - expr_ref neg_rhs(m.mk_not(rhs),m); - sctx.assert_expr(neg_rhs); - lbool smt_res = sctx.check(); - return smt_res==l_false; - } - -}; diff --git a/src/muz/pdr/pdr_manager.h b/src/muz/pdr/pdr_manager.h deleted file mode 100644 index ccbbbe356..000000000 --- a/src/muz/pdr/pdr_manager.h +++ /dev/null @@ -1,304 +0,0 @@ -/*++ -Copyright (c) 2011 Microsoft Corporation - -Module Name: - - pdr_manager.h - -Abstract: - - A manager class for PDR, taking care of creating of AST - objects and conversions between them. - -Author: - - Krystof Hoder (t-khoder) 2011-8-25. - -Revision History: - ---*/ - -#ifndef PDR_MANAGER_H_ -#define PDR_MANAGER_H_ - -#include -#include -#include "ast/rewriter/bool_rewriter.h" -#include "ast/rewriter/expr_replacer.h" -#include "ast/expr_substitution.h" -#include "util/map.h" -#include "util/ref_vector.h" -#include "smt/smt_kernel.h" -#include "muz/pdr/pdr_util.h" -#include "muz/pdr/pdr_sym_mux.h" -#include "muz/pdr/pdr_farkas_learner.h" -#include "muz/pdr/pdr_smt_context_manager.h" -#include "muz/base/dl_rule.h" - - -namespace smt { - class context; -} - -namespace pdr { - - struct relation_info { - func_decl_ref m_pred; - func_decl_ref_vector m_vars; - expr_ref m_body; - relation_info(ast_manager& m, func_decl* pred, ptr_vector const& vars, expr* b): - m_pred(pred, m), m_vars(m, vars.size(), vars.c_ptr()), m_body(b, m) {} - relation_info(relation_info const& other): m_pred(other.m_pred), m_vars(other.m_vars), m_body(other.m_body) {} - }; - - class unknown_exception {}; - - class inductive_property { - ast_manager& m; - model_converter_ref m_mc; - vector m_relation_info; - expr_ref fixup_clauses(expr* property) const; - expr_ref fixup_clause(expr* clause) const; - public: - inductive_property(ast_manager& m, model_converter_ref& mc, vector const& relations): - m(m), - m_mc(mc), - m_relation_info(relations) {} - - std::string to_string() const; - - expr_ref to_expr() const; - - void to_model(model_ref& md) const; - - void display(datalog::rule_manager& rm, ptr_vector const& rules, std::ostream& out) const; - }; - - class manager - { - ast_manager& m; - smt_params& m_fparams; - - mutable bool_rewriter m_brwr; - - sym_mux m_mux; - expr_ref m_background; - decl_vector m_o0_preds; - pdr::smt_context_manager m_contexts; - - /** whenever we need an unique number, we get this one and increase */ - unsigned m_next_unique_num; - - - unsigned n_index() const { return 0; } - unsigned o_index(unsigned i) const { return i+1; } - - void add_new_state(func_decl * s); - - public: - manager(smt_params& fparams, unsigned max_num_contexts, ast_manager & manager); - - ast_manager& get_manager() const { return m; } - smt_params& get_fparams() const { return m_fparams; } - bool_rewriter& get_brwr() const { return m_brwr; } - - expr_ref mk_and(unsigned sz, expr* const* exprs); - expr_ref mk_and(expr_ref_vector const& exprs) { - return mk_and(exprs.size(), exprs.c_ptr()); - } - expr_ref mk_and(expr* a, expr* b) { - expr* args[2] = { a, b }; - return mk_and(2, args); - } - expr_ref mk_or(unsigned sz, expr* const* exprs); - expr_ref mk_or(expr_ref_vector const& exprs) { - return mk_or(exprs.size(), exprs.c_ptr()); - } - - expr_ref mk_not_and(expr_ref_vector const& exprs); - - void get_or(expr* e, expr_ref_vector& result); - - //"o" predicates stand for the old states and "n" for the new states - func_decl * get_o_pred(func_decl * s, unsigned idx); - func_decl * get_n_pred(func_decl * s); - - /** - Marks symbol as non-model which means it will not appear in models collected by - get_state_cube_from_model function. - This is to take care of auxiliary symbols introduced by the disjunction relations - to relativize lemmas coming from disjuncts. - */ - void mark_as_non_model(func_decl * p) { - m_mux.mark_as_non_model(p); - } - - - func_decl * const * begin_o0_preds() const { return m_o0_preds.begin(); } - func_decl * const * end_o0_preds() const { return m_o0_preds.end(); } - - bool is_state_pred(func_decl * p) const { return m_mux.is_muxed(p); } - func_decl * to_o0(func_decl * p) { return m_mux.conv(m_mux.get_primary(p), 0, o_index(0)); } - - bool is_o(func_decl * p, unsigned idx) const { - return m_mux.has_index(p, o_index(idx)); - } - bool is_o(expr* e, unsigned idx) const { - return is_app(e) && is_o(to_app(e)->get_decl(), idx); - } - bool is_o(func_decl * p) const { - unsigned idx; - return m_mux.try_get_index(p, idx) && idx!=n_index(); - } - bool is_o(expr* e) const { - return is_app(e) && is_o(to_app(e)->get_decl()); - } - bool is_n(func_decl * p) const { - return m_mux.has_index(p, n_index()); - } - bool is_n(expr* e) const { - return is_app(e) && is_n(to_app(e)->get_decl()); - } - - /** true if p should not appead in models propagates into child relations */ - bool is_non_model_sym(func_decl * p) const - { return m_mux.is_non_model_sym(p); } - - - /** true if f doesn't contain any n predicates */ - bool is_o_formula(expr * f) const { - return !m_mux.contains(f, n_index()); - } - - /** true if f contains only o state preds of index o_idx */ - bool is_o_formula(expr * f, unsigned o_idx) const { - return m_mux.is_homogenous_formula(f, o_index(o_idx)); - } - /** true if f doesn't contain any o predicates */ - bool is_n_formula(expr * f) const { - return m_mux.is_homogenous_formula(f, n_index()); - } - - func_decl * o2n(func_decl * p, unsigned o_idx) { - return m_mux.conv(p, o_index(o_idx), n_index()); - } - func_decl * o2o(func_decl * p, unsigned src_idx, unsigned tgt_idx) { - return m_mux.conv(p, o_index(src_idx), o_index(tgt_idx)); - } - func_decl * n2o(func_decl * p, unsigned o_idx) { - return m_mux.conv(p, n_index(), o_index(o_idx)); - } - - void formula_o2n(expr * f, expr_ref & result, unsigned o_idx, bool homogenous=true) - { m_mux.conv_formula(f, o_index(o_idx), n_index(), result, homogenous); } - - void formula_n2o(expr * f, expr_ref & result, unsigned o_idx, bool homogenous=true) - { m_mux.conv_formula(f, n_index(), o_index(o_idx), result, homogenous); } - - void formula_n2o(unsigned o_idx, bool homogenous, expr_ref & result) - { m_mux.conv_formula(result.get(), n_index(), o_index(o_idx), result, homogenous); } - - void formula_o2o(expr * src, expr_ref & tgt, unsigned src_idx, unsigned tgt_idx, bool homogenous=true) - { m_mux.conv_formula(src, o_index(src_idx), o_index(tgt_idx), tgt, homogenous); } - - /** - Return true if all state symbols which e contains are of one kind (either "n" or one of "o"). - */ - bool is_homogenous_formula(expr * e) const { - return m_mux.is_homogenous_formula(e); - } - - /** - Collect indices used in expression. - */ - void collect_indices(expr* e, unsigned_vector& indices) const { - m_mux.collect_indices(e, indices); - } - - /** - Collect used variables of each index. - */ - void collect_variables(expr* e, vector >& vars) const { - m_mux.collect_variables(e, vars); - } - - /** - Return true iff both s1 and s2 are either "n" or "o" of the same index. - If one (or both) of them are not state symbol, return false. - */ - bool have_different_state_kinds(func_decl * s1, func_decl * s2) const { - unsigned i1, i2; - return m_mux.try_get_index(s1, i1) && m_mux.try_get_index(s2, i2) && i1!=i2; - } - - /** - Increase indexes of state symbols in formula by dist. - The 'N' index becomes 'O' index with number dist-1. - */ - void formula_shift(expr * src, expr_ref & tgt, unsigned dist) { - SASSERT(n_index()==0); - SASSERT(o_index(0)==1); - m_mux.shift_formula(src, dist, tgt); - } - - void mk_model_into_cube(const expr_ref_vector & mdl, expr_ref & res); - void mk_core_into_cube(const expr_ref_vector & core, expr_ref & res); - void mk_cube_into_lemma(expr * cube, expr_ref & res); - void mk_lemma_into_cube(expr * lemma, expr_ref & res); - - /** - Remove from vec all atoms that do not have an "o" state. - The order of elements in vec may change. - An assumption is that atoms having "o" state of given index - do not have "o" states of other indexes or "n" states. - */ - void filter_o_atoms(expr_ref_vector& vec, unsigned o_idx) const - { m_mux.filter_idx(vec, o_index(o_idx)); } - void filter_n_atoms(expr_ref_vector& vec) const - { m_mux.filter_idx(vec, n_index()); } - - /** - Partition literals into o_lits and others. - */ - void partition_o_atoms(expr_ref_vector const& lits, - expr_ref_vector& o_lits, - expr_ref_vector& other, - unsigned o_idx) const { - m_mux.partition_o_idx(lits, o_lits, other, o_index(o_idx)); - } - - void filter_out_non_model_atoms(expr_ref_vector& vec) const - { m_mux.filter_non_model_lits(vec); } - - bool try_get_state_and_value_from_atom(expr * atom, app *& state, app_ref& value); - bool try_get_state_decl_from_atom(expr * atom, func_decl *& state); - - - std::string pp_model(const model_core & mdl) const - { return m_mux.pp_model(mdl); } - - - void set_background(expr* b) { m_background = b; } - - expr* get_background() const { return m_background; } - - - /** - Return true if we can show that lhs => rhs. The function can have false negatives - (i.e. when smt::context returns unknown), but no false positives. - - bg is background knowledge and can be null - */ - bool implication_surely_holds(expr * lhs, expr * rhs, expr * bg=nullptr); - - unsigned get_unique_num() { return m_next_unique_num++; } - - pdr::smt_context* mk_fresh() { return m_contexts.mk_fresh(); } - - void collect_statistics(statistics& st) const { m_contexts.collect_statistics(st); } - - void reset_statistics() { m_contexts.reset_statistics(); } - }; -} - -#endif diff --git a/src/muz/pdr/pdr_prop_solver.cpp b/src/muz/pdr/pdr_prop_solver.cpp deleted file mode 100644 index 8ebc9b9cb..000000000 --- a/src/muz/pdr/pdr_prop_solver.cpp +++ /dev/null @@ -1,459 +0,0 @@ -/*++ -Copyright (c) 2011 Microsoft Corporation - -Module Name: - - prop_solver.cpp - -Abstract: - - SMT solver abstraction for PDR. - -Author: - - Krystof Hoder (t-khoder) 2011-8-17. - -Revision History: - ---*/ - -#include -#include "model/model.h" -#include "muz/pdr/pdr_util.h" -#include "muz/pdr/pdr_prop_solver.h" -#include "ast/ast_smt2_pp.h" -#include "muz/base/dl_util.h" -#include "model/model_pp.h" -#include "smt/params/smt_params.h" -#include "ast/datatype_decl_plugin.h" -#include "ast/bv_decl_plugin.h" -#include "muz/pdr/pdr_farkas_learner.h" -#include "ast/ast_smt2_pp.h" -#include "ast/rewriter/expr_replacer.h" - -// -// Auxiliary structure to introduce propositional names for assumptions that are not -// propositional. It is to work with the smt::context's restriction -// that assumptions be propositional literals. -// - -namespace pdr { - - class prop_solver::safe_assumptions { - prop_solver& s; - ast_manager& m; - expr_ref_vector m_atoms; - expr_ref_vector m_assumptions; - obj_map m_proxies2expr; - obj_map m_expr2proxies; - unsigned m_num_proxies; - - app * mk_proxy(expr* literal) { - app* res; - SASSERT(!is_var(literal)); //it doesn't make sense to introduce names to variables - if (m_expr2proxies.find(literal, res)) { - return res; - } - SASSERT(s.m_proxies.size() >= m_num_proxies); - if (m_num_proxies == s.m_proxies.size()) { - std::stringstream name; - name << "pdr_proxy_" << s.m_proxies.size(); - res = m.mk_const(symbol(name.str().c_str()), m.mk_bool_sort()); - s.m_proxies.push_back(res); - s.m_aux_symbols.insert(res->get_decl()); - } - else { - res = s.m_proxies[m_num_proxies].get(); - } - ++m_num_proxies; - m_expr2proxies.insert(literal, res); - m_proxies2expr.insert(res, literal); - expr_ref implies(m.mk_or(m.mk_not(res), literal), m); - s.m_ctx->assert_expr(implies); - m_assumptions.push_back(implies); - TRACE("pdr_verbose", tout << "name asserted " << mk_pp(implies, m) << "\n";); - return res; - } - - void mk_safe(expr_ref_vector& conjs) { - flatten_and(conjs); - expand_literals(conjs); - for (unsigned i = 0; i < conjs.size(); ++i) { - expr * lit = conjs[i].get(); - expr * lit_core = lit; - m.is_not(lit, lit_core); - SASSERT(!m.is_true(lit)); - if (!is_uninterp(lit_core) || to_app(lit_core)->get_num_args() != 0) { - conjs[i] = mk_proxy(lit); - } - } - m_assumptions.append(conjs); - } - - expr* apply_accessor( - ptr_vector const& acc, - unsigned j, - func_decl* f, - expr* c) { - if (is_app(c) && to_app(c)->get_decl() == f) { - return to_app(c)->get_arg(j); - } - else { - return m.mk_app(acc[j], c); - } - } - - void expand_literals(expr_ref_vector& conjs) { - arith_util arith(m); - datatype_util dt(m); - bv_util bv(m); - expr* e1, *e2, *c, *val; - rational r; - unsigned bv_size; - - TRACE("pdr", - tout << "begin expand\n"; - for (unsigned i = 0; i < conjs.size(); ++i) { - tout << mk_pp(conjs[i].get(), m) << "\n"; - }); - - for (unsigned i = 0; i < conjs.size(); ++i) { - expr* e = conjs[i].get(); - if (m.is_eq(e, e1, e2) && arith.is_int_real(e1)) { - conjs[i] = arith.mk_le(e1,e2); - if (i+1 == conjs.size()) { - conjs.push_back(arith.mk_ge(e1, e2)); - } - else { - conjs.push_back(conjs[i+1].get()); - conjs[i+1] = arith.mk_ge(e1, e2); - } - ++i; - } - else if ((m.is_eq(e, c, val) && is_app(val) && dt.is_constructor(to_app(val))) || - (m.is_eq(e, val, c) && is_app(val) && dt.is_constructor(to_app(val)))){ - func_decl* f = to_app(val)->get_decl(); - func_decl* r = dt.get_constructor_is(f); - conjs[i] = m.mk_app(r, c); - ptr_vector const& acc = *dt.get_constructor_accessors(f); - for (unsigned j = 0; j < acc.size(); ++j) { - conjs.push_back(m.mk_eq(apply_accessor(acc, j, f, c), to_app(val)->get_arg(j))); - } - } - else if ((m.is_eq(e, c, val) && bv.is_numeral(val, r, bv_size)) || - (m.is_eq(e, val, c) && bv.is_numeral(val, r, bv_size))) { - rational two(2); - for (unsigned j = 0; j < bv_size; ++j) { - parameter p(j); - //expr* e = m.mk_app(bv.get_family_id(), OP_BIT2BOOL, 1, &p, 1, &c); - expr* e = m.mk_eq(m.mk_app(bv.get_family_id(), OP_BIT1), bv.mk_extract(j, j, c)); - if ((r % two).is_zero()) { - e = m.mk_not(e); - } - r = div(r, two); - if (j == 0) { - conjs[i] = e; - } - else { - conjs.push_back(e); - } - } - } - } - TRACE("pdr", - tout << "end expand\n"; - for (unsigned i = 0; i < conjs.size(); ++i) { - tout << mk_pp(conjs[i].get(), m) << "\n"; - }); - } - - public: - safe_assumptions(prop_solver& s, expr_ref_vector const& assumptions): - s(s), m(s.m), m_atoms(assumptions), m_assumptions(m), m_num_proxies(0) { - mk_safe(m_atoms); - } - - ~safe_assumptions() { - } - - expr_ref_vector const& atoms() const { return m_atoms; } - - unsigned assumptions_size() const { return m_assumptions.size(); } - - expr* assumptions(unsigned i) const { return m_assumptions[i]; } - - void undo_proxies(expr_ref_vector& es) { - expr_ref e(m); - expr* r; - for (unsigned i = 0; i < es.size(); ++i) { - e = es[i].get(); - if (is_app(e) && m_proxies2expr.find(to_app(e), r)) { - es[i] = r; - } - } - } - - void elim_proxies(expr_ref_vector& es) { - expr_substitution sub(m, false, m.proofs_enabled()); - proof_ref pr(m); - if (m.proofs_enabled()) { - pr = m.mk_asserted(m.mk_true()); - } - obj_map::iterator it = m_proxies2expr.begin(), end = m_proxies2expr.end(); - for (; it != end; ++it) { - sub.insert(it->m_key, m.mk_true(), pr); - } - scoped_ptr rep = mk_default_expr_replacer(m); - rep->set_substitution(&sub); - replace_proxies(*rep, es); - } - private: - - void replace_proxies(expr_replacer& rep, expr_ref_vector& es) { - expr_ref e(m); - for (unsigned i = 0; i < es.size(); ++i) { - e = es[i].get(); - rep(e); - es[i] = e; - if (m.is_true(e)) { - es[i] = es.back(); - es.pop_back(); - --i; - } - } - } - }; - - - prop_solver::prop_solver(manager& pm, symbol const& name) : - m_fparams(pm.get_fparams()), - m(pm.get_manager()), - m_pm(pm), - m_name(name), - m_ctx(pm.mk_fresh()), - m_pos_level_atoms(m), - m_neg_level_atoms(m), - m_proxies(m), - m_core(nullptr), - m_model(nullptr), - m_consequences(nullptr), - m_subset_based_core(false), - m_use_farkas(false), - m_in_level(false), - m_current_level(0) - { - m_ctx->assert_expr(m_pm.get_background()); - } - - void prop_solver::add_level() { - unsigned idx = level_cnt(); - std::stringstream name; - name << m_name << "#level_" << idx; - func_decl * lev_pred = m.mk_fresh_func_decl(name.str().c_str(), 0, nullptr,m.mk_bool_sort()); - m_aux_symbols.insert(lev_pred); - m_level_preds.push_back(lev_pred); - - app_ref pos_la(m.mk_const(lev_pred), m); - app_ref neg_la(m.mk_not(pos_la.get()), m); - - m_pos_level_atoms.push_back(pos_la); - m_neg_level_atoms.push_back(neg_la); - - m_level_atoms_set.insert(pos_la.get()); - m_level_atoms_set.insert(neg_la.get()); - } - - void prop_solver::ensure_level(unsigned lvl) { - while (lvl>=level_cnt()) { - add_level(); - } - } - - unsigned prop_solver::level_cnt() const { - return m_level_preds.size(); - } - - void prop_solver::push_level_atoms(unsigned level, expr_ref_vector& tgt) const { - unsigned lev_cnt = level_cnt(); - for (unsigned i=0; i=level; - app * lev_atom = active ? m_neg_level_atoms[i] : m_pos_level_atoms[i]; - tgt.push_back(lev_atom); - } - } - - void prop_solver::add_formula(expr * form) { - SASSERT(!m_in_level); - m_ctx->assert_expr(form); - IF_VERBOSE(21, verbose_stream() << "$ asserted " << mk_pp(form, m) << "\n";); - TRACE("pdr", tout << "add_formula: " << mk_pp(form, m) << "\n";); - } - - void prop_solver::add_level_formula(expr * form, unsigned level) { - ensure_level(level); - app * lev_atom = m_pos_level_atoms[level].get(); - app_ref lform(m.mk_or(form, lev_atom), m); - add_formula(lform.get()); - } - - - lbool prop_solver::check_safe_assumptions( - safe_assumptions& safe, - const expr_ref_vector& atoms) - { - flet _model(m_fparams.m_model, m_model != nullptr); - expr_ref_vector expr_atoms(m); - expr_atoms.append(atoms.size(), atoms.c_ptr()); - - if (m_in_level) { - push_level_atoms(m_current_level, expr_atoms); - } - - lbool result = m_ctx->check(expr_atoms); - - TRACE("pdr", - tout << mk_pp(m_pm.mk_and(expr_atoms), m) << "\n"; - tout << result << "\n";); - - if (result == l_true && m_model) { - m_ctx->get_model(*m_model); - TRACE("pdr_verbose", model_pp(tout, **m_model); ); - } - - if (result == l_false) { - unsigned core_size = m_ctx->get_unsat_core_size(); - m_assumes_level = false; - for (unsigned i = 0; i < core_size; ++i) { - if (m_level_atoms_set.contains(m_ctx->get_unsat_core_expr(i))) { - m_assumes_level = true; - break; - } - } - } - - if (result == l_false && - m_core && - m.proofs_enabled() && - m_use_farkas && - !m_subset_based_core) { - extract_theory_core(safe); - } - else if (result == l_false && m_core) { - extract_subset_core(safe); - SASSERT(expr_atoms.size() >= m_core->size()); - } - m_core = nullptr; - m_model = nullptr; - m_subset_based_core = false; - return result; - } - - void prop_solver::extract_subset_core(safe_assumptions& safe) { - unsigned core_size = m_ctx->get_unsat_core_size(); - m_core->reset(); - for (unsigned i = 0; i < core_size; ++i) { - expr * core_expr = m_ctx->get_unsat_core_expr(i); - SASSERT(is_app(core_expr)); - - if (m_level_atoms_set.contains(core_expr)) { - continue; - } - if (m_ctx->is_aux_predicate(core_expr)) { - continue; - } - m_core->push_back(to_app(core_expr)); - } - - safe.undo_proxies(*m_core); - - TRACE("pdr", - tout << "core_exprs: "; - for (unsigned i = 0; i < core_size; ++i) { - tout << mk_pp(m_ctx->get_unsat_core_expr(i), m) << " "; - } - tout << "\n"; - tout << "core: " << mk_pp(m_pm.mk_and(*m_core), m) << "\n"; - ); - } - - - void prop_solver::extract_theory_core(safe_assumptions& safe) { - proof_ref pr(m); - pr = m_ctx->get_proof(); - IF_VERBOSE(21, verbose_stream() << mk_ismt2_pp(pr, m) << "\n";); - farkas_learner fl(m_fparams, m); - expr_ref_vector lemmas(m); - obj_hashtable bs; - for (unsigned i = 0; i < safe.assumptions_size(); ++i) { - bs.insert(safe.assumptions(i)); - } - fl.get_lemmas(pr, bs, lemmas); - safe.elim_proxies(lemmas); - fl.simplify_lemmas(lemmas); // redundant? - - bool outside_of_logic = - (m_fparams.m_arith_mode == AS_DIFF_LOGIC && - !is_difference_logic(m, lemmas.size(), lemmas.c_ptr())) || - (m_fparams.m_arith_mode == AS_UTVPI && - !is_utvpi_logic(m, lemmas.size(), lemmas.c_ptr())); - - if (outside_of_logic) { - IF_VERBOSE(2, - verbose_stream() << "not diff\n"; - for (unsigned i = 0; i < lemmas.size(); ++i) { - verbose_stream() << mk_pp(lemmas[i].get(), m) << "\n"; - }); - extract_subset_core(safe); - } - else { - - IF_VERBOSE(2, - verbose_stream() << "Lemmas\n"; - for (unsigned i = 0; i < lemmas.size(); ++i) { - verbose_stream() << mk_pp(lemmas[i].get(), m) << "\n"; - }); - - m_core->reset(); - m_core->append(lemmas); - - if (m_consequences) { - fl.get_consequences(pr, bs, *m_consequences); - } - } - } - - lbool prop_solver::check_assumptions(const expr_ref_vector & atoms) { - return check_assumptions_and_formula(atoms, m.mk_true()); - } - - lbool prop_solver::check_conjunction_as_assumptions(expr * conj) { - expr_ref_vector asmp(m); - asmp.push_back(conj); - return check_assumptions(asmp); - } - - lbool prop_solver::check_assumptions_and_formula(const expr_ref_vector & atoms, expr * form) - { - pdr::smt_context::scoped _scoped(*m_ctx); - safe_assumptions safe(*this, atoms); - m_ctx->assert_expr(form); - CTRACE("pdr", !m.is_true(form), tout << "check with formula: " << mk_pp(form, m) << "\n";); - lbool res = check_safe_assumptions(safe, safe.atoms()); - - // - // we don't have to undo model naming, as from the model - // we extract the values for state variables directly - // - return res; - } - - void prop_solver::collect_statistics(statistics& st) const { - } - - void prop_solver::reset_statistics() { - } - - - - -} diff --git a/src/muz/pdr/pdr_prop_solver.h b/src/muz/pdr/pdr_prop_solver.h deleted file mode 100644 index 463163fbd..000000000 --- a/src/muz/pdr/pdr_prop_solver.h +++ /dev/null @@ -1,139 +0,0 @@ -/*++ -Copyright (c) 2011 Microsoft Corporation - -Module Name: - - prop_solver.h - -Abstract: - - SAT solver abstraction for PDR. - -Author: - - Krystof Hoder (t-khoder) 2011-8-17. - -Revision History: - ---*/ - -#ifndef PROP_SOLVER_H_ -#define PROP_SOLVER_H_ - -#include -#include -#include -#include "ast/ast.h" -#include "util/obj_hashtable.h" -#include "smt/smt_kernel.h" -#include "util/util.h" -#include "util/vector.h" -#include "muz/pdr/pdr_manager.h" -#include "muz/pdr/pdr_smt_context_manager.h" - - -namespace pdr { - class prop_solver { - - private: - smt_params& m_fparams; - ast_manager& m; - manager& m_pm; - symbol m_name; - scoped_ptr m_ctx; - decl_vector m_level_preds; - app_ref_vector m_pos_level_atoms; // atoms used to identify level - app_ref_vector m_neg_level_atoms; // - obj_hashtable m_level_atoms_set; - app_ref_vector m_proxies; // predicates for assumptions - expr_ref_vector* m_core; - model_ref* m_model; - expr_ref_vector* m_consequences; - bool m_subset_based_core; - bool m_assumes_level; - bool m_use_farkas; - func_decl_set m_aux_symbols; - bool m_in_level; - unsigned m_current_level; // set when m_in_level - - /** Add level atoms activating certain level into a vector */ - void push_level_atoms(unsigned level, expr_ref_vector & tgt) const; - - void ensure_level(unsigned lvl); - - class safe_assumptions; - - void extract_theory_core(safe_assumptions& assumptions); - - void extract_subset_core(safe_assumptions& assumptions); - - lbool check_safe_assumptions( - safe_assumptions& assumptions, - expr_ref_vector const& atoms); - - - public: - prop_solver(pdr::manager& pm, symbol const& name); - - /** return true is s is a symbol introduced by prop_solver */ - bool is_aux_symbol(func_decl * s) const { - return - m_aux_symbols.contains(s) || - m_ctx->is_aux_predicate(s); - } - - void set_core(expr_ref_vector* core) { m_core = core; } - void set_model(model_ref* mdl) { m_model = mdl; } - void set_subset_based_core(bool f) { m_subset_based_core = f; } - void set_consequences(expr_ref_vector* consequences) { m_consequences = consequences; } - - bool assumes_level() const { return m_assumes_level; } - - void add_level(); - unsigned level_cnt() const; - - class scoped_level { - bool& m_lev; - public: - scoped_level(prop_solver& ps, unsigned lvl):m_lev(ps.m_in_level) { - SASSERT(!m_lev); m_lev = true; ps.m_current_level = lvl; - } - ~scoped_level() { m_lev = false; } - }; - - void set_use_farkas(bool f) { m_use_farkas = f; } - bool get_use_farkas() const { return m_use_farkas; } - - void add_formula(expr * form); - void add_level_formula(expr * form, unsigned level); - - /** - * Return true iff conjunction of atoms is consistent with the current state of - * the solver. - * - * If the conjunction of atoms is inconsistent with the solver state and core is non-zero, - * core will contain an unsatisfiable core of atoms. - * - * If the conjunction of atoms is consistent with the solver state and o_model is non-zero, - * o_model will contain the "o" literals true in the assignment. - */ - lbool check_assumptions(const expr_ref_vector & atoms); - - lbool check_conjunction_as_assumptions(expr * conj); - - /** - * Like check_assumptions, except it also asserts an extra formula - */ - lbool check_assumptions_and_formula( - const expr_ref_vector & atoms, - expr * form); - - void collect_statistics(statistics& st) const; - - void reset_statistics(); - - }; -} - - -#endif diff --git a/src/muz/pdr/pdr_reachable_cache.cpp b/src/muz/pdr/pdr_reachable_cache.cpp deleted file mode 100644 index 5d553df4d..000000000 --- a/src/muz/pdr/pdr_reachable_cache.cpp +++ /dev/null @@ -1,132 +0,0 @@ -/*++ -Copyright (c) 2011 Microsoft Corporation - -Module Name: - - reachable_cache.cpp - -Abstract: - - Object for caching of reachable states. - -Author: - - Krystof Hoder (t-khoder) 2011-9-14. - -Revision History: - ---*/ - -#include "muz/pdr/pdr_reachable_cache.h" - -namespace pdr { - - reachable_cache::reachable_cache(pdr::manager & pm, datalog::PDR_CACHE_MODE cm) - : m(pm.get_manager()), - m_pm(pm), - m_ctx(nullptr), - m_ref_holder(m), - m_disj_connector(m), - m_cache_mode(cm) { - if (m_cache_mode == datalog::CONSTRAINT_CACHE) { - m_ctx = pm.mk_fresh(); - m_ctx->assert_expr(m_pm.get_background()); - } - } - - - void reachable_cache::add_disjuncted_formula(expr * f) { - app_ref new_connector(m.mk_fresh_const("disj_conn", m.mk_bool_sort()), m); - app_ref neg_new_connector(m.mk_not(new_connector), m); - app_ref extended_form(m); - - if(m_disj_connector) { - extended_form = m.mk_or(m_disj_connector, neg_new_connector, f); - } - else { - extended_form = m.mk_or(neg_new_connector, f); - } - if (m_ctx) { - m_ctx->assert_expr(extended_form); - } - - m_disj_connector = new_connector; - } - - void reachable_cache::add_reachable(expr * cube) { - - switch (m_cache_mode) { - case datalog::NO_CACHE: - break; - - case datalog::HASH_CACHE: - m_stats.m_inserts++; - m_cache.insert(cube); - m_ref_holder.push_back(cube); - break; - - case datalog::CONSTRAINT_CACHE: - m_stats.m_inserts++; - TRACE("pdr", tout << mk_pp(cube, m) << "\n";); - add_disjuncted_formula(cube); - break; - - default: - UNREACHABLE(); - } - } - - bool reachable_cache::is_reachable(expr * cube) { - bool found = false; - switch (m_cache_mode) { - case datalog::NO_CACHE: - return false; - - case datalog::HASH_CACHE: - found = m_cache.contains(cube); - break; - - case datalog::CONSTRAINT_CACHE: { - if(!m_disj_connector) { - found = false; - break; - } - expr * connector = m_disj_connector.get(); - expr_ref_vector assms(m); - assms.push_back(connector); - m_ctx->push(); - m_ctx->assert_expr(cube); - lbool res = m_ctx->check(assms); - m_ctx->pop(); - - TRACE("pdr", tout << "is_reachable: " << res << " " << mk_pp(cube, m) << "\n";); - - found = res == l_true; - break; - } - - default: - UNREACHABLE(); - break; - } - if (found) { - m_stats.m_hits++; - } - else { - m_stats.m_miss++; - } - return found; - } - - void reachable_cache::collect_statistics(statistics& st) const { - st.update("cache inserts", m_stats.m_inserts); - st.update("cache miss", m_stats.m_miss); - st.update("cache hits", m_stats.m_hits); - } - - void reachable_cache::reset_statistics() { - m_stats.reset(); - } - - -} diff --git a/src/muz/pdr/pdr_reachable_cache.h b/src/muz/pdr/pdr_reachable_cache.h deleted file mode 100644 index 0833541ba..000000000 --- a/src/muz/pdr/pdr_reachable_cache.h +++ /dev/null @@ -1,66 +0,0 @@ -/*++ -Copyright (c) 2011 Microsoft Corporation - -Module Name: - - reachable_cache.h - -Abstract: - - Object for caching of reachable states. - -Author: - - Krystof Hoder (t-khoder) 2011-9-14. - -Revision History: - ---*/ - - -#ifndef REACHABLE_CACHE_H_ -#define REACHABLE_CACHE_H_ -#include "ast/ast.h" -#include "util/ref_vector.h" -#include "muz/pdr/pdr_manager.h" -#include "muz/pdr/pdr_smt_context_manager.h" - -namespace pdr { - class reachable_cache { - struct stats { - unsigned m_hits; - unsigned m_miss; - unsigned m_inserts; - stats() { reset(); } - void reset() { memset(this, 0, sizeof(*this)); } - }; - - ast_manager & m; - manager & m_pm; - scoped_ptr m_ctx; - ast_ref_vector m_ref_holder; - app_ref m_disj_connector; - obj_hashtable m_cache; - stats m_stats; - datalog::PDR_CACHE_MODE m_cache_mode; - - void add_disjuncted_formula(expr * f); - - public: - reachable_cache(pdr::manager & pm, datalog::PDR_CACHE_MODE cm); - - void add_init(app * f) { add_disjuncted_formula(f); } - - /** add cube whose all models are reachable */ - void add_reachable(expr * cube); - - /** return true if there is a model of cube which is reachable */ - bool is_reachable(expr * cube); - - void collect_statistics(statistics& st) const; - - void reset_statistics(); - }; -} - -#endif diff --git a/src/muz/pdr/pdr_smt_context_manager.cpp b/src/muz/pdr/pdr_smt_context_manager.cpp deleted file mode 100644 index 88734049b..000000000 --- a/src/muz/pdr/pdr_smt_context_manager.cpp +++ /dev/null @@ -1,167 +0,0 @@ -/*++ -Copyright (c) 2011 Microsoft Corporation - -Module Name: - - pdr_smt_context_manager.cpp - -Abstract: - - Manager of smt contexts - -Author: - - Nikolaj Bjorner (nbjorner) 2011-11-26. - -Revision History: - ---*/ - -#include "muz/pdr/pdr_smt_context_manager.h" -#include "ast/has_free_vars.h" -#include "ast/ast_pp.h" -#include "ast/ast_smt_pp.h" -#include -#include "smt/params/smt_params.h" - -namespace pdr { - - smt_context::smt_context(smt_context_manager& p, ast_manager& m, app* pred): - m_pred(pred, m), - m_parent(p), - m_in_delay_scope(false), - m_pushed(false) - {} - - bool smt_context::is_aux_predicate(func_decl* p) { - return m_parent.is_aux_predicate(p); - } - - smt_context::scoped::scoped(smt_context& ctx): m_ctx(ctx) { - SASSERT(!m_ctx.m_in_delay_scope); - SASSERT(!m_ctx.m_pushed); - m_ctx.m_in_delay_scope = true; - } - - smt_context::scoped::~scoped() { - SASSERT(m_ctx.m_in_delay_scope); - if (m_ctx.m_pushed) { - m_ctx.pop(); - m_ctx.m_pushed = false; - } - m_ctx.m_in_delay_scope = false; - } - - - _smt_context::_smt_context(smt::kernel & ctx, smt_context_manager& p, app* pred): - smt_context(p, ctx.m(), pred), - m_context(ctx) - {} - - void _smt_context::assert_expr(expr* e) { - ast_manager& m = m_context.m(); - if (m.is_true(e)) { - return; - } - CTRACE("pdr", has_free_vars(e), tout << mk_pp(e, m) << "\n";); - SASSERT(!has_free_vars(e)); - if (m_in_delay_scope && !m_pushed) { - m_context.push(); - m_pushed = true; - } - expr_ref fml(m); - fml = m_pushed?e:m.mk_implies(m_pred, e); - m_context.assert_expr(fml); - } - - lbool _smt_context::check(expr_ref_vector& assumptions) { - ast_manager& m = m_pred.get_manager(); - if (!m.is_true(m_pred)) { - assumptions.push_back(m_pred); - } - TRACE("pdr_check", - { - ast_smt_pp pp(m); - for (unsigned i = 0; i < m_context.size(); ++i) { - pp.add_assumption(m_context.get_formula(i)); - } - for (unsigned i = 0; i < assumptions.size(); ++i) { - pp.add_assumption(assumptions[i].get()); - } - - static unsigned lemma_id = 0; - std::ostringstream strm; - strm << "pdr-lemma-" << lemma_id << ".smt2"; - std::ofstream out(strm.str().c_str()); - pp.display_smt2(out, m.mk_true()); - out.close(); - lemma_id++; - tout << "pdr_check: " << strm.str() << "\n"; - }); - lbool result = m_context.check(assumptions.size(), assumptions.c_ptr()); - if (!m.is_true(m_pred)) { - assumptions.pop_back(); - } - return result; - } - - void _smt_context::get_model(model_ref& model) { - m_context.get_model(model); - } - - proof* _smt_context::get_proof() { - return m_context.get_proof(); - } - - smt_context_manager::smt_context_manager(smt_params& fp, unsigned max_num_contexts, ast_manager& m): - m_fparams(fp), - m(m), - m_max_num_contexts(max_num_contexts), - m_num_contexts(0), - m_predicate_list(m) { - } - - - smt_context_manager::~smt_context_manager() { - TRACE("pdr",tout << "\n";); - std::for_each(m_contexts.begin(), m_contexts.end(), delete_proc()); - } - - smt_context* smt_context_manager::mk_fresh() { - ++m_num_contexts; - app_ref pred(m); - smt::kernel * ctx = nullptr; - if (m_max_num_contexts == 0) { - m_contexts.push_back(alloc(smt::kernel, m, m_fparams)); - pred = m.mk_true(); - ctx = m_contexts[m_num_contexts-1]; - } - else { - if (m_contexts.size() < m_max_num_contexts) { - m_contexts.push_back(alloc(smt::kernel, m, m_fparams)); - } - std::stringstream name; - name << "#context" << m_num_contexts; - pred = m.mk_const(symbol(name.str().c_str()), m.mk_bool_sort()); - m_predicate_list.push_back(pred); - m_predicate_set.insert(pred->get_decl()); - ctx = m_contexts[(m_num_contexts-1)%m_max_num_contexts]; - } - return alloc(_smt_context, *ctx, *this, pred); - } - - void smt_context_manager::collect_statistics(statistics& st) const { - for (unsigned i = 0; i < m_contexts.size(); ++i) { - m_contexts[i]->collect_statistics(st); - } - } - - void smt_context_manager::reset_statistics() { - for (unsigned i = 0; i < m_contexts.size(); ++i) { - m_contexts[i]->reset_statistics(); - } - } - - -}; - diff --git a/src/muz/pdr/pdr_smt_context_manager.h b/src/muz/pdr/pdr_smt_context_manager.h deleted file mode 100644 index 747cd6457..000000000 --- a/src/muz/pdr/pdr_smt_context_manager.h +++ /dev/null @@ -1,92 +0,0 @@ -/*++ -Copyright (c) 2011 Microsoft Corporation - -Module Name: - - pdr_smt_context_manager.h - -Abstract: - - Manager of smt contexts - -Author: - - Nikolaj Bjorner (nbjorner) 2011-11-26. - -Revision History: - ---*/ - -#ifndef PDR_SMT_CONTEXT_MANAGER_H_ -#define PDR_SMT_CONTEXT_MANAGER_H_ - -#include "smt/smt_kernel.h" -#include "ast/func_decl_dependencies.h" -#include "muz/base/dl_util.h" - -namespace pdr { - - class smt_context_manager; - - class smt_context { - protected: - app_ref m_pred; - smt_context_manager& m_parent; - bool m_in_delay_scope; - bool m_pushed; - public: - smt_context(smt_context_manager& p, ast_manager& m, app* pred); - virtual ~smt_context() {} - virtual void assert_expr(expr* e) = 0; - virtual lbool check(expr_ref_vector& assumptions) = 0; - virtual void get_model(model_ref& model) = 0; - virtual proof* get_proof() = 0; - virtual unsigned get_unsat_core_size() = 0; - virtual expr* get_unsat_core_expr(unsigned i) = 0; - virtual void push() = 0; - virtual void pop() = 0; - bool is_aux_predicate(func_decl* p); - bool is_aux_predicate(expr* p) { return is_app(p) && is_aux_predicate(to_app(p)->get_decl()); } - class scoped { - smt_context& m_ctx; - public: - scoped(smt_context& ctx); - ~scoped(); - }; - }; - - class _smt_context : public smt_context { - smt::kernel & m_context; - public: - _smt_context(smt::kernel & ctx, smt_context_manager& p, app* pred); - ~_smt_context() override {} - void assert_expr(expr* e) override; - lbool check(expr_ref_vector& assumptions) override; - void get_model(model_ref& model) override; - proof* get_proof() override; - void push() override { m_context.push(); } - void pop() override { m_context.pop(1); } - unsigned get_unsat_core_size() override { return m_context.get_unsat_core_size(); } - expr* get_unsat_core_expr(unsigned i) override { return m_context.get_unsat_core_expr(i); } - }; - - class smt_context_manager { - smt_params& m_fparams; - ast_manager& m; - unsigned m_max_num_contexts; - ptr_vector m_contexts; - unsigned m_num_contexts; - app_ref_vector m_predicate_list; - func_decl_set m_predicate_set; - public: - smt_context_manager(smt_params& fp, unsigned max_num_contexts, ast_manager& m); - ~smt_context_manager(); - smt_context* mk_fresh(); - void collect_statistics(statistics& st) const; - void reset_statistics(); - bool is_aux_predicate(func_decl* p) const { return m_predicate_set.contains(p); } - }; - -}; - -#endif diff --git a/src/muz/pdr/pdr_sym_mux.cpp b/src/muz/pdr/pdr_sym_mux.cpp deleted file mode 100644 index 72549f2d6..000000000 --- a/src/muz/pdr/pdr_sym_mux.cpp +++ /dev/null @@ -1,601 +0,0 @@ -/*++ -Copyright (c) 2011 Microsoft Corporation - -Module Name: - - sym_mux.cpp - -Abstract: - - A symbol multiplexer that helps with having multiple versions of each of a set of symbols. - -Author: - - Krystof Hoder (t-khoder) 2011-9-8. - -Revision History: - ---*/ - -#include -#include "ast/ast_pp.h" -#include "ast/for_each_expr.h" -#include "model/model.h" -#include "ast/rewriter/rewriter.h" -#include "ast/rewriter/rewriter_def.h" -#include "muz/pdr/pdr_util.h" -#include "muz/pdr/pdr_sym_mux.h" - -using namespace pdr; - -sym_mux::sym_mux(ast_manager & m) - : m(m), m_ref_holder(m), - m_next_sym_suffix_idx(0) { - m_suffixes.push_back("_n"); - size_t suf_sz = m_suffixes.size(); - for(unsigned i = 0; i < suf_sz; ++i) { - symbol suff_sym = symbol(m_suffixes[i].c_str()); - m_used_suffixes.insert(suff_sym); - } -} - -std::string sym_mux::get_suffix(unsigned i) { - while(m_suffixes.size() <= i) { - std::string new_suffix; - symbol new_syffix_sym; - do { - std::stringstream stm; - stm<<'_'<0); - while(tuple.size()get_name().str(); - for(unsigned i=0; iget_arity()==arity); - SASSERT(tuple[i]->get_range()==range); - //domain should match as well, but we won't bother checking an array equality - } - else { - std::string name = pre+get_suffix(i); - tuple[i] = m.mk_func_decl(symbol(name.c_str()), arity, domain, range); - } - m_ref_holder.push_back(tuple[i]); - m_sym2idx.insert(tuple[i], i); - m_sym2prim.insert(tuple[i], tuple[0]); - } - - m_prim2all.insert(tuple[0], tuple); - m_prefix2prim.insert(prefix, tuple[0]); - m_prim2prefix.insert(tuple[0], prefix); - m_prim_preds.push_back(tuple[0]); - m_ref_holder.push_back(prefix); -} - -void sym_mux::ensure_tuple_size(func_decl * prim, unsigned sz) { - SASSERT(m_prim2all.contains(prim)); - decl_vector& tuple = m_prim2all.find_core(prim)->get_data().m_value; - SASSERT(tuple[0]==prim); - - if(sz <= tuple.size()) { return; } - - func_decl * prefix; - TRUSTME(m_prim2prefix.find(prim, prefix)); - std::string prefix_name = prefix->get_name().bare_str(); - for(unsigned i = tuple.size(); i < sz; ++i) { - std::string name = prefix_name + get_suffix(i); - func_decl * new_sym = m.mk_func_decl(symbol(name.c_str()), prefix->get_arity(), - prefix->get_domain(), prefix->get_range()); - - tuple.push_back(new_sym); - m_ref_holder.push_back(new_sym); - m_sym2idx.insert(new_sym, i); - m_sym2prim.insert(new_sym, prim); - } -} - -func_decl * sym_mux::conv(func_decl * sym, unsigned src_idx, unsigned tgt_idx) -{ - if(src_idx==tgt_idx) { return sym; } - func_decl * prim = (src_idx==0) ? sym : get_primary(sym); - if(tgt_idx>src_idx) { - ensure_tuple_size(prim, tgt_idx+1); - } - decl_vector & sym_vect = m_prim2all.find_core(prim)->get_data().m_value; - SASSERT(sym_vect[src_idx]==sym); - return sym_vect[tgt_idx]; -} - - -func_decl * sym_mux::get_or_create_symbol_by_prefix(func_decl* prefix, unsigned idx, - unsigned arity, sort * const * domain, sort * range) -{ - func_decl * prim = try_get_primary_by_prefix(prefix); - if(prim) { - SASSERT(prim->get_arity()==arity); - SASSERT(prim->get_range()==range); - //domain should match as well, but we won't bother checking an array equality - - return conv(prim, 0, idx); - } - - decl_vector syms; - create_tuple(prefix, arity, domain, range, idx+1, syms); - return syms[idx]; -} - -bool sym_mux::is_muxed_lit(expr * e, unsigned idx) const -{ - if(!is_app(e)) { return false; } - app * a = to_app(e); - if(m.is_not(a) && is_app(a->get_arg(0))) { - a = to_app(a->get_arg(0)); - } - return is_muxed(a->get_decl()); -} - - -struct sym_mux::formula_checker -{ - formula_checker(const sym_mux & parent, bool all, unsigned idx) : - m_parent(parent), m_all(all), m_idx(idx), - m_found_what_needed(false) - { - } - - void operator()(expr * e) - { - if(m_found_what_needed || !is_app(e)) { return; } - - func_decl * sym = to_app(e)->get_decl(); - unsigned sym_idx; - if(!m_parent.try_get_index(sym, sym_idx)) { return; } - - bool have_idx = sym_idx==m_idx; - - if( m_all ? (!have_idx) : have_idx ) { - m_found_what_needed = true; - } - - } - - bool all_have_idx() const - { - SASSERT(m_all); //we were looking for the queried property - return !m_found_what_needed; - } - - bool some_with_idx() const - { - SASSERT(!m_all); //we were looking for the queried property - return m_found_what_needed; - } - -private: - const sym_mux & m_parent; - bool m_all; - unsigned m_idx; - - /** - If we check whether all muxed symbols are of given index, we look for - counter-examples, checking whether form contains a muxed symbol of an index, - we look for symbol of index m_idx. - */ - bool m_found_what_needed; -}; - -bool sym_mux::contains(expr * e, unsigned idx) const -{ - formula_checker chck(*this, false, idx); - for_each_expr(chck, m_visited, e); - m_visited.reset(); - return chck.some_with_idx(); -} - -bool sym_mux::is_homogenous_formula(expr * e, unsigned idx) const -{ - formula_checker chck(*this, true, idx); - for_each_expr(chck, m_visited, e); - m_visited.reset(); - return chck.all_have_idx(); -} - -bool sym_mux::is_homogenous(const expr_ref_vector & vect, unsigned idx) const -{ - expr * const * begin = vect.c_ptr(); - expr * const * end = begin + vect.size(); - for(expr * const * it = begin; it!=end; it++) { - if(!is_homogenous_formula(*it, idx)) { - return false; - } - } - return true; -} - -class sym_mux::index_collector { - sym_mux const& m_parent; - svector m_indices; -public: - index_collector(sym_mux const& s): - m_parent(s) {} - - void operator()(expr * e) { - if (is_app(e)) { - func_decl * sym = to_app(e)->get_decl(); - unsigned idx; - if (m_parent.try_get_index(sym, idx)) { - SASSERT(idx > 0); - --idx; - if (m_indices.size() <= idx) { - m_indices.resize(idx+1, false); - } - m_indices[idx] = true; - } - } - } - - void extract(unsigned_vector& indices) { - for (unsigned i = 0; i < m_indices.size(); ++i) { - if (m_indices[i]) { - indices.push_back(i); - } - } - } -}; - - - -void sym_mux::collect_indices(expr* e, unsigned_vector& indices) const { - indices.reset(); - index_collector collector(*this); - for_each_expr(collector, m_visited, e); - m_visited.reset(); - collector.extract(indices); -} - -class sym_mux::variable_collector { - sym_mux const& m_parent; - vector >& m_vars; -public: - variable_collector(sym_mux const& s, vector >& vars): - m_parent(s), m_vars(vars) {} - - void operator()(expr * e) { - if (is_app(e)) { - func_decl * sym = to_app(e)->get_decl(); - unsigned idx; - if (m_parent.try_get_index(sym, idx)) { - SASSERT(idx > 0); - --idx; - if (m_vars.size() <= idx) { - m_vars.resize(idx+1, ptr_vector()); - } - m_vars[idx].push_back(to_app(e)); - } - } - } -}; - -void sym_mux::collect_variables(expr* e, vector >& vars) const { - vars.reset(); - variable_collector collector(*this, vars); - for_each_expr(collector, m_visited, e); - m_visited.reset(); -} - -class sym_mux::hmg_checker { - const sym_mux & m_parent; - - bool m_found_idx; - unsigned m_idx; - bool m_multiple_indexes; - -public: - hmg_checker(const sym_mux & parent) : - m_parent(parent), m_found_idx(false), m_multiple_indexes(false) - { - } - - void operator()(expr * e) - { - if(m_multiple_indexes || !is_app(e)) { return; } - - func_decl * sym = to_app(e)->get_decl(); - unsigned sym_idx; - if(!m_parent.try_get_index(sym, sym_idx)) { return; } - - if(!m_found_idx) { - m_found_idx = true; - m_idx = sym_idx; - return; - } - if(m_idx==sym_idx) { return; } - m_multiple_indexes = true; - } - - bool has_multiple_indexes() const - { - return m_multiple_indexes; - } -}; - -bool sym_mux::is_homogenous_formula(expr * e) const { - hmg_checker chck(*this); - for_each_expr(chck, m_visited, e); - m_visited.reset(); - return !chck.has_multiple_indexes(); -} - - -struct sym_mux::conv_rewriter_cfg : public default_rewriter_cfg -{ -private: - ast_manager & m; - sym_mux & m_parent; - unsigned m_from_idx; - unsigned m_to_idx; - bool m_homogenous; -public: - conv_rewriter_cfg(sym_mux & parent, unsigned from_idx, unsigned to_idx, bool homogenous) - : m(parent.get_manager()), - m_parent(parent), - m_from_idx(from_idx), - m_to_idx(to_idx), - m_homogenous(homogenous) {} - - bool get_subst(expr * s, expr * & t, proof * & t_pr) { - if(!is_app(s)) { return false; } - app * a = to_app(s); - func_decl * sym = a->get_decl(); - if(!m_parent.has_index(sym, m_from_idx)) { - (void) m_homogenous; - SASSERT(!m_homogenous || !m_parent.is_muxed(sym)); - return false; - } - func_decl * tgt = m_parent.conv(sym, m_from_idx, m_to_idx); - - t = m.mk_app(tgt, a->get_args()); - return true; - } -}; - -void sym_mux::conv_formula(expr * f, unsigned src_idx, unsigned tgt_idx, expr_ref & res, bool homogenous) -{ - if(src_idx==tgt_idx) { - res = f; - return; - } - conv_rewriter_cfg r_cfg(*this, src_idx, tgt_idx, homogenous); - rewriter_tpl rwr(m, false, r_cfg); - rwr(f, res); -} - -struct sym_mux::shifting_rewriter_cfg : public default_rewriter_cfg -{ -private: - ast_manager & m; - sym_mux & m_parent; - int m_shift; -public: - shifting_rewriter_cfg(sym_mux & parent, int shift) - : m(parent.get_manager()), - m_parent(parent), - m_shift(shift) {} - - bool get_subst(expr * s, expr * & t, proof * & t_pr) { - if(!is_app(s)) { return false; } - app * a = to_app(s); - func_decl * sym = a->get_decl(); - - unsigned idx; - if(!m_parent.try_get_index(sym, idx)) { - return false; - } - SASSERT(static_cast(idx)+m_shift>=0); - func_decl * tgt = m_parent.conv(sym, idx, idx+m_shift); - t = m.mk_app(tgt, a->get_args()); - return true; - } -}; - -void sym_mux::shift_formula(expr * f, int dist, expr_ref & res) -{ - if(dist==0) { - res = f; - return; - } - shifting_rewriter_cfg r_cfg(*this, dist); - rewriter_tpl rwr(m, false, r_cfg); - rwr(f, res); -} - -void sym_mux::conv_formula_vector(const expr_ref_vector & vect, unsigned src_idx, unsigned tgt_idx, - expr_ref_vector & res) -{ - res.reset(); - expr * const * begin = vect.c_ptr(); - expr * const * end = begin + vect.size(); - for(expr * const * it = begin; it!=end; it++) { - expr_ref converted(m); - conv_formula(*it, src_idx, tgt_idx, converted); - res.push_back(converted); - } -} - -void sym_mux::filter_idx(expr_ref_vector & vect, unsigned idx) const { - unsigned i = 0; - while (i < vect.size()) { - expr* e = vect[i].get(); - if (contains(e, idx) && is_homogenous_formula(e, idx)) { - i++; - } - else { - // we don't allow mixing states inside vector elements - SASSERT(!contains(e, idx)); - vect[i] = vect.back(); - vect.pop_back(); - } - } -} - -void sym_mux::partition_o_idx( - expr_ref_vector const& lits, - expr_ref_vector& o_lits, - expr_ref_vector& other, unsigned idx) const { - - for (unsigned i = 0; i < lits.size(); ++i) { - if (contains(lits[i], idx) && is_homogenous_formula(lits[i], idx)) { - o_lits.push_back(lits[i]); - } - else { - other.push_back(lits[i]); - } - } -} - - - -class sym_mux::nonmodel_sym_checker { - const sym_mux & m_parent; - - bool m_found; -public: - nonmodel_sym_checker(const sym_mux & parent) : - m_parent(parent), m_found(false) { - } - - void operator()(expr * e) { - if(m_found || !is_app(e)) { return; } - - func_decl * sym = to_app(e)->get_decl(); - - if(m_parent.is_non_model_sym(sym)) { - m_found = true; - } - } - - bool found() const { - return m_found; - } -}; - -bool sym_mux::has_nonmodel_symbol(expr * e) const { - nonmodel_sym_checker chck(*this); - for_each_expr(chck, e); - return chck.found(); -} - -void sym_mux::filter_non_model_lits(expr_ref_vector & vect) const { - unsigned i = 0; - while (i < vect.size()) { - if (!has_nonmodel_symbol(vect[i].get())) { - i++; - } - else { - vect[i] = vect.back(); - vect.pop_back(); - } - } -} - -class sym_mux::decl_idx_comparator -{ - const sym_mux & m_parent; -public: - decl_idx_comparator(const sym_mux & parent) - : m_parent(parent) - { } - - bool operator()(func_decl * sym1, func_decl * sym2) - { - unsigned idx1, idx2; - if (!m_parent.try_get_index(sym1, idx1)) { idx1 = UINT_MAX; } - if (!m_parent.try_get_index(sym2, idx2)) { idx2 = UINT_MAX; } - - if (idx1 != idx2) { return idx1get_name(), sym2->get_name()); - } -}; - -std::string sym_mux::pp_model(const model_core & mdl) const { - decl_vector consts; - unsigned sz = mdl.get_num_constants(); - for (unsigned i = 0; i < sz; i++) { - func_decl * d = mdl.get_constant(i); - consts.push_back(d); - } - - std::sort(consts.begin(), consts.end(), decl_idx_comparator(*this)); - - std::stringstream res; - - decl_vector::iterator end = consts.end(); - for (decl_vector::iterator it = consts.begin(); it!=end; it++) { - func_decl * d = *it; - std::string name = d->get_name().str(); - const char * arrow = " -> "; - res << name << arrow; - unsigned indent = static_cast(name.length() + strlen(arrow)); - res << mk_pp(mdl.get_const_interp(d), m, indent) << "\n"; - - if (it+1 != end) { - unsigned idx1, idx2; - if (!try_get_index(*it, idx1)) { idx1 = UINT_MAX; } - if (!try_get_index(*(it+1), idx2)) { idx2 = UINT_MAX; } - if (idx1 != idx2) { res << "\n"; } - } - } - return res.str(); -} - - -#if 0 - -class sym_mux::index_renamer_cfg : public default_rewriter_cfg{ - const sym_mux & m_parent; - unsigned m_idx; - -public: - index_renamer_cfg(const sym_mux & p, unsigned idx) : m_parent(p), m_idx(idx) {} - - bool get_subst(expr * s, expr * & t, proof * & t_pr) { - if (!is_app(s)) return false; - app * a = to_app(s); - if (a->get_family_id() != null_family_id) { - return false; - } - func_decl * sym = a->get_decl(); - unsigned idx; - if(!m_parent.try_get_index(sym, idx)) { - return false; - } - if (m_idx == idx) { - return false; - } - ast_manager& m = m_parent.get_manager(); - symbol name = symbol((sym->get_name().str() + "!").c_str()); - func_decl * tgt = m.mk_func_decl(name, sym->get_arity(), sym->get_domain(), sym->get_range()); - t = m.mk_app(tgt, a->get_num_args(), a->get_args()); - return true; - } -}; - -#endif diff --git a/src/muz/pdr/pdr_sym_mux.h b/src/muz/pdr/pdr_sym_mux.h deleted file mode 100644 index 64a2878a9..000000000 --- a/src/muz/pdr/pdr_sym_mux.h +++ /dev/null @@ -1,247 +0,0 @@ -/*++ -Copyright (c) 2011 Microsoft Corporation - -Module Name: - - sym_mux.h - -Abstract: - - A symbol multiplexer that helps with having multiple versions of each of a set of symbols. - -Author: - - Krystof Hoder (t-khoder) 2011-9-8. - -Revision History: - ---*/ - -#ifndef SYM_MUX_H_ -#define SYM_MUX_H_ - -#include "ast/ast.h" -#include "util/map.h" -#include "util/vector.h" -#include - -class model_core; - -namespace pdr { -class sym_mux -{ -public: - typedef ptr_vector app_vector; - typedef ptr_vector decl_vector; -private: - typedef obj_map sym2u; - typedef obj_map sym2dv; - typedef obj_map sym2sym; - typedef obj_map sym2pred; - typedef hashtable symbols; - - ast_manager & m; - mutable ast_ref_vector m_ref_holder; - mutable expr_mark m_visited; - - mutable unsigned m_next_sym_suffix_idx; - mutable symbols m_used_suffixes; - /** Here we have default suffixes for each of the variants */ - std::vector m_suffixes; - - - /** - Primary symbol is the 0-th variant. This member maps from primary symbol - to vector of all its variants (including the primary variant). - */ - sym2dv m_prim2all; - - /** - For each symbol contains its variant index - */ - mutable sym2u m_sym2idx; - /** - For each symbol contains its primary variant - */ - mutable sym2sym m_sym2prim; - - /** - Maps prefixes passed to the create_tuple to - the primary symbol created from it. - */ - sym2pred m_prefix2prim; - - /** - Maps pripary symbols to prefixes that were used to create them. - */ - sym2sym m_prim2prefix; - - decl_vector m_prim_preds; - - obj_hashtable m_non_model_syms; - - struct formula_checker; - struct conv_rewriter_cfg; - struct shifting_rewriter_cfg; - class decl_idx_comparator; - class hmg_checker; - class nonmodel_sym_checker; - class index_renamer_cfg; - class index_collector; - class variable_collector; - - std::string get_suffix(unsigned i); - void ensure_tuple_size(func_decl * prim, unsigned sz); - -public: - sym_mux(ast_manager & m); - - ast_manager & get_manager() const { return m; } - - bool is_muxed(func_decl * sym) const { return m_sym2idx.contains(sym); } - - bool try_get_index(func_decl * sym, unsigned & idx) const { - return m_sym2idx.find(sym,idx); - } - - bool has_index(func_decl * sym, unsigned idx) const { - unsigned actual_idx; - return try_get_index(sym, actual_idx) && idx==actual_idx; - } - - /** Return primary symbol. sym must be muxed. */ - func_decl * get_primary(func_decl * sym) const { - func_decl * prim; - TRUSTME(m_sym2prim.find(sym, prim)); - return prim; - } - - /** - Return primary symbol created from prefix, or 0 if the prefix was never used. - */ - func_decl * try_get_primary_by_prefix(func_decl* prefix) const { - func_decl * res; - if(!m_prefix2prim.find(prefix, res)) { - return nullptr; - } - return res; - } - - /** - Return symbol created from prefix, or 0 if the prefix was never used. - */ - func_decl * try_get_by_prefix(func_decl* prefix, unsigned idx) { - func_decl * prim = try_get_primary_by_prefix(prefix); - if(!prim) { - return nullptr; - } - return conv(prim, 0, idx); - } - - /** - Marks symbol as non-model which means it will not appear in models collected by - get_muxed_cube_from_model function. - This is to take care of auxiliary symbols introduced by the disjunction relations - to relativize lemmas coming from disjuncts. - */ - void mark_as_non_model(func_decl * sym) { - SASSERT(is_muxed(sym)); - m_non_model_syms.insert(get_primary(sym)); - } - - func_decl * get_or_create_symbol_by_prefix(func_decl* prefix, unsigned idx, - unsigned arity, sort * const * domain, sort * range); - - - - bool is_muxed_lit(expr * e, unsigned idx) const; - - bool is_non_model_sym(func_decl * s) const { - return is_muxed(s) && m_non_model_syms.contains(get_primary(s)); - } - - /** - Create a multiplexed tuple of propositional constants. - Symbols may be suplied in the tuple vector, - those beyond the size of the array and those with corresponding positions - assigned to zero will be created using prefix. - Tuple length must be at least one. - */ - void create_tuple(func_decl* prefix, unsigned arity, sort * const * domain, sort * range, - unsigned tuple_length, decl_vector & tuple); - - /** - Return true if the only multiplexed symbols which e contains are of index idx. - */ - bool is_homogenous_formula(expr * e, unsigned idx) const; - bool is_homogenous(const expr_ref_vector & vect, unsigned idx) const; - - /** - Return true if all multiplexed symbols which e contains are of one index. - */ - bool is_homogenous_formula(expr * e) const; - - /** - Return true if expression e contains a muxed symbol of index idx. - */ - bool contains(expr * e, unsigned idx) const; - - /** - Collect indices used in expression. - */ - void collect_indices(expr* e, unsigned_vector& indices) const; - - /** - Collect used variables of each index. - */ - void collect_variables(expr* e, vector >& vars) const; - - /** - Convert symbol sym which has to be of src_idx variant into variant tgt_idx. - */ - func_decl * conv(func_decl * sym, unsigned src_idx, unsigned tgt_idx); - - - /** - Convert src_idx symbols in formula f variant into tgt_idx. - If homogenous is true, formula cannot contain symbols of other variants. - */ - void conv_formula(expr * f, unsigned src_idx, unsigned tgt_idx, expr_ref & res, bool homogenous=true); - void conv_formula_vector(const expr_ref_vector & vect, unsigned src_idx, unsigned tgt_idx, - expr_ref_vector & res); - - /** - Shifts the muxed symbols in f by dist. Dist can be negative, but it should never shift - symbol index to a negative value. - */ - void shift_formula(expr * f, int dist, expr_ref & res); - - /** - Remove from vect literals (atoms or negations of atoms) of symbols - that contain multiplexed symbols with indexes other than idx. - - Each of the literals can contain only symbols multiplexed with one index - (this trivially holds if the literals are propositional). - - Order of elements in vect may be modified by this function - */ - void filter_idx(expr_ref_vector & vect, unsigned idx) const; - - /** - Partition literals into o_literals and others. - */ - void partition_o_idx(expr_ref_vector const& lits, - expr_ref_vector& o_lits, - expr_ref_vector& other, unsigned idx) const; - - bool has_nonmodel_symbol(expr * e) const; - void filter_non_model_lits(expr_ref_vector & vect) const; - - func_decl * const * begin_prim_preds() const { return m_prim_preds.begin(); } - func_decl * const * end_prim_preds() const { return m_prim_preds.end(); } - - std::string pp_model(const model_core & mdl) const; -}; -} - -#endif diff --git a/src/muz/pdr/pdr_util.cpp b/src/muz/pdr/pdr_util.cpp deleted file mode 100644 index ad75ae799..000000000 --- a/src/muz/pdr/pdr_util.cpp +++ /dev/null @@ -1,508 +0,0 @@ -/*++ -Copyright (c) 2011 Microsoft Corporation - -Module Name: - - pdr_util.cpp - -Abstract: - - Utility functions for PDR. - -Author: - - Krystof Hoder (t-khoder) 2011-8-19. - -Revision History: - - -Notes: - - ---*/ - -#include -#include "util/util.h" -#include "util/ref_vector.h" -#include "ast/array_decl_plugin.h" -#include "ast/ast_pp.h" -#include "ast/for_each_expr.h" -#include "ast/scoped_proof.h" -#include "ast/arith_decl_plugin.h" -#include "ast/rewriter/expr_replacer.h" -#include "ast/rewriter/bool_rewriter.h" -#include "ast/rewriter/poly_rewriter.h" -#include "ast/rewriter/poly_rewriter_def.h" -#include "ast/rewriter/arith_rewriter.h" -#include "ast/rewriter/rewriter.h" -#include "ast/rewriter/rewriter_def.h" -#include "smt/params/smt_params.h" -#include "model/model.h" -#include "muz/base/dl_util.h" -#include "muz/pdr/pdr_manager.h" -#include "muz/pdr/pdr_util.h" -#include "model/model_smt2_pp.h" - - - -namespace pdr { - - unsigned ceil_log2(unsigned u) { - if (u == 0) { return 0; } - unsigned pow2 = next_power_of_two(u); - return get_num_1bits(pow2-1); - } - - std::string pp_cube(const ptr_vector& model, ast_manager& m) { - return pp_cube(model.size(), model.c_ptr(), m); - } - - std::string pp_cube(const expr_ref_vector& model, ast_manager& m) { - return pp_cube(model.size(), model.c_ptr(), m); - } - - std::string pp_cube(const app_ref_vector& model, ast_manager& m) { - return pp_cube(model.size(), model.c_ptr(), m); - } - - std::string pp_cube(const app_vector& model, ast_manager& m) { - return pp_cube(model.size(), model.c_ptr(), m); - } - - std::string pp_cube(unsigned sz, app * const * lits, ast_manager& m) { - return pp_cube(sz, (expr * const *)(lits), m); - } - - std::string pp_cube(unsigned sz, expr * const * lits, ast_manager& m) { - std::stringstream res; - res << "("; - expr * const * end = lits+sz; - for (expr * const * it = lits; it!=end; it++) { - res << mk_pp(*it, m); - if (it+1!=end) { - res << ", "; - } - } - res << ")"; - return res.str(); - } - - void reduce_disequalities(model& model, unsigned threshold, expr_ref& fml) { - ast_manager& m = fml.get_manager(); - expr_ref_vector conjs(m); - flatten_and(fml, conjs); - obj_map diseqs; - expr* n, *lhs, *rhs; - for (unsigned i = 0; i < conjs.size(); ++i) { - if (m.is_not(conjs[i].get(), n) && - m.is_eq(n, lhs, rhs)) { - if (!m.is_value(rhs)) { - std::swap(lhs, rhs); - } - if (!m.is_value(rhs)) { - continue; - } - diseqs.insert_if_not_there2(lhs, 0)->get_data().m_value++; - } - } - expr_substitution sub(m); - - unsigned orig_size = conjs.size(); - unsigned num_deleted = 0; - expr_ref val(m), tmp(m); - proof_ref pr(m); - pr = m.mk_asserted(m.mk_true()); - obj_map::iterator it = diseqs.begin(); - obj_map::iterator end = diseqs.end(); - for (; it != end; ++it) { - if (it->m_value >= threshold) { - model.eval(it->m_key, val); - sub.insert(it->m_key, val, pr); - conjs.push_back(m.mk_eq(it->m_key, val)); - num_deleted += it->m_value; - } - } - if (orig_size < conjs.size()) { - scoped_ptr rep = mk_expr_simp_replacer(m); - rep->set_substitution(&sub); - for (unsigned i = 0; i < orig_size; ++i) { - tmp = conjs[i].get(); - (*rep)(tmp); - if (m.is_true(tmp)) { - conjs[i] = conjs.back(); - SASSERT(orig_size <= conjs.size()); - conjs.pop_back(); - SASSERT(orig_size <= 1 + conjs.size()); - if (i + 1 == orig_size) { - // no-op. - } - else if (orig_size <= conjs.size()) { - // no-op - } - else { - SASSERT(orig_size == 1 + conjs.size()); - --orig_size; - --i; - } - } - else { - conjs[i] = tmp; - } - } - IF_VERBOSE(2, verbose_stream() << "Deleted " << num_deleted << " disequalities " << conjs.size() << " conjuncts\n";); - } - fml = m.mk_and(conjs.size(), conjs.c_ptr()); - } - - class test_diff_logic { - ast_manager& m; - arith_util a; - bv_util bv; - bool m_is_dl; - bool m_test_for_utvpi; - - bool is_numeric(expr* e) const { - if (a.is_numeral(e)) { - return true; - } - expr* cond, *th, *el; - if (m.is_ite(e, cond, th, el)) { - return is_numeric(th) && is_numeric(el); - } - return false; - } - - bool is_arith_expr(expr *e) const { - return is_app(e) && a.get_family_id() == to_app(e)->get_family_id(); - } - - bool is_offset(expr* e) const { - if (a.is_numeral(e)) { - return true; - } - expr* cond, *th, *el, *e1, *e2; - if (m.is_ite(e, cond, th, el)) { - return is_offset(th) && is_offset(el); - } - // recognize offsets. - if (a.is_add(e, e1, e2)) { - if (is_numeric(e1)) { - return is_offset(e2); - } - if (is_numeric(e2)) { - return is_offset(e1); - } - return false; - } - if (m_test_for_utvpi) { - if (a.is_mul(e, e1, e2)) { - if (is_minus_one(e1)) { - return is_offset(e2); - } - if (is_minus_one(e2)) { - return is_offset(e1); - } - } - } - return !is_arith_expr(e); - } - - bool is_minus_one(expr const * e) const { - rational r; return a.is_numeral(e, r) && r.is_minus_one(); - } - - bool test_ineq(expr* e) const { - SASSERT(a.is_le(e) || a.is_ge(e) || m.is_eq(e)); - SASSERT(to_app(e)->get_num_args() == 2); - expr * lhs = to_app(e)->get_arg(0); - expr * rhs = to_app(e)->get_arg(1); - if (is_offset(lhs) && is_offset(rhs)) - return true; - if (!is_numeric(rhs)) - std::swap(lhs, rhs); - if (!is_numeric(rhs)) - return false; - // lhs can be 'x' or '(+ x (* -1 y))' - if (is_offset(lhs)) - return true; - expr* arg1, *arg2; - if (!a.is_add(lhs, arg1, arg2)) - return false; - // x - if (m_test_for_utvpi) { - return is_offset(arg1) && is_offset(arg2); - } - if (is_arith_expr(arg1)) - std::swap(arg1, arg2); - if (is_arith_expr(arg1)) - return false; - // arg2: (* -1 y) - expr* m1, *m2; - if (!a.is_mul(arg2, m1, m2)) - return false; - return is_minus_one(m1) && is_offset(m2); - } - - bool test_eq(expr* e) const { - expr* lhs = nullptr, *rhs = nullptr; - VERIFY(m.is_eq(e, lhs, rhs)); - if (!a.is_int_real(lhs)) { - return true; - } - if (a.is_numeral(lhs) || a.is_numeral(rhs)) { - return test_ineq(e); - } - return - test_term(lhs) && - test_term(rhs) && - !a.is_mul(lhs) && - !a.is_mul(rhs); - } - - bool test_term(expr* e) const { - if (m.is_bool(e)) { - return true; - } - if (a.is_numeral(e)) { - return true; - } - if (is_offset(e)) { - return true; - } - expr* lhs, *rhs; - if (a.is_add(e, lhs, rhs)) { - if (!a.is_numeral(lhs)) { - std::swap(lhs, rhs); - } - return a.is_numeral(lhs) && is_offset(rhs); - } - if (a.is_mul(e, lhs, rhs)) { - return is_minus_one(lhs) || is_minus_one(rhs); - } - return false; - } - - bool is_non_arith_or_basic(expr* e) { - if (!is_app(e)) { - return false; - } - family_id fid = to_app(e)->get_family_id(); - - if (fid == null_family_id && - !m.is_bool(e) && - to_app(e)->get_num_args() > 0) { - return true; - } - return - fid != m.get_basic_family_id() && - fid != null_family_id && - fid != a.get_family_id() && - fid != bv.get_family_id(); - } - - public: - test_diff_logic(ast_manager& m): m(m), a(m), bv(m), m_is_dl(true), m_test_for_utvpi(false) {} - - void test_for_utvpi() { m_test_for_utvpi = true; } - - void operator()(expr* e) { - if (!m_is_dl) { - return; - } - if (a.is_le(e) || a.is_ge(e)) { - m_is_dl = test_ineq(e); - } - else if (m.is_eq(e)) { - m_is_dl = test_eq(e); - } - else if (is_non_arith_or_basic(e)) { - m_is_dl = false; - } - else if (is_app(e)) { - app* a = to_app(e); - for (unsigned i = 0; m_is_dl && i < a->get_num_args(); ++i) { - m_is_dl = test_term(a->get_arg(i)); - } - } - - if (!m_is_dl) { - char const* msg = "non-diff: "; - if (m_test_for_utvpi) { - msg = "non-utvpi: "; - } - IF_VERBOSE(1, verbose_stream() << msg << mk_pp(e, m) << "\n";); - } - } - - bool is_dl() const { return m_is_dl; } - }; - - bool is_difference_logic(ast_manager& m, unsigned num_fmls, expr* const* fmls) { - test_diff_logic test(m); - expr_fast_mark1 mark; - for (unsigned i = 0; i < num_fmls; ++i) { - quick_for_each_expr(test, mark, fmls[i]); - } - return test.is_dl(); - } - - bool is_utvpi_logic(ast_manager& m, unsigned num_fmls, expr* const* fmls) { - test_diff_logic test(m); - test.test_for_utvpi(); - expr_fast_mark1 mark; - for (unsigned i = 0; i < num_fmls; ++i) { - quick_for_each_expr(test, mark, fmls[i]); - } - return test.is_dl(); - } - - class arith_normalizer : public poly_rewriter { - ast_manager& m; - arith_util m_util; - enum op_kind { LE, GE, EQ }; - public: - arith_normalizer(ast_manager& m, params_ref const& p = params_ref()): poly_rewriter(m, p), m(m), m_util(m) {} - - br_status mk_app_core(func_decl* f, unsigned num_args, expr* const* args, expr_ref& result) { - br_status st = BR_FAILED; - if (m.is_eq(f)) { - SASSERT(num_args == 2); return mk_eq_core(args[0], args[1], result); - } - - if (f->get_family_id() != get_fid()) { - return st; - } - switch (f->get_decl_kind()) { - case OP_NUM: st = BR_FAILED; break; - case OP_IRRATIONAL_ALGEBRAIC_NUM: st = BR_FAILED; break; - case OP_LE: SASSERT(num_args == 2); st = mk_le_core(args[0], args[1], result); break; - case OP_GE: SASSERT(num_args == 2); st = mk_ge_core(args[0], args[1], result); break; - case OP_LT: SASSERT(num_args == 2); st = mk_lt_core(args[0], args[1], result); break; - case OP_GT: SASSERT(num_args == 2); st = mk_gt_core(args[0], args[1], result); break; - default: st = BR_FAILED; break; - } - return st; - } - - private: - - br_status mk_eq_core(expr* arg1, expr* arg2, expr_ref& result) { - return mk_le_ge_eq_core(arg1, arg2, EQ, result); - } - br_status mk_le_core(expr* arg1, expr* arg2, expr_ref& result) { - return mk_le_ge_eq_core(arg1, arg2, LE, result); - } - br_status mk_ge_core(expr* arg1, expr* arg2, expr_ref& result) { - return mk_le_ge_eq_core(arg1, arg2, GE, result); - } - br_status mk_lt_core(expr* arg1, expr* arg2, expr_ref& result) { - result = m.mk_not(m_util.mk_ge(arg1, arg2)); - return BR_REWRITE2; - } - br_status mk_gt_core(expr* arg1, expr* arg2, expr_ref& result) { - result = m.mk_not(m_util.mk_le(arg1, arg2)); - return BR_REWRITE2; - } - - br_status mk_le_ge_eq_core(expr* arg1, expr* arg2, op_kind kind, expr_ref& result) { - if (m_util.is_real(arg1)) { - numeral g(0); - get_coeffs(arg1, g); - get_coeffs(arg2, g); - if (!g.is_one() && !g.is_zero()) { - SASSERT(g.is_pos()); - expr_ref new_arg1 = rdiv_polynomial(arg1, g); - expr_ref new_arg2 = rdiv_polynomial(arg2, g); - switch(kind) { - case LE: result = m_util.mk_le(new_arg1, new_arg2); return BR_DONE; - case GE: result = m_util.mk_ge(new_arg1, new_arg2); return BR_DONE; - case EQ: result = m_util.mk_eq(new_arg1, new_arg2); return BR_DONE; - } - } - } - return BR_FAILED; - } - - void update_coeff(numeral const& r, numeral& g) { - if (g.is_zero() || abs(r) < g) { - g = abs(r); - } - } - - void get_coeffs(expr* e, numeral& g) { - rational r; - unsigned sz; - expr* const* args = get_monomials(e, sz); - for (unsigned i = 0; i < sz; ++i) { - expr* arg = args[i]; - if (!m_util.is_numeral(arg, r)) { - get_power_product(arg, r); - } - update_coeff(r, g); - } - } - - expr_ref rdiv_polynomial(expr* e, numeral const& g) { - rational r; - SASSERT(g.is_pos()); - SASSERT(!g.is_one()); - expr_ref_vector monomes(m); - unsigned sz; - expr* const* args = get_monomials(e, sz); - for (unsigned i = 0; i < sz; ++i) { - expr* arg = args[i]; - if (m_util.is_numeral(arg, r)) { - monomes.push_back(m_util.mk_numeral(r/g, false)); - } - else { - expr* p = get_power_product(arg, r); - r /= g; - if (r.is_one()) { - monomes.push_back(p); - } - else { - monomes.push_back(m_util.mk_mul(m_util.mk_numeral(r, false), p)); - } - } - } - expr_ref result(m); - mk_add(monomes.size(), monomes.c_ptr(), result); - return result; - } - - }; - - - struct arith_normalizer_cfg: public default_rewriter_cfg { - arith_normalizer m_r; - bool rewrite_patterns() const { return false; } - br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) { - return m_r.mk_app_core(f, num, args, result); - } - arith_normalizer_cfg(ast_manager & m, params_ref const & p):m_r(m,p) {} - }; - - class arith_normalizer_star : public rewriter_tpl { - arith_normalizer_cfg m_cfg; - public: - arith_normalizer_star(ast_manager & m, params_ref const & p): - rewriter_tpl(m, false, m_cfg), - m_cfg(m, p) {} - }; - - - void normalize_arithmetic(expr_ref& t) { - ast_manager& m = t.get_manager(); - scoped_no_proof _sp(m); - params_ref p; - arith_normalizer_star rw(m, p); - expr_ref tmp(m); - rw(t, tmp); - t = tmp; - } - -} - -template class rewriter_tpl; - - diff --git a/src/muz/pdr/pdr_util.h b/src/muz/pdr/pdr_util.h deleted file mode 100644 index 51f6978ec..000000000 --- a/src/muz/pdr/pdr_util.h +++ /dev/null @@ -1,81 +0,0 @@ -/*++ -Copyright (c) 2011 Microsoft Corporation - -Module Name: - - pdr_util.h - -Abstract: - - Utility functions for PDR. - -Author: - - Krystof Hoder (t-khoder) 2011-8-19. - -Revision History: - ---*/ - -#ifndef PDR_UTIL_H_ -#define PDR_UTIL_H_ - -#include "ast/ast.h" -#include "ast/ast_pp.h" -#include "ast/ast_util.h" -#include "util/obj_hashtable.h" -#include "util/ref_vector.h" -#include "util/trace.h" -#include "util/vector.h" -#include "ast/arith_decl_plugin.h" -#include "ast/array_decl_plugin.h" -#include "ast/bv_decl_plugin.h" - - -class model; -class model_core; - -namespace pdr { - - /** - * Return the ceiling of base 2 logarithm of a number, - * or zero if the nmber is zero. - */ - unsigned ceil_log2(unsigned u); - - typedef ptr_vector app_vector; - typedef ptr_vector decl_vector; - typedef obj_hashtable func_decl_set; - - std::string pp_cube(const ptr_vector& model, ast_manager& manager); - std::string pp_cube(const expr_ref_vector& model, ast_manager& manager); - std::string pp_cube(const ptr_vector& model, ast_manager& manager); - std::string pp_cube(const app_ref_vector& model, ast_manager& manager); - std::string pp_cube(unsigned sz, app * const * lits, ast_manager& manager); - std::string pp_cube(unsigned sz, expr * const * lits, ast_manager& manager); - - - /** - \brief replace variables that are used in many disequalities by - an equality using the model. - - Assumption: the model satisfies the conjunctions. - */ - void reduce_disequalities(model& model, unsigned threshold, expr_ref& fml); - - /** - \brief normalize coefficients in polynomials so that least coefficient is 1. - */ - void normalize_arithmetic(expr_ref& t); - - - /** - \brief determine if formulas belong to difference logic or UTVPI fragment. - */ - bool is_difference_logic(ast_manager& m, unsigned num_fmls, expr* const* fmls); - - bool is_utvpi_logic(ast_manager& m, unsigned num_fmls, expr* const* fmls); - -} - -#endif