From 5fdf5b67a45bf7cc9259ad30273eef148c16f6d5 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 1 Apr 2019 12:17:49 -0700 Subject: [PATCH] remove not Signed-off-by: Nikolaj Bjorner --- src/ast/ast_util.h | 3 +-- src/tactic/core/special_relations_tactic.cpp | 8 ++++---- 2 files changed, 5 insertions(+), 6 deletions(-) diff --git a/src/ast/ast_util.h b/src/ast/ast_util.h index a8c9131c7..e317d14ec 100644 --- a/src/ast/ast_util.h +++ b/src/ast/ast_util.h @@ -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()); } /** diff --git a/src/tactic/core/special_relations_tactic.cpp b/src/tactic/core/special_relations_tactic.cpp index 75f8e270c..a8b74db31 100644 --- a/src/tactic/core/special_relations_tactic.cpp +++ b/src/tactic/core/special_relations_tactic.cpp @@ -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);