* FLAGIFFOVERFLOW -- flag is set iff the operation overflows
* IGNORE -- doesn't constrain output if the result cannot be represented
* WRAPAROUND -- wraps around like stand integer arithmetic
+ * NOOVERFLOW -- client has ensured that overflow is impossible
*/
-enum OverFlowBehavior {IGNORE, WRAPAROUND, FLAGFORCESOVERFLOW, OVERFLOWSETSFLAG, FLAGIFFOVERFLOW};
+enum OverFlowBehavior {IGNORE, WRAPAROUND, FLAGFORCESOVERFLOW, OVERFLOWSETSFLAG, FLAGIFFOVERFLOW, NOOVERFLOW};
enum BooleanType {_ORDER, _BOOLEAN};
struct FunctionEncoding;
typedef struct FunctionEncoding FunctionEncoding;
+typedef enum ArithOp ArithOp;
+typedef enum LogicOp LogicOp;
+typedef enum CompOp CompOp;
+typedef enum OrderType OrderType;
+typedef enum OverFlowBehavior OverFlowBehavior;
+
typedef unsigned int uint;
typedef uint64_t VarType;
#endif
return boolean;
}
-Function * createFunctionOperator(CSolver *solver, enum ArithOp op, Set ** domain, uint numDomain, Set * range,
- enum OverFlowBehavior overflowbehavior, Boolean * overflowstatus) {
+Function * createFunctionOperator(CSolver *solver, ArithOp op, Set ** domain, uint numDomain, Set * range,
+ OverFlowBehavior overflowbehavior) {
return NULL;
}
-Predicate * createPredicateOperator(CSolver *solver, enum CompOp op, Set ** domain, uint numDomain) {
+Predicate * createPredicateOperator(CSolver *solver, CompOp op, Set ** domain, uint numDomain) {
return allocPredicate(op, domain,numDomain);
}
return NULL;
}
-Element * applyFunction(CSolver *solver, Function * function, Element ** array) {
+Element * applyFunction(CSolver *solver, Function * function, Element ** array, Boolean * overflowstatus) {
return NULL;
}
return NULL;
}
-Boolean * applyLogicalOperation(CSolver *solver, enum LogicOp op, Boolean ** array) {
+Boolean * applyLogicalOperation(CSolver *solver, LogicOp op, Boolean ** array) {
return NULL;
}
pushVectorBoolean(this->constraints, constraint);
}
-Order * createOrder(CSolver *solver, enum OrderType type, Set * set) {
+Order * createOrder(CSolver *solver, OrderType type, Set * set) {
return allocOrder(type, set);
}
/** This function creates a function operator. */
-Function * createFunctionOperator(CSolver *solver, enum ArithOp op, Set ** domain, uint numDomain, Set * range,
- enum OverFlowBehavior overflowbehavior, Boolean * overflowstatus);
+Function * createFunctionOperator(CSolver *solver, ArithOp op, Set ** domain, uint numDomain, Set * range,
+ OverFlowBehavior overflowbehavior);
/** This function creates a predicate operator. */
/** This function applies a function to the Elements in its input. */
-Element * applyFunction(CSolver *, Function * function, Element ** array);
+Element * applyFunction(CSolver *, Function * function, Element ** array, Boolean * overflowstatus);
/** This function applies a predicate to the Elements in its input. */