Merge from decision branch (ITE support)

Major changes from last merge
* ITEs supported
* Don't share theory lemmas to DE, only assertions

Should probably be noted that 'make regress' doesn't quite
pass with --decision=justification. Throws off search in couple
of arith benchmarks.

No serious performance changes expected. Keep an eye.

1 files changed, 10 insertions, 6 deletions

diff --git a/src/util/ite_removal.h b/src/util/ite_removal.h
index 248ce4efa..7327d4a64 100644
--- a/src/util/ite_removal.h
+++ b/src/util/ite_removal.h
@@ -33,16 +33,20 @@ class RemoveITE {
 public:
 
   /**
-   * Removes the ITE nodes by introducing skolem variables. All additional assertions are pushed into assertions.
-   * iteSkolemMap contains a map from introduced skolem variables to the index in assertions containing the new
-   * Boolean ite created in conjunction with that skolem variable.
+   * Removes the ITE nodes by introducing skolem variables. All
+   * additional assertions are pushed into assertions. iteSkolemMap
+   * contains a map from introduced skolem variables to the index in
+   * assertions containing the new Boolean ite created in conjunction
+   * with that skolem variable.
    */
   static void run(std::vector<Node>& assertions, IteSkolemMap& iteSkolemMap);
 
   /**
-   * Removes the ITE from the node by introducing skolem variables. All additional assertions are pushed into assertions.
-   * iteSkolemMap contains a map from introduced skolem variables to the index in assertions containing the new
-   * Boolean ite created in conjunction with that skolem variable.
+   * Removes the ITE from the node by introducing skolem
+   * variables. All additional assertions are pushed into
+   * assertions. iteSkolemMap contains a map from introduced skolem
+   * variables to the index in assertions containing the new Boolean
+   * ite created in conjunction with that skolem variable.
    */
   static Node run(TNode node, std::vector<Node>& additionalAssertions,
                   IteSkolemMap& iteSkolemMap);