diff options
Diffstat (limited to 'src/util/options.h')
-rw-r--r-- | src/util/options.h | 40 |
1 files changed, 23 insertions, 17 deletions
diff --git a/src/util/options.h b/src/util/options.h index 896f77297..9c36a471d 100644 --- a/src/util/options.h +++ b/src/util/options.h @@ -203,9 +203,6 @@ struct CVC4_PUBLIC Options { /** Log to write replay instructions to; NULL if not logging. */ std::ostream* replayLog; - /** Turn on and of arithmetic propagation. */ - bool arithPropagation; - /** * Frequency for the sat solver to make random decisions. * Should be between 0 and 1. @@ -230,9 +227,17 @@ struct CVC4_PUBLIC Options { /** Restart interval increase factor for Minisat */ double satRestartInc; + /** Determines the type of Arithmetic Presolve Lemmas are generated.*/ + typedef enum { NO_PRESOLVE_LEMMAS, INEQUALITY_PRESOLVE_LEMMAS, EQUALITY_PRESOLVE_LEMMAS, ALL_PRESOLVE_LEMMAS} ArithUnateLemmaMode; + ArithUnateLemmaMode arithUnateLemmaMode; + + /** Determines the mode of arithmetic propagation. */ + typedef enum { NO_PROP, UNATE_PROP, BOUND_INFERENCE_PROP, BOTH_PROP} ArithPropagationMode; + ArithPropagationMode arithPropagationMode; + /** The pivot rule for arithmetic */ typedef enum { MINIMUM, BREAK_TIES, MAXIMUM } ArithPivotRule; - ArithPivotRule pivotRule; + ArithPivotRule arithPivotRule; /** * The number of pivots before Bland's pivot rule is used on a basic @@ -246,22 +251,10 @@ 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; - - /** - * Whether the user explicitly requested that the symmetry - * breaker be enabled or disabled. - */ - bool ufSymmetryBreakerSetByUser; - - /** * Whether to do the linear diophantine equation solver * in Arith as described by Griggio JSAT 2012 (on by default). */ - bool dioSolver; + bool arithDioSolver; /** * Whether to split (= x y) into (and (<= x y) (>= x y)) in @@ -274,6 +267,19 @@ struct CVC4_PUBLIC Options { */ bool arithRewriteEqSetByUser; + /** + * Whether to do the symmetry-breaking preprocessing in UF as + * described by Deharbe et al. in CADE 2011 (on by default). + */ + bool ufSymmetryBreaker; + + /** + * Whether the user explicitly requested that the symmetry + * breaker be enabled or disabled. + */ + bool ufSymmetryBreakerSetByUser; + + /** The output channel to receive notfication events for new lemmas */ LemmaOutputChannel* lemmaOutputChannel; LemmaInputChannel* lemmaInputChannel; |