Adding SMT Interpreters

[satune.git] / src / AST / ops.h

diff --git a/src/AST/ops.h b/src/AST/ops.h
index 8ad60c7545ad1884d7c18247473025749540a2aa..6d6fd97a36242e1eac656145f145fc05bd348c86 100644 (file)
--- a/src/AST/ops.h
+++ b/src/AST/ops.h
@@ -1,6 +1,6 @@
 #ifndef OPS_H
 #define OPS_H
-enum LogicOp {SATC_AND, SATC_OR, SATC_NOT, SATC_XOR, SATC_IMPLIES};
+enum LogicOp {SATC_AND, SATC_OR, SATC_NOT, SATC_XOR, SATC_IFF, SATC_IMPLIES};
 typedef enum LogicOp LogicOp;
 
 enum ArithOp {SATC_ADD, SATC_SUB};
@@ -12,9 +12,6 @@ typedef enum CompOp CompOp;
 enum OrderType {SATC_PARTIAL, SATC_TOTAL};
 typedef enum OrderType OrderType;
 
-enum HappenedBefore {SATC_FIRST, SATC_SECOND, SATC_UNORDERED};
-typedef enum HappenedBefore HappenedBefore;
-
 /**
  *    SATC_FLAGFORCESOVERFLOW forces the operation to overflow if the boolean flag is true
  *  SATC_OVERFLOWSETSFLAG -- sets the flag if the operation overflows
@@ -29,4 +26,8 @@ typedef enum OverFlowBehavior OverFlowBehavior;
 enum UndefinedBehavior {SATC_IGNOREBEHAVIOR, SATC_FLAGFORCEUNDEFINED, SATC_UNDEFINEDSETSFLAG, SATC_FLAGIFFUNDEFINED};
 typedef enum UndefinedBehavior UndefinedBehavior;
 
+enum InterpreterType {SATUNE, ALLOY, Z3, MATHSAT, SMTRAT};
+typedef enum InterpreterType InterpreterType;
+
+
 #endif