DASCA
/
WALA
2
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

more logic cleanup 

git-svn-id: https://wala.svn.sourceforge.net/svnroot/wala/trunk@1942 f5eafffb-2e1d-0410-98e4-8ec43c5233c4
This commit is contained in:
sjfink 2007-10-24 19:26:31 +00:00
parent d4574334a8
commit 9d2dd66260
3 changed files with 17 additions and 112 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

56
com.ibm.wala.core/src/com/ibm/wala/logic/BinaryRelation.java
View File

@ -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<IFormula> buildConstraints(IBinaryNaturalRelation r, BinaryRelation R, IntPair domain) {
if (domain == null) {
throw new IllegalArgumentException("domain is null");
}
Set<IFormula> 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);
}

40
com.ibm.wala.core/src/com/ibm/wala/logic/ConstrainedIntVariable.java
View File

@ -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;
}
}

33
com.ibm.wala.core/src/com/ibm/wala/logic/Simplifier.java
View File

@ -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<? extends IFormula> eliminateQuantifiers(IFormula s) {
if (s.getKind().equals(IFormula.Kind.QUANTIFIED)) {
Collection<IFormula> 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<IFormula> 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);
// }
}
/**