From: Hamed <hamed.gorjiara@gmail.com>
Date: Tue, 11 Jul 2017 17:45:09 +0000 (-0700)
Subject: Fixing bugs + resolving conflicts
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=4829c9e49aac9037ec1c04ccda9730d01d76ee4e;p=satune.git

Fixing bugs + resolving conflicts
---

4829c9e49aac9037ec1c04ccda9730d01d76ee4e
diff --cc src/Backend/satencoder.c
index 0299740,0aa0df7..ad59903
--- a/src/Backend/satencoder.c
+++ b/src/Backend/satencoder.c
@@@ -82,10 -68,10 +68,10 @@@ void encodeAllSATEncoder(CSolver *csolv
  	uint size=getSizeVectorBoolean(constraints);
  	for(uint i=0;i<size;i++) {
  		Boolean *constraint=getVectorBoolean(constraints, i);
- 		Constraint* c= encodeConstraintSATEncoder(This, constraint);
- 		printConstraint(c);
- 		model_print("\n\n");
- 		addConstraintToSATSolver(c, This->satSolver);
+ 		Edge c= encodeConstraintSATEncoder(This, constraint);
+ 		printCNF(c);
 -		printf("\n");
++		printf("\n\n");
+ 		addConstraint(This->cnf, c);
  	}
  }
  
@@@ -339,16 -314,15 +314,15 @@@ Edge encodeEnumTablePredicateSATEncoder
  			} else {
  				carray[j] = tmpc;
  			}
- 			ASSERT(carray[j]!= NULL);
  		}
- 		constraints[i]=allocArrayConstraint(AND, inputNum, carray);
+ 		constraints[i]=constraintAND(This->cnf, inputNum, carray);
  	}
- 	Constraint* result= allocArrayConstraint(OR, size, constraints);
- 	//FIXME: if it didn't match with any entry
- 	return encType==ENUMERATEIMPLICATIONS? result: negateConstraint(result);
+ 	Edge result=constraintOR(This->cnf, size, constraints);
+ 
 -	return generationNegation ? result: constraintNegate(result);
++	return generateNegation ? result: constraintNegate(result);
  }
  
- Constraint * encodeOperatorPredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint){
+ Edge encodeOperatorPredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint){
  	switch(constraint->encoding.type){
  		case ENUMERATEIMPLICATIONS:
  			return encodeEnumOperatorPredicateSATEncoder(This, constraint);
@@@ -417,43 -388,32 +388,40 @@@ Edge encodeTableElementFunctionSATEncod
  		default:
  			ASSERT(0);
  	}
- 	return NULL;
+ 	return E_BOGUS;
  }
  
