diff options
Diffstat (limited to 'src/expr')
-rw-r--r-- | src/expr/expr_template.cpp | 2 | ||||
-rw-r--r-- | src/expr/node.h | 10 | ||||
-rw-r--r-- | src/expr/node_manager.cpp | 7 | ||||
-rw-r--r-- | src/expr/node_manager.h | 3 |
4 files changed, 11 insertions, 11 deletions
diff --git a/src/expr/expr_template.cpp b/src/expr/expr_template.cpp index 43e4a7b76..dad437bc6 100644 --- a/src/expr/expr_template.cpp +++ b/src/expr/expr_template.cpp @@ -528,7 +528,7 @@ Expr Expr::iffExpr(const Expr& e) const { "Don't have an expression manager for this expression!"); PrettyCheckArgument(d_exprManager == e.d_exprManager, e, "Different expression managers!"); - return d_exprManager->mkExpr(IFF, *this, e); + return d_exprManager->mkExpr(EQUAL, *this, e); } Expr Expr::impExpr(const Expr& e) const { diff --git a/src/expr/node.h b/src/expr/node.h index c9bfb75a4..6dbb5aa2b 100644 --- a/src/expr/node.h +++ b/src/expr/node.h @@ -893,8 +893,6 @@ public: NodeTemplate<true> iteNode(const NodeTemplate<ref_count2>& thenpart, const NodeTemplate<ref_count3>& elsepart) const; template <bool ref_count2> - NodeTemplate<true> iffNode(const NodeTemplate<ref_count2>& right) const; - template <bool ref_count2> NodeTemplate<true> impNode(const NodeTemplate<ref_count2>& right) const; template <bool ref_count2> NodeTemplate<true> xorNode(const NodeTemplate<ref_count2>& right) const; @@ -1203,14 +1201,6 @@ NodeTemplate<ref_count>::iteNode(const NodeTemplate<ref_count2>& thenpart, template <bool ref_count> template <bool ref_count2> NodeTemplate<true> -NodeTemplate<ref_count>::iffNode(const NodeTemplate<ref_count2>& right) const { - assertTNodeNotExpired(); - return NodeManager::currentNM()->mkNode(kind::IFF, *this, right); -} - -template <bool ref_count> -template <bool ref_count2> -NodeTemplate<true> NodeTemplate<ref_count>::impNode(const NodeTemplate<ref_count2>& right) const { assertTNodeNotExpired(); return NodeManager::currentNM()->mkNode(kind::IMPLIES, *this, right); diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp index a9be51418..ebf78f541 100644 --- a/src/expr/node_manager.cpp +++ b/src/expr/node_manager.cpp @@ -780,6 +780,13 @@ Node NodeManager::mkInstConstant(const TypeNode& type) { return n; } +Node NodeManager::mkBooleanTermVariable() { + Node n = NodeBuilder<0>(this, kind::BOOLEAN_TERM_VARIABLE); + n.setAttribute(TypeAttr(), booleanType()); + n.setAttribute(TypeCheckedAttr(), true); + return n; +} + Node NodeManager::mkUniqueVar(const TypeNode& type, Kind k) { std::map< TypeNode, Node >::iterator it = d_unique_vars[k].find( type ); if( it==d_unique_vars[k].end() ){ diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index d85ff23d5..d2b45a636 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -528,6 +528,9 @@ public: /** Create a instantiation constant with the given type. */ Node mkInstConstant(const TypeNode& type); + + /** Create a boolean term variable. */ + Node mkBooleanTermVariable(); /** Make a new abstract value with the given type. */ Node mkAbstractValue(const TypeNode& type); |