summaryrefslogtreecommitdiff
path: root/src/util/options.h
diff options
context:
space:
mode:
authorClark Barrett <barrett@cs.nyu.edu>2012-05-30 20:33:40 +0000
committerClark Barrett <barrett@cs.nyu.edu>2012-05-30 20:33:40 +0000
commit03305bfae27642ed714eab144cf977d1943bb88d (patch)
tree42e24296848e69a7c6d2f5dd3eed53b518dc1954 /src/util/options.h
parent81b78827f65b42f22f16874bbf0c8269ed0734fc (diff)
Added BitwiseEq bitvector rewrite
Added option "--repeat-simp" which repeats nonclausal simplification: 4 times, twice before ite removal and twice after Enabled these options (plus ite-simp) on QF_AUFBV, obtaining significant speedup on dwp examples
Diffstat (limited to 'src/util/options.h')
-rw-r--r--src/util/options.h8
1 files changed, 8 insertions, 0 deletions
diff --git a/src/util/options.h b/src/util/options.h
index 9c36a471d..e6135dacb 100644
--- a/src/util/options.h
+++ b/src/util/options.h
@@ -154,6 +154,14 @@ struct CVC4_PUBLIC Options {
*/
bool doITESimpSetByUser;
+ /** Whether to do multiple rounds of nonclausal simplification */
+ bool repeatSimp;
+
+ /**
+ * Whether the user explicitly requested multiple rounds of nonclausal simplification
+ */
+ bool repeatSimpSetByUser;
+
/** Whether we're in interactive mode or not */
bool interactive;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback