summaryrefslogtreecommitdiff
path: root/src/expr/node_manager.h
diff options
context:
space:
mode:
authorMathias Preiner <mathias.preiner@gmail.com>2021-04-21 10:21:34 -0700
committerGitHub <noreply@github.com>2021-04-21 10:21:34 -0700
commitae5ee4b07dc3d3c792e7fe7f382ff490dd28aca4 (patch)
treea7c2ab8013f46dbea75fcd6e7da3fb83e2012b2f /src/expr/node_manager.h
parent86aa9bc35ba9dc9a57913a2ffc71619c7657cc35 (diff)
Goodbye CVC4, hello cvc5! (#6371)
This commits changes the build system to cvc5 and removes the remaining occurrences of CVC4. It further cleans up outdated/unused scripts in contrib/.
Diffstat (limited to 'src/expr/node_manager.h')
-rw-r--r--src/expr/node_manager.h16
1 files changed, 1 insertions, 15 deletions
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index 528cdcfc7..6cda50075 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -338,20 +338,6 @@ class NodeManager
expr::NodeValue* child[N];
};/* struct NodeManager::NVStorage<N> */
- /* A note on isAtomic() and isAtomicFormula() (in CVC3 parlance)..
- *
- * It has been decided for now to hold off on implementations of
- * these functions, as they may only be needed in CNF conversion,
- * where it's pointless to do a lazy isAtomic determination by
- * searching through the DAG, and storing it, since the result will
- * only be used once. For more details see the 4/27/2010 cvc5
- * developer's meeting notes at:
- *
- * http://cvc4.cs.stanford.edu/wiki/Meeting_Minutes_-_April_27,_2010#isAtomic.28.29_and_isAtomicFormula.28.29
- */
- // bool containsDecision(TNode); // is "atomic"
- // bool properlyContainsDecision(TNode); // all children are atomic
-
// undefined private copy constructor (disallow copy)
NodeManager(const NodeManager&) = delete;
@@ -1079,7 +1065,7 @@ class NodeManager
/**
* This function gives developers a hook into the NodeManager.
- * This can be changed in node_manager.cpp without recompiling most of cvc4.
+ * This can be changed in node_manager.cpp without recompiling most of cvc5.
*
* debugHook is a debugging only function, and should not be present in
* any published code!
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback