X-Git-Url: http://plrg.eecs.uci.edu/git/?p=satune.git;a=blobdiff_plain;f=src%2Fccsolver.cc;h=a1dd75898acc356574fe5089097f35d52b1d3913;hp=f9ebdbbfe8d2beae9557423d4847497d70150107;hb=3c33c8ed7c4600da543b2a82bcffd5aca86f0eb9;hpb=19c299fd9e91386883e788f445d153abfe58430a

diff --git a/src/ccsolver.cc b/src/ccsolver.cc
index f9ebdbb..a1dd758 100644
--- a/src/ccsolver.cc
+++ b/src/ccsolver.cc
@@ -10,6 +10,10 @@ void deleteCCSolver(void *solver) {
 	delete CCSOLVER(solver);
 }
 
+void resetCCSolver(void *solver) {
+	CCSOLVER(solver)->resetSolver();
+}
+
 void *createSet(void *solver,unsigned int type, long *elements, unsigned int num) {
 	return CCSOLVER(solver)->createSet((VarType) type, (uint64_t *)elements, (uint) num);
 }
@@ -50,6 +54,14 @@ void *getBooleanVar(void *solver,unsigned int type) {
 	return CCSOLVER(solver)->getBooleanVar((VarType) type).getRaw();
 }
 
+void *getBooleanTrue(void *solver) {
+	return CCSOLVER(solver)->getBooleanTrue().getRaw();
+}
+
+void *getBooleanFalse(void *solver) {
+	return CCSOLVER(solver)->getBooleanFalse().getRaw();
+}
+
 void *createFunctionOperator(void *solver,unsigned int op, void *range,unsigned int overflowbehavior) {
 	return CCSOLVER(solver)->createFunctionOperator((ArithOp) op, (Set *)range, (OverFlowBehavior) overflowbehavior);
 }
@@ -90,8 +102,28 @@ void *applyPredicate(void *solver,void *predicate, void **inputs, unsigned int n
 	return CCSOLVER(solver)->applyPredicate((Predicate *)predicate, (Element **)inputs, (uint) numInputs).getRaw();
 }
 
-void *applyLogicalOperation(void *solver,unsigned int op, void *array, unsigned int asize) {
-	return CCSOLVER(solver)->applyLogicalOperation((LogicOp) op, (BooleanEdge *)array, (uint) asize).getRaw();
+void *applyLogicalOperation(void *solver,unsigned int op, void **array, unsigned int asize) {
+	BooleanEdge constr [asize];
+	for (uint i = 0; i < asize; i++) {
+		constr[i] = BooleanEdge((Boolean *)array[i]);
+	}
+	return CCSOLVER(solver)->applyLogicalOperation((LogicOp) op, constr, (uint) asize).getRaw();
+}
+
+void *applyExactlyOneConstraint(void *solver, void **array, unsigned int asize) {
+	BooleanEdge constr [asize];
+	for (uint i = 0; i < asize; i++) {
+		constr[i] = BooleanEdge((Boolean *)array[i]);
+	}
+	return CCSOLVER(solver)->applyExactlyOneConstraint( constr, (uint) asize).getRaw();
+}
+
+void *applyAtMostOneConstraint(void *solver, void **array, unsigned int asize) {
+	BooleanEdge constr [asize];
+	for (uint i = 0; i < asize; i++) {
+		constr[i] = BooleanEdge((Boolean *)array[i]);
+	}
+	return CCSOLVER(solver)->applyAtMostOneConstraint( constr, (uint) asize).getRaw();
 }
 
 void *applyLogicalOperationTwo(void *solver,unsigned int op, void *arg1, void *arg2) {
@@ -106,6 +138,10 @@ void addConstraint(void *solver,void *constraint) {
 	CCSOLVER(solver)->addConstraint(BooleanEdge((Boolean *) constraint));
 }
 
+void printConstraint(void *solver,void *constraint) {
+	CCSOLVER(solver)->printConstraint(BooleanEdge((Boolean *) constraint));
+}
+
 void *createOrder(void *solver,unsigned int type, void *set) {
 	return CCSOLVER(solver)->createOrder((OrderType) type, (Set *)set);
 }
@@ -118,10 +154,18 @@ int solve(void *solver) {
 	return CCSOLVER(solver)->solve();
 }
 
+int solveIncremental(void *solver) {
+	return CCSOLVER(solver)->solveIncremental();
+}
+
 long getElementValue(void *solver,void *element) {
 	return (long) CCSOLVER(solver)->getElementValue((Element *)element);
 }
 
+void freezeElement(void *solver,void *element) {
+	CCSOLVER(solver)->freezeElement((Element *)element);
+}
+
 int getBooleanValue(void *solver, void *boolean) {
 	return CCSOLVER(solver)->getBooleanValue(BooleanEdge((Boolean *) boolean));
 }
@@ -134,6 +178,9 @@ void printConstraints(void *solver) {
 	CCSOLVER(solver)->printConstraints();
 }
 
+void turnoffOptimizations(void *solver) {
+	CCSOLVER(solver)->turnoffOptimizations();
+}
 
 
 void serialize(void *solver) {
@@ -145,6 +192,10 @@ void mustHaveValue(void *solver, void *element) {
 	CCSOLVER(solver)->mustHaveValue( (Element *) element);
 }
 
+void setInterpreter(void *solver, unsigned int type) {
+	CCSOLVER(solver)->setInterpreter((InterpreterType)type);
+}
+
 void *clone(void *solver) {
 	return CCSOLVER(solver)->clone();
-}
\ No newline at end of file
+}