#Ignoring netbeans configs
nbproject/
-sat_solver
+sat_solver*
setup.sh
#Ignoring binary files
--- /dev/null
+#!/bin/bash
+
+#Terminate the script if even one command fails
+set -e
+
+BASE=../
+SERVERS="dc-8.calit2.uci.edu dc-9.calit2.uci.edu dc-10.calit2.uci.edu dc-11.calit2.uci.edu"
+REMOTEDIR="/scratch/hamed/"
+INFILE="constraint_compiler/"
+SRC="constraint_compiler/src/"
+OUTFILE=csolver.tar.gz
+USER=hamed
+
+cd $BASE
+
+rm -f $OUTFILE
+tar -czvf $OUTFILE $INFILE
+
+for SERVER in $SERVERS; do
+ scp $OUTFILE "$USER@$SERVER:$REMOTEDIR"
+ ssh $USER@$SERVER "cd $REMOTEDIR; sudo rm -r $SRC; tar -xzvf $OUTFILE; cd $SRC; make clean; ./setup.sh"
+done
case SATC_LT: {
for(uint i=0; i<size; i++) {
uint64_t val = s->getElement(i);
- if (val >= cvalue)
+ if (val < cvalue)
elemArray[count++] = val;
}
break;
case SATC_GT: {
for(uint i=0; i<size; i++) {
uint64_t val = s->getElement(i);
- if (val <= cvalue)
+ if (val > cvalue)
elemArray[count++] = val;
}
break;
case SATC_LTE: {
for(uint i=0; i<size; i++) {
uint64_t val = s->getElement(i);
- if (val > cvalue)
+ if (val <= cvalue)
elemArray[count++] = val;
}
break;
case SATC_GTE: {
for(uint i=0; i<size; i++) {
uint64_t val = s->getElement(i);
- if (val < cvalue)
+ if (val >= cvalue)
elemArray[count++] = val;
}
break;
else
printf("UNSAT\n");
deleteCCSolver(solver);
+ return 0;
}
uint64_t getElementValueUnarySATTranslator(CSolver *This, ElementEncoding *elemEnc) {
uint i;
- bool overflow = true;
for (i = 0; i < elemEnc->numVars; i++) {
if (!getValueSolver(This->getSATEncoder()->getCNF()->solver, getEdgeVar( elemEnc->variables[i] )) ) {
- overflow = false;
break;
}
}
- if(overflow)
- model_print("WARNING: Element has undefined value!\n");
+
return elemEnc->encodingArray[i];
}
void mustHaveValue(void *solver, void *element){
CCSOLVER(solver)->mustHaveValue( (Element*) element);
}
+
+void* clone(void * solver){
+ return CCSOLVER(solver)->clone();
+}
\ No newline at end of file
void printConstraints(void* solver);
void serialize(void* solver);
void mustHaveValue(void *solver, void *element);
+void* clone(void * solver);
#ifdef __cplusplus
}
#endif
Element *CSolver::applyFunction(Function *function, Element **array, uint numArrays, BooleanEdge overflowstatus) {
+ ASSERT(numArrays == 2);
Element *element = new ElementFunction(function,array,numArrays,overflowstatus);
Element *e = elemMap.get(element);
if (e == NULL) {
csolverlb.getOrderConstraintValue.restype = c_int
csolverlb.printConstraints.argtypes = [c_void_p]
csolverlb.printConstraints.restype = None
+ csolverlb.clone.argtypes = [c_void_p]
+ csolverlb.clone.restype = c_void_p
csolverlb.serialize.argtypes = [c_void_p]
csolverlb.serialize.restype = None
return csolverlb