mirror of
https://github.com/Z3Prover/z3
synced 2025-04-15 13:28:47 +00:00
Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable
Conflicts: src/muz_qe/dl_mk_karr_invariants.cpp
This commit is contained in:
Nikolaj Bjorner
commit
cbb4c12191
|
|
@ -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); }
|
||||
|
|
|
|||
|
|
@ -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;
|
||||
|
|
|
|||
|
|
@ -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;
|
||||
|
|
|
|||
|
|
@ -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);
|
||||
}
|
||||
|
||||
|
||||
|
|
|
|||
|
|
@ -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;
|
||||
|
|
|
|||
|
|
@ -296,18 +296,40 @@ namespace datalog {
|
|||
br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result,
|
||||
proof_ref & result_pr)
|
||||
{
|
||||
if (m.is_not(f)) {
|
||||
|
||||
if (m.is_not(f) && (m.is_and(args[0]) || m.is_or(args[0]))) {
|
||||
SASSERT(num==1);
|
||||
if (m.is_and(args[0]) || m.is_or(args[0])) {
|
||||
expr_ref e(m.mk_not(args[0]),m);
|
||||
if (push_toplevel_junction_negation_inside(e)) {
|
||||
result = e;
|
||||
expr_ref tmp(m);
|
||||
app* a = to_app(args[0]);
|
||||
m_app_args.reset();
|
||||
for (unsigned i = 0; i < a->get_num_args(); ++i) {
|
||||
m_brwr.mk_not(a->get_arg(i), tmp);
|
||||
m_app_args.push_back(tmp);
|
||||
}
|
||||
if (m.is_and(args[0])) {
|
||||
result = m.mk_or(m_app_args.size(), m_app_args.c_ptr());
|
||||
}
|
||||
else {
|
||||
result = m.mk_and(m_app_args.size(), m_app_args.c_ptr());
|
||||
}
|
||||
return BR_REWRITE2;
|
||||
}
|
||||
if (!m.is_and(f) && !m.is_or(f)) {
|
||||
return BR_FAILED;
|
||||
}
|
||||
if (num == 0) {
|
||||
if (m.is_and(f)) {
|
||||
result = m.mk_true();
|
||||
}
|
||||
else {
|
||||
result = m.mk_false();
|
||||
}
|
||||
return BR_DONE;
|
||||
}
|
||||
if (num == 1) {
|
||||
result = args[0];
|
||||
return BR_DONE;
|
||||
}
|
||||
if (!m.is_and(f) && !m.is_or(f)) { return BR_FAILED; }
|
||||
if (num<2) { return BR_FAILED; }
|
||||
|
||||
m_app_args.reset();
|
||||
m_app_args.append(num, args);
|
||||
|
|
@ -318,30 +340,18 @@ namespace datalog {
|
|||
|
||||
bool have_rewritten_args = false;
|
||||
|
||||
if (m.is_or(f) || m.is_and(f)) {
|
||||
have_rewritten_args = detect_equivalences(m_app_args, m.is_or(f));
|
||||
#if 0
|
||||
if (have_rewritten_args) {
|
||||
std::sort(m_app_args.c_ptr(), m_app_args.c_ptr()+m_app_args.size(), m_expr_cmp);
|
||||
|
||||
app_ref orig(m.mk_app(f, num, args),m);
|
||||
app_ref res(m.mk_app(f, m_app_args.size(), m_app_args.c_ptr()),m);
|
||||
std::cout<<"s:"<<mk_pp(orig, m)<<"\n";
|
||||
std::cout<<"t:"<<mk_pp(res, m)<<"\n";
|
||||
}
|
||||
#endif
|
||||
}
|
||||
|
||||
if (m_app_args.size()==1) {
|
||||
result = m_app_args[0].get();
|
||||
}
|
||||
else {
|
||||
if (m.is_and(f)) {
|
||||
m_brwr.mk_and(m_app_args.size(), m_app_args.c_ptr(), result);
|
||||
result = m.mk_and(m_app_args.size(), m_app_args.c_ptr());
|
||||
}
|
||||
else {
|
||||
SASSERT(m.is_or(f));
|
||||
m_brwr.mk_or(m_app_args.size(), m_app_args.c_ptr(), result);
|
||||
result = m.mk_or(m_app_args.size(), m_app_args.c_ptr());
|
||||
}
|
||||
}
|
||||
|
||||
|
|
|
|||
File diff suppressed because it is too large
Load diff
|
|
@ -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_ */
|
||||
|
|
|
|||
|
|
@ -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;
|
||||
|
|
|
|||
|
|
@ -223,6 +223,7 @@ namespace datalog {
|
|||
relation_fact & to);
|
||||
|
||||
|
||||
void set_cancel(bool f);
|
||||
|
||||
|
||||
// -----------------------------------
|
||||
|
|
|
|||
|
|
@ -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";
|
||||
}
|
||||
|
||||
}
|
||||
|
||||
};
|
||||
|
|
|
|||
|
|
@ -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;
|
||||
};
|
||||
|
||||
/**
|
||||
|
|
|
|||
|
|
@ -153,35 +153,6 @@ namespace datalog {
|
|||
flatten_or(result);
|
||||
}
|
||||
|
||||
bool push_toplevel_junction_negation_inside(expr_ref& e)
|
||||
{
|
||||
ast_manager& m = e.get_manager();
|
||||
bool_rewriter brwr(m);
|
||||
|
||||
expr * arg;
|
||||
if(!m.is_not(e, arg)) { return false; }
|
||||
bool is_and = m.is_and(arg);
|
||||
if(!is_and && !m.is_or(arg)) { return false; }
|
||||
|
||||
//now we know we have formula we need to transform
|
||||
app * junction = to_app(arg);
|
||||
expr_ref_vector neg_j_args(m);
|
||||
unsigned num_args = junction->get_num_args();
|
||||
for(unsigned i=0; i<num_args; ++i) {
|
||||
expr_ref neg_j_arg(m);
|
||||
brwr.mk_not(junction->get_arg(i), neg_j_arg);
|
||||
neg_j_args.push_back(neg_j_arg);
|
||||
}
|
||||
if(is_and) {
|
||||
brwr.mk_or(neg_j_args.size(), neg_j_args.c_ptr(), e);
|
||||
}
|
||||
else {
|
||||
brwr.mk_and(neg_j_args.size(), neg_j_args.c_ptr(), e);
|
||||
}
|
||||
return true;
|
||||
}
|
||||
|
||||
|
||||
bool contains_var(expr * trm, unsigned var_idx) {
|
||||
ptr_vector<sort> vars;
|
||||
::get_free_vars(trm, vars);
|
||||
|
|
|
|||
|
|
@ -81,19 +81,6 @@ namespace datalog {
|
|||
|
||||
void flatten_or(expr* fml, expr_ref_vector& result);
|
||||
|
||||
/**
|
||||
Transform
|
||||
~(a1 | ... | aN)
|
||||
into
|
||||
~a1 | ... | ~aN
|
||||
and
|
||||
~(a1 & ... & aN)
|
||||
into
|
||||
~a1 | ... | ~aN
|
||||
|
||||
Return true if something was done.
|
||||
*/
|
||||
bool push_toplevel_junction_negation_inside(expr_ref& e);
|
||||
|
||||
|
||||
bool contains_var(expr * trm, unsigned var_idx);
|
||||
|
|
|
|||
|
|
@ -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());
|
||||
|
|
|
|||
|
|
@ -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) {
|
||||
|
|
|
|||
|
|
@ -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) {
|
||||
|
|
|
|||
|
|
@ -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.
|
||||
|
|
|
|||
Loading…
Reference in a new issue