diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-08-23 10:15:43 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-08-23 10:15:43 -0500 |
commit | fd385efcc6b1e55431430af4213172594781e05f (patch) | |
tree | c9859677f48b91f31023d4004f6a5c59e60045f7 | |
parent | 847f415d9bd9aa98470109fbdc37fd379a79cb4e (diff) |
Minor update to term util (#3208)
-rw-r--r-- | src/theory/quantifiers/term_util.cpp | 11 |
1 files changed, 9 insertions, 2 deletions
diff --git a/src/theory/quantifiers/term_util.cpp b/src/theory/quantifiers/term_util.cpp index 1243d8d4a..94bc2c3f8 100644 --- a/src/theory/quantifiers/term_util.cpp +++ b/src/theory/quantifiers/term_util.cpp @@ -612,14 +612,21 @@ bool TermUtil::containsUninterpretedConstant( Node n ) { return n.getAttribute(ContainsUConstAttribute())!=0; } -Node TermUtil::simpleNegate( Node n ){ +Node TermUtil::simpleNegate(Node n) +{ + Assert(n.getType().isBoolean()); + NodeManager* nm = NodeManager::currentNM(); if( n.getKind()==OR || n.getKind()==AND ){ std::vector< Node > children; for (const Node& cn : n) { children.push_back(simpleNegate(cn)); } - return NodeManager::currentNM()->mkNode( n.getKind()==OR ? AND : OR, children ); + return nm->mkNode(n.getKind() == OR ? AND : OR, children); + } + else if (n.isConst()) + { + return nm->mkConst(!n.getConst<bool>()); } return n.negate(); } |