[splint.git] / src / constraintResolve.c

/*
*
** constraintResolve.c
*/

//#define DEBUGPRINT 1

# include <ctype.h> /* for isdigit */
# include "lclintMacros.nf"
# include "basic.h"
# include "cgrammar.h"
# include "cgrammar_tokens.h"

# include "exprChecks.h"
# include "aliasChecks.h"
# include "exprNodeSList.h"
//# include "exprData.i"

#include "constraintExpr.h"


constraintList reflectChanges (constraintList pre2, constraintList post1);
constraint substitute (constraint c, constraintList p);
constraint constraint_searchandreplace (constraint c, constraintExpr old, constraintExpr new);
bool rangeCheck (arithType ar1, constraintExpr expr1, arithType ar2, constraintExpr expr2);
bool satifies (constraint pre, constraint post);
bool resolve (constraint c, constraintList p);
constraintList reflectChangesEnsures (constraintList pre2, constraintList post1);
constraint constraint_simplify (constraint c);

constraintList constraintList_fixConflicts (constraintList list1, constraintList list2);

constraintList constraintList_subsumeEnsures (constraintList list1, constraintList list2);

constraintList constraintList_mergeEnsures (constraintList list1, constraintList list2);
constraint  inequalitySubstitute  (constraint c, constraintList p);

/*********************************************/

					    
constraintList constraintList_mergeEnsures (constraintList list1, constraintList list2)
{
  constraintList ret;
  constraintList temp;
  ret = constraintList_new();
  
  ret = reflectChangesEnsures (list1, list2);
  ret = constraintList_fixConflicts (ret, list2);
  ret = constraintList_subsumeEnsures (ret, list2);
  list2 = constraintList_subsumeEnsures (list2, ret);
  temp = constraintList_copy(list2);

  temp = constraintList_addList (temp, ret);
  return temp;
  //ret = constraintList_addList (ret, list2);
  //return ret;
}

					    
/* constraintList constraintList_resolveRequires (constraintList requires, constraintList ensures) */
/* { */
  
/*   constraintList ret; */
/*   constraintList temp; */
/*   ret = constraintList_new(); */
  
/*   ret = reflectChangesEnsures (list1, list2); */
/*   ret = constraintList_fixConflicts (ret, list2); */
/*   ret = constraintList_subsumeEnsures (ret, list2); */
/*   list2 = constraintList_subsumeEnsures (list2, ret); */
/*   temp = constraintList_copy(list2); */

/*   temp = constraintList_addList (temp, ret); */
/*   return temp; */
/*   //ret = constraintList_addList (ret, list2); */
/*   //return ret; */
/* } */


constraintList checkCall (exprNode fcn, exprNodeList arglist)
{
  constraintList preconditions;
  uentry temp;
  DPRINTF ( (message ("Got call that %s ( %s) ",  exprNode_unparse(fcn),   exprNodeList_unparse (arglist ) ) ) );

  temp = exprNode_getUentry (fcn);

  preconditions = uentry_getFcnPreconditions (temp);

  if (preconditions)
    {
      preconditions = constraintList_copy(preconditions);
      preconditions = constraintList_doSRefFixBaseParam (preconditions, arglist);
    }
  else
    {
      preconditions = constraintList_new();
    }
  
  return preconditions;
}

void mergeResolve (exprNode parent, exprNode child1, exprNode child2)
{
  constraintList temp;

  DPRINTF( (message ("magically merging constraint into parent:%s for", exprNode_unparse (parent) )));

  DPRINTF( (message (" children:  %s and %s", exprNode_unparse (child1), exprNode_unparse(child2) ) ) );

  if (exprNode_isError (child1)  || exprNode_isError(child2) )
     {
       if (exprNode_isError (child1) && !exprNode_isError(child2) )
	 {
	   parent->requiresConstraints = constraintList_copy (child2->requiresConstraints);
	   parent->ensuresConstraints = constraintList_copy (child2->ensuresConstraints);
	   DPRINTF((message ("Copied child constraints: pre: %s and post: %s",
			     constraintList_print( child2->requiresConstraints),
			     constraintList_print (child2->ensuresConstraints)
			     )
		    ));
	   return;
	 }
       else
	 {
	   llassert(exprNode_isError(child2) );
	   parent->requiresConstraints = constraintList_new();
	   parent->ensuresConstraints = constraintList_new();
	   return;
	 }
     }

   llassert(!exprNode_isError (child1)  && ! exprNode_isError(child2) );
   
  DPRINTF( (message ("Child constraints are %s %s and %s %s",
		     constraintList_print (child1->requiresConstraints),
		     constraintList_print (child1->ensuresConstraints),
		     constraintList_print (child2->requiresConstraints),
		     constraintList_print (child2->ensuresConstraints)
		     ) ) );
 
  parent->requiresConstraints = constraintList_new();
  parent->ensuresConstraints = constraintList_new();

  parent->requiresConstraints = constraintList_copy (child1->requiresConstraints);
  
  temp = reflectChanges (child2->requiresConstraints, child1->ensuresConstraints);
  parent->requiresConstraints = constraintList_addList (parent->requiresConstraints, temp);

  parent->ensuresConstraints = constraintList_mergeEnsures(child1->ensuresConstraints,
							   child2->ensuresConstraints);
  
  DPRINTF( (message ("Parent constraints are %s and %s ",
		     constraintList_print (parent->requiresConstraints),
		     constraintList_print (parent->ensuresConstraints)
		     ) ) );
 
}


