This commit merges in the branch arithmetic/cprop.

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;