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

remove not

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-04-01 12:17:49 -07:00
parent 7e7cdf3635
commit 5fdf5b67a4
2 changed files with 5 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/ast/ast_util.h
View file

@ -140,8 +140,7 @@ expr * mk_not(ast_manager & m, expr * arg);
expr_ref mk_not(const expr_ref& e);
inline expr_ref not(const expr_ref& e) { return mk_not(e); }
inline app_ref not(const app_ref& e) { return app_ref(e.m().mk_not(e), e.m()); }
inline app_ref mk_not(const app_ref& e) { return app_ref(e.m().mk_not(e), e.m()); }
/**

8
src/tactic/core/special_relations_tactic.cpp
View file

@ -80,7 +80,7 @@ void special_relations_tactic::initialize() {
fml = m.mk_or(m.mk_not(Rxy), m.mk_not(Ryz), Rxz);
q = m.mk_forall(3, As, xyz, fml, 0, symbol::null, symbol::null, 1, pats);
register_pattern(m_pm.initialize(q), sr_transitive);
fml = m.mk_or(not(Rxy & Ryz), Rxz);
fml = m.mk_or(mk_not(Rxy & Ryz), Rxz);
q = m.mk_forall(3, As, xyz, fml, 0, symbol::null, symbol::null, 1, pats);
register_pattern(m_pm.initialize(q), sr_transitive);
@ -91,21 +91,21 @@ void special_relations_tactic::initialize() {
fml = m.mk_or(nRxy, nRyx, m.mk_eq(x, y));
q = m.mk_forall(2, As, xyz, fml, 0, symbol::null, symbol::null, 1, pats);
register_pattern(m_pm.initialize(q), sr_antisymmetric);
fml = m.mk_or(not(Rxy & Ryx), m.mk_eq(x, y));
fml = m.mk_or(mk_not(Rxy & Ryx), m.mk_eq(x, y));
q = m.mk_forall(2, As, xyz, fml, 0, symbol::null, symbol::null, 1, pats);
register_pattern(m_pm.initialize(q), sr_antisymmetric);
fml = m.mk_or(nRyx, nRzx, Ryz, Rzy);
q = m.mk_forall(3, As, xyz, fml, 0, symbol::null, symbol::null, 1, pats);
register_pattern(m_pm.initialize(q), sr_lefttree);
fml = m.mk_or(not (Ryx & Rzx), Ryz, Rzy);
fml = m.mk_or(mk_not (Ryx & Rzx), Ryz, Rzy);
q = m.mk_forall(3, As, xyz, fml, 0, symbol::null, symbol::null, 1, pats);
register_pattern(m_pm.initialize(q), sr_lefttree);
fml = m.mk_or(nRxy, nRxz, Ryz, Rzy);
q = m.mk_forall(3, As, xyz, fml, 0, symbol::null, symbol::null, 1, pats);
register_pattern(m_pm.initialize(q), sr_righttree);
fml = m.mk_or(not(Rxy & Rxz), Ryz, Rzy);
fml = m.mk_or(mk_not(Rxy & Rxz), Ryz, Rzy);
q = m.mk_forall(3, As, xyz, fml, 0, symbol::null, symbol::null, 1, pats);
register_pattern(m_pm.initialize(q), sr_righttree);