constraintList constraintList_subsumeEnsures (constraintList list1, constraintList list2)
{
  constraintList ret;
  ret = constraintList_new();
  constraintList_elements (list1, el)
    {
      
      DPRINTF ((message ("Examining %s", constraint_print (el) ) ) );
      if (!resolve (el, list2) )
	{
	    ret = constraintList_add (ret, el);
	}
      else
	{
	  DPRINTF ( (message ("Subsuming %s", constraint_print (el) ) ) );
	}
    } end_constraintList_elements;

    return ret;
}


constraintList reflectChanges (constraintList pre2, constraintList post1)
{
  
  constraintList ret;
  constraint temp;
  ret = constraintList_new();
  constraintList_elements (pre2, el)
    {
      if (!resolve (el, post1) )
	{
	  temp = substitute (el, post1);
	  if (!resolve (temp, post1) )
	    {
	      // try inequality substitution
	      constraint temp2;
	      
	      // the inequality substitution may cause us to lose information
	      //so we don't want to store the result but we do it anyway
	      temp2 = constraint_copy (temp);
	      temp2 = inequalitySubstitute (temp, post1);
	      if (!resolve (temp2, post1) )
		  ret = constraintList_add (ret, temp2);
	    }
	}
    } end_constraintList_elements;

    return ret;
}


constraintList reflectChangesEnsures (constraintList pre2, constraintList post1)
{  
  constraintList ret;
  constraint temp;
  ret = constraintList_new();
  constraintList_elements (pre2, el)
    {
      if (!resolve (el, post1) )
	{
	  temp = substitute (el, post1);
	  llassert (temp != NULL);

	  if (!resolve (temp, post1) )
	    ret = constraintList_add (ret, temp);
	}
      else
	{
	  DPRINTF ( (message ("Resolved away %s ", constraint_print(el) ) ) );
	}
    } end_constraintList_elements;

    return ret;
}


bool constraint_conflict (constraint c1, constraint c2)
{
  
  if (constraintExpr_similar(c1->lexpr, c2->lexpr) )
    {
      if (c1->ar == EQ)
	if (c1->ar == c2->ar)
	  {
	    DPRINTF ( (message ("%s conflicts with %s ", constraint_print (c1), constraint_print(c2) ) ) );
	    return TRUE;
	  }
    }  

  DPRINTF ( (message ("%s doesn't conflict with %s ", constraint_print (c1), constraint_print(c2) ) ) );

  return FALSE; 

}

void constraint_fixConflict (constraint good, constraint conflicting)
{
  constraint temp;
  if (conflicting->ar ==EQ )
    {
      good->expr = constraintExpr_searchandreplace (good->expr, conflicting->lexpr, conflicting->expr);
      temp = constraint_simplify (good);
      constraint_overWrite (good, temp);
    }


}

bool conflict (constraint c, constraintList list)
{
  
   constraintList_elements (list, el)
    {
      if ( constraint_conflict(el, c) )
	{
	  constraint_fixConflict (el, c);
	  return TRUE;
	}
    } end_constraintList_elements;

    return FALSE;
  

}

//check if constraint in list1 and conflict with constraints in List2.  If so we
//remove form list1 and (optionally) change list2.
constraintList constraintList_fixConflicts (constraintList list1, constraintList list2)
{
  constraintList ret;
  ret = constraintList_new();
  constraintList_elements (list1, el)
    {
      if (! conflict (el, list2) )
	{
	    ret = constraintList_add (ret, el);
	}
    } end_constraintList_elements;

    return ret;
  
    
}

bool resolve (constraint c, constraintList p)
{
  constraintList_elements (p, el)
    {
      if ( satifies (c, el) )
	{
	  DPRINTF ( (message ("\n%s Satifies %s\n ", constraint_print(el), constraint_print(c) ) ) );
	  return TRUE;
	}
    }
  end_constraintList_elements;
  DPRINTF ( (message ("no constraints satify %s", constraint_print(c) ) ));
  return FALSE;
}


