*** empty log message ***

diff --git a/src/Headers/constraint.h b/src/Headers/constraint.h
index 18785213012c313cc5b83435a2c8e8239d8013cc..12a52a6a55d7e9a4cdb66f797bba55bacccdf852 100644 (file)
--- a/src/Headers/constraint.h
+++ b/src/Headers/constraint.h
@@ -1,10 +1,20 @@
 typedef union constraintTermValue_
 {
+  constraintExpr constrExpr;
   exprNode expr;
   sRef     sref;
   int      intlit;
 } constraintTermValue;
 
+
+typedef enum
+{
+ EXPRNODE, SREF,
+ CONSTRAINTEXPR,
+ INTLITERAL
+} constraintTermType;
+
+
 typedef enum
 {
   LT, LTE, GT, GTE, EQ, NONNEGATIVE, POSITIVE
@@ -13,10 +23,10 @@ arithType;
 
 typedef enum
 {
- BUFFSIZE, STRINGLEN, VALUE, CALLSAFE,
+  //BUFFSIZE, STRINGLEN,
+ VALUE, CALLSAFE,
  MAXSET, MINSET, MAXREAD, MINREAD,
  NULLTERMINATED,
- INCOP,
  UNDEFINED
 }
 constraintType;
@@ -29,13 +39,6 @@ typedef enum
 constraintExprOp;
 
 
-typedef enum
-{
-EXPRNODE, SREF,
-INTLITERAL
-} constraintTermType;
-
-
 struct _constraintTerm {
   constraintType constrType;
   fileloc loc;
@@ -53,19 +56,18 @@ struct constraintExpr_ {
 };
 # define constraintExpr_undefined ((constraintExpr)NULL)
 
-typedef struct constraintExpr_ * constraintExpr;
-abst_typedef struct constr_ * constr;
+
+//abst_typedef struct constr_ * constr;
 
 
 struct _constraint {
+  constraint     orig;
   constraintExpr lexpr;
   arithType       ar;
   constraintExpr  expr;
   bool post;
 } ;
 
-#define max_constraints 100
-
 //constraint constraint_create (exprNode e1, exprNode e2,  arithType restriction, constraintType kind);
 
 constraint constraint_createReadSafe (exprNode p_e1, exprNode p_e2);

diff --git a/src/Headers/forwardTypes.h b/src/Headers/forwardTypes.h
index 4d1334754696650a2abe702a008583cbcca3dc75..5d575f5c8c3c848fd75df9ce209e5499bf2b424f 100644 (file)
--- a/src/Headers/forwardTypes.h
+++ b/src/Headers/forwardTypes.h
@@ -23,6 +23,9 @@ abst_typedef /*@null@*/ struct _environmentTable *environmentTable;
 
 abst_typedef /*@null@*/ struct _constraint *constraint;
 
+/* DRL modified 9 26 00 */
+
+abst_typedef struct constraintExpr_ * constraintExpr;
 
 /*@-cppnames@*/
 typedef int bool;

diff --git a/src/constraint.c b/src/constraint.c
index f6090836e3487ad148b6314ef69d3cb32822083e..4b7b5c244dbf80ca06e4611a415d40c5036b523b 100644 (file)
--- a/src/constraint.c
+++ b/src/constraint.c
@@ -26,10 +26,15 @@ constraint constraint_copy (constraint c)
 {
   constraint ret;
   ret = constraint_makeNew();
-  ret->lexpr = c->lexpr;
+  ret->lexpr = constraintExpr_copy (c->lexpr);
   ret->ar = c->ar;
-  ret->expr = c->expr;
+  ret->expr =  constraintExpr_copy (c->expr);
   ret->post = c->post;
+  /*@i33 fix this*/
+  if (c->orig != NULL)
+    ret->orig = constraint_copy (c->orig);
+  else
+    ret->orig = NULL;
   return ret;
 }
 
@@ -49,6 +54,7 @@ bool constraint_resolve (/*@unused@*/ constraint c)
   ret->expr = NULL;
   ret->ar = LT;
   ret->post = FALSE;
+  ret->orig = NULL;
   /*@i23*/return ret;
 }
 /*@-czechfcns@*/
@@ -76,7 +82,7 @@ constraintExpr constraintExpr_copy (constraintExpr expr)
     {
       ret->expr = NULL;
     }
-  
+  return ret;
 }
 
 constraintExpr constraintExpr_makeMaxSetExpr (exprNode expr)
