X-Git-Url: http://plrg.eecs.uci.edu/git/?p=satune.git;a=blobdiff_plain;f=src%2Fccsolver.h;h=091303fb18540a420da62aaac0c8ad1f632489e3;hp=a17bd1cfd1c9601e379245d747e705baf441b77a;hb=3e65b7dbdb78b63c39350090a5c5bb4eec4f4af9;hpb=dd44a9ad309116b641b812ac8c38c3c55d726d4c

diff --git a/src/ccsolver.h b/src/ccsolver.h
index a17bd1c..091303f 100644
--- a/src/ccsolver.h
+++ b/src/ccsolver.h
@@ -2,46 +2,54 @@
 #define __CCSOLVER_H
 
 
-typedef void* CCSolver;
+typedef void *CCSolver;
 #ifdef __cplusplus
 extern "C" {
 #endif
-void* createCCSolver();
-void deleteCCSolver(void* solver);
-void *createSet(void* solver,unsigned int type, long *elements, unsigned int num);
-void *createRangeSet(void* solver,unsigned int type, long lowrange, long highrange);
-void *createRangeVar(void* solver,unsigned int type, long lowrange, long highrange);
-void *createMutableSet(void* solver,unsigned int type);
-void addItem(void* solver,void *set, long element);
-void finalizeMutableSet(void* solver,void *set);
-void *getElementVar(void* solver,void *set);
-void *getElementConst(void* solver,unsigned int type, long value);
-void *getElementRange (void* solver,void *element);
-void* getBooleanVar(void* solver,unsigned int type);
-void *createFunctionOperator(void* solver,unsigned int op, void *range,unsigned int overflowbehavior);
-void *createPredicateOperator(void* solver,unsigned int op);
-void *createPredicateTable(void* solver,void *table, unsigned int behavior);
-void *createTable(void* solver, void *range);
-void *createTableForPredicate(void* solver);
-void addTableEntry(void* solver,void *table, void *inputs, unsigned int inputSize, long result);
-void *completeTable(void* solver,void *table, unsigned int behavior);
-void *applyFunction(void* solver,void *function, void**array, unsigned int numArrays, void* overflowstatus);
-void* applyPredicateTable(void* solver,void *predicate, void **inputs, unsigned int numInputs, void* undefinedStatus);
-void* applyPredicate(void* solver,void *predicate, void **inputs, unsigned int numInputs);
-void* applyLogicalOperation(void* solver,unsigned int op, void *array, unsigned int asize);
-void* applyLogicalOperationTwo(void* solver,unsigned int op, void* arg1, void* arg2);
-void* applyLogicalOperationOne(void* solver,unsigned int op, void* arg);
-void addConstraint(void* solver,void* constraint);
-void *createOrder(void* solver,unsigned int type, void *set);
-void* orderConstraint(void* solver,void *order, long first, long second);
-int solve(void* solver);
-long getElementValue(void* solver,void *element);
-int getBooleanValue(void* solver,void* boolean);
-int getOrderConstraintValue(void* solver,void *order, long first, long second);
-void printConstraints(void* solver);
-void serialize(void* solver);
+void *createCCSolver();
+void deleteCCSolver(void *solver);
+void resetCCSolver(void *solver);
+void *createSet(void *solver,unsigned int type, long *elements, unsigned int num);
+void *createRangeSet(void *solver,unsigned int type, long lowrange, long highrange);
+void *createRangeVar(void *solver,unsigned int type, long lowrange, long highrange);
+void *createMutableSet(void *solver,unsigned int type);
+void addItem(void *solver,void *set, long element);
+void finalizeMutableSet(void *solver,void *set);
+void *getElementVar(void *solver,void *set);
+void *getElementConst(void *solver,unsigned int type, long value);
+void *getElementRange (void *solver,void *element);
+void *getBooleanVar(void *solver,unsigned int type);
+void *getBooleanTrue(void *solver);
+void *getBooleanFalse(void *solver);
+void *createFunctionOperator(void *solver,unsigned int op, void *range,unsigned int overflowbehavior);
+void *createPredicateOperator(void *solver,unsigned int op);
+void *createPredicateTable(void *solver,void *table, unsigned int behavior);
+void *createTable(void *solver, void *range);
+void *createTableForPredicate(void *solver);
+void addTableEntry(void *solver,void *table, void *inputs, unsigned int inputSize, long result);
+void *completeTable(void *solver,void *table, unsigned int behavior);
+void *applyFunction(void *solver,void *function, void **array, unsigned int numArrays, void *overflowstatus);
+void *applyPredicateTable(void *solver,void *predicate, void **inputs, unsigned int numInputs, void *undefinedStatus);
+void *applyPredicate(void *solver,void *predicate, void **inputs, unsigned int numInputs);
+void *applyLogicalOperation(void *solver,unsigned int op, void **array, unsigned int asize);
+void *applyExactlyOneConstraint(void *solver,void **array, unsigned int asize);
+void *applyLogicalOperationTwo(void *solver,unsigned int op, void *arg1, void *arg2);
+void *applyLogicalOperationOne(void *solver,unsigned int op, void *arg);
+void addConstraint(void *solver,void *constraint);
+void printConstraint(void *solver,void *constraint);
+void *createOrder(void *solver,unsigned int type, void *set);
+void *orderConstraint(void *solver,void *order, long first, long second);
+int solve(void *solver);
+int solveIncremental(void *solver);
+long getElementValue(void *solver,void *element);
+void freezeElement(void *solver,void *element);
+int getBooleanValue(void *solver,void *boolean);
+int getOrderConstraintValue(void *solver,void *order, long first, long second);
+void printConstraints(void *solver);
+void serialize(void *solver);
 void mustHaveValue(void *solver, void *element);
-void* clone(void * solver);
+void setInterpreter(void *solver, unsigned int type);
+void *clone(void *solver);
 #ifdef __cplusplus
 }
 #endif