/*returns true if cosntraint post satifies cosntriant pre */
bool satifies (constraint pre, constraint post)
{
  if (!constraintExpr_similar (pre->lexpr, post->lexpr) )
    {
      return FALSE;
    }
  if (post->expr == NULL)
    {
      llassert(FALSE);
      return FALSE;
    }

  return rangeCheck (pre->ar, pre->expr, post->ar, post->expr);
}

bool arithType_canResolve (arithType ar1, arithType ar2)
{
  switch (ar1)
    {
    case GTE:
    case GT:
      if ( (ar2 == GT) || (ar2 == GTE) || (ar2 == EQ) )
	{
	  return TRUE;
	}
      break;

    case EQ:
      if (ar2 == EQ)
	return TRUE;
      break;

    case LT:
    case LTE:
      //      llassert(FALSE); 
      if ( (ar2 == LT) || (ar2 == LTE) || (ar2 == EQ) )
	return TRUE;
    }
  return FALSE;	  
}

bool rangeCheck (arithType ar1, constraintExpr expr1, arithType ar2, constraintExpr expr2)

{
  DPRINTF ((message ("Doing Range CHECK %s and %s", constraintExpr_unparse(expr1), constraintExpr_unparse(expr2) ) ));

  if (! arithType_canResolve (ar1, ar2) )
    return FALSE;
  
  switch (ar1)
 {
 case GTE:
 case GT:
   if (!  (constraintExpr_canGetValue (expr1) &&
	   constraintExpr_canGetValue (expr2) ) )
     {
       DPRINTF( ("Can't Get value"));
       return FALSE;
     }
   
   if (constraintExpr_compare (expr2, expr1) >= 0)
     return TRUE;
  
  return FALSE;
 case EQ:
   if (constraintExpr_similar (expr1, expr2) )
	 return TRUE;
   
   return FALSE;
   
 default:
   DPRINTF(("case not handled"));
 }
  return FALSE;
}


constraint constraint_searchandreplace (constraint c, constraintExpr old, constraintExpr new)
{
  DPRINTF (("Doing replace for lexpr") );
  c->lexpr = constraintExpr_searchandreplace (c->lexpr, old, new);
  DPRINTF (("Doing replace for expr") );
  c->expr = constraintExpr_searchandreplace (c->expr, old, new);
  return c;
}

bool constraint_search (constraint c, constraintExpr old)
{
  bool ret;
  ret = FALSE;

  ret  = constraintExpr_search (c->lexpr, old);
  ret = ret || constraintExpr_search (c->expr, old);
  return ret;
}

//adjust file locs and stuff
constraint constraint_adjust (constraint substitute, constraint old)
{
  fileloc loc1, loc2, loc3;

  DPRINTF ( (message("Start adjust on %s and %s", constraint_print(substitute),
		     constraint_print(old))
		   ));

  loc1 = constraint_getFileloc (old);

  loc2 = constraintExpr_getFileloc (substitute->lexpr);

  loc3 = constraintExpr_getFileloc (substitute->expr);

  
  // special case of an equality that "contains itself"
  if (constraintExpr_search (substitute->expr, substitute->lexpr) )
      if (fileloc_closer (loc1, loc3, loc2))
      {
	constraintExpr temp;
	DPRINTF ( (message("Doing adjust on %s", constraint_print(substitute) )
		   ));
	temp = substitute->lexpr;
	substitute->lexpr = substitute->expr;
	substitute->expr  = temp;
	substitute = constraint_simplify(substitute);
      }

  return substitute;
  
}

constraint  inequalitySubstitute  (constraint c, constraintList p)
{
  if (c->ar != GTE)
    return c;
  
  constraintList_elements (p, el)
    {
       if ( el->ar == LT)
	 //	 if (!constraint_conflict (c, el) )
	   {
	     constraint temp;
	     temp = constraint_copy(el);
	     
	     //	     temp = constraint_adjust(temp, c);

	     if (constraintExpr_same (el->lexpr, c->expr) )
	       {
		 DPRINTF((message ("Replacing %s in %s with  %s",
				   constraintExpr_print (c->expr),
				   constraint_print (c),
				   constraintExpr_print (el->expr) )
			  ));
		 c->expr = constraintExpr_copy (el->expr);
	       }
	     
	   }
    }
  end_constraintList_elements;

  c = constraint_simplify(c);
  return c;
}