@@ -227,8 +233,7 @@ constraintExpr makeMaxSetPostOpInc (exprNode e)
 {
   constraintExpr ret;
   ret = constraintExpr_makeValueExpr (e);
-  ret->term  = constraintTerm_makeMaxSetexpr (e);
-  ret->op = MINUS;
+  ret->op = PLUS;
   ret->expr =  makeConstraintExprIntlit (1);
   return ret;
 }
@@ -239,7 +244,7 @@ constraint constraint_makeMaxSetSideEffectPostIncrement (exprNode e, fileloc seq
   //constraintTerm term;
   exprNode t2;
   e = exprNode_fakeCopy(e);
-  ret->lexpr = constraintExpr_makeMaxSetExpr(e);
+  ret->lexpr = constraintExpr_makeValueExpr (e);
   ret->ar = EQ;
   ret->post = TRUE;
   ret->expr = makeMaxSetPostOpInc(e);
@@ -334,6 +339,22 @@ cstring constraintExpr_print (constraintExpr ex)
 }
 
 
+cstring  constraint_printDetailed (constraint c)
+{
+  cstring st = cstring_undefined;
+
+  if (!c->post)
+    {
+      
+    st = message ("Unresolved constraint:\nLclint is unable to resolve %s needed to satisy %s", constraint_print (c), constraint_print(c->orig) );
+    }
+  else
+    {
+    st = message ("Function Post condition:\nBased on the constraint %s this function appears to have the post condition %s", constraint_print (c), constraint_print(c->orig) );
+    }
+  return st;
+}
+
 cstring  constraint_print (constraint c)
 {
   cstring st = cstring_undefined;
@@ -356,6 +377,37 @@ cstring  constraint_print (constraint c)
   return st;
 }
 
+bool constraint_hasTerm (constraint c, constraintTerm term)
+{
+  DPRINTF((message ("Constraint %s", constraint_print (c) ) ) );
+  
+  if (constraintExpr_includesTerm (c->lexpr, term) )
+    return TRUE;
+
+  if (constraintExpr_includesTerm (c->expr, term) )
+    return TRUE;
+
+  return FALSE;
+}
+
+bool constraintExpr_includesTerm (constraintExpr expr, constraintTerm term)
+{
+  if (constraintTerm_hasTerm (expr->term, term) )
+    return TRUE;
+
+  if ( (expr->expr) != NULL)
+    {
+      return ( constraintExpr_includesTerm (expr->expr, term) );
+    }
+  return FALSE;
+
+}
+
+constraint constraint_preserveOrig (constraint c)
+{
+  c->orig = constraint_copy (c);
+  return c;
+}
 /*@=fcnuse*/
 /*@=assignexpose*/
 /*@=czechfcns@*/

diff --git a/src/constraintGeneration.c b/src/constraintGeneration.c
index e7f4f7b7e61c58e678ac0fb8f1d3ab2f711a4d70..ed0bbd7b17eab0053dd53ba74b6599d4ae995b2d 100644 (file)
--- a/src/constraintGeneration.c
+++ b/src/constraintGeneration.c
@@ -94,13 +94,14 @@ void /*@alt bool@*/ exprNode_generateConstraints (/*@temp@*/ exprNode e)
   
   if (exprNode_isMultiStatement ( e) )
     {
-      return  exprNode_multiStatement(e);
+      exprNode_multiStatement(e);
     }
   else
     {
       llassert(FALSE);
     }
-
+  printf ("%s", (message ("%s", constraintList_printDetailed (e->requiresConstraints) ) ) );
+  printf ("%s", (message ("%s", constraintList_printDetailed (e->ensuresConstraints) ) ) );
   return FALSE;
 }
 
