3 enum LogicOp {SATC_AND, SATC_OR, SATC_NOT, SATC_XOR, 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;
15 enum HappenedBefore {SATC_FIRST, SATC_SECOND, SATC_UNORDERED};
16 typedef enum HappenedBefore HappenedBefore;
19 * FLAGFORCESOVERFLOW forces the operation to overflow if the boolean flag is true
20 * OVERFLOWSETSFLAG -- sets the flag if the operation overflows
21 * FLAGIFFOVERFLOW -- flag is set iff the operation overflows
22 * SATC_IGNORE -- doesn't constrain output if the result cannot be represented
23 * SATC_WRAPAROUND -- wraps around like stand integer arithmetic
24 * NOOVERFLOW -- client has ensured that overflow is impossible
26 enum OverFlowBehavior {SATC_IGNORE, SATC_WRAPAROUND, FLAGFORCESOVERFLOW, OVERFLOWSETSFLAG, FLAGIFFOVERFLOW, NOOVERFLOW};
27 typedef enum OverFlowBehavior OverFlowBehavior;
29 enum UndefinedBehavior {SATC_IGNOREBEHAVIOR, FLAGFORCEUNDEFINED, UNDEFINEDSETSFLAG, FLAGIFFUNDEFINED};
30 typedef enum UndefinedBehavior UndefinedBehavior;
32 enum FunctionType {TABLEFUNC, OPERATORFUNC};
33 typedef enum FunctionType FunctionType;
35 enum PredicateType {TABLEPRED, OPERATORPRED};
36 typedef enum PredicateType PredicateType;
38 enum ASTNodeType {ORDERCONST, BOOLEANVAR, LOGICOP, PREDICATEOP, BOOLCONST, ELEMSET, ELEMFUNCRETURN, ELEMCONST};
39 typedef enum ASTNodeType ASTNodeType;
41 enum Polarity {P_UNDEFINED=0, P_TRUE=1, P_FALSE=2, P_BOTHTRUEFALSE=3};
42 typedef enum Polarity Polarity;
44 enum BooleanValue {BV_UNDEFINED=0, BV_MUSTBETRUE=1, BV_MUSTBEFALSE=2, BV_UNSAT=3};
45 typedef enum BooleanValue BooleanValue;