constraint substitute (constraint c, constraintList p)
{
  constraintList_elements (p, el)
    {
       if ( el->ar == EQ)
	 if (!constraint_conflict (c, el) )

	   {
	     constraint temp;
	     temp = constraint_copy(el);
	     
	     temp = constraint_adjust(temp, c);

	     DPRINTF((message ("Substituting %s for %s",
			       constraint_print (temp), constraint_print (c)
			       ) ) );
			       
	  
	     c = constraint_searchandreplace (c, temp->lexpr, temp->expr);
	   }
    }
  end_constraintList_elements;

  c = constraint_simplify(c);
  return c;
}


constraint constraint_solve (constraint c)
{
  DPRINTF( (message ("Solving %s\n", constraint_print(c) ) ) );
  c->expr = constraintExpr_solveBinaryExpr (c->lexpr, c->expr);
  DPRINTF( (message ("Solved and got %s\n", constraint_print(c) ) ) );

  return c;
}


constraint constraint_simplify (constraint c)
{
  c->lexpr = constraintExpr_simplify (c->lexpr);
  c->expr  = constraintExpr_simplify (c->expr);
  
  c = constraint_solve (c);
  
  c->lexpr = constraintExpr_simplify (c->lexpr);
  c->expr  = constraintExpr_simplify (c->expr);
  
  return c;
}


/* returns true  if fileloc for term1 is closer to file for term2 than term3*/

bool fileloc_closer (fileloc  loc1, fileloc  loc2, fileloc  loc3)
{
   if ( fileloc_lessthan (loc1, loc2) )
     {
       if (fileloc_lessthan (loc2, loc3) )
	 {
	   llassert (fileloc_lessthan (loc1, loc3) );
	   return TRUE;
	 }
       else
	 {
	   return FALSE;
	 }
     }

   if ( !fileloc_lessthan (loc1, loc2) )
     {
       if (!fileloc_lessthan (loc2, loc3) )
	 {
	   llassert (!fileloc_lessthan (loc1, loc3) );
	   return TRUE;
	 }
       else
	 {
	   return FALSE;
	 }
     }

   llassert(FALSE);
   return FALSE;
}
Commit	Line	Data
361091cc	1	/*
754746a0	2	*
361091cc	3	** constraintResolve.c
	4	*/
	5
f5ac53de	6	//#define DEBUGPRINT 1
f5ac53de	7
361091cc	8	# include <ctype.h> /* for isdigit */
	9	# include "lclintMacros.nf"
	10	# include "basic.h"
	11	# include "cgrammar.h"
	12	# include "cgrammar_tokens.h"
	13
	14	# include "exprChecks.h"
	15	# include "aliasChecks.h"
	16	# include "exprNodeSList.h"
93307a76	17	//# include "exprData.i"
361091cc	18
92c4a786	19	#include "constraintExpr.h"
361091cc	20
f5ac53de	21
f5ac53de	22
92c4a786	23	constraintList reflectChanges (constraintList pre2, constraintList post1);
	24	constraint substitute (constraint c, constraintList p);
	25	constraint constraint_searchandreplace (constraint c, constraintExpr old, constraintExpr new);
	26	bool rangeCheck (arithType ar1, constraintExpr expr1, arithType ar2, constraintExpr expr2);
	27	bool satifies (constraint pre, constraint post);
	28	bool resolve (constraint c, constraintList p);
	29	constraintList reflectChangesEnsures (constraintList pre2, constraintList post1);
	30	constraint constraint_simplify (constraint c);
361091cc	31
754746a0	32	constraintList constraintList_fixConflicts (constraintList list1, constraintList list2);
	33
	34	constraintList constraintList_subsumeEnsures (constraintList list1, constraintList list2);
	35
	36	constraintList constraintList_mergeEnsures (constraintList list1, constraintList list2);
f5ac53de	37	constraint inequalitySubstitute (constraint c, constraintList p);
754746a0	38
	39	/*********************************************/
	40
	41
	42	constraintList constraintList_mergeEnsures (constraintList list1, constraintList list2)
	43	{
	44	constraintList ret;
	45	constraintList temp;
	46	ret = constraintList_new();
	47
	48	ret = reflectChangesEnsures (list1, list2);
	49	ret = constraintList_fixConflicts (ret, list2);
	50	ret = constraintList_subsumeEnsures (ret, list2);
	51	list2 = constraintList_subsumeEnsures (list2, ret);
	52	temp = constraintList_copy(list2);
	53
	54	temp = constraintList_addList (temp, ret);
	55	return temp;
	56	//ret = constraintList_addList (ret, list2);
	57	//return ret;
	58	}
	59