@@ -178,9 +179,9 @@ bool exprNode_stmt (exprNode e)
   loc = exprNode_getNextSequencePoint(e); /* reduces to an expression */
   notError = exprNode_exprTraverse (snode, FALSE, FALSE, loc);
   e->requiresConstraints = exprNode_traversRequiresConstraints(snode);
-  printf ("%s\n", constraintList_print(e->requiresConstraints) );
+  // printf ("%s\n", constraintList_print(e->requiresConstraints) );
   e->ensuresConstraints  = exprNode_traversEnsuresConstraints(snode);
-  printf ("Ensures that:\n %s\n", constraintList_print(e->ensuresConstraints) );
+  // printf ("Ensures that:\n %s\n", constraintList_print(e->ensuresConstraints) );
   llassert(notError);
   return notError;
   
@@ -217,7 +218,7 @@ bool exprNode_stmtList  (exprNode e)
   exprNode_stmt (stmt2);
 
   mergeResolve (e, stmt1, stmt2 );
-  TPRINTF ( (message ("smtlist constraints are: pre: %s \n and \t post %s\n",
+  DPRINTF ( (message ("smtlist constraints are: pre: %s \n and \t post %s\n",
                      constraintList_print(e->requiresConstraints),
                      constraintList_print(e->ensuresConstraints) ) ) );
   return TRUE;
@@ -356,8 +357,8 @@ bool exprNode_exprTraverse (exprNode e, bool definatelv, bool definaterv,  filel
       e->requiresConstraints = constraintList_add(e->requiresConstraints, cons);
       cons = constraint_makeEnsureMaxReadAtLeast (t1, t2, sequencePoint);
       e->ensuresConstraints = constraintList_add(e->ensuresConstraints, cons);
-      cons = constraint_makeEnsureMinReadAtMost (t1, t2, sequencePoint);
-      e->ensuresConstraints = constraintList_add(e->ensuresConstraints, cons);
+      //      cons = constraint_makeEnsureMinReadAtMost (t1, t2, sequencePoint);
+      // e->ensuresConstraints = constraintList_add(e->ensuresConstraints, cons);
        
       exprNode_exprTraverse (exprData_getPairA (data), FALSE, TRUE, sequencePoint);
       exprNode_exprTraverse (exprData_getPairB (data), FALSE, TRUE, sequencePoint);
@@ -393,7 +394,7 @@ bool exprNode_exprTraverse (exprNode e, bool definatelv, bool definaterv,  filel
     case XPR_PARENS: 
       exprNode_exprTraverse (exprData_getUopNode (e->edata), definatelv, definaterv, sequencePoint);
       //    e->constraints = constraintList_exprNodemerge (exprData_getUopNode (e->edata), exprNode_undefined);
-      break;
+      break; 
     case XPR_ASSIGN:
       exprNode_exprTraverse (exprData_getOpA (data), TRUE, definaterv, sequencePoint ); 
       lltok_unparse (exprData_getOpTok (data));
@@ -455,18 +456,21 @@ bool exprNode_exprTraverse (exprNode e, bool definatelv, bool definaterv,  filel
       lltok_unparse (exprData_getUopTok (data));
       if (lltok_isInc_Op (exprData_getUopTok (data) ) )
        {
-         TPRINTF(("doing ++"));
+         DPRINTF(("doing ++"));
          t1 = exprData_getUopNode (data);
          cons = constraint_makeMaxSetSideEffectPostIncrement (t1, sequencePoint );
          e->ensuresConstraints = constraintList_add (e->ensuresConstraints, cons);
-         cons = constraint_makeMaxReadSideEffectPostIncrement (t1, sequencePoint );
-         e->ensuresConstraints = constraintList_add (e->ensuresConstraints, cons);
+         //      cons = constraint_makeMaxReadSideEffectPostIncrement (t1, sequencePoint );
+         //e->ensuresConstraints = constraintList_add (e->ensuresConstraints, cons);
        }
       break;
     default:
       handledExprNode = FALSE;
     }
 
+  e->requiresConstraints =  constraintList_preserveOrig ( e->requiresConstraints);
+  e->ensuresConstraints  =  constraintList_preserveOrig ( e->ensuresConstraints);
+  
   return handledExprNode; 
 }
 

diff --git a/src/constraintList.c b/src/constraintList.c
index 88488b6ab350eaef5aed8542e9ece51acd9269f1..21bd987c0929b3b2a5044633101be89f33243bde 100644 (file)
--- a/src/constraintList.c
+++ b/src/constraintList.c
@@ -120,6 +120,41 @@ constraintList_print (constraintList s)
   return st;
 }
 
+
+cstring
+constraintList_printDetailed (constraintList s)
+{
+  int i;
+  cstring st = cstring_undefined;
+  bool first = TRUE;
+
+  if (s->nelements == 0)
+    st = cstring_makeLiteral("<List Empty>");
+  
+  for (i = 0; i < s->nelements; i++)
+    {
+      cstring type = cstring_undefined;
+      constraint current = s->elements[i];
+
+      if (current != NULL)
+       {
+         cstring temp1 = constraint_printDetailed (current);
+         type = message ("%s %s\n", type, temp1 );
+       }
+
+      if (first)
+       {
+         st = type;
+         first = FALSE;
+       }
+      else
+       {
+         st = message ("%s %s", st, type);
+       }
+    }
+  return st;
+}
+
 void
 constraintList_free (constraintList s)
 {
@@ -146,4 +181,12 @@ constraintList_copy (constraintList s)
   return ret;
 }
 
-
+constraintList constraintList_preserveOrig (constraintList c)
+{
+  constraintList_elements (c, el);
+  {
+    el = constraint_preserveOrig (el);
+  }
+  end_constraintList_elements;
+  return c;
+}

diff --git a/src/constraintResolve.c b/src/constraintResolve.c
index e85e4d1ffc6a1fab31706bdc3a092df703953544..24d43cf8aec7e4539e557bf3bf64bb00d51fc53c 100644 (file)
--- a/src/constraintResolve.c
+++ b/src/constraintResolve.c
@@ -89,11 +89,10 @@ bool satifies (constraint pre, constraint post)
     {
       return FALSE;
     }
-  if (post->expr->expr == NULL)
+  if (post->expr == NULL)
     return FALSE;
+
   return rangeCheck (pre->ar, pre->expr, post->ar, post->expr);
-  
-  return TRUE;
 }
 
 constraintExpr constraintExpr_simplify (constraintExpr expr)
@@ -101,18 +100,30 @@ constraintExpr constraintExpr_simplify (constraintExpr expr)
   
   expr->term = constraintTerm_simplify (expr->term);
   if (expr->expr == NULL)
-    return expr;
+    {
+      if ( (expr->term->kind == CONSTRAINTEXPR) &&  (expr->term->constrType == VALUE) )
+       {
+         expr->op =  expr->term->value.constrExpr->op;
+         expr->expr = expr->term->value.constrExpr->expr;
+         expr->term = expr->term->value.constrExpr->term;
+       }
+         
+      return expr;
+    }
   
     expr->expr = constraintExpr_simplify (expr->expr);
-  if ( (expr->term->constrType == INTLITERAL) && (expr->expr->term->constrType == INTLITERAL)  )
+
+    
+    
+  if ( (expr->term->kind == INTLITERAL) && (expr->expr->term->kind == INTLITERAL)  )
     {
-      TPRINTF( ("EVENTUAL IMPLEMENTATION OF LITERAL MERGE " ));
+      DPRINTF( ("INTLITERAL MERGE " ));
 
-      TPRINTF ( (message ("Expression is %s ", constraintExpr_print (expr) ) ) );
+      DPRINTF ( (message ("Expression is %s ", constraintExpr_print (expr) ) ) );
       
       if (expr->op == PLUS )
        {
-         TPRINTF( (message ("Adding %d and %d ", expr->term->value.intlit,
+         DPRINTF( (message ("Adding %d and %d ", expr->term->value.intlit,
                             expr->expr->term->value.intlit) ) );
          expr->term->value.intlit += expr->expr->term->value.intlit;
        }
@@ -124,6 +135,7 @@ constraintExpr constraintExpr_simplify (constraintExpr expr)
 
       expr->expr = expr->expr->expr;
     }
+  
   return expr;
   
 }
@@ -165,7 +177,7 @@ constraint solveforterm (constraint c)
     p = c->lexpr;
     while (p->expr != NULL)
       {
-       TPRINTF( (message("Moving %s", constraintExpr_print (c->expr) ) ) );
+       DPRINTF( (message("Moving %s", constraintExpr_print (c->expr) ) ) );
        c->expr = termMove(c->expr, p);
        p->op = p->expr->op;
        #warning memleak
@@ -189,24 +201,57 @@ bool resolve (constraint c, constraintList p)
     {
       if ( satifies (c, el) )
        {
-         TPRINTF ( (message ("\n%s Satifies %s\n ", constraint_print(el), constraint_print(c) ) ) );
+         DPRINTF ( (message ("\n%s Satifies %s\n ", constraint_print(el), constraint_print(c) ) ) );
          return TRUE;
        }
     }
   end_constraintList_elements;
-  TPRINTF ( (message ("no constraints satify %s", constraint_print(c) ) ));
+  DPRINTF ( (message ("no constraints satify %s", constraint_print(c) ) ));
   return FALSE;
 }
 
+
+constraintTerm  constraintTerm_substituteTerm (constraintTerm term, constraintTerm oldterm, constraintExpr replacement)
+{
+  if ( constraintTerm_similar (term, oldterm) )
+    {
+      // do the substitution
+      term->kind = CONSTRAINTEXPR;
+      term->value.constrExpr = constraintExpr_copy (replacement);
+    }
+  return term;    
+}
+
+constraintExpr constraintExpr_substituteTerm (constraintExpr expr, constraintTerm oldterm, constraintExpr replacement)
+{
+   expr->term = constraintTerm_substituteTerm (expr->term, oldterm, replacement);
+   if (expr->expr != NULL)
+     expr->expr = constraintExpr_substituteTerm (expr->expr, oldterm, replacement);
+
+   return expr;
+}
+constraint constraint_substituteTerm (constraint c, constraintTerm oldterm, constraintExpr replacement)
+{
+  c->lexpr = constraintExpr_substituteTerm (c->lexpr, oldterm, replacement);
+  c->expr   = constraintExpr_substituteTerm (c->expr, oldterm, replacement);
+  return c;
+}
+
 constraint substitute (constraint c, constraintList p)
 {
   constraintList_elements (p, el)
     {
-      if (constraintTerm_same(c->lexpr->term, el->lexpr->term) )
-       {
-         if ( el->ar == EQ)
+      if ( el->ar == EQ)
+       if (constraint_hasTerm (c, el->lexpr->term) )
+         //        constraintTerm_same(c->lexpr->term, el->lexpr->term) )
+         {
            {
-             c->lexpr = constraintExpr_copy (el->expr);
+             DPRINTF((message ("doing substitute for %s", constraint_print (c) ) ) );
+             c = constraint_substituteTerm (c, el->lexpr->term, el->expr); 
+             DPRINTF((message ("substituted constraint is now %s", constraint_print (c) ) ) );
+             // c->lexpr = constraintExpr_copy (el->expr);
+             c = constraint_simplify(c);
+             c = constraint_simplify(c);
              c = constraint_simplify(c);
              return c;
            }
@@ -250,7 +295,7 @@ bool constraintExpr_hasTerm (constraint c, constraintTerm term)
 
       p = p->expr->expr;
     }
-  TPRINTF((
+  DPRINTF((
           message ("constraintExpr_hasTerm returned fallse for %s %S",
                    constraint_print(c), constraintTerm_print(term)
                    )
@@ -262,10 +307,10 @@ constraintExpr solveEq (constraint c, constraintTerm t)
 {
   constraintExpr p;
   c = constraint_copy (c);
-  TPRINTF(("\ndoing solveEq\n"));
+  DPRINTF(("\ndoing solveEq\n"));
   if (! constraintTerm_same (c->expr->term, t) )
     {
-      TPRINTF ( (message ("\n\nconstraintTerms: %s %s not same ", constraintTerm_print(c->expr->term),
+      DPRINTF ( (message ("\n\nconstraintTerms: %s %s not same ", constraintTerm_print(c->expr->term),
                          constraintTerm_print(t) )
                 ) );
       return NULL;
@@ -274,7 +319,7 @@ constraintExpr solveEq (constraint c, constraintTerm t)
   p = c->expr;
   while (p->expr != NULL)
     {
-      TPRINTF( (message("\n\nMoving %s", constraintExpr_print (c->expr) ) ) );
+      DPRINTF( (message("\n\nMoving %s", constraintExpr_print (c->expr) ) ) );
       c->lexpr = termMove(c->lexpr, p);
       p->expr = p->expr->expr;
     }
@@ -285,13 +330,13 @@ constraintExpr solveEq (constraint c, constraintTerm t)
 
 constraint updateConstraint (constraint c, constraintList p)
 {
-  TPRINTF(("start updateConstraints"));
+  DPRINTF(("start updateConstraints"));
   constraintList_elements (p, el)
     {
       
       if (constraintTerm_same(c->lexpr->term, el->lexpr->term) )
        {
-         TPRINTF((""));
+         DPRINTF((""));
          if ( el->ar == EQ)
            {
                  TPRINTF((""));
@@ -314,7 +359,7 @@ constraint updateConstraint (constraint c, constraintList p)
   end_constraintList_elements;
   c = constraint_simplify(c);
   
-  TPRINTF(("end updateConstraints"));
+  DPRINTF(("end updateConstraints"));
   return c;
 }
 
@@ -340,7 +385,7 @@ constraintList reflectChangesEnsures (constraintList pre2, constraintList post1)
 void mergeResolve (exprNode parent, exprNode child1, exprNode child2)
 {
   constraintList temp;
-  TPRINTF( (message ("magically merging constraint into parent:%s for children:  %s and %s", exprNode_unparse (parent), exprNode_unparse (child1), exprNode_unparse(child2) )
+  DPRINTF( (message ("magically merging constraint into parent:%s for children:  %s and %s", exprNode_unparse (parent), exprNode_unparse (child1), exprNode_unparse(child2) )
            ) );
   llassert (!exprNode_isError (child1)  || !exprNode_isError(child2) );
   if (exprNode_isError (child1) )
@@ -357,7 +402,7 @@ void mergeResolve (exprNode parent, exprNode child1, exprNode child2)
 
   llassert(!exprNode_isError(child2) );
   
-  TPRINTF( (message ("Child constraints are %s %s and %s %s",
+  DPRINTF( (message ("Child constraints are %s %s and %s %s",
                     constraintList_print (child1->requiresConstraints),
                     constraintList_print (child1->ensuresConstraints),
                     constraintList_print (child2->requiresConstraints),
@@ -380,10 +425,11 @@ void mergeResolve (exprNode parent, exprNode child1, exprNode child2)
   parent->ensuresConstraints = constraintList_copy (child2->ensuresConstraints);
   parent->ensuresConstraints = constraintList_addList (parent->ensuresConstraints, temp);
   
-  TPRINTF( (message ("Parent constraints are %s and %s ",
+  DPRINTF( (message ("Parent constraints are %s and %s ",
                     constraintList_print (parent->requiresConstraints),
                     constraintList_print (parent->ensuresConstraints)
                     ) ) );
  
 }
 
+

diff --git a/src/constraintTerm.c b/src/constraintTerm.c
index 8f2418e7bd928a90b65c796561eee09a5cddafa4..471dae77401a498bd6a21ebc79cba1f286454bce 100644 (file)
--- a/src/constraintTerm.c
+++ b/src/constraintTerm.c
@@ -51,7 +51,39 @@ constraintTerm constraintTerm_simplify (constraintTerm term)
        }
 
     }
+
+  if (term->kind == CONSTRAINTEXPR )
+    {
+      if ( (term->constrType == MAXREAD) || (term->constrType == MAXSET) )
+       {
+         // ms(var + intlit) = ms (var) - intlit
+         if (term->value.constrExpr->expr == NULL)
+           return term;
+
+         if (term->value.constrExpr->expr->term->kind == INTLITERAL)
+           {
+             if (term->constrType == MAXREAD) 
+               term->value.constrExpr->term->constrType = MAXREAD;
+             else if (term->constrType == MAXSET) 
+               term->value.constrExpr->term->constrType = MAXSET;
+             else
+               llassert(FALSE);
+
+             term->constrType = VALUE;
+
+             if (term->value.constrExpr->op == PLUS)
+               term->value.constrExpr->op = MINUS;
+             else
+               term->value.constrExpr->op = PLUS;
+           }
+         
+       }
+      
+    }
+  
+
   return term;
+
 }
 
 constraintTerm constraintTerm_copy (constraintTerm term)
@@ -219,13 +251,29 @@ cstring constraintTerm_print (constraintTerm term)
       s = cstring_makeLiteral("Not Implemented\n");
       llassert(FALSE);
       break;
+    case CONSTRAINTEXPR:
+      s = message ("%s ", constraintExpr_print (term->value.constrExpr) );
     }
-  s = message (" %s %s ", constraintType_print (term->constrType), s);
+  s = message (" %s  ( %s ) ", constraintType_print (term->constrType), s);
   return s;
   
 }
 
 
+bool constraintTerm_hasTerm (constraintTerm term, constraintTerm searchTerm)
+{
+  if (term->kind == CONSTRAINTEXPR)
+    return (constraintExpr_includesTerm (term->value.constrExpr, searchTerm) );
+
+  if ( (term->kind == EXPRNODE) && (searchTerm->kind == EXPRNODE) )
+    {
+      return sRef_same (term->value.expr->sref, searchTerm->value.expr->sref);
+    }
+  return FALSE;
+    
+}
+
+/* same and similar are similar but not the same*/
 
 bool constraintTerm_same (constraintTerm term1, constraintTerm term2)
 {
@@ -248,12 +296,44 @@ bool constraintTerm_same (constraintTerm term1, constraintTerm term2)
  
  if (sRef_same (term1->value.expr->sref, term2->value.expr->sref) )
    {
-     TPRINTF ((message (" %s and %s are same", constraintTerm_print(term1), constraintTerm_print(term2)  )  ));
+     DPRINTF ((message (" %s and %s are same", constraintTerm_print(term1), constraintTerm_print(term2)  )  ));
+     return TRUE;
+   }
+ else
+   {
+     DPRINTF ((message (" %s and %s are not same", constraintTerm_print(term1), constraintTerm_print(term2)  )  ));
+     return FALSE;
+   }     
+    
+}
+
+bool constraintTerm_similar (constraintTerm term1, constraintTerm term2)
+{
+  llassert (term1 !=NULL && term2 !=NULL);
+
+  //  if (term1->constrType != term2->constrType)
+  //    {
+  //      return FALSE;
+  //    }
+  if ( (term1->kind != term2->kind) || (term1->kind != EXPRNODE) )
+    {
+      return FALSE;
+    }
+      
+ DPRINTF ( (message
+           ("Comparing srefs for %s and  %s ", constraintTerm_print(term1), constraintTerm_print(term2)
+            )
+           )
+          );
+ 
+ if (sRef_same (term1->value.expr->sref, term2->value.expr->sref) )
+   {
+     DPRINTF ((message (" %s and %s are same", constraintTerm_print(term1), constraintTerm_print(term2)  )  ));
      return TRUE;
    }
  else
    {
-     TPRINTF ((message (" %s and %s are not same", constraintTerm_print(term1), constraintTerm_print(term2)  )  ));
+     DPRINTF ((message (" %s and %s are not same", constraintTerm_print(term1), constraintTerm_print(term2)  )  ));
      return FALSE;
    }