X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=src%2Fccsolver.cc;h=d77352288e709f45aaed97f217891dfbeabad31a;hb=250304ccf75e2f6f6544022234dd5ad3ca7adbb2;hp=e5958ed5cc89aa8ca5641d0307fd255d3dc90624;hpb=3896ad686a910868d7bf2988cd83a4fe3da700b2;p=satune.git diff --git a/src/ccsolver.cc b/src/ccsolver.cc index e5958ed..d773522 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); } @@ -106,6 +118,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); } @@ -135,7 +151,6 @@ void printConstraints(void *solver) { } - void serialize(void *solver) { CCSOLVER(solver)->serialize(); } @@ -145,10 +160,10 @@ void mustHaveValue(void *solver, void *element) { CCSOLVER(solver)->mustHaveValue( (Element *) element); } -void setAlloyEncoder(void *solver){ - CCSOLVER(solver)->setAlloyEncoder(); +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 +}