34f0c5e7	60
	61	/* constraintList constraintList_resolveRequires (constraintList requires, constraintList ensures) */
	62	/* { */
	63
	64	/* constraintList ret; */
	65	/* constraintList temp; */
	66	/* ret = constraintList_new(); */
	67
	68	/* ret = reflectChangesEnsures (list1, list2); */
	69	/* ret = constraintList_fixConflicts (ret, list2); */
	70	/* ret = constraintList_subsumeEnsures (ret, list2); */
	71	/* list2 = constraintList_subsumeEnsures (list2, ret); */
	72	/* temp = constraintList_copy(list2); */
	73
	74	/* temp = constraintList_addList (temp, ret); */
	75	/* return temp; */
	76	/* //ret = constraintList_addList (ret, list2); */
	77	/* //return ret; */
	78	/* } */
	79
	80
93307a76	81	constraintList checkCall (exprNode fcn, exprNodeList arglist)
	82	{
	83	constraintList preconditions;
	84	uentry temp;
	85	DPRINTF ( (message ("Got call that %s ( %s) ", exprNode_unparse(fcn), exprNodeList_unparse (arglist ) ) ) );
	86
	87	temp = exprNode_getUentry (fcn);
	88
	89	preconditions = uentry_getFcnPreconditions (temp);
	90
	91	if (preconditions)
	92	{
	93	preconditions = constraintList_copy(preconditions);
	94	preconditions = constraintList_doSRefFixBaseParam (preconditions, arglist);
	95	}
	96	else
	97	{
	98	preconditions = constraintList_new();
	99	}
	100
	101	return preconditions;
	102	}
	103
92c4a786	104	void mergeResolve (exprNode parent, exprNode child1, exprNode child2)
361091cc	105	{
92c4a786	106	constraintList temp;
754746a0	107
93307a76	108	DPRINTF( (message ("magically merging constraint into parent:%s for", exprNode_unparse (parent) )));
754746a0	109
93307a76	110	DPRINTF( (message (" children: %s and %s", exprNode_unparse (child1), exprNode_unparse(child2) ) ) );
754746a0	111
754746a0	112	if (exprNode_isError (child1) \|\| exprNode_isError(child2) )
92c4a786	113	{
	114	if (exprNode_isError (child1) && !exprNode_isError(child2) )
	115	{
	116	parent->requiresConstraints = constraintList_copy (child2->requiresConstraints);
	117	parent->ensuresConstraints = constraintList_copy (child2->ensuresConstraints);
93307a76	118	DPRINTF((message ("Copied child constraints: pre: %s and post: %s",
92c4a786	119	constraintList_print( child2->requiresConstraints),
	120	constraintList_print (child2->ensuresConstraints)
	121	)
	122	));
	123	return;
	124	}
	125	else
	126	{
	127	llassert(exprNode_isError(child2) );
	128	parent->requiresConstraints = constraintList_new();
	129	parent->ensuresConstraints = constraintList_new();
	130	return;
	131	}
	132	}
361091cc	133
92c4a786	134	llassert(!exprNode_isError (child1) && ! exprNode_isError(child2) );
92c4a786	135
93307a76	136	DPRINTF( (message ("Child constraints are %s %s and %s %s",
92c4a786	137	constraintList_print (child1->requiresConstraints),
	138	constraintList_print (child1->ensuresConstraints),
	139	constraintList_print (child2->requiresConstraints),
	140	constraintList_print (child2->ensuresConstraints)
	141	) ) );
	142
	143	parent->requiresConstraints = constraintList_new();
	144	parent->ensuresConstraints = constraintList_new();
361091cc	145
92c4a786	146	parent->requiresConstraints = constraintList_copy (child1->requiresConstraints);
	147
	148	temp = reflectChanges (child2->requiresConstraints, child1->ensuresConstraints);
	149	parent->requiresConstraints = constraintList_addList (parent->requiresConstraints, temp);
361091cc	150
754746a0	151	parent->ensuresConstraints = constraintList_mergeEnsures(child1->ensuresConstraints,
754746a0	152	child2->ensuresConstraints);
92c4a786	153
93307a76	154	DPRINTF( (message ("Parent constraints are %s and %s ",
92c4a786	155	constraintList_print (parent->requiresConstraints),
	156	constraintList_print (parent->ensuresConstraints)
	157	) ) );
	158
361091cc	159	}
361091cc	160
361091cc	161
92c4a786	162
754746a0	163
	164	constraintList constraintList_subsumeEnsures (constraintList list1, constraintList list2)
	165	{
	166	constraintList ret;
	167	ret = constraintList_new();
	168	constraintList_elements (list1, el)
	169	{
	170
93307a76	171	DPRINTF ((message ("Examining %s", constraint_print (el) ) ) );
754746a0	172	if (!resolve (el, list2) )
	173	{
	174	ret = constraintList_add (ret, el);
	175	}
	176	else
	177	{
93307a76	178	DPRINTF ( (message ("Subsuming %s", constraint_print (el) ) ) );
754746a0	179	}
	180	} end_constraintList_elements;
	181
	182	return ret;
	183	}
	184
	185
