AndClauseLinkedList.c

#include "ADNF.h"
#include <stdlib.h>
#include <stdio.h>

void InitAndClauseLinkedList(ADNFClause *dnf)
{
	*dnf = malloc(sizeof(AAndClause));
	(*dnf) -> next=0;
	(*dnf) -> prev=0;
}

AAndClause * RemoveClause(AAndClause *a)
{
  AAndClause *prev = a->prev;
	prev->next= a->next;
	
	if (a->next)
		a->next->prev= prev;
	
	free(a);
	return prev;
}


AAndClause * AddClauseNoQuestionsAsked(AAndClause *prev, ASet clause)
{
	AAndClause *next= prev->next;
	
	prev->next= malloc(sizeof(AAndClause));	//from this point on, prev->next is the CURRENT RECORD
	
	prev->next->set= clause;			//COPY THE SET, This may change if we ever go beyond 8x8
	
	prev->next->prev= prev;
	prev->next->next= next;
	
	return prev->next;
}

int AddClause(ADNFClause dnf, ASet clause) //returns address if really added
{
	int i;
	AAndClause *cur= dnf;
	ASet allAtomsIntersection;

	if (SET_ISFALSE(clause))	//Not adding ( a AND NOT(a) )
		return 0;
	

	while (cur->next)
	{
		cur=cur->next;


		switch (Contains( &(cur->set), &clause) )// The one in the chain is preferred if they are equal
		{
		case 1:	//The one in the chain contains the one to be added ( Is more specific)
//				printf("head %d head->prev->next %d\n", head, head->prev->next);
							
			cur= RemoveClause(cur);
			break;
			
		case -1:	//The one to be added contains (is more specific than) the one already in the chain
			#ifdef LOG_LINKEDLIST
			printf("Clause %d>%d already there in wire %d at stack entry %d\n", clause, cur->set, w, cur->inQueue);
			#endif
			break;
				
		case 0: //Nothing to see here
			allAtomsIntersection= SET_INTERSECTION( SET_ALL_ATOMS(cur->set), SET_ALL_ATOMS(clause) );
		
			for (i=0; i<ASET_SIZE_HALF; i++)
			{
				if (SET_MEMBER(allAtomsIntersection, i) )	//looking for a and ~a
				{
					if ( LOGIC_NORMALIZE(SET_MEMBER(cur->set, i)) != LOGIC_NORMALIZE(SET_MEMBER(clause, i)) ) //one of them has a and the other ~a
					{
						ASet f1, f2;
						if ( SET_MEMBER(clause, i))
						{
							f1=clause;
							f2=cur->set;
						}
						else
						{
							f2= clause;
							f1= cur->set;
						}
						// f1 has a and f2 has ~a
						SET_REMOVE(f2, SET_INDEX_NEGATE(i));
						SET_REMOVE(f1, i);
					
						//Now neither has either!!
						
						if (f1==f2)
						{
							RemoveClause(cur);
							clause= f1;
							cur= dnf;
							break;	//break out of the for loop.
						}
						else
						{
							int fa=	//1 if it is of form fa + ff'~a, -1 if f~a + ff'a, 0 if neither
								SET_CONTAINS(f2,f1);
							
							if (fa==1)	//fa+ ff'~a = fa + ff'a. f1=f, f2=ff'
							{
								//if fa is in the chain, we need not touch it! Just simplify ff'~a to ff'
								if ( SET_MEMBER(cur->set, i))
									clause= f2;

								else // if ff'~a is in the chain, we have to delete it and insert ff' in again. Then fa will be added back. (Is it necessary?)
								{
									RemoveClause(cur);
									AddClause(dnf, f2);
								}
								
								cur= dnf;// Restart the outer while loop
								break; //from the for loop
		
							}
							else if (fa==-1)//ff'a + f~a= ff' + f~a. f1=ff', f2=f
							{
								//if f~a is in the chain, we need not touch it. Just simplify ff'a to ff'
								if (SET_MEMBER(cur->set, SET_INDEX_NEGATE(i)) )
									clause= f1;
								else // if ff'a is in the chain, we delete it and insert ff' in again. Then f~a will be added again.
								{
									RemoveClause(cur);
									AddClause(dnf, f1);
								}
								
								cur= dnf;
								break;
							}
						}//end if
					
					}//end if
				}//end if
			}//end for

		}//end switch

		
		
		
	}
	
	return AddClauseNoQuestionsAsked(cur, clause);
}


AAndClause * Last(ADNFClause head)
{
	for (; head->next; head= head->next);
	
	return head;
}

int DNFSize(ADNFClause dnf)
{
	int i=0;
	for (dnf=dnf->next; dnf; dnf=dnf->next)
		i++;
		
	return i;
}

void PrintDNFClause(ADNFClause dnf)
{
	AAndClause *andClause= dnf;
	while (andClause->next)
	{
		andClause = andClause->next;
		
		PrintSet_IncNeg(andClause->set);
		 
	}
	printf("\n");
}

void ClearDNFClause(ADNFClause dnf)
{
	ADNFClause next, cur= dnf->next;

	dnf->next=0;
	
	for (; cur; cur=next)
	{
		next= cur->next;
		free(cur);
	}
}

void QuickSort(ASet *a, int size)
{
	int p, barrier;
	ASet t;
	
	if (size<=1)
		return;
//partition		
	p=0;
	
	for (barrier=1; barrier<size; barrier++)
	{
		if (a[barrier]>= a[p])
			continue; //it is where it should be!
			
		//if it should be on the other side:
		t= a[barrier];
		a[barrier]= a[p+1];
		a[p+1]= a[p];
		a[p]= t;
		p++;
	}
//recursion
	
	QuickSort(a, p);
	QuickSort(a+p+1, size-p-1);
}

ASet* BinSearch(ASet v, ASet *a, int size)
{
	if (size==0)
		return 0;
	else if (v < a[size/2])
		return BinSearch( v, a, size/2);
	else if (v > a[size/2])
		return BinSearch( v, a+ size/2+1, size - size/2 -1);
	else
		return a + size/2;

}

void AddDontCare(ADNFClause dst, ADNFClause src)
{
  int dontCaresSize= DNFSize(src);
  ASet * dontCares= malloc(dontCaresSize);
  AAndClause *curDontCare;
  
  dontCaresSize=0;
  for (src=src->next; src; src= src->next)
  {
  	curDontCare= AddClause(dst, src->set); //add the and clause and keep a record of it
  	
//  	if (curDontCare && curDontCare->set== src->set) //if it is really added and not yet proven useful
  	//if the set is different than what was originally added, means it has simplified.
//  	{
 		dontCares[dontCaresSize]= src->set;
 		dontCaresSize++;
//  	}
  }
  
  QuickSort(dontCares, dontCaresSize);
  
  //Delete the ones who didn't make a difference
  for (dst= dst->next; dst; dst=dst->next)
  	if (BinSearch(dst->set, dontCares, dontCaresSize))
  		dst = RemoveClause(dst);	//go back to prev
}