X-Git-Url: http://plrg.eecs.uci.edu/git/?p=satune.git;a=blobdiff_plain;f=src%2Fccsolver.h;h=638527c54f0d3370233bf6d556441c97357d94da;hp=2051cc91b9126e2e8b8ccfbdd61c6cb9eca46df0;hb=3c33c8ed7c4600da543b2a82bcffd5aca86f0eb9;hpb=3896ad686a910868d7bf2988cd83a4fe3da700b2

diff --git a/src/ccsolver.h b/src/ccsolver.h
index 2051cc9..638527c 100644
--- a/src/ccsolver.h
+++ b/src/ccsolver.h
@@ -8,6 +8,7 @@ extern "C" {
 #endif
 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);
@@ -18,6 +19,8 @@ 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);
@@ -28,20 +31,26 @@ 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 *applyLogicalOperation(void *solver,unsigned int op, void **array, unsigned int asize);
+void *applyExactlyOneConstraint(void *solver,void **array, unsigned int asize);
+void *applyAtMostOneConstraint(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 turnoffOptimizations(void *solver);
 void serialize(void *solver);
 void mustHaveValue(void *solver, void *element);
-void setAlloyEncoder(void *solver);
+void setInterpreter(void *solver, unsigned int type);
 void *clone(void *solver);
 #ifdef __cplusplus
 }