92c4a786	186	constraintList reflectChanges (constraintList pre2, constraintList post1)
	187	{
	188
	189	constraintList ret;
	190	constraint temp;
	191	ret = constraintList_new();
	192	constraintList_elements (pre2, el)
361091cc	193	{
92c4a786	194	if (!resolve (el, post1) )
	195	{
	196	temp = substitute (el, post1);
754746a0	197	if (!resolve (temp, post1) )
34f0c5e7	198	{
	199	// try inequality substitution
	200	constraint temp2;
	201
	202	// the inequality substitution may cause us to lose information
	203	//so we don't want to store the result but we do it anyway
	204	temp2 = constraint_copy (temp);
	205	temp2 = inequalitySubstitute (temp, post1);
	206	if (!resolve (temp2, post1) )
	207	ret = constraintList_add (ret, temp2);
	208	}
92c4a786	209	}
92c4a786	210	} end_constraintList_elements;
361091cc	211
92c4a786	212	return ret;
361091cc	213	}
361091cc	214
361091cc	215
361091cc	216
92c4a786	217	constraintList reflectChangesEnsures (constraintList pre2, constraintList post1)
	218	{
	219	constraintList ret;
	220	constraint temp;
	221	ret = constraintList_new();
	222	constraintList_elements (pre2, el)
361091cc	223	{
92c4a786	224	if (!resolve (el, post1) )
	225	{
	226	temp = substitute (el, post1);
754746a0	227	llassert (temp != NULL);
	228
	229	if (!resolve (temp, post1) )
92c4a786	230	ret = constraintList_add (ret, temp);
92c4a786	231	}
754746a0	232	else
754746a0	233	{
93307a76	234	DPRINTF ( (message ("Resolved away %s ", constraint_print(el) ) ) );
754746a0	235	}
92c4a786	236	} end_constraintList_elements;
bf92e32c	237
92c4a786	238	return ret;
361091cc	239	}
361091cc	240
92c4a786	241
92c4a786	242	bool constraint_conflict (constraint c1, constraint c2)
361091cc	243	{
361091cc	244
92c4a786	245	if (constraintExpr_similar(c1->lexpr, c2->lexpr) )
bf92e32c	246	{
754746a0	247	if (c1->ar == EQ)
	248	if (c1->ar == c2->ar)
	249	{
93307a76	250	DPRINTF ( (message ("%s conflicts with %s ", constraint_print (c1), constraint_print(c2) ) ) );
754746a0	251	return TRUE;
754746a0	252	}
92c4a786	253	}
bf92e32c	254
754746a0	255	DPRINTF ( (message ("%s doesn't conflict with %s ", constraint_print (c1), constraint_print(c2) ) ) );
361091cc	256
92c4a786	257	return FALSE;
361091cc	258
361091cc	259	}
361091cc	260
92c4a786	261	void constraint_fixConflict (constraint good, constraint conflicting)
361091cc	262	{
92c4a786	263	constraint temp;
92c4a786	264	if (conflicting->ar ==EQ )
361091cc	265	{
92c4a786	266	good->expr = constraintExpr_searchandreplace (good->expr, conflicting->lexpr, conflicting->expr);
	267	temp = constraint_simplify (good);
	268	constraint_overWrite (good, temp);
361091cc	269	}
361091cc	270
361091cc	271
361091cc	272	}
361091cc	273
92c4a786	274	bool conflict (constraint c, constraintList list)
361091cc	275	{
361091cc	276
92c4a786	277	constraintList_elements (list, el)
	278	{
	279	if ( constraint_conflict(el, c) )
	280	{
	281	constraint_fixConflict (el, c);
	282	return TRUE;
	283	}
	284	} end_constraintList_elements;
361091cc	285
92c4a786	286	return FALSE;
92c4a786	287
361091cc	288
361091cc	289	}
361091cc	290
92c4a786	291	//check if constraint in list1 and conflict with constraints in List2. If so we
	292	//remove form list1 and (optionally) change list2.
	293	constraintList constraintList_fixConflicts (constraintList list1, constraintList list2)
6364363c	294	{
92c4a786	295	constraintList ret;
	296	ret = constraintList_new();
	297	constraintList_elements (list1, el)
	298	{
	299	if (! conflict (el, list2) )
	300	{
	301	ret = constraintList_add (ret, el);
	302	}
	303	} end_constraintList_elements;
6364363c	304
92c4a786	305	return ret;
	306
	307
361091cc	308	}
	309
	310	bool resolve (constraint c, constraintList p)
	311	{
	312	constraintList_elements (p, el)
	313	{
	314	if ( satifies (c, el) )
	315	{
93307a76	316	DPRINTF ( (message ("\n%s Satifies %s\n ", constraint_print(el), constraint_print(c) ) ) );
361091cc	317	return TRUE;
	318	}
	319	}
	320	end_constraintList_elements;
754746a0	321	DPRINTF ( (message ("no constraints satify %s", constraint_print(c) ) ));
361091cc	322	return FALSE;
	323	}
	324
