mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-14 21:08:46 +00:00
Code Activity

remove pdr

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-06-06 13:11:48 -07:00 committed by Arie Gurfinkel
parent cefdb8c01d
commit 6adaed718f
29 changed files with 70 additions and 8691 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/CMakeLists.txt
View file

@ -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)

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

@ -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:

2
src/muz/base/dl_engine_base.h
View file

@ -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,

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

@ -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",
"<no-slicing>=> GetId(i) = i, <smash> => 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"),

1
src/muz/fp/CMakeLists.txt
View file

@ -9,7 +9,6 @@ z3_add_component(fp
clp
ddnf
muz
pdr
rel
spacer
tab

4
src/muz/fp/dl_register_engine.cpp
View file

@ -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:

20
src/muz/pdr/CMakeLists.txt
View file

@ -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
)

177
src/muz/pdr/pdr_closure.cpp
View file

@ -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<func_decl, expr*>* 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<expr> 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;
}
}

67
src/muz/pdr/pdr_closure.h
View file

@ -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<expr, expr*> m_cache[2];
expr* m_k;
obj_map<func_decl, expr*>* m_translate;
public:
scaler(ast_manager& m): m(m), a(m), m_translate(nullptr) {}
expr_ref operator()(expr* e, expr* k, obj_map<func_decl, expr*>* 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<obj_map<func_decl, expr*> > 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

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

File diff suppressed because it is too large Load diff

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

@ -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 <deque>
#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<datalog::rule const, app_ref_vector*> rule2inst;
typedef obj_map<func_decl, pred_transformer*> 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<datalog::rule const, expr*> rule2expr;
typedef obj_map<datalog::rule const, ptr_vector<app> > 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<pred_transformer> m_use; // places where 'this' is referenced.
ptr_vector<datalog::rule> m_rules; // rules used to derive transformer
prop_solver m_solver; // solver context
vector<expr_ref_vector> m_levels; // level formulas
expr_ref_vector m_invariants; // properties that are invariant.
obj_map<expr, unsigned> m_prop2level; // map property to level where it occurs.
obj_map<expr, datalog::rule const*> 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<func_decl> 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<datalog::rule const>& 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<datalog::rule> 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<func_decl>& 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<app>& 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<app>& 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<model_node> 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<model_node> 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_node> model_nodes;
bool m_bfs;
model_node* m_root;
model_node* m_goal;
vector<obj_map<expr, model_nodes > > m_cache;
obj_map<expr, model_nodes>& cache(model_node const& n);
void erase_children(model_node& n, bool backtrack);
void 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<std::pair<expr_ref_vector,bool> > 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<core_generalizer> 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<relation_info> & 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

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

@ -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<func_decl, func_decl*> const& preds = slice->get_predicates();
obj_map<func_decl, func_decl*>::iterator it = preds.begin();
obj_map<func_decl, func_decl*>::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();
}

78
src/muz/pdr/pdr_dl_interface.h
View file

@ -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<func_decl, func_decl*> 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

1012
src/muz/pdr/pdr_farkas_learner.cpp
View file

File diff suppressed because it is too large Load diff

128
src/muz/pdr/pdr_farkas_learner.h
View file

@ -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> expr_set;
smt_params m_proof_params;
ast_manager m_pr;
scoped_ptr<smt::kernel> 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<expr>& 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

777
src/muz/pdr/pdr_generalizers.cpp
View file

@ -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<expr> 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<expr> 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<eq> 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<term_loc_t> 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<eq>& 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<term_loc_t> & terms1 = it->m_value;
vector<term_loc_t> 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<symbol> 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<sort> sorts;
svector<symbol> 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<datalog::rule> 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<datalog::rule> 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<pred_transformer> 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<datalog::rule> 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;
}
}
};

110
src/muz/pdr/pdr_generalizers.h
View file

@ -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 <typename T>
class r_map : public map<rational, T, rational::hash_proc, rational::eq_proc> {
};
class core_arith_inductive_generalizer : public core_generalizer {
typedef std::pair<expr*, unsigned> term_loc_t;
typedef r_map<vector<term_loc_t> > 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<eq>& 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<expr, expr*> 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

321
src/muz/pdr/pdr_manager.cpp
View file

@ -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 <sstream>
#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, symbol_hash_proc, symbol_eq_proc> 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<relation_info> 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<model_converter_ref&>(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<datalog::rule> 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;
}
};

304
src/muz/pdr/pdr_manager.h
View file

