Migrate the rest symbolic analysis stuff to BasicConstraintManager.

git-svn-id: https://llvm.org/svn/llvm-project/cfe/trunk@55536 91177308-0d34-0410-b5e6-96231b3b80d8

5 files changed, 208 insertions, 168 deletions

diff --git a/include/clang/Analysis/PathSensitive/ConstraintManager.h b/include/clang/Analysis/PathSensitive/ConstraintManager.h
index 39e5918c19..6014e66015 100644
--- a/include/clang/Analysis/PathSensitive/ConstraintManager.h
+++ b/include/clang/Analysis/PathSensitive/ConstraintManager.h
@@ -1,17 +1,39 @@
-#ifndef CONSTRAINT_MANAGER_H
-#define CONSTRAINT_MANAGER_H
+#ifndef LLVM_CLANG_ANALYSIS_CONSTRAINT_MANAGER_H
+#define LLVM_CLANG_ANALYSIS_CONSTRAINT_MANAGER_H
+
+// FIXME: Typedef LiveSymbolsTy/DeadSymbolsTy at a more appropriate place.
+#include "clang/Analysis/PathSensitive/Store.h"
+
+namespace llvm {
+class APSInt;
+}
 
 namespace clang {
 
 class GRState;
 class GRStateManager;
 class RVal;
+class SymbolID;
 
 class ConstraintManager {
 public:
   virtual ~ConstraintManager();
   virtual const GRState* Assume(const GRState* St, RVal Cond, bool Assumption,
                                 bool& isFeasible) = 0;
+
+  virtual const GRState* AddNE(const GRState* St, SymbolID sym, 
+                               const llvm::APSInt& V) = 0;
+  virtual const llvm::APSInt* getSymVal(const GRState* St, SymbolID sym) = 0;
+
+  virtual bool isEqual(const GRState* St, SymbolID sym, 
+                       const llvm::APSInt& V) const = 0;
+
+  virtual const GRState* RemoveDeadBindings(const GRState* St,
+                                    StoreManager::LiveSymbolsTy& LSymbols,
+                                    StoreManager::DeadSymbolsTy& DSymbols) = 0;
+
+  virtual void print(const GRState* St, std::ostream& Out, 
+                     const char* nl, const char *sep) = 0;
 };
 
 ConstraintManager* CreateBasicConstraintManager(GRStateManager& statemgr);
diff --git a/include/clang/Analysis/PathSensitive/GRState.h b/include/clang/Analysis/PathSensitive/GRState.h
index 8570a9d0c2..993977984f 100644
--- a/include/clang/Analysis/PathSensitive/GRState.h
+++ b/include/clang/Analysis/PathSensitive/GRState.h
@@ -115,13 +115,6 @@ public:
     Profile(ID, this);
   }
   
-  // Queries.
-  
-  bool isNotEqual(SymbolID sym, const llvm::APSInt& V) const;
-  bool isEqual(SymbolID sym, const llvm::APSInt& V) const;
-  
-  const llvm::APSInt* getSymVal(SymbolID sym) const;
- 
   RVal LookupExpr(Expr* E) const {
     return Env.LookupExpr(E);
   }
@@ -153,7 +146,8 @@ public:
   void* const* FindGDM(void* K) const;
   
   template <typename T>
-  typename GRStateTrait<T>::data_type get() const {
+  typename GRStateTrait<T>::data_type
+  get() const {
     return GRStateTrait<T>::MakeData(FindGDM(GRStateTrait<T>::GDMIndex()));
   }
   
@@ -173,6 +167,7 @@ public:
   };
 
   void print(std::ostream& Out, StoreManager& StoreMgr,
+             ConstraintManager& ConstraintMgr,
              Printer **Beg = 0, Printer **End = 0,
              const char* nl = "\n", const char *sep = "") const;  
 };
@@ -412,12 +407,6 @@ public:
   
   const GRState* getPersistentState(GRState& Impl);
   
-  const GRState* AddEQ(const GRState* St, SymbolID sym,
-                          const llvm::APSInt& V);
-
-  const GRState* AddNE(const GRState* St, SymbolID sym,
-                          const llvm::APSInt& V);
-  
   bool isEqual(const GRState* state, Expr* Ex, const llvm::APSInt& V);
   bool isEqual(const GRState* state, Expr* Ex, uint64_t);
   