bf92e32c	325
92c4a786	326	/returns true if cosntraint post satifies cosntriant pre /
92c4a786	327	bool satifies (constraint pre, constraint post)
bf92e32c	328	{
92c4a786	329	if (!constraintExpr_similar (pre->lexpr, post->lexpr) )
bf92e32c	330	{
92c4a786	331	return FALSE;
	332	}
	333	if (post->expr == NULL)
	334	{
	335	llassert(FALSE);
	336	return FALSE;
bf92e32c	337	}
92c4a786	338
92c4a786	339	return rangeCheck (pre->ar, pre->expr, post->ar, post->expr);
bf92e32c	340	}
bf92e32c	341
754746a0	342	bool arithType_canResolve (arithType ar1, arithType ar2)
	343	{
	344	switch (ar1)
	345	{
	346	case GTE:
	347	case GT:
	348	if ( (ar2 == GT) \|\| (ar2 == GTE) \|\| (ar2 == EQ) )
	349	{
	350	return TRUE;
	351	}
	352	break;
	353
	354	case EQ:
	355	if (ar2 == EQ)
	356	return TRUE;
	357	break;
	358
	359	case LT:
	360	case LTE:
34f0c5e7	361	// llassert(FALSE);
754746a0	362	if ( (ar2 == LT) \|\| (ar2 == LTE) \|\| (ar2 == EQ) )
	363	return TRUE;
	364	}
	365	return FALSE;
	366	}
92c4a786	367
	368	bool rangeCheck (arithType ar1, constraintExpr expr1, arithType ar2, constraintExpr expr2)
	369
bf92e32c	370	{
754746a0	371	DPRINTF ((message ("Doing Range CHECK %s and %s", constraintExpr_unparse(expr1), constraintExpr_unparse(expr2) ) ));
	372
	373	if (! arithType_canResolve (ar1, ar2) )
	374	return FALSE;
	375
92c4a786	376	switch (ar1)
	377	{
	378	case GTE:
	379	case GT:
754746a0	380	if (! (constraintExpr_canGetValue (expr1) &&
	381	constraintExpr_canGetValue (expr2) ) )
	382	{
	383	DPRINTF( ("Can't Get value"));
	384	return FALSE;
	385	}
	386
	387	if (constraintExpr_compare (expr2, expr1) >= 0)
	388	return TRUE;
	389
	390	return FALSE;
	391	case EQ:
	392	if (constraintExpr_similar (expr1, expr2) )
	393	return TRUE;
	394
	395	return FALSE;
	396
92c4a786	397	default:
754746a0	398	DPRINTF(("case not handled"));
92c4a786	399	}
	400	return FALSE;
	401	}
bf92e32c	402
754746a0	403
92c4a786	404	constraint constraint_searchandreplace (constraint c, constraintExpr old, constraintExpr new)
92c4a786	405	{
754746a0	406	DPRINTF (("Doing replace for lexpr") );
92c4a786	407	c->lexpr = constraintExpr_searchandreplace (c->lexpr, old, new);
754746a0	408	DPRINTF (("Doing replace for expr") );
92c4a786	409	c->expr = constraintExpr_searchandreplace (c->expr, old, new);
92c4a786	410	return c;
bf92e32c	411	}
6364363c	412
754746a0	413	bool constraint_search (constraint c, constraintExpr old)
	414	{
	415	bool ret;
	416	ret = FALSE;
	417
	418	ret = constraintExpr_search (c->lexpr, old);
	419	ret = ret \|\| constraintExpr_search (c->expr, old);
	420	return ret;
	421	}
	422
