From e48b76ad214d0144f35ee31099617cbc6dedbdc4 Mon Sep 17 00:00:00 2001
From: sjfink <sjfink@f5eafffb-2e1d-0410-98e4-8ec43c5233c4>
Date: Thu, 13 Mar 2008 19:41:27 +0000
Subject: [PATCH] tweak NotFormula stuff to work better with CNF

git-svn-id: https://wala.svn.sourceforge.net/svnroot/wala/trunk@2704 f5eafffb-2e1d-0410-98e4-8ec43c5233c4
---
 com.ibm.wala.core/src/com/ibm/wala/logic/CNFFormula.java        | 2 +-
 com.ibm.wala.core/src/com/ibm/wala/logic/NotFormula.java        | 2 +-
 com.ibm.wala.core/src/com/ibm/wala/logic/NotFormulaMaxTerm.java | 2 +-
 com.ibm.wala.core/src/com/ibm/wala/logic/Simplifier.java        | 2 +-
 4 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/com.ibm.wala.core/src/com/ibm/wala/logic/CNFFormula.java b/com.ibm.wala.core/src/com/ibm/wala/logic/CNFFormula.java
index 465eb4013..607e27762 100644
--- a/com.ibm.wala.core/src/com/ibm/wala/logic/CNFFormula.java
+++ b/com.ibm.wala.core/src/com/ibm/wala/logic/CNFFormula.java
@@ -143,7 +143,7 @@ public class CNFFormula extends AbstractBinaryFormula implements ICNFFormula {
     case NEGATION:
       NotFormula n = (NotFormula) f;
       if (n.getFormula() instanceof RelationFormula) {
-        IMaxTerm t = NotFormulaMaxTerm.make((RelationFormula)n.getFormula());
+        IMaxTerm t = NotFormulaMaxTerm.createNotFormulaMaxTerm((RelationFormula)n.getFormula());
         return Collections.singleton(t);
       } else {
         // should not get here if other logic is working.
diff --git a/com.ibm.wala.core/src/com/ibm/wala/logic/NotFormula.java b/com.ibm.wala.core/src/com/ibm/wala/logic/NotFormula.java
index 78a1b4ae2..08d3d064f 100644
--- a/com.ibm.wala.core/src/com/ibm/wala/logic/NotFormula.java
+++ b/com.ibm.wala.core/src/com/ibm/wala/logic/NotFormula.java
@@ -54,7 +54,7 @@ public class NotFormula implements IFormula {
       if (r.getRelation().equals(BinaryRelation.LT)) {
         return RelationFormula.make(BinaryRelation.GE, r.getTerms());
       }
-      return new NotFormula(f);
+      return NotFormulaMaxTerm.createNotFormulaMaxTerm(r);
     case CONSTANT:
       if (f.equals(BooleanConstantFormula.TRUE)) {
         return BooleanConstantFormula.FALSE;
diff --git a/com.ibm.wala.core/src/com/ibm/wala/logic/NotFormulaMaxTerm.java b/com.ibm.wala.core/src/com/ibm/wala/logic/NotFormulaMaxTerm.java
index 1c051aaf7..47af0b555 100644
--- a/com.ibm.wala.core/src/com/ibm/wala/logic/NotFormulaMaxTerm.java
+++ b/com.ibm.wala.core/src/com/ibm/wala/logic/NotFormulaMaxTerm.java
@@ -23,7 +23,7 @@ import java.util.Collections;
  */
 public class NotFormulaMaxTerm extends NotFormula implements IMaxTerm {
 
-  public static NotFormulaMaxTerm make(RelationFormula f) {
+  public static NotFormulaMaxTerm createNotFormulaMaxTerm(RelationFormula f) {
     return new NotFormulaMaxTerm(f);
   }
 
diff --git a/com.ibm.wala.core/src/com/ibm/wala/logic/Simplifier.java b/com.ibm.wala.core/src/com/ibm/wala/logic/Simplifier.java
index b58c17da0..a9f41bdc8 100644
--- a/com.ibm.wala.core/src/com/ibm/wala/logic/Simplifier.java
+++ b/com.ibm.wala.core/src/com/ibm/wala/logic/Simplifier.java
@@ -418,7 +418,7 @@ public class Simplifier {
       NotFormulaMaxTerm n = (NotFormulaMaxTerm) formula;
       RelationFormula F = (RelationFormula) n.getFormula();
       RelationFormula subF = (RelationFormula)substitute(F, t1, t2);
-      return (F != subF ? NotFormulaMaxTerm.make(subF) : formula);
+      return (F != subF ? NotFormulaMaxTerm.createNotFormulaMaxTerm(subF) : formula);
     case QUANTIFIED:
       Assertions.UNREACHABLE();
       return null;