mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-06 06:03:23 +00:00
Code Activity

pruning simplifier dependencies

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-08-23 16:56:55 -07:00
parent 8ff8470809
commit f91496f5ff
2 changed files with 8 additions and 7 deletions
Download patch file Download diff file Expand all files Collapse all files

10
src/ast/simplifier/pull_ite_tree.cpp
View file

@ -21,9 +21,9 @@ Revision History:
#include "ast/for_each_expr.h" #include "ast/for_each_expr.h"
#include "ast/ast_pp.h" #include "ast/ast_pp.h"
pull_ite_tree::pull_ite_tree(ast_manager & m, simplifier & s): pull_ite_tree::pull_ite_tree(ast_manager & m):
m_manager(m), m_manager(m),
m_simplifier(s), m_rewriter(m),
m_cache(m) { m_cache(m) {
} }
@ -64,7 +64,7 @@ void pull_ite_tree::reduce(expr * n) {
get_cached(e_old, e, e_pr); get_cached(e_old, e, e_pr);
expr_ref r(m_manager); expr_ref r(m_manager);
expr * args[3] = {c, t, e}; expr * args[3] = {c, t, e};
m_simplifier.mk_app(to_app(n)->get_decl(), 3, args, r); r = m_rewriter.mk_app(to_app(n)->get_decl(), 3, args);
if (!m_manager.proofs_enabled()) { if (!m_manager.proofs_enabled()) {
// expr * r = m_manager.mk_ite(c, t, e); // expr * r = m_manager.mk_ite(c, t, e);
cache_result(n, r, 0); cache_result(n, r, 0);
@ -117,7 +117,7 @@ void pull_ite_tree::reduce(expr * n) {
else { else {
expr_ref r(m_manager); expr_ref r(m_manager);
m_args[m_arg_idx] = n; m_args[m_arg_idx] = n;
m_simplifier.mk_app(m_p, m_args.size(), m_args.c_ptr(), r); r = m_rewriter.mk_app(m_p, m_args.size(), m_args.c_ptr());
if (!m_manager.proofs_enabled()) { if (!m_manager.proofs_enabled()) {
// expr * r = m_manager.mk_app(m_p, m_args.size(), m_args.c_ptr()); // expr * r = m_manager.mk_app(m_p, m_args.size(), m_args.c_ptr());
cache_result(n, r, 0); cache_result(n, r, 0);
@ -181,7 +181,7 @@ void pull_ite_tree::operator()(app * n, app_ref & r, proof_ref & pr) {
pull_ite_tree_star::pull_ite_tree_star(ast_manager & m, simplifier & s): pull_ite_tree_star::pull_ite_tree_star(ast_manager & m, simplifier & s):
simplifier(m), simplifier(m),
m_proc(m, s) { m_proc(m) {
borrow_plugins(s); borrow_plugins(s);
} }

5
src/ast/simplifier/pull_ite_tree.h
View file

@ -20,6 +20,7 @@ Revision History:
#define PULL_ITE_TREE_H_ #define PULL_ITE_TREE_H_
#include "ast/ast.h" #include "ast/ast.h"
#include "ast/rewriter/th_rewriter.h"
#include "ast/simplifier/simplifier.h" #include "ast/simplifier/simplifier.h"
#include "ast/recurse_expr.h" #include "ast/recurse_expr.h"
#include "util/obj_hashtable.h" #include "util/obj_hashtable.h"
@ -34,7 +35,7 @@ Revision History:
*/ */
class pull_ite_tree { class pull_ite_tree {
ast_manager & m_manager; ast_manager & m_manager;
simplifier & m_simplifier; th_rewriter m_rewriter;
func_decl * m_p; func_decl * m_p;
ptr_vector<expr> m_args; ptr_vector<expr> m_args;
unsigned m_arg_idx; //!< position of the ite argument unsigned m_arg_idx; //!< position of the ite argument
@ -56,7 +57,7 @@ class pull_ite_tree {
return m_manager.mk_app(m_p, m_args.size(), m_args.c_ptr()); return m_manager.mk_app(m_p, m_args.size(), m_args.c_ptr());
} }
public: public:
pull_ite_tree(ast_manager & m, simplifier & s); pull_ite_tree(ast_manager & m);
/** /**
\brief Apply the transformation above if n contains an ite-expression. \brief Apply the transformation above if n contains an ite-expression.
Store the result in r. If n does not contain an ite-expression, then Store the result in r. If n does not contain an ite-expression, then