- Constraint* encodeOperatorElementFunctionSATEncoder(SATEncoder* encoder, ElementFunction* This){
+ Edge encodeOperatorElementFunctionSATEncoder(SATEncoder* encoder, ElementFunction* This){
  	ASSERT(GETFUNCTIONTYPE(This->function) == OPERATORFUNC);
  	ASSERT(getSizeArrayElement(&This->inputs)==2 );
- 	Constraint *elemc1=NULL, *elemc2 = NULL;
 -	ElementEncoding* elem1 = getElementEncoding( getArrayElement(&This->inputs,0) );
 -	ElementEncoding* elem2 = getElementEncoding( getArrayElement(&This->inputs,1) );
 -	Edge carray[elem1->encArraySize*elem2->encArraySize];
++	Edge elemc1 = E_NULL, elemc2 = E_NULL;
 +	Element* elem1 = getArrayElement(&This->inputs,0);
 +	Element* elem2 = getArrayElement(&This->inputs,1);
 +	if( GETELEMENTTYPE(elem1) == ELEMFUNCRETURN)
 +		elemc1 = encodeFunctionElementSATEncoder(encoder, (ElementFunction*) elem1);
 +	if( GETELEMENTTYPE(elem2) == ELEMFUNCRETURN)
 +		elemc2 = encodeFunctionElementSATEncoder(encoder , (ElementFunction*) elem2);
 +	
- 	ElementEncoding* elemEnc1 = getElementEncoding( elem1 );
- 	ElementEncoding* elemEnc2 = getElementEncoding( elem2 );
- 	Constraint* carray[elemEnc1->encArraySize*elemEnc2->encArraySize];
++	ElementEncoding* elemEnc1 = getElementEncoding( getArrayElement(&This->inputs,0) );
++	ElementEncoding* elemEnc2 = getElementEncoding( getArrayElement(&This->inputs,1) );
++	Edge carray[elemEnc1->encArraySize*elemEnc2->encArraySize];
  	uint size=0;
- 	Constraint* overFlowConstraint = ((BooleanVar*) This->overflowstatus)->var;
+ 	Edge overFlowConstraint = ((BooleanVar*) This->overflowstatus)->var;
 -	for(uint i=0; i<elem1->encArraySize; i++){
 -		if(isinUseElement(elem1, i)){
 -			for( uint j=0; j<elem2->encArraySize; j++){
 -				if(isinUseElement(elem2, j)){
 +	for(uint i=0; i<elemEnc1->encArraySize; i++){
 +		if(isinUseElement(elemEnc1, i)){
 +			for( uint j=0; j<elemEnc2->encArraySize; j++){
 +				if(isinUseElement(elemEnc2, j)){
  					bool isInRange = false;
 -					uint64_t result= applyFunctionOperator((FunctionOperator*)This->function,elem1->encodingArray[i],
 -						elem2->encodingArray[j], &isInRange);
 +					uint64_t result= applyFunctionOperator((FunctionOperator*)This->function,elemEnc1->encodingArray[i],
 +						elemEnc2->encodingArray[j], &isInRange);
  					//FIXME: instead of getElementValueConstraint, it might be useful to have another function
  					// that doesn't iterate over encodingArray and treats more efficient ...
- 					Constraint* valConstrIn1 = getElementValueConstraint(encoder, elemEnc1->element, elemEnc1->encodingArray[i]);
- 					ASSERT(valConstrIn1 != NULL);
- 					Constraint* valConstrIn2 = getElementValueConstraint(encoder, elemEnc2->element, elemEnc2->encodingArray[j]);
- 					ASSERT(valConstrIn2 != NULL);
- 					Constraint* valConstrOut = getElementValueConstraint(encoder, (Element*) This, result);
- 					if(valConstrOut == NULL)
 -					Edge valConstrIn1 = getElementValueConstraint(encoder, elem1->element, elem1->encodingArray[i]);
 -					Edge valConstrIn2 = getElementValueConstraint(encoder, elem2->element, elem2->encodingArray[j]);
++					Edge valConstrIn1 = getElementValueConstraint(encoder, elemEnc1->element, elemEnc1->encodingArray[i]);
++					Edge valConstrIn2 = getElementValueConstraint(encoder, elemEnc2->element, elemEnc2->encodingArray[j]);
+ 					Edge valConstrOut = getElementValueConstraint(encoder, (Element*) This, result);
+ 					if(edgeIsNull(valConstrOut))
  						continue; //FIXME:Should talk to brian about it!
- 					Constraint* OpConstraint = allocConstraint(IMPLIES, 
- 						allocConstraint(AND, valConstrIn1, valConstrIn2) , valConstrOut);
+ 					Edge OpConstraint = constraintIMPLIES(encoder->cnf, constraintAND2(encoder->cnf, valConstrIn1, valConstrIn2), valConstrOut);
  					switch( ((FunctionOperator*)This->function)->overflowbehavior ){
  						case IGNORE:
  							if(isInRange){
@@@ -506,15 -458,10 +466,15 @@@
  			}
  		}
  	}
- 	Constraint* result = allocArrayConstraint(OR, size, carray);
- 	if(elemc1 != NULL)
- 		result = allocConstraint(AND, result, elemc1);
- 	if(elemc2 != NULL)
- 		result = allocConstraint(AND, result, elemc2);
 -	return constraintAND(encoder->cnf, size, carray);
++	Edge result = constraintAND(encoder->cnf, size, carray); 
++	if (!edgeIsNull(elemc1))
++		result = constraintAND2(encoder->cnf, result, elemc1);
++	if (!edgeIsNull(elemc2))
++		result = constraintAND2(encoder->cnf, result, elemc2);
 +	return result;
  }
  
- Constraint* encodeEnumTableElemFunctionSATEncoder(SATEncoder* encoder, ElementFunction* This){
+ Edge encodeEnumTableElemFunctionSATEncoder(SATEncoder* encoder, ElementFunction* This){
  	ASSERT(GETFUNCTIONTYPE(This->function)==TABLEFUNC);
  	ArrayElement* elements= &This->inputs;
  	Table* table = ((FunctionTable*) (This->function))->table;
diff --cc src/csolver.c
index 3e18833,d903044..8c4f22e
--- a/src/csolver.c
+++ b/src/csolver.c
@@@ -175,13 -175,8 +175,12 @@@ void startEncoding(CSolver* solver)
  	naiveEncodingDecision(solver);
  	SATEncoder* satEncoder = allocSATEncoder();
  	encodeAllSATEncoder(solver, satEncoder);
- 	finishedClauses(satEncoder->satSolver);
- 	int result= solve(satEncoder->satSolver);
- 	model_print("sat_solver's result:%d\tsolutionSize=%d\n", result, satEncoder->satSolver->solutionsize);
- 	for(uint i=1; i<=satEncoder->satSolver->solutionsize; i++){
- 		model_print("%d, ", satEncoder->satSolver->solution[i]);
+ 	int result= solveCNF(satEncoder->cnf);
 -	model_print("sat_solver's result:%d\n", result);
++	model_print("sat_solver's result:%d\tsolutionSize=%d\n", result, satEncoder->cnf->solver->solutionsize);
++	for(uint i=1; i<=satEncoder->cnf->solver->solutionsize; i++){
++		model_print("%d, ", satEncoder->cnf->solver->solution[i]);
 +	}
 +	model_print("\n");
  	//For now, let's just delete it, and in future for doing queries 
  	//we may need it.
  	deleteSATEncoder(satEncoder);