summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/trigger.h
diff options
context:
space:
mode:
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>2014-01-28 09:51:33 -0600
committerAndrew Reynolds <andrew.j.reynolds@gmail.com>2014-01-28 09:51:44 -0600
commitd3822db24e15e255766866a47e6ffa0d8d91911b (patch)
tree221298973f410f4305f74cd6041b6a017aaa3075 /src/theory/quantifiers/trigger.h
parent587bc5c82e2921a72cec58dc2ec69e3e0ed71866 (diff)
More optimizations of quantifier instantiation data structures.
Diffstat (limited to 'src/theory/quantifiers/trigger.h')
-rw-r--r--src/theory/quantifiers/trigger.h2
1 files changed, 2 insertions, 0 deletions
diff --git a/src/theory/quantifiers/trigger.h b/src/theory/quantifiers/trigger.h
index 28fb2acda..23cf5f5d0 100644
--- a/src/theory/quantifiers/trigger.h
+++ b/src/theory/quantifiers/trigger.h
@@ -114,12 +114,14 @@ public:
static bool isBooleanTermTrigger( Node n );
inline void toStream(std::ostream& out) const {
+ /*
out << "TRIGGER( ";
for( int i=0; i<(int)d_nodes.size(); i++ ){
if( i>0 ){ out << ", "; }
out << d_nodes[i];
}
out << " )";
+ */
}
};
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback