diff options
author | Kshitij Bansal <kshitij@cs.nyu.edu> | 2012-05-09 05:45:36 +0000 |
---|---|---|
committer | Kshitij Bansal <kshitij@cs.nyu.edu> | 2012-05-09 05:45:36 +0000 |
commit | 6243fba11e0189891acf21de3c6daa072b038e13 (patch) | |
tree | 8265abfa3e583831a972acdf97989930ae9c3592 /src/util/ite_removal.h | |
parent | 9f74cfbd847663f80c362cf06bda7e749f0f694b (diff) |
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.
Diffstat (limited to 'src/util/ite_removal.h')
-rw-r--r-- | src/util/ite_removal.h | 16 |
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); |