@@ -460,12 +449,19 @@ public:
     
     return GRStateTrait<T>::MakeContext(p);
   }
-  
-  // Assumption logic.
+
   const GRState* Assume(const GRState* St, RVal Cond, bool Assumption,
                            bool& isFeasible) {
     return ConstraintMgr->Assume(St, Cond, Assumption, isFeasible);
   }
+
+  const GRState* AddNE(const GRState* St, SymbolID sym, const llvm::APSInt& V) {
+    return ConstraintMgr->AddNE(St, sym, V);
+  }
+
+  const llvm::APSInt* getSymVal(const GRState* St, SymbolID sym) {
+    return ConstraintMgr->getSymVal(St, sym);
+  }
 };
   
 //===----------------------------------------------------------------------===//
diff --git a/lib/Analysis/BasicConstraintManager.cpp b/lib/Analysis/BasicConstraintManager.cpp
index efe5b93da4..7298d355c4 100644
--- a/lib/Analysis/BasicConstraintManager.cpp
+++ b/lib/Analysis/BasicConstraintManager.cpp
@@ -1,17 +1,19 @@
 #include "clang/Analysis/PathSensitive/ConstraintManager.h"
 #include "clang/Analysis/PathSensitive/GRState.h"
+#include "clang/Analysis/PathSensitive/GRStateTrait.h"
 #include "llvm/Support/Compiler.h"
+#include "llvm/Support/raw_ostream.h"
 
 using namespace clang;
 
 namespace {
 
+typedef llvm::ImmutableMap<SymbolID,GRState::IntSetTy> ConstNotEqTy;
+typedef llvm::ImmutableMap<SymbolID,const llvm::APSInt*> ConstEqTy;
+
 // BasicConstraintManager only tracks equality and inequality constraints of
 // constants and integer variables.
 class VISIBILITY_HIDDEN BasicConstraintManager : public ConstraintManager {
-  typedef llvm::ImmutableMap<SymbolID, GRState::IntSetTy> ConstNotEqTy;
-  typedef llvm::ImmutableMap<SymbolID, const llvm::APSInt*> ConstEqTy;
-
   GRStateManager& StateMgr;
 
 public:
@@ -52,7 +54,22 @@ public:
 
   const GRState* AssumeSymLE(const GRState* St, SymbolID sym,
                              const llvm::APSInt& V, bool& isFeasible);
-  };
+
+  const GRState* AddEQ(const GRState* St, SymbolID sym, const llvm::APSInt& V);
+
+  const GRState* AddNE(const GRState* St, SymbolID sym, const llvm::APSInt& V);
+
+  const llvm::APSInt* getSymVal(const GRState* St, SymbolID sym);
+  bool isNotEqual(const GRState* St, SymbolID sym, const llvm::APSInt& V) const;
+  bool isEqual(const GRState* St, SymbolID sym, const llvm::APSInt& V) const;
+
+  const GRState* RemoveDeadBindings(const GRState* St,
+                                    StoreManager::LiveSymbolsTy& LSymbols,
+                                    StoreManager::DeadSymbolsTy& DSymbols);
+
+  void print(const GRState* St, std::ostream& Out, 
+             const char* nl, const char *sep);
+};
 
 } // end anonymous namespace
 
@@ -205,17 +222,19 @@ BasicConstraintManager::AssumeSymInt(const GRState* St, bool Assumption,
   } // end switch
 }
 