@ -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 <utility>
#include <map>
#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<func_decl> 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<relation_info> 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<relation_info> 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<datalog::rule> 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<ptr_vector<app> >& 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

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

@ -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 <sstream>
#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<app,expr *> m_proxies2expr;
obj_map<expr, app*> 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<func_decl> 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<func_decl> 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<app,expr*>::iterator it = m_proxies2expr.begin(), end = m_proxies2expr.end();
for (; it != end; ++it) {
sub.insert(it->m_key, m.mk_true(), pr);
}
scoped_ptr<expr_replacer> 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<lev_cnt; i++) {
bool active = 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<bool> _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<expr> 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() {
}
}

139
src/muz/pdr/pdr_prop_solver.h
View file

@ -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 <map>
#include <string>
#include <utility>
#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<pdr::smt_context> 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<expr> 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

132
src/muz/pdr/pdr_reachable_cache.cpp
View file

@ -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();
}
}

66
src/muz/pdr/pdr_reachable_cache.h
View file

@ -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<smt_context> m_ctx;
ast_ref_vector m_ref_holder;
app_ref m_disj_connector;
obj_hashtable<expr> 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

167
src/muz/pdr/pdr_smt_context_manager.cpp
View file

@ -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 <sstream>
#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::kernel>());
}
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();
}
}
};

92
src/muz/pdr/pdr_smt_context_manager.h
View file

@ -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<smt::kernel> 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

601
src/muz/pdr/pdr_sym_mux.cpp
View file

@ -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 <sstream>
#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<<'_'<<m_next_sym_suffix_idx;
m_next_sym_suffix_idx++;
new_suffix = stm.str();
new_syffix_sym = symbol(new_suffix.c_str());
}
while (m_used_suffixes.contains(new_syffix_sym));
m_used_suffixes.insert(new_syffix_sym);
m_suffixes.push_back(new_suffix);
}
std::string result = m_suffixes[i];
return result;
}
void sym_mux::create_tuple(func_decl* prefix, unsigned arity, sort * const * domain, sort * range,
unsigned tuple_length, decl_vector & tuple)
{
SASSERT(tuple_length>0);
while(tuple.size()<tuple_length) {
tuple.push_back(0);
}
SASSERT(tuple.size()==tuple_length);
std::string pre = prefix->get_name().str();
for(unsigned i=0; i<tuple_length; i++) {
if (tuple[i] != 0) {
SASSERT(tuple[i]->get_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<bool> 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<ptr_vector<app> >& m_vars;
public:
variable_collector(sym_mux const& s, vector<ptr_vector<app> >& 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<app>());
}
m_vars[idx].push_back(to_app(e));
}
}
}
};
void sym_mux::collect_variables(expr* e, vector<ptr_vector<app> >& 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<conv_rewriter_cfg> 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<int>(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<shifting_rewriter_cfg> 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 idx1<idx2; }
return lt(sym1->get_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<unsigned>(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

247
src/muz/pdr/pdr_sym_mux.h
View file

@ -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 <vector>
class model_core;
namespace pdr {
class sym_mux
{
public:
typedef ptr_vector<app> app_vector;
typedef ptr_vector<func_decl> decl_vector;
private:
typedef obj_map<func_decl,unsigned> sym2u;
typedef obj_map<func_decl, decl_vector> sym2dv;
typedef obj_map<func_decl,func_decl *> sym2sym;
typedef obj_map<func_decl, func_decl *> sym2pred;
typedef hashtable<symbol, symbol_hash_proc, symbol_eq_proc> 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<std::string> 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<func_decl> 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<ptr_vector<app> >& 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

508
src/muz/pdr/pdr_util.cpp
View file

@ -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 <sstream>
#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<expr>& 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<expr, unsigned> 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<expr, unsigned>::iterator it = diseqs.begin();
obj_map<expr, unsigned>::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<expr_replacer> 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<arith_rewriter_core> {
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<arith_rewriter_core>(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> {
arith_normalizer_cfg m_cfg;
public:
arith_normalizer_star(ast_manager & m, params_ref const & p):
rewriter_tpl<arith_normalizer_cfg>(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<pdr::arith_normalizer_cfg>;

81
src/muz/pdr/pdr_util.h
View file

@ -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> app_vector;
typedef ptr_vector<func_decl> decl_vector;
typedef obj_hashtable<func_decl> func_decl_set;
std::string pp_cube(const ptr_vector<expr>& model, ast_manager& manager);
std::string pp_cube(const expr_ref_vector& model, ast_manager& manager);
std::string pp_cube(const ptr_vector<app>& 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