mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

extract karr invariants as a Datalog relation

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2013-03-31 16:40:10 -07:00
parent cd48a5164e
commit 4138e17b3f
15 changed files with 1082 additions and 574 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/muz_qe/dl_base.h
View file

@ -233,6 +233,7 @@ namespace datalog {
symbol const& get_name() const { return m_name; }
virtual void set_cancel(bool f) {}
relation_manager & get_manager() const { return m_manager; }
ast_manager& get_ast_manager() const { return datalog::get_ast_manager_from_rel_manager(m_manager); }

2
src/muz_qe/dl_compiler.cpp
View file

@ -1028,6 +1028,8 @@ namespace datalog {
func_decl * head_pred = *preds.begin();
const rule_vector & rules = m_rule_set.get_predicate_rules(head_pred);
reg_idx output_delta;
if (!output_deltas.find(head_pred, output_delta)) {
output_delta = execution_context::void_register;

4
src/muz_qe/dl_context.cpp
View file

@ -954,6 +954,7 @@ namespace datalog {
if (m_pdr.get()) m_pdr->cancel();
if (m_bmc.get()) m_bmc->cancel();
if (m_tab.get()) m_tab->cancel();
if (m_rel.get()) m_rel->set_cancel(true);
}
void context::cleanup() {
@ -962,6 +963,7 @@ namespace datalog {
if (m_pdr.get()) m_pdr->cleanup();
if (m_bmc.get()) m_bmc->cleanup();
if (m_tab.get()) m_tab->cleanup();
if (m_rel.get()) m_rel->set_cancel(false);
}
class context::engine_type_proc {
@ -1231,7 +1233,7 @@ namespace datalog {
return m_rel->result_contains_fact(f);
}
// TBD: algebraic data-types declarations will not be printed.
// NB: algebraic data-types declarations will not be printed.
class free_func_visitor {
ast_manager& m;
func_decl_set m_funcs;

8
src/muz_qe/dl_interval_relation.cpp
View file

@ -21,6 +21,7 @@ Revision History:
#include "optional.h"
#include "ast_pp.h"
#include "dl_interval_relation.h"
#include "bool_rewriter.h"
namespace datalog {
@ -30,8 +31,7 @@ namespace datalog {
interval_relation_plugin::interval_relation_plugin(relation_manager& m):
relation_plugin(interval_relation_plugin::get_name(), m),
m_empty(m_dep),
m_arith(get_ast_manager()),
m_bsimp(get_ast_manager()) {
m_arith(get_ast_manager()) {
}
bool interval_relation_plugin::can_handle_signature(const relation_signature & sig) {
@ -374,7 +374,6 @@ namespace datalog {
void interval_relation::to_formula(expr_ref& fml) const {
ast_manager& m = get_plugin().get_ast_manager();
arith_util& arith = get_plugin().m_arith;
basic_simplifier_plugin& bsimp = get_plugin().m_bsimp;
expr_ref_vector conjs(m);
relation_signature const& sig = get_signature();
for (unsigned i = 0; i < sig.size(); ++i) {
@ -405,7 +404,8 @@ namespace datalog {
}
}
}
bsimp.mk_and(conjs.size(), conjs.c_ptr(), fml);
bool_rewriter br(m);
br.mk_and(conjs.size(), conjs.c_ptr(), fml);
}

1
src/muz_qe/dl_interval_relation.h
View file

@ -34,7 +34,6 @@ namespace datalog {
v_dependency_manager m_dep;
interval m_empty;
arith_util m_arith;
basic_simplifier_plugin m_bsimp;
class join_fn;
class project_fn;

1221
src/muz_qe/dl_mk_karr_invariants.cpp
View file

File diff suppressed because it is too large Load diff

81
src/muz_qe/dl_mk_karr_invariants.h
View file

@ -30,7 +30,6 @@ namespace datalog {
/**
\brief Rule transformer that strengthens bodies with invariants.
*/
class mk_karr_invariants : public rule_transformer::plugin {
struct matrix {
vector<vector<rational> > A;
@ -46,25 +45,17 @@ namespace datalog {
static void display_ineq(
std::ostream& out, vector<rational> const& row, rational const& b, bool is_eq);
};
class mk_karr_invariants : public rule_transformer::plugin {
class add_invariant_model_converter;
context& m_ctx;
ast_manager& m;
rule_manager& rm;
context m_inner_ctx;
arith_util a;
obj_map<func_decl, matrix*> m_constraints;
obj_map<func_decl, matrix*> m_dual_constraints;
hilbert_basis m_hb;
bool is_linear(expr* e, vector<rational>& row, rational& b, rational const& mul);
bool is_eq(expr* e, var*& v, rational& n);
bool get_transition_relation(rule const& r, matrix& M);
void intersect_matrix(app* p, matrix const& Mp, unsigned num_columns, matrix& M);
matrix* get_constraints(func_decl* p);
matrix& get_dual_constraints(func_decl* p);
void dualizeH(matrix& dst, matrix const& src);
void dualizeI(matrix& dst, matrix const& src);
void update_body(rule_set& rules, rule& r);
void update_body(rel_context& rctx, rule_set& result, rule& r);
public:
mk_karr_invariants(context & ctx, unsigned priority);
@ -77,6 +68,68 @@ namespace datalog {
};
class karr_relation;
class karr_relation_plugin : public relation_plugin {
arith_util a;
hilbert_basis m_hb;
class join_fn;
class project_fn;
class rename_fn;
class union_fn;
class filter_equal_fn;
class filter_identical_fn;
class filter_interpreted_fn;
friend class karr_relation;
public:
karr_relation_plugin(relation_manager& rm):
relation_plugin(karr_relation_plugin::get_name(), rm),
a(get_ast_manager())
{}
virtual bool can_handle_signature(const relation_signature & sig) {
for (unsigned i = 0; i < sig.size(); ++i) {
if (a.is_int(sig[i])) {
return true;
}
}
return false;
}
static symbol get_name() { return symbol("karr_relation"); }
virtual void set_cancel(bool f);
virtual relation_base * mk_empty(const relation_signature & s);
virtual relation_base * mk_full(func_decl* p, const relation_signature & s);
static karr_relation& get(relation_base& r);
static karr_relation const & get(relation_base const& r);
virtual relation_join_fn * mk_join_fn(
const relation_base & t1, const relation_base & t2,
unsigned col_cnt, const unsigned * cols1, const unsigned * cols2);
virtual relation_transformer_fn * mk_project_fn(const relation_base & t, unsigned col_cnt,
const unsigned * removed_cols);
virtual relation_transformer_fn * mk_rename_fn(const relation_base & t, unsigned permutation_cycle_len,
const unsigned * permutation_cycle);
virtual relation_union_fn * mk_union_fn(const relation_base & tgt, const relation_base & src,
const relation_base * delta);
virtual relation_mutator_fn * mk_filter_identical_fn(const relation_base & t, unsigned col_cnt,
const unsigned * identical_cols);
virtual relation_mutator_fn * mk_filter_equal_fn(const relation_base & t, const relation_element & value,
unsigned col);
virtual relation_mutator_fn * mk_filter_interpreted_fn(const relation_base & t, app * condition);
private:
bool dualizeI(matrix& dst, matrix const& src);
void dualizeH(matrix& dst, matrix const& src);
};
};
#endif /* _DL_MK_KARR_INVARIANTS_H_ */

6
src/muz_qe/dl_relation_manager.cpp
View file

@ -468,6 +468,12 @@ namespace datalog {
}
}
void relation_manager::set_cancel(bool f) {
for (unsigned i = 0; i < m_relation_plugins.size(); ++i) {
m_relation_plugins[i]->set_cancel(f);
}
}
std::string relation_manager::to_nice_string(const relation_element & el) const {
uint64 val;
std::stringstream stm;

1
src/muz_qe/dl_relation_manager.h
View file

@ -223,6 +223,7 @@ namespace datalog {
relation_fact & to);
void set_cancel(bool f);
// -----------------------------------

30
src/muz_qe/dl_rule_set.cpp
View file

@ -107,6 +107,7 @@ namespace datalog {
}
void rule_dependencies::populate(rule const* r) {
TRACE("dl_verbose", tout << r->get_decl()->get_name() << "\n";);
m_visited.reset();
func_decl * d = r->get_head()->get_decl();
func_decl_set & s = ensure_key(d);
@ -293,7 +294,7 @@ namespace datalog {
m_stratifier(0) {
add_rules(rs);
if (rs.m_stratifier) {
TRUSTME(close());
VERIFY(close());
}
}
@ -347,13 +348,14 @@ namespace datalog {
void rule_set::ensure_closed()
{
if (!is_closed()) {
TRUSTME(close());
VERIFY(close());
}
}
bool rule_set::close() {
SASSERT(!is_closed()); //the rule_set is not already closed
m_deps.populate(*this);
m_stratifier = alloc(rule_stratifier, m_deps);
@ -531,7 +533,7 @@ namespace datalog {
}
while (!m_stack_P.empty()) {
unsigned on_stack_num;
TRUSTME( m_preorder_nums.find(m_stack_P.back(), on_stack_num) );
VERIFY( m_preorder_nums.find(m_stack_P.back(), on_stack_num) );
if (on_stack_num <= p_num) {
break;
}
@ -598,7 +600,7 @@ namespace datalog {
item_set * out_edges = it->m_value;
unsigned el_comp;
TRUSTME( m_component_nums.find(el, el_comp) );
VERIFY( m_component_nums.find(el, el_comp) );
item_set::iterator eit = out_edges->begin();
item_set::iterator eend = out_edges->end();
@ -640,7 +642,7 @@ namespace datalog {
for (; eit!=eend; ++eit) {
T * tgt = *eit;
unsigned tgt_comp;
TRUSTME( m_component_nums.find(tgt, tgt_comp) );
VERIFY( m_component_nums.find(tgt, tgt_comp) );
//m_components[tgt_comp]==0 means the edge is intra-component.
//Otherwise it would go to another component, but it is not possible, since
@ -653,8 +655,6 @@ namespace datalog {
m_components[tgt_comp] = 0;
}
}
traverse(*cit);
}
}
@ -675,7 +675,6 @@ namespace datalog {
item_set::iterator cend=comp->end();
for (; cit != cend; ++cit) {
T * el = *cit;
m_pred_strat_nums.insert(el, strat_index);
}
}
@ -686,6 +685,21 @@ namespace datalog {
m_stack_P.finalize();
m_component_nums.finalize();
m_components.finalize();
}
void rule_stratifier::display(std::ostream& out) const {
m_deps.display(out << "dependencies\n");
out << "strata\n";
for (unsigned i = 0; i < m_strats.size(); ++i) {
item_set::iterator it = m_strats[i]->begin();
item_set::iterator end = m_strats[i]->end();
for (; it != end; ++it) {
out << (*it)->get_name() << " ";
}
out << "\n";
}
}
};

2
src/muz_qe/dl_rule_set.h
View file

@ -146,6 +146,8 @@ namespace datalog {
const comp_vector & get_strats() const { return m_strats; }
unsigned get_predicate_strat(func_decl * pred) const;
void display( std::ostream & out ) const;
};
/**

3
src/muz_qe/hilbert_basis.cpp
View file

@ -744,7 +744,6 @@ void hilbert_basis::reset() {
if (m_passive2) {
m_passive2->reset();
}
m_cancel = false;
if (m_index) {
m_index->reset(1);
}
@ -867,7 +866,7 @@ lbool hilbert_basis::saturate() {
stopwatch sw;
sw.start();
lbool r = saturate(m_ineqs[m_current_ineq], m_iseq[m_current_ineq]);
IF_VERBOSE(1,
IF_VERBOSE(3,
{ statistics st;
collect_statistics(st);
st.display(verbose_stream());

5
src/muz_qe/hilbert_basis.h
View file

@ -37,10 +37,13 @@ typedef vector<rational> rational_vector;
class hilbert_basis {
static const bool check = false;
static const bool check = true;
typedef checked_int64<check> numeral;
typedef vector<numeral> num_vector;
static checked_int64<check> to_numeral(rational const& r) {
if (!r.is_int64()) {
throw checked_int64<check>::overflow_exception();
}
return checked_int64<check>(r.get_int64());
}
static rational to_rational(checked_int64<check> const& i) {

7
src/muz_qe/rel_context.cpp
View file

@ -27,6 +27,7 @@ Revision History:
#include"dl_product_relation.h"
#include"dl_bound_relation.h"
#include"dl_interval_relation.h"
#include"dl_mk_karr_invariants.h"
#include"dl_finite_product_relation.h"
#include"dl_sparse_table.h"
#include"dl_table.h"
@ -54,6 +55,8 @@ namespace datalog {
get_rmanager().register_plugin(alloc(bound_relation_plugin, get_rmanager()));
get_rmanager().register_plugin(alloc(interval_relation_plugin, get_rmanager()));
get_rmanager().register_plugin(alloc(karr_relation_plugin, get_rmanager()));
}
@ -427,6 +430,10 @@ namespace datalog {
get_rmanager().set_predicate_kind(pred, target_kind);
}
void rel_context::set_cancel(bool f) {
get_rmanager().set_cancel(f);
}
relation_plugin & rel_context::get_ordinary_relation_plugin(symbol relation_name) {
relation_plugin * plugin = get_rmanager().get_relation_plugin(relation_name);
if (!plugin) {

2
src/muz_qe/rel_context.h
View file

@ -63,7 +63,6 @@ namespace datalog {
bool output_profile() const;
lbool query(expr* q);
lbool query(unsigned num_rels, func_decl * const* rels);
@ -72,6 +71,7 @@ namespace datalog {
void inherit_predicate_kind(func_decl* new_pred, func_decl* orig_pred);
void set_cancel(bool f);
/**
\brief Restrict the set of used predicates to \c res.