+
+
 const GRState*
 BasicConstraintManager::AssumeSymNE(const GRState* St, SymbolID sym,
                                     const llvm::APSInt& V, bool& isFeasible) {
   // First, determine if sym == X, where X != V.
-  if (const llvm::APSInt* X = St->getSymVal(sym)) {
+  if (const llvm::APSInt* X = getSymVal(St, sym)) {
     isFeasible = (*X != V);
     return St;
   }
 
   // Second, determine if sym != V.
-  if (St->isNotEqual(sym, V)) {
+  if (isNotEqual(St, sym, V)) {
     isFeasible = true;
     return St;
   }
@@ -223,20 +242,20 @@ BasicConstraintManager::AssumeSymNE(const GRState* St, SymbolID sym,
   // If we reach here, sym is not a constant and we don't know if it is != V.
   // Make that assumption.
   isFeasible = true;
-  return StateMgr.AddNE(St, sym, V);
+  return AddNE(St, sym, V);
 }
 
 const GRState*
 BasicConstraintManager::AssumeSymEQ(const GRState* St, SymbolID sym,
                                     const llvm::APSInt& V, bool& isFeasible) {
   // First, determine if sym == X, where X != V.
-  if (const llvm::APSInt* X = St->getSymVal(sym)) {
+  if (const llvm::APSInt* X = getSymVal(St, sym)) {
     isFeasible = *X == V;
     return St;
   }
 
   // Second, determine if sym != V.
-  if (St->isNotEqual(sym, V)) {
+  if (isNotEqual(St, sym, V)) {
     isFeasible = false;
     return St;
   }
@@ -245,7 +264,7 @@ BasicConstraintManager::AssumeSymEQ(const GRState* St, SymbolID sym,
   // Make that assumption.
 
   isFeasible = true;
-  return StateMgr.AddEQ(St, sym, V);
+  return AddEQ(St, sym, V);
 }
 
 // These logic will be handled in another ConstraintManager.
@@ -272,7 +291,7 @@ BasicConstraintManager::AssumeSymGE(const GRState* St, SymbolID sym,
   // FIXME: Primitive logic for now.  Only reject a path if the value of
   //  sym is a constant X and !(X >= V).
 
-  if (const llvm::APSInt* X = St->getSymVal(sym)) {
+  if (const llvm::APSInt* X = getSymVal(St, sym)) {
     isFeasible = *X >= V;
     return St;
   }
@@ -288,7 +307,7 @@ BasicConstraintManager::AssumeSymLE(const GRState* St, SymbolID sym,
   // FIXME: Primitive logic for now.  Only reject a path if the value of
   //  sym is a constant X and !(X <= V).
 
-  if (const llvm::APSInt* X = St->getSymVal(sym)) {
+  if (const llvm::APSInt* X = getSymVal(St, sym)) {
     isFeasible = *X <= V;
     return St;
   }
@@ -296,3 +315,136 @@ BasicConstraintManager::AssumeSymLE(const GRState* St, SymbolID sym,
   isFeasible = true;
   return St;
 }
+
+static int ConstEqTyIndex = 0;
+static int ConstNotEqTyIndex = 0;
+
+namespace clang {
+  template<>
+  struct GRStateTrait<ConstNotEqTy> : public GRStatePartialTrait<ConstNotEqTy> {
+    static inline void* GDMIndex() { return &ConstNotEqTyIndex; }  
+  };
+  
+  template<>
+  struct GRStateTrait<ConstEqTy> : public GRStatePartialTrait<ConstEqTy> {
+    static inline void* GDMIndex() { return &ConstEqTyIndex; }  
+  };
+}
+
+const GRState* BasicConstraintManager::AddEQ(const GRState* St, SymbolID sym,
+                                             const llvm::APSInt& V) {
+  // Create a new state with the old binding replaced.
+  GRStateRef state(St, StateMgr);
+  return state.set<ConstEqTy>(sym, &V);
+}
+
+const GRState* BasicConstraintManager::AddNE(const GRState* St, SymbolID sym,
+                                             const llvm::APSInt& V) {
+  GRState::IntSetTy::Factory ISetFactory(StateMgr.getAllocator());
+  GRStateRef state(St, StateMgr);
+
+  // First, retrieve the NE-set associated with the given symbol.
+  ConstNotEqTy::data_type* T = state.get<ConstNotEqTy>(sym);
+  GRState::IntSetTy S = T ? *T : ISetFactory.GetEmptySet();
+
+  
+  // Now add V to the NE set.
+  S = ISetFactory.Add(S, &V);
+  
+  // Create a new state with the old binding replaced.
+  return state.set<ConstNotEqTy>(sym, S);
+}
+
+const llvm::APSInt* BasicConstraintManager::getSymVal(const GRState* St,
+                                                      SymbolID sym) {
+  const ConstEqTy::data_type* T = St->get<ConstEqTy>(sym);
+  return T ? *T : NULL;  
+}
+
+bool BasicConstraintManager::isNotEqual(const GRState* St, SymbolID sym, 
+                                        const llvm::APSInt& V) const {
+
+  // Retrieve the NE-set associated with the given symbol.
+  const ConstNotEqTy::data_type* T = St->get<ConstNotEqTy>(sym);
+
+  // See if V is present in the NE-set.
+  return T ? T->contains(&V) : false;
+}
+
+bool BasicConstraintManager::isEqual(const GRState* St, SymbolID sym,
+                                     const llvm::APSInt& V) const {
+  // Retrieve the EQ-set associated with the given symbol.
+  const ConstEqTy::data_type* T = St->get<ConstEqTy>(sym);
+  // See if V is present in the EQ-set.
+  return T ? **T == V : false;
+}
+
+const GRState* BasicConstraintManager::RemoveDeadBindings(const GRState* St,
+                                        StoreManager::LiveSymbolsTy& LSymbols,
+                                        StoreManager::DeadSymbolsTy& DSymbols) {
+  GRStateRef state(St, StateMgr);
+  ConstEqTy CE = state.get<ConstEqTy>();
+  ConstEqTy::Factory& CEFactory = state.get_context<ConstEqTy>();
+
+  for (ConstEqTy::iterator I = CE.begin(), E = CE.end(); I!=E; ++I) {
+    SymbolID sym = I.getKey();        
+    if (!LSymbols.count(sym)) {
+      DSymbols.insert(sym);
+      CE = CEFactory.Remove(CE, sym);
+    }
+  }
+  state = state.set<ConstEqTy>(CE);
+
+  ConstNotEqTy CNE = state.get<ConstNotEqTy>();
+  ConstNotEqTy::Factory& CNEFactory = state.get_context<ConstNotEqTy>();
+
+  for (ConstNotEqTy::iterator I = CNE.begin(), E = CNE.end(); I != E; ++I) {
+    SymbolID sym = I.getKey();    
+    if (!LSymbols.count(sym)) {
+      DSymbols.insert(sym);
+      CNE = CNEFactory.Remove(CNE, sym);
+    }
+  }
+  
+  return state.set<ConstNotEqTy>(CNE);
+}
+
+void BasicConstraintManager::print(const GRState* St, std::ostream& Out, 
+                                   const char* nl, const char *sep) {
+  // Print equality constraints.
+
+  ConstEqTy CE = St->get<ConstEqTy>();
+
+  if (!CE.isEmpty()) {
+    Out << nl << sep << "'==' constraints:";
+
+    for (ConstEqTy::iterator I = CE.begin(), E = CE.end(); I!=E; ++I) {
+      Out << nl << " $" << I.getKey();
+      llvm::raw_os_ostream OS(Out);
+      OS << " : "   << *I.getData();
+    }
+  }
+
+  // Print != constraints.
+  
+  ConstNotEqTy CNE = St->get<ConstNotEqTy>();
+  
+  if (!CNE.isEmpty()) {
+    Out << nl << sep << "'!=' constraints:";
+  
+    for (ConstNotEqTy::iterator I = CNE.begin(), EI = CNE.end(); I!=EI; ++I) {
+      Out << nl << " $" << I.getKey() << " : ";
+      bool isFirst = true;
+    
+      GRState::IntSetTy::iterator J = I.getData().begin(), 
+                                  EJ = I.getData().end();      
+      
+      for ( ; J != EJ; ++J) {        
+        if (isFirst) isFirst = false;
+        else Out << ", ";
+      
+        Out << *J;
+      }
+    }
+  }
+}
\ No newline at end of file
diff --git a/lib/Analysis/CFRefCount.cpp b/lib/Analysis/CFRefCount.cpp
index 3ed4894fa1..8ea8301134 100644
--- a/lib/Analysis/CFRefCount.cpp
+++ b/lib/Analysis/CFRefCount.cpp
@@ -1905,7 +1905,7 @@ const GRState* CFRefCount::EvalAssume(GRStateManager& VMgr,
   for (RefBindings::iterator I=B.begin(), E=B.end(); I!=E; ++I) {    
     // Check if the symbol is null (or equal to any constant).
     // If this is the case, stop tracking the symbol.
-    if (St->getSymVal(I.getKey())) {
+    if (VMgr.getSymVal(St, I.getKey())) {
       changed = true;
       B = RefBFactory.Remove(B, I.getKey());
     }
diff --git a/lib/Analysis/GRState.cpp b/lib/Analysis/GRState.cpp
index 8ea1191b7e..72eeda97b1 100644
--- a/lib/Analysis/GRState.cpp
+++ b/lib/Analysis/GRState.cpp
@@ -32,50 +32,6 @@ GRStateManager::~GRStateManager() {
     I->second.second(I->second.first);
 }
 
-//===----------------------------------------------------------------------===//
-//  Basic symbolic analysis.  This will eventually be refactored into a
-//  separate component.
-//===----------------------------------------------------------------------===//
-
-typedef llvm::ImmutableMap<SymbolID,GRState::IntSetTy> ConstNotEqTy;
-typedef llvm::ImmutableMap<SymbolID,const llvm::APSInt*> ConstEqTy;
-
-static int ConstEqTyIndex = 0;
-static int ConstNotEqTyIndex = 0;
-
-namespace clang {
-  template<>
-  struct GRStateTrait<ConstNotEqTy> : public GRStatePartialTrait<ConstNotEqTy> {
-    static inline void* GDMIndex() { return &ConstNotEqTyIndex; }  
-  };
-  
-  template<>
-  struct GRStateTrait<ConstEqTy> : public GRStatePartialTrait<ConstEqTy> {
-    static inline void* GDMIndex() { return &ConstEqTyIndex; }  
-  };
-}
-
-bool GRState::isNotEqual(SymbolID sym, const llvm::APSInt& V) const {
-
-  // Retrieve the NE-set associated with the given symbol.
-  const ConstNotEqTy::data_type* T = get<ConstNotEqTy>(sym);
-
-  // See if V is present in the NE-set.
-  return T ? T->contains(&V) : false;
-}
-
-bool GRState::isEqual(SymbolID sym, const llvm::APSInt& V) const {
-  // Retrieve the EQ-set associated with the given symbol.
-  const ConstEqTy::data_type* T = get<ConstEqTy>(sym);
-  // See if V is present in the EQ-set.
-  return T ? **T == V : false;
-}
-
-const llvm::APSInt* GRState::getSymVal(SymbolID sym) const {
-  const ConstEqTy::data_type* T = get<ConstEqTy>(sym);
-  return T ? *T : NULL;  
-}
-
 const GRState*
 GRStateManager::RemoveDeadBindings(const GRState* St, Stmt* Loc,
                                    const LiveVariables& Liveness,
@@ -99,37 +55,9 @@ GRStateManager::RemoveDeadBindings(const GRState* St, Stmt* Loc,
   DSymbols.clear();
   NewSt.St = StMgr->RemoveDeadBindings(St->getStore(), Loc, Liveness, DRoots,
                                        LSymbols, DSymbols);
-  
-  
-  GRStateRef state(getPersistentState(NewSt), *this);
-
-  // Remove the dead symbols from the symbol tracker.
-  // FIXME: Refactor into something else that manages symbol values.
-
-  ConstEqTy CE = state.get<ConstEqTy>();
-  ConstEqTy::Factory& CEFactory = state.get_context<ConstEqTy>();
-
-  for (ConstEqTy::iterator I = CE.begin(), E = CE.end(); I!=E; ++I) {
-    SymbolID sym = I.getKey();        
-    if (!LSymbols.count(sym)) {
-      DSymbols.insert(sym);
-      CE = CEFactory.Remove(CE, sym);
-    }
-  }
-  state = state.set<ConstEqTy>(CE);
-
-  ConstNotEqTy CNE = state.get<ConstNotEqTy>();
-  ConstNotEqTy::Factory& CNEFactory = state.get_context<ConstNotEqTy>();
 
-  for (ConstNotEqTy::iterator I = CNE.begin(), E = CNE.end(); I != E; ++I) {
-    SymbolID sym = I.getKey();    
-    if (!LSymbols.count(sym)) {
-      DSymbols.insert(sym);
-      CNE = CNEFactory.Remove(CNE, sym);
-    }
-  }
-  
-  return state.set<ConstNotEqTy>(CNE);
+  return ConstraintMgr->RemoveDeadBindings(getPersistentState(NewSt), 
+                                           LSymbols, DSymbols);
 }
 
 const GRState* GRStateManager::SetRVal(const GRState* St, LVal LV,
@@ -177,30 +105,6 @@ const GRState* GRStateManager::Unbind(const GRState* St, LVal LV) {
   return getPersistentState(NewSt);    
 }
 
-
-const GRState* GRStateManager::AddNE(const GRState* St, SymbolID sym,
-                                     const llvm::APSInt& V) {
-  
-  GRStateRef state(St, *this);
-
-  // First, retrieve the NE-set associated with the given symbol.
-  ConstNotEqTy::data_type* T = state.get<ConstNotEqTy>(sym);  
-  GRState::IntSetTy S = T ? *T : ISetFactory.GetEmptySet();
-  
-  // Now add V to the NE set.
-  S = ISetFactory.Add(S, &V);
-  
-  // Create a new state with the old binding replaced.
-  return state.set<ConstNotEqTy>(sym, S);
-}
-
-const GRState* GRStateManager::AddEQ(const GRState* St, SymbolID sym,
-                                           const llvm::APSInt& V) {
-  // Create a new state with the old binding replaced.
-  GRStateRef state(St, *this);
-  return state.set<ConstEqTy>(sym, &V);
-}
-
 const GRState* GRStateManager::getInitialState() {
 
   GRState StateImpl(EnvMgr.getInitialEnvironment(), 
@@ -231,6 +135,7 @@ const GRState* GRStateManager::getPersistentState(GRState& State) {
 //===----------------------------------------------------------------------===//
 
 void GRState::print(std::ostream& Out, StoreManager& StoreMgr,
+                    ConstraintManager& ConstraintMgr,
                     Printer** Beg, Printer** End,
                     const char* nl, const char* sep) const {
   
@@ -271,42 +176,7 @@ void GRState::print(std::ostream& Out, StoreManager& StoreMgr,
     I.getData().print(Out);
   }
   
-  // Print equality constraints.
-  // FIXME: Make just another printer do this.
-  ConstEqTy CE = get<ConstEqTy>();
-
-  if (!CE.isEmpty()) {
-    Out << nl << sep << "'==' constraints:";
-
-    for (ConstEqTy::iterator I = CE.begin(), E = CE.end(); I!=E; ++I) {
-      Out << nl << " $" << I.getKey();
-      llvm::raw_os_ostream OS(Out);
-      OS << " : "   << *I.getData();
-    }
-  }
-
-  // Print != constraints.
-  // FIXME: Make just another printer do this.
-  
-  ConstNotEqTy CNE = get<ConstNotEqTy>();
-  
-  if (!CNE.isEmpty()) {
-    Out << nl << sep << "'!=' constraints:";
-  
-    for (ConstNotEqTy::iterator I = CNE.begin(), EI = CNE.end(); I!=EI; ++I) {
-      Out << nl << " $" << I.getKey() << " : ";
-      isFirst = true;
-    
-      IntSetTy::iterator J = I.getData().begin(), EJ = I.getData().end();      
-      
-      for ( ; J != EJ; ++J) {        
-        if (isFirst) isFirst = false;
-        else Out << ", ";
-      
-        Out << *J;
-      }
-    }
-  }
+  ConstraintMgr.print(this, Out, nl, sep);
   
   // Print checker-specific data. 
   for ( ; Beg != End ; ++Beg) (*Beg)->Print(Out, this, nl, sep);
@@ -323,7 +193,7 @@ void GRStateRef::printStdErr() const {
 void GRStateRef::print(std::ostream& Out, const char* nl, const char* sep)const{
   GRState::Printer **beg = Mgr->Printers.empty() ? 0 : &Mgr->Printers[0];
   GRState::Printer **end = !beg ? 0 : beg + Mgr->Printers.size();  
-  St->print(Out, *Mgr->StMgr, beg, end, nl, sep);
+  St->print(Out, *Mgr->StMgr, *Mgr->ConstraintMgr, beg, end, nl, sep);
 }
 
 //===----------------------------------------------------------------------===//
@@ -376,10 +246,10 @@ bool GRStateManager::isEqual(const GRState* state, Expr* Ex,
     return X->getValue() == Y;
     
   if (nonlval::SymbolVal* X = dyn_cast<nonlval::SymbolVal>(&V))
-    return state->isEqual(X->getSymbol(), Y);
+    return ConstraintMgr->isEqual(state, X->getSymbol(), Y);
   
   if (lval::SymbolVal* X = dyn_cast<lval::SymbolVal>(&V))
-    return state->isEqual(X->getSymbol(), Y);
+    return ConstraintMgr->isEqual(state, X->getSymbol(), Y);
   
   return false;
 }