34f0c5e7	423	//adjust file locs and stuff
92c4a786	424	constraint constraint_adjust (constraint substitute, constraint old)
bf92e32c	425	{
92c4a786	426	fileloc loc1, loc2, loc3;
6364363c	427
754746a0	428	DPRINTF ( (message("Start adjust on %s and %s", constraint_print(substitute),
	429	constraint_print(old))
	430	));
	431
92c4a786	432	loc1 = constraint_getFileloc (old);
6364363c	433
92c4a786	434	loc2 = constraintExpr_getFileloc (substitute->lexpr);
6364363c	435
92c4a786	436	loc3 = constraintExpr_getFileloc (substitute->expr);
6364363c	437
754746a0	438
	439	// special case of an equality that "contains itself"
	440	if (constraintExpr_search (substitute->expr, substitute->lexpr) )
	441	if (fileloc_closer (loc1, loc3, loc2))
6364363c	442	{
92c4a786	443	constraintExpr temp;
754746a0	444	DPRINTF ( (message("Doing adjust on %s", constraint_print(substitute) )
754746a0	445	));
92c4a786	446	temp = substitute->lexpr;
	447	substitute->lexpr = substitute->expr;
	448	substitute->expr = temp;
	449	substitute = constraint_simplify(substitute);
6364363c	450	}
6364363c	451
92c4a786	452	return substitute;
92c4a786	453
bf92e32c	454	}
bf92e32c	455
34f0c5e7	456	constraint inequalitySubstitute (constraint c, constraintList p)
	457	{
	458	if (c->ar != GTE)
	459	return c;
	460
	461	constraintList_elements (p, el)
	462	{
	463	if ( el->ar == LT)
	464	// if (!constraint_conflict (c, el) )
	465	{
	466	constraint temp;
	467	temp = constraint_copy(el);
	468
	469	// temp = constraint_adjust(temp, c);
	470
	471	if (constraintExpr_same (el->lexpr, c->expr) )
	472	{
	473	DPRINTF((message ("Replacing %s in %s with %s",
	474	constraintExpr_print (c->expr),
	475	constraint_print (c),
	476	constraintExpr_print (el->expr) )
	477	));
	478	c->expr = constraintExpr_copy (el->expr);
	479	}
	480
	481	}
	482	}
	483	end_constraintList_elements;
	484
	485	c = constraint_simplify(c);
	486	return c;
	487	}
	488
361091cc	489	constraint substitute (constraint c, constraintList p)
	490	{
	491	constraintList_elements (p, el)
	492	{
92c4a786	493	if ( el->ar == EQ)
	494	if (!constraint_conflict (c, el) )
	495
	496	{
92c4a786	497	constraint temp;
	498	temp = constraint_copy(el);
	499
	500	temp = constraint_adjust(temp, c);
754746a0	501
	502	DPRINTF((message ("Substituting %s for %s",
	503	constraint_print (temp), constraint_print (c)
	504	) ) );
	505
92c4a786	506
754746a0	507	c = constraint_searchandreplace (c, temp->lexpr, temp->expr);
92c4a786	508	}
361091cc	509	}
	510	end_constraintList_elements;
	511
	512	c = constraint_simplify(c);
	513	return c;
	514	}
	515
361091cc	516
92c4a786	517	constraint constraint_solve (constraint c)
6364363c	518	{
754746a0	519	DPRINTF( (message ("Solving %s\n", constraint_print(c) ) ) );
92c4a786	520	c->expr = constraintExpr_solveBinaryExpr (c->lexpr, c->expr);
754746a0	521	DPRINTF( (message ("Solved and got %s\n", constraint_print(c) ) ) );
361091cc	522
92c4a786	523	return c;
361091cc	524	}
361091cc	525
361091cc	526
92c4a786	527	constraint constraint_simplify (constraint c)
361091cc	528	{
92c4a786	529	c->lexpr = constraintExpr_simplify (c->lexpr);
92c4a786	530	c->expr = constraintExpr_simplify (c->expr);
361091cc	531
92c4a786	532	c = constraint_solve (c);
754746a0	533
92c4a786	534	c->lexpr = constraintExpr_simplify (c->lexpr);
92c4a786	535	c->expr = constraintExpr_simplify (c->expr);
754746a0	536
361091cc	537	return c;
	538	}
	539
	540
361091cc	541
361091cc	542
92c4a786	543	/* returns true if fileloc for term1 is closer to file for term2 than term3*/
	544
	545	bool fileloc_closer (fileloc loc1, fileloc loc2, fileloc loc3)
361091cc	546	{
92c4a786	547	if ( fileloc_lessthan (loc1, loc2) )
6364363c	548	{
92c4a786	549	if (fileloc_lessthan (loc2, loc3) )
6364363c	550	{
92c4a786	551	llassert (fileloc_lessthan (loc1, loc3) );
92c4a786	552	return TRUE;
6364363c	553	}
	554	else
	555	{
92c4a786	556	return FALSE;
6364363c	557	}
	558	}
	559
92c4a786	560	if ( !fileloc_lessthan (loc1, loc2) )
	561	{
	562	if (!fileloc_lessthan (loc2, loc3) )
	563	{
	564	llassert (!fileloc_lessthan (loc1, loc3) );
	565	return TRUE;
	566	}
	567	else
	568	{
	569	return FALSE;
	570	}
	571	}
361091cc	572
92c4a786	573	llassert(FALSE);
92c4a786	574	return FALSE;
361091cc	575	}
361091cc	576
754746a0	577