summaryrefslogtreecommitdiff
path: root/src/util/options.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/util/options.h')
-rw-r--r--src/util/options.h9
1 files changed, 9 insertions, 0 deletions
diff --git a/src/util/options.h b/src/util/options.h
index 06ca20073..ce2bc71e7 100644
--- a/src/util/options.h
+++ b/src/util/options.h
@@ -89,6 +89,9 @@ struct CVC4_PUBLIC Options {
/** Should we exit after parsing? */
bool parseOnly;
+ /** Should we exit after preprocessing? */
+ bool preprocessOnly;
+
/** Should the parser do semantic checks? */
bool semanticChecks;
@@ -194,6 +197,12 @@ struct CVC4_PUBLIC Options {
*/
uint16_t arithPropagateMaxLength;
+ /**
+ * Whether to do the symmetry-breaking preprocessing in UF as
+ * described by Deharbe et al. in CADE 2011 (on by default).
+ */
+ bool ufSymmetryBreaker;
+
Options();
/**
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback