3 enum LogicOp {SATC_AND, SATC_OR, SATC_NOT, SATC_XOR, SATC_IFF, SATC_IMPLIES};
4 typedef enum LogicOp LogicOp;
6 enum ArithOp {SATC_ADD, SATC_SUB};
7 typedef enum ArithOp ArithOp;
9 enum CompOp {SATC_EQUALS, SATC_LT, SATC_GT, SATC_LTE, SATC_GTE};
10 typedef enum CompOp CompOp;
12 enum OrderType {SATC_PARTIAL, SATC_TOTAL};
13 typedef enum OrderType OrderType;
16 * SATC_FLAGFORCESOVERFLOW forces the operation to overflow if the boolean flag is true
17 * SATC_OVERFLOWSETSFLAG -- sets the flag if the operation overflows
18 * SATC_FLAGIFFOVERFLOW -- flag is set iff the operation overflows
19 * SATC_IGNORE -- doesn't constrain output if the result cannot be represented
20 * SATC_WRAPAROUND -- wraps around like stand integer arithmetic
21 * SATC_NOOVERFLOW -- client has ensured that overflow is impossible
23 enum OverFlowBehavior {SATC_IGNORE, SATC_WRAPAROUND, SATC_FLAGFORCESOVERFLOW, SATC_OVERFLOWSETSFLAG, SATC_FLAGIFFOVERFLOW, SATC_NOOVERFLOW};
24 typedef enum OverFlowBehavior OverFlowBehavior;
26 enum UndefinedBehavior {SATC_IGNOREBEHAVIOR, SATC_FLAGFORCEUNDEFINED, SATC_UNDEFINEDSETSFLAG, SATC_FLAGIFFUNDEFINED};
27 typedef enum UndefinedBehavior UndefinedBehavior;
29 enum InterpreterType {SATUNE, ALLOY, Z3, MATHSAT, SMTRAT};
30 typedef enum InterpreterType InterpreterType;