mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-20 11:22:04 +00:00
Code Activity

tidy

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-06-07 21:07:46 -07:00 • committed by Arie Gurfinkel
parent 1920450f98
commit f3466bb3e4
2 changed files with 573 additions and 992 deletions
Download patch file Download diff file Expand all files Collapse all files

832
src/muz/spacer/spacer_util.cpp
View file

File diff suppressed because it is too large Load diff

119
src/muz/spacer/spacer_util.h
View file

@ -44,51 +44,50 @@ class model_evaluator;
namespace spacer { namespace spacer {
inline unsigned infty_level () {return UINT_MAX;} inline unsigned infty_level () {
return UINT_MAX;
}
inline bool is_infty_level(unsigned lvl) inline bool is_infty_level(unsigned lvl) {
{ return lvl == infty_level (); } return lvl == infty_level ();
}
inline unsigned next_level(unsigned lvl) inline unsigned next_level(unsigned lvl) {
{ return is_infty_level(lvl)?lvl:(lvl+1); } return is_infty_level(lvl)?lvl:(lvl+1);
}
inline unsigned prev_level (unsigned lvl) inline unsigned prev_level (unsigned lvl) {
{ if (is_infty_level(lvl)) return infty_level();
if(is_infty_level(lvl)) { return infty_level(); } if (lvl == 0) return 0;
if(lvl == 0) { return 0; } return lvl - 1;
return lvl -1; }
}
struct pp_level { struct pp_level {
unsigned m_level; unsigned m_level;
pp_level(unsigned l): m_level(l) {} pp_level(unsigned l): m_level(l) {}
}; };
inline std::ostream& operator<<(std::ostream& out, pp_level const& p) inline std::ostream& operator<<(std::ostream& out, pp_level const& p) {
{
if (is_infty_level(p.m_level)) { if (is_infty_level(p.m_level)) {
return out << "oo"; return out << "oo";
} else { } else {
return out << p.m_level; return out << p.m_level;
} }
} }
typedef ptr_vector<app> app_vector;
typedef ptr_vector<func_decl> decl_vector;
typedef obj_hashtable<func_decl> func_decl_set;
// TBD: deprecate
class model_evaluator_util {
typedef ptr_vector<app> app_vector;
typedef ptr_vector<func_decl> decl_vector;
typedef obj_hashtable<func_decl> func_decl_set;
class model_evaluator_util {
ast_manager& m; ast_manager& m;
model_ref m_model; model_ref m_model;
model_evaluator* m_mev; model_evaluator* m_mev;
/// initialize with a given model. All previous state is lost. model can be NULL /// initialize with a given model. All previous state is lost. model can be NULL
void reset (model *model); void reset (model *model);
public: public:
model_evaluator_util(ast_manager& m); model_evaluator_util(ast_manager& m);
~model_evaluator_util(); ~model_evaluator_util();
@ -96,7 +95,7 @@ public:
model_ref &get_model() {return m_model;} model_ref &get_model() {return m_model;}
ast_manager& get_ast_manager() const {return m;} ast_manager& get_ast_manager() const {return m;}
public: public:
bool is_true (const expr_ref_vector &v); bool is_true (const expr_ref_vector &v);
bool is_false(expr* x); bool is_false(expr* x);
bool is_true(expr* x); bool is_true(expr* x);
@ -105,74 +104,60 @@ public:
/// evaluates an expression /// evaluates an expression
bool eval (expr *e, expr_ref &result, bool model_completion); bool eval (expr *e, expr_ref &result, bool model_completion);
// expr_ref eval(expr* e, bool complete=true); // expr_ref eval(expr* e, bool complete=true);
}; };
/**
/**
\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 hoist non-boolean if expressions. \brief hoist non-boolean if expressions.
*/ */
void hoist_non_bool_if(expr_ref& fml);
bool is_difference_logic(ast_manager& m, unsigned num_fmls, expr* const* fmls); void to_mbp_benchmark(std::ostream &out, const expr* fml, const app_ref_vector &vars);
bool is_utvpi_logic(ast_manager& m, unsigned num_fmls, expr* const* fmls);
void to_mbp_benchmark(std::ostream &out, const expr* fml, // TBD: deprecate by qe::mbp
const app_ref_vector &vars); /**
/**
* do the following in sequence * do the following in sequence
* 1. use qe_lite to cheaply eliminate vars * 1. use qe_lite to cheaply eliminate vars
* 2. for remaining boolean vars, substitute using M * 2. for remaining boolean vars, substitute using M
* 3. use MBP for remaining array and arith variables * 3. use MBP for remaining array and arith variables
* 4. for any remaining arith variables, substitute using M * 4. for any remaining arith variables, substitute using M
*/ */
void qe_project (ast_manager& m, app_ref_vector& vars, expr_ref& fml, void qe_project (ast_manager& m, app_ref_vector& vars, expr_ref& fml,
const model_ref& M, bool reduce_all_selects=false, bool native_mbp=false, const model_ref& M, bool reduce_all_selects=false, bool native_mbp=false,
bool dont_sub=false); bool dont_sub=false);
void qe_project (ast_manager& m, app_ref_vector& vars, expr_ref& fml, model_ref& M, expr_map& map); void qe_project (ast_manager& m, app_ref_vector& vars, expr_ref& fml, model_ref& M, expr_map& map);
void expand_literals(ast_manager &m, expr_ref_vector& conjs); // TBD: sort out
void compute_implicant_literals (model_evaluator_util &mev, void expand_literals(ast_manager &m, expr_ref_vector& conjs);
expr_ref_vector &formula, expr_ref_vector &res); void compute_implicant_literals (model_evaluator_util &mev, expr_ref_vector &formula, expr_ref_vector &res);
void simplify_bounds (expr_ref_vector &lemmas); void simplify_bounds (expr_ref_vector &lemmas);
void normalize(expr *e, expr_ref &out, bool use_simplify_bounds = true, bool factor_eqs = false); void normalize(expr *e, expr_ref &out, bool use_simplify_bounds = true, bool factor_eqs = false);
/** Ground expression by replacing all free variables by skolem /**
** constants. On return, out is the resulting expression, and vars is * Ground expression by replacing all free variables by skolem
** a map from variable ids to corresponding skolem constants. * constants. On return, out is the resulting expression, and vars is
* a map from variable ids to corresponding skolem constants.
*/ */
void ground_expr (expr *e, expr_ref &out, app_ref_vector &vars); void ground_expr (expr *e, expr_ref &out, app_ref_vector &vars);
void mbqi_project (model &M, app_ref_vector &vars, expr_ref &fml);
void mbqi_project (model &M, app_ref_vector &vars, expr_ref &fml); bool contains_selects (expr* fml, ast_manager& m);
void get_select_indices (expr* fml, app_ref_vector& indices, ast_manager& m);
bool contains_selects (expr* fml, ast_manager& m); void find_decls (expr* fml, app_ref_vector& decls, std::string& prefix);
void get_select_indices (expr* fml, app_ref_vector& indices, ast_manager& m);
void find_decls (expr* fml, app_ref_vector& decls, std::string& prefix); /**
* extended pretty-printer
/** extended pretty-printer
* used for debugging * used for debugging
* disables aliasing of common sub-expressions * disables aliasing of common sub-expressions
*/ */
struct mk_epp : public mk_pp { struct mk_epp : public mk_pp {
params_ref m_epp_params; params_ref m_epp_params;
expr_ref m_epp_expr; expr_ref m_epp_expr;
mk_epp(ast *t, ast_manager &m, unsigned indent = 0, unsigned num_vars = 0, char const * var_prefix = nullptr); mk_epp(ast *t, ast_manager &m, unsigned indent = 0, unsigned num_vars = 0, char const * var_prefix = nullptr);
void rw(expr *e, expr_ref &out); void rw(expr *e, expr_ref &out);
};
};
} }
#endif #endif