From 9d2dd6626033e3b07327c501f13f2d8fcd2e4080 Mon Sep 17 00:00:00 2001 From: sjfink Date: Wed, 24 Oct 2007 19:26:31 +0000 Subject: [PATCH] more logic cleanup git-svn-id: https://wala.svn.sourceforge.net/svnroot/wala/trunk@1942 f5eafffb-2e1d-0410-98e4-8ec43c5233c4 --- .../com/ibm/wala/logic/BinaryRelation.java | 56 ------------------- .../wala/logic/ConstrainedIntVariable.java | 40 ------------- .../src/com/ibm/wala/logic/Simplifier.java | 33 +++++------ 3 files changed, 17 insertions(+), 112 deletions(-) delete mode 100644 com.ibm.wala.core/src/com/ibm/wala/logic/ConstrainedIntVariable.java diff --git a/com.ibm.wala.core/src/com/ibm/wala/logic/BinaryRelation.java b/com.ibm.wala.core/src/com/ibm/wala/logic/BinaryRelation.java index 51e4b82ae..b779f662c 100644 --- a/com.ibm.wala.core/src/com/ibm/wala/logic/BinaryRelation.java +++ b/com.ibm.wala.core/src/com/ibm/wala/logic/BinaryRelation.java @@ -10,16 +10,9 @@ *******************************************************************************/ package com.ibm.wala.logic; -import java.util.Collection; import java.util.Map; -import java.util.Set; import com.ibm.wala.util.collections.HashMapFactory; -import com.ibm.wala.util.collections.HashSetFactory; -import com.ibm.wala.util.intset.IBinaryNaturalRelation; -import com.ibm.wala.util.intset.IntIterator; -import com.ibm.wala.util.intset.IntPair; -import com.ibm.wala.util.intset.IntSet; public class BinaryRelation implements IRelation { @@ -97,55 +90,6 @@ public class BinaryRelation implements IRelation { return symbol; } - /** - * build a constraint saying v \in s - * - * @throws IllegalArgumentException - * if s is null - */ - public static IFormula makeSetConstraint(ConstrainedIntVariable v, IntSet s) { - if (s == null) { - throw new IllegalArgumentException("s is null"); - } - if (s.isEmpty()) { - // a hack. TODO: support primitives for "true" and "false" - return RelationFormula.makeEquals(IntConstant.make(0), IntConstant.make(1)); - } - IntIterator it = s.intIterator(); - int first = it.next(); - IFormula result = RelationFormula.makeEquals(v, first); - while (it.hasNext()) { - int i = it.next(); - result = BinaryFormula.or(result, RelationFormula.makeEquals(v, i)); - } - return result; - } - - /** - * Build constraints which ensure that the relation r fully defines the - * relation R over the given range of integers. - * - * @throws IllegalArgumentException - * if domain is null - * - */ - public static Collection buildConstraints(IBinaryNaturalRelation r, BinaryRelation R, IntPair domain) { - if (domain == null) { - throw new IllegalArgumentException("domain is null"); - } - Set result = HashSetFactory.make(); - for (int i = domain.getX(); i <= domain.getY(); i++) { - IntSet s = r.getRelated(i); - if (s != null) { - ConstrainedIntVariable v0 = ConstrainedIntVariable.make(0, domain); - IFormula inSet = makeSetConstraint(v0, s); - IFormula f = BinaryFormula.biconditional(inSet, RelationFormula.make(R, i, v0)); - result.add(QuantifiedFormula.forall(v0, f)); - } - } - return result; - } - public static BinaryRelation make(String symbol) { return new BinaryRelation(symbol); } diff --git a/com.ibm.wala.core/src/com/ibm/wala/logic/ConstrainedIntVariable.java b/com.ibm.wala.core/src/com/ibm/wala/logic/ConstrainedIntVariable.java deleted file mode 100644 index 3bbcd9fdc..000000000 --- a/com.ibm.wala.core/src/com/ibm/wala/logic/ConstrainedIntVariable.java +++ /dev/null @@ -1,40 +0,0 @@ -/******************************************************************************* - * Copyright (c) 2006 IBM Corporation. - * All rights reserved. This program and the accompanying materials - * are made available under the terms of the Eclipse Public License v1.0 - * which accompanies this distribution, and is available at - * http://www.eclipse.org/legal/epl-v10.html - * - * Contributors: - * IBM Corporation - initial API and implementation - *******************************************************************************/ -package com.ibm.wala.logic; - -import com.ibm.wala.util.intset.IntPair; - -/** - * A term that represents a variable in a formula - * - * @author sjfink - */ -public class ConstrainedIntVariable extends IntVariable { - - /** - * universe of valid integer constants this variable can assume. - */ - private final IntPair range; - - protected ConstrainedIntVariable(int number, IntPair range) { - super(number); - assert range != null; - this.range = range; - } - - public static ConstrainedIntVariable make(int number, IntPair range) { - return new ConstrainedIntVariable(number, range); - } - - public IntPair getRange() { - return range; - } -} 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 188b6c4fe..e93d705df 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 @@ -20,7 +20,6 @@ import java.util.Map; import com.ibm.wala.util.collections.HashMapFactory; import com.ibm.wala.util.collections.HashSetFactory; import com.ibm.wala.util.debug.Assertions; -import com.ibm.wala.util.intset.IntPair; /** * Utilities for simplifying logic expressions @@ -51,21 +50,23 @@ public class Simplifier { * quantified variable */ private static Collection eliminateQuantifiers(IFormula s) { - if (s.getKind().equals(IFormula.Kind.QUANTIFIED)) { - Collection result = HashSetFactory.make(); - QuantifiedFormula f = (QuantifiedFormula) s; - assert f.getBoundVar() instanceof ConstrainedIntVariable; - ConstrainedIntVariable v = (ConstrainedIntVariable) f.getBoundVar(); - IntPair range = v.getRange(); - assert range.getX() >= 0; - assert range.getY() >= range.getX(); - for (int i = range.getX(); i <= range.getY(); i++) { - result.add(substitute(f.getFormula(), v, IntConstant.make(i))); - } - return result; - } else { - return Collections.singleton(s); - } + Assertions.UNREACHABLE("implement me"); + return null; +// if (s.getKind().equals(IFormula.Kind.QUANTIFIED)) { +// Collection result = HashSetFactory.make(); +// QuantifiedFormula f = (QuantifiedFormula) s; +// assert f.getBoundVar() instanceof ConstrainedIntVariable; +// ConstrainedIntVariable v = (ConstrainedIntVariable) f.getBoundVar(); +// IntPair range = v.getRange(); +// assert range.getX() >= 0; +// assert range.getY() >= range.getX(); +// for (int i = range.getX(); i <= range.getY(); i++) { +// result.add(substitute(f.getFormula(), v, IntConstant.make(i))); +// } +// return result; +// } else { +// return Collections.singleton(s); +// } } /**