mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-04 21:31:22 +00:00
Code Activity

remove simplify dependencies

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-08-26 00:48:49 -07:00
parent 2897b98ed2
commit 881f90d17d
4 changed files with 2 additions and 190 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/ast/macros/macro_manager.h
View file

@ -21,7 +21,6 @@ Revision History:
#include "util/obj_hashtable.h" #include "util/obj_hashtable.h"
#include "ast/ast_util.h" #include "ast/ast_util.h"
#include "ast/simplifier/simplifier.h"
#include "ast/recurse_expr.h" #include "ast/recurse_expr.h"
#include "ast/func_decl_dependencies.h" #include "ast/func_decl_dependencies.h"
#include "ast/macros/macro_util.h" #include "ast/macros/macro_util.h"

187
src/ast/pattern/pattern_inference.h
View file

@ -20,7 +20,6 @@ Revision History:
#define PATTERN_INFERENCE_H_ #define PATTERN_INFERENCE_H_
#include "ast/ast.h" #include "ast/ast.h"
#include "ast/simplifier/simplifier.h"
#include "ast/rewriter/rewriter.h" #include "ast/rewriter/rewriter.h"
#include "ast/pattern/pattern_inference_params.h" #include "ast/pattern/pattern_inference_params.h"
#include "util/vector.h" #include "util/vector.h"
@ -61,192 +60,6 @@ public:
bool operator()(unsigned num_bindings, expr * p1, expr * p2); bool operator()(unsigned num_bindings, expr * p1, expr * p2);
}; };
#if 0
class pattern_inference_old : public simplifier {
pattern_inference_params & m_params;
family_id m_bfid;
family_id m_afid;
svector<family_id> m_forbidden;
obj_hashtable<func_decl> m_preferred;
smaller_pattern m_le;
unsigned m_num_bindings;
unsigned m_num_no_patterns;
expr * const * m_no_patterns;
bool m_nested_arith_only;
bool m_block_loop_patterns;
struct info {
uint_set m_free_vars;
unsigned m_size;
info(uint_set const & vars, unsigned size):
m_free_vars(vars),
m_size(size) {
}
info():
m_free_vars(),
m_size(0) {
}
};
typedef obj_map<expr, info> expr2info;
expr2info m_candidates_info; // candidate -> set of free vars + size
app_ref_vector m_candidates;
ptr_vector<app> m_tmp1;
ptr_vector<app> m_tmp2;
ptr_vector<app> m_todo;
// Compare candidates patterns based on their usefulness
// p1 < p2 if
// - p1 has more free variables than p2
// - p1 and p2 has the same number of free variables,
// and p1 is smaller than p2.
struct pattern_weight_lt {
expr2info & m_candidates_info;
pattern_weight_lt(expr2info & i):
m_candidates_info(i) {
}
bool operator()(expr * n1, expr * n2) const;
};
pattern_weight_lt m_pattern_weight_lt;
//
// Functor for collecting candidates.
//
class collect {
struct entry {
expr * m_node;
unsigned m_delta;
entry():m_node(0), m_delta(0) {}
entry(expr * n, unsigned d):m_node(n), m_delta(d) {}
unsigned hash() const {
return hash_u_u(m_node->get_id(), m_delta);
}
bool operator==(entry const & e) const {
return m_node == e.m_node && m_delta == e.m_delta;
}
};
struct info {
expr_ref m_node;
uint_set m_free_vars;
unsigned m_size;
info(ast_manager & m, expr * n, uint_set const & vars, unsigned sz):
m_node(n, m), m_free_vars(vars), m_size(sz) {}
};
ast_manager & m;
pattern_inference_old & m_owner;
family_id m_afid;
unsigned m_num_bindings;
typedef map<entry, info *, obj_hash<entry>, default_eq<entry> > cache;
cache m_cache;
ptr_vector<info> m_info;
svector<entry> m_todo;
void visit(expr * n, unsigned delta, bool & visited);
bool visit_children(expr * n, unsigned delta);
void save(expr * n, unsigned delta, info * i);
void save_candidate(expr * n, unsigned delta);
void reset();
public:
collect(ast_manager & m, pattern_inference_old & o):m(m), m_owner(o), m_afid(m.mk_family_id("arith")) {}
void operator()(expr * n, unsigned num_bindings);
};
collect m_collect;
void add_candidate(app * n, uint_set const & s, unsigned size);
void filter_looping_patterns(ptr_vector<app> & result);
bool has_preferred_patterns(ptr_vector<app> & candidate_patterns, app_ref_buffer & result);
void filter_bigger_patterns(ptr_vector<app> const & patterns, ptr_vector<app> & result);
class contains_subpattern {
pattern_inference_old & m_owner;
nat_set m_already_processed;
ptr_vector<expr> m_todo;
void save(expr * n);
public:
contains_subpattern(pattern_inference_old & owner):
m_owner(owner) {}
bool operator()(expr * n);
};
contains_subpattern m_contains_subpattern;
bool contains_subpattern(expr * n);
struct pre_pattern {
ptr_vector<app> m_exprs; // elements of the pattern.
uint_set m_free_vars; // set of free variables in m_exprs
unsigned m_idx; // idx of the next candidate to process.
pre_pattern():
m_idx(0) {
}
};
ptr_vector<pre_pattern> m_pre_patterns;
expr_pattern_match m_database;
void candidates2unary_patterns(ptr_vector<app> const & candidate_patterns,
ptr_vector<app> & remaining_candidate_patterns,
app_ref_buffer & result);
void candidates2multi_patterns(unsigned max_num_patterns,
ptr_vector<app> const & candidate_patterns,
app_ref_buffer & result);
void reset_pre_patterns();
/**
\brief All minimal unary patterns (i.e., expressions that
contain all bound variables) are copied to result. If there
are unary patterns, then at most num_extra_multi_patterns multi
patterns are created. If there are no unary pattern, then at
most 1 + num_extra_multi_patterns multi_patterns are created.
*/
void mk_patterns(unsigned num_bindings, // IN number of bindings.
expr * n, // IN node where the patterns are going to be extracted.
unsigned num_no_patterns, // IN num. patterns that should not be used.
expr * const * no_patterns, // IN patterns that should not be used.
app_ref_buffer & result); // OUT result
virtual void reduce1_quantifier(quantifier * q);
public:
pattern_inference_old(ast_manager & m, pattern_inference_params & params);
void register_forbidden_family(family_id fid) {
SASSERT(fid != m_bfid);
m_forbidden.push_back(fid);
}
/**
\brief Register f as a preferred function symbol. The inference algorithm
gives preference to patterns rooted by this kind of function symbol.
*/
void register_preferred(func_decl * f) {
m_preferred.insert(f);
}
void register_preferred(unsigned num, func_decl * const * fs) { for (unsigned i = 0; i < num; i++) register_preferred(fs[i]); }
bool is_forbidden(func_decl const * decl) const {
family_id fid = decl->get_family_id();
if (fid == m_bfid && decl->get_decl_kind() != OP_TRUE && decl->get_decl_kind() != OP_FALSE)
return true;
return std::find(m_forbidden.begin(), m_forbidden.end(), fid) != m_forbidden.end();
}
bool is_forbidden(app * n) const;
};
#endif
class pattern_inference_cfg : public default_rewriter_cfg { class pattern_inference_cfg : public default_rewriter_cfg {
ast_manager& m; ast_manager& m;
pattern_inference_params & m_params; pattern_inference_params & m_params;

1
src/muz/transforms/dl_mk_quantifier_instantiation.cpp
View file

@ -27,6 +27,7 @@ Revision History:
#include "muz/base/dl_context.h" #include "muz/base/dl_context.h"
#include "ast/pattern/pattern_inference.h" #include "ast/pattern/pattern_inference.h"
#include "ast/rewriter/rewriter_def.h" #include "ast/rewriter/rewriter_def.h"
#include "ast/ast_util.h"
namespace datalog { namespace datalog {

3
src/smt/elim_term_ite.h
View file

@ -19,9 +19,9 @@ Revision History:
#ifndef ELIM_TERM_ITE_H_ #ifndef ELIM_TERM_ITE_H_
#define ELIM_TERM_ITE_H_ #define ELIM_TERM_ITE_H_
#include "ast/simplifier/simplifier.h"
#include "ast/normal_forms/defined_names.h" #include "ast/normal_forms/defined_names.h"
#include "ast/rewriter/rewriter.h" #include "ast/rewriter/rewriter.h"
#include "ast/simplifier/simplifier.h"
class elim_term_ite : public simplifier { class elim_term_ite : public simplifier {
defined_names & m_defined_names; defined_names & m_defined_names;
@ -48,7 +48,6 @@ public:
}; };
class elim_term_ite_cfg : public default_rewriter_cfg { class elim_term_ite_cfg : public default_rewriter_cfg {
ast_manager& m; ast_manager& m;
defined_names & m_defined_names; defined_names & m_defined_names;