summaryrefslogtreecommitdiff
path: root/src/util/ite_removal.h
diff options
context:
space:
mode:
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>2013-03-11 16:29:22 -0500
committerAndrew Reynolds <andrew.j.reynolds@gmail.com>2013-03-11 16:29:33 -0500
commit63c1d547b7598e3dba35f865ba3749c15a105a6f (patch)
treed98dc90b48ab978654e4c0f23503230075b0d6bf /src/util/ite_removal.h
parent56b7a4f494dfe069fc4cbdb1dcd05c23c9b59a1d (diff)
ite removal option for quantifiers --ite-remove-quant, e-matching for boolean terms, improvement for pre skolemization
Diffstat (limited to 'src/util/ite_removal.h')
-rw-r--r--src/util/ite_removal.h2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/util/ite_removal.h b/src/util/ite_removal.h
index 77e9c39db..6c0c74cd4 100644
--- a/src/util/ite_removal.h
+++ b/src/util/ite_removal.h
@@ -55,7 +55,7 @@ public:
* ite created in conjunction with that skolem variable.
*/
Node run(TNode node, std::vector<Node>& additionalAssertions,
- IteSkolemMap& iteSkolemMap);
+ IteSkolemMap& iteSkolemMap, std::vector<Node>& quantVar);
};/* class RemoveTTE */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback