Fixing bugs + resolving conflicts

diff --cc src/Backend/inc_solver.c
Simple merge

diff --cc src/Backend/satencoder.c
index 02997405d4557fce498cf702d23e2633efaec631,0aa0df716cf4de7ffd10605bf0c6378cf51031c1..ad59903889b0bedfa2de8c8b8970dcea8ea51e7e
--- 1/src/Backend/satencoder.c
--- 2/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 3e18833fa709bfc4011224cdec4b520c919455ec,d90304431634c30faf0d4fbfad73dd81f6af2743..8c4f22e079a4a651d7806e46d72a4a807d792c93
--- 1/src/csolver.c
--- 2/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);