diff options
author | Clark Barrett <barrett@cs.nyu.edu> | 2012-05-30 20:33:40 +0000 |
---|---|---|
committer | Clark Barrett <barrett@cs.nyu.edu> | 2012-05-30 20:33:40 +0000 |
commit | 03305bfae27642ed714eab144cf977d1943bb88d (patch) | |
tree | 42e24296848e69a7c6d2f5dd3eed53b518dc1954 /src/util/options.h | |
parent | 81b78827f65b42f22f16874bbf0c8269ed0734fc (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.h | 8 |
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; |