delete half-baked logic package
git-svn-id: https://wala.svn.sourceforge.net/svnroot/wala/trunk@2750 f5eafffb-2e1d-0410-98e4-8ec43c5233c4
This commit is contained in:
sjfink
parent
30f9303ee1
commit
7856cc7773
|
|
@ -50,7 +50,6 @@ Export-Package: .,
|
|||
com.ibm.wala.ipa.slicer,
|
||||
com.ibm.wala.ipa.slicer.thin,
|
||||
com.ibm.wala.ipa.summaries,
|
||||
com.ibm.wala.logic,
|
||||
com.ibm.wala.model,
|
||||
com.ibm.wala.model.java.lang,
|
||||
com.ibm.wala.model.java.lang.reflect,
|
||||
|
|
|
|||
|
|
@ -1,38 +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.logic.ILogicConstants.BinaryConnective;
|
||||
|
||||
public abstract class AbstractBinaryFormula implements IFormula {
|
||||
|
||||
protected AbstractBinaryFormula() {
|
||||
super();
|
||||
}
|
||||
|
||||
public final Kind getKind() {
|
||||
return Kind.BINARY;
|
||||
}
|
||||
|
||||
public abstract BinaryConnective getConnective();
|
||||
|
||||
public abstract IFormula getF1();
|
||||
|
||||
public abstract IFormula getF2();
|
||||
|
||||
@Override
|
||||
public abstract boolean equals(Object obj);
|
||||
|
||||
@Override
|
||||
public abstract int hashCode();
|
||||
|
||||
|
||||
}
|
||||
|
|
@ -1,49 +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 java.util.Collection;
|
||||
import java.util.Collections;
|
||||
|
||||
|
||||
public abstract class AbstractConstant implements IConstant {
|
||||
|
||||
public Kind getKind() {
|
||||
return Kind.CONSTANT;
|
||||
}
|
||||
|
||||
public String prettyPrint(ILogicDecorator d) throws IllegalArgumentException {
|
||||
if (d == null) {
|
||||
throw new IllegalArgumentException("d == null");
|
||||
}
|
||||
return d.prettyPrint(this);
|
||||
}
|
||||
|
||||
public Collection<AbstractVariable> getFreeVariables() {
|
||||
return Collections.emptySet();
|
||||
}
|
||||
|
||||
public Collection<? extends IConstant> getConstants() {
|
||||
return Collections.singleton(this);
|
||||
}
|
||||
|
||||
public Collection<? extends ITerm> getAllTerms() {
|
||||
return Collections.singleton(this);
|
||||
}
|
||||
|
||||
|
||||
@Override
|
||||
public abstract boolean equals(Object obj);
|
||||
|
||||
@Override
|
||||
public abstract int hashCode();
|
||||
|
||||
}
|
||||
|
|
@ -1,62 +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;
|
||||
|
||||
|
||||
/**
|
||||
* A term that represents a variable in a formula
|
||||
*
|
||||
* @author sjfink
|
||||
*/
|
||||
public abstract class AbstractNumberedVariable extends AbstractVariable implements Comparable<AbstractNumberedVariable> {
|
||||
|
||||
private final int number;
|
||||
|
||||
protected AbstractNumberedVariable(int number) {
|
||||
this.number = number;
|
||||
}
|
||||
|
||||
@Override
|
||||
public final int hashCode() {
|
||||
final int PRIME = 31;
|
||||
int result = 1;
|
||||
result = PRIME * result + number;
|
||||
return result;
|
||||
}
|
||||
|
||||
@Override
|
||||
public final boolean equals(Object obj) {
|
||||
if (this == obj)
|
||||
return true;
|
||||
if (obj == null)
|
||||
return false;
|
||||
if (getClass() != obj.getClass())
|
||||
return false;
|
||||
final AbstractNumberedVariable other = (AbstractNumberedVariable) obj;
|
||||
if (number != other.number)
|
||||
return false;
|
||||
return true;
|
||||
}
|
||||
|
||||
public final int getNumber() {
|
||||
return number;
|
||||
}
|
||||
|
||||
@Override
|
||||
public String toString() {
|
||||
return "v" + getNumber();
|
||||
}
|
||||
|
||||
public final int compareTo(AbstractNumberedVariable o) throws NullPointerException {
|
||||
return this.getNumber() - o.getNumber();
|
||||
}
|
||||
|
||||
}
|
||||
|
|
@ -1,35 +0,0 @@
|
|||
/*******************************************************************************
|
||||
* Copyright (c) 2007 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 java.util.Collection;
|
||||
import java.util.Collections;
|
||||
|
||||
/**
|
||||
* Abstract base class for decision procedures.
|
||||
*
|
||||
* @author sjfink
|
||||
*/
|
||||
public abstract class AbstractSemiDecisionProcedure implements ISemiDecisionProcedure {
|
||||
|
||||
public final boolean isTautology(IFormula f) {
|
||||
Collection<IMaxTerm> emptyTheory = Collections.emptySet();
|
||||
return isTautology(f, emptyTheory);
|
||||
}
|
||||
|
||||
public final boolean isContradiction(IFormula f) {
|
||||
Collection<IMaxTerm> emptyTheory = Collections.emptySet();
|
||||
return isContradiction(f, emptyTheory);
|
||||
}
|
||||
|
||||
|
||||
|
||||
}
|
||||
|
|
@ -1,21 +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;
|
||||
|
||||
public abstract class AbstractTerm implements ITerm {
|
||||
|
||||
@Override
|
||||
public abstract boolean equals(Object obj);
|
||||
|
||||
@Override
|
||||
public abstract int hashCode();
|
||||
|
||||
}
|
||||
|
|
@ -1,43 +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 java.util.Collection;
|
||||
import java.util.TreeSet;
|
||||
|
||||
public abstract class AbstractTheory extends DefaultDecorator implements ITheory {
|
||||
|
||||
@Override
|
||||
public String toString() {
|
||||
StringBuffer result = new StringBuffer(getClass().toString());
|
||||
result.append(":\n");
|
||||
result.append(getVocabulary());
|
||||
result.append("Sentences:\n");
|
||||
TreeSet<String> sorted = new TreeSet<String>();
|
||||
for (IFormula f : getSentences()) {
|
||||
sorted.add(f.toString());
|
||||
}
|
||||
for (String s : sorted) {
|
||||
result.append(s);
|
||||
result.append("\n");
|
||||
}
|
||||
return result.toString();
|
||||
}
|
||||
|
||||
/**
|
||||
* by default, just return all sentences
|
||||
*/
|
||||
public Collection<? extends IFormula> getSentencesRelevantToConstraints(Collection<? extends IFormula> constraints) {
|
||||
return getSentences();
|
||||
}
|
||||
|
||||
|
||||
}
|
||||
|
|
@ -1,59 +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 java.util.Collection;
|
||||
import java.util.Collections;
|
||||
|
||||
/**
|
||||
* A term that represents a variable in a formula
|
||||
*
|
||||
* @author sjfink
|
||||
*/
|
||||
public abstract class AbstractVariable extends AbstractTerm {
|
||||
|
||||
|
||||
protected AbstractVariable() {
|
||||
}
|
||||
|
||||
public final Kind getKind() {
|
||||
return Kind.VARIABLE;
|
||||
}
|
||||
|
||||
@Override
|
||||
public abstract int hashCode();
|
||||
|
||||
@Override
|
||||
public abstract boolean equals(Object obj);
|
||||
|
||||
|
||||
@Override
|
||||
public abstract String toString();
|
||||
|
||||
public String prettyPrint(ILogicDecorator d) throws IllegalArgumentException {
|
||||
if (d == null) {
|
||||
throw new IllegalArgumentException("d == null");
|
||||
}
|
||||
return d.prettyPrint(this);
|
||||
}
|
||||
|
||||
public final Collection<AbstractVariable> getFreeVariables() {
|
||||
return Collections.singleton(this);
|
||||
}
|
||||
|
||||
public final Collection<? extends IConstant> getConstants() {
|
||||
return Collections.emptySet();
|
||||
}
|
||||
|
||||
public final Collection<? extends ITerm> getAllTerms() {
|
||||
return Collections.singleton(this);
|
||||
}
|
||||
}
|
||||
|
|
@ -1,54 +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;
|
||||
|
||||
|
||||
public abstract class AbstractVocabulary<T extends IConstant> implements IVocabulary<T> {
|
||||
|
||||
@Override
|
||||
public String toString() {
|
||||
StringBuffer result = new StringBuffer();
|
||||
result.append("Functions:\n");
|
||||
if (getFunctions().isEmpty()) {
|
||||
result.append(" <none> ");
|
||||
} else {
|
||||
for (IFunction f : getFunctions()) {
|
||||
result.append(f).append("\n");
|
||||
}
|
||||
}
|
||||
result.append("Relations:\n");
|
||||
if (getRelations().isEmpty()) {
|
||||
result.append(" <none> ");
|
||||
} else {
|
||||
for (IRelation r : getRelations()) {
|
||||
result.append(r).append("\n");
|
||||
}
|
||||
}
|
||||
result.append("Constants:\n");
|
||||
if (getConstants().isEmpty()) {
|
||||
result.append(" <none> ");
|
||||
} else {
|
||||
for (IConstant c : getConstants()) {
|
||||
result.append(c).append("\n");
|
||||
}
|
||||
}
|
||||
result.append("Variables:\n");
|
||||
if (getVariables().isEmpty()) {
|
||||
result.append(" <none> ");
|
||||
} else {
|
||||
for (AbstractVariable v : getVariables()) {
|
||||
result.append(v).append("\n");
|
||||
}
|
||||
}
|
||||
return result.toString();
|
||||
}
|
||||
|
||||
}
|
||||
|
|
@ -1,288 +0,0 @@
|
|||
/*******************************************************************************
|
||||
* Copyright (c) 2007 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 java.util.Collection;
|
||||
|
||||
import com.ibm.wala.logic.ILogicConstants.BinaryConnective;
|
||||
|
||||
/**
|
||||
* Ad-hoc decision logic.
|
||||
*
|
||||
* @author sjfink
|
||||
*/
|
||||
public class AdHocSemiDecisionProcedure extends AbstractSemiDecisionProcedure {
|
||||
|
||||
private final static AdHocSemiDecisionProcedure INSTANCE = new AdHocSemiDecisionProcedure();
|
||||
|
||||
public static AdHocSemiDecisionProcedure singleton() {
|
||||
return INSTANCE;
|
||||
}
|
||||
|
||||
protected AdHocSemiDecisionProcedure() {
|
||||
}
|
||||
|
||||
/*
|
||||
* @see com.ibm.wala.logic.ISemiDecisionProcedure#isContradiction(com.ibm.wala.logic.IFormula,
|
||||
* java.util.Collection)
|
||||
*/
|
||||
public boolean isContradiction(IFormula f, Collection<IMaxTerm> facts) throws IllegalArgumentException {
|
||||
return contradiction(f, facts);
|
||||
}
|
||||
|
||||
/*
|
||||
* @see com.ibm.wala.logic.ISemiDecisionProcedure#isTautology(com.ibm.wala.logic.IFormula,
|
||||
* java.util.Collection)
|
||||
*/
|
||||
public boolean isTautology(IFormula f, Collection<IMaxTerm> facts) throws IllegalArgumentException {
|
||||
return tautology(f, facts);
|
||||
}
|
||||
|
||||
// some ad-hoc formula normalization
|
||||
// 1) change >, >= to <, <=
|
||||
// TODO: do normalization in a principled manner
|
||||
static IFormula normalize(IFormula f) throws IllegalArgumentException {
|
||||
if (f == null) {
|
||||
throw new IllegalArgumentException("f == null");
|
||||
}
|
||||
switch (f.getKind()) {
|
||||
case RELATION:
|
||||
RelationFormula r = (RelationFormula) f;
|
||||
if (r.getRelation().equals(BinaryRelation.GE) || r.getRelation().equals(BinaryRelation.GT)) {
|
||||
BinaryRelation swap = BinaryRelation.swap(r.getRelation());
|
||||
return RelationFormula.make(swap, r.getTerms().get(1), r.getTerms().get(0));
|
||||
}
|
||||
return f;
|
||||
default:
|
||||
return f;
|
||||
}
|
||||
}
|
||||
|
||||
/**
|
||||
* Primitive logic to determine if axiom implies f. This CANNOT invoke
|
||||
* tautology or contradiction recursively.
|
||||
*/
|
||||
protected boolean atomicImplies(IFormula axiom, IFormula f) {
|
||||
if (AdHocSemiDecisionProcedure.normalize(axiom).equals(AdHocSemiDecisionProcedure.normalize(f))) {
|
||||
return true;
|
||||
}
|
||||
return false;
|
||||
}
|
||||
|
||||
private boolean contradicts(IMaxTerm axiom, IFormula f) {
|
||||
IFormula notF = NotFormula.make(f);
|
||||
return atomicImplies(axiom, notF);
|
||||
}
|
||||
|
||||
/**
|
||||
* @param facts
|
||||
* formulae that can be treated as axioms
|
||||
* @return true if we can easily prove f is a contradiction
|
||||
* @throws IllegalArgumentException
|
||||
* if facts == null
|
||||
*/
|
||||
private boolean contradiction(IFormula f, Collection<IMaxTerm> facts) throws IllegalArgumentException {
|
||||
if (facts == null) {
|
||||
throw new IllegalArgumentException("facts == null");
|
||||
}
|
||||
for (IMaxTerm d : facts) {
|
||||
if (contradicts(d, f)) {
|
||||
return true;
|
||||
}
|
||||
}
|
||||
switch (f.getKind()) {
|
||||
case BINARY:
|
||||
AbstractBinaryFormula b = (AbstractBinaryFormula) f;
|
||||
if (b.getConnective().equals(BinaryConnective.AND)) {
|
||||
if (contradiction(b.getF1(), facts) || contradiction(b.getF2(), facts)) {
|
||||
return true;
|
||||
}
|
||||
IFormula not1 = NotFormula.make(b.getF1());
|
||||
if (atomicImplies(b.getF2(), not1)) {
|
||||
return true;
|
||||
}
|
||||
IFormula not2 = NotFormula.make(b.getF2());
|
||||
if (atomicImplies(b.getF1(), not2)) {
|
||||
return true;
|
||||
}
|
||||
} else if (b.getConnective().equals(BinaryConnective.OR)) {
|
||||
if (contradiction(b.getF1(), facts) && contradiction(b.getF2(), facts)) {
|
||||
return true;
|
||||
}
|
||||
}
|
||||
break;
|
||||
case CONSTANT:
|
||||
BooleanConstantFormula bc = (BooleanConstantFormula) f;
|
||||
return bc.equals(BooleanConstantFormula.FALSE);
|
||||
case NEGATION:
|
||||
NotFormula nf = (NotFormula)f;
|
||||
return isTautology(nf.getFormula(), facts);
|
||||
case QUANTIFIED:
|
||||
return false;
|
||||
case RELATION:
|
||||
RelationFormula r = (RelationFormula) f;
|
||||
if (r.getRelation().equals(BinaryRelation.EQUALS)) {
|
||||
ITerm lhs = r.getTerms().get(0);
|
||||
ITerm rhs = r.getTerms().get(1);
|
||||
if (lhs.getKind().equals(ITerm.Kind.CONSTANT) && rhs.getKind().equals(ITerm.Kind.CONSTANT)) {
|
||||
if (!lhs.equals(rhs)) {
|
||||
return true;
|
||||
}
|
||||
}
|
||||
} else if (r.getRelation().equals(BinaryRelation.NE)) {
|
||||
ITerm lhs = r.getTerms().get(0);
|
||||
ITerm rhs = r.getTerms().get(1);
|
||||
if (lhs.equals(rhs)) {
|
||||
return true;
|
||||
}
|
||||
} else if (r.getRelation().equals(BinaryRelation.LT)) {
|
||||
ITerm lhs = r.getTerms().get(0);
|
||||
ITerm rhs = r.getTerms().get(1);
|
||||
if (lhs.getKind().equals(ITerm.Kind.CONSTANT) && rhs.getKind().equals(ITerm.Kind.CONSTANT)) {
|
||||
if (lhs instanceof IntConstant && rhs instanceof IntConstant) {
|
||||
IntConstant c1 = (IntConstant) lhs;
|
||||
IntConstant c2 = (IntConstant) rhs;
|
||||
return c1.getVal().intValue() >= c2.getVal().intValue();
|
||||
}
|
||||
}
|
||||
} else if (r.getRelation().equals(BinaryRelation.LE)) {
|
||||
ITerm lhs = r.getTerms().get(0);
|
||||
ITerm rhs = r.getTerms().get(1);
|
||||
if (lhs.getKind().equals(ITerm.Kind.CONSTANT) && rhs.getKind().equals(ITerm.Kind.CONSTANT)) {
|
||||
if (lhs instanceof IntConstant && rhs instanceof IntConstant) {
|
||||
IntConstant c1 = (IntConstant) lhs;
|
||||
IntConstant c2 = (IntConstant) rhs;
|
||||
return c1.getVal().intValue() > c2.getVal().intValue();
|
||||
}
|
||||
}
|
||||
}
|
||||
break;
|
||||
}
|
||||
return false;
|
||||
}
|
||||
|
||||
/**
|
||||
* @param facts
|
||||
* formulae that can be treated as axioms
|
||||
* @return true if we can easily prove f is a tautology
|
||||
* @throws IllegalArgumentException
|
||||
* if facts == null
|
||||
*/
|
||||
private boolean tautology(IFormula f, Collection<IMaxTerm> facts) throws IllegalArgumentException {
|
||||
if (facts == null) {
|
||||
throw new IllegalArgumentException("facts == null");
|
||||
}
|
||||
for (IMaxTerm d : facts) {
|
||||
if (atomicImplies(d, f)) {
|
||||
return true;
|
||||
}
|
||||
}
|
||||
switch (f.getKind()) {
|
||||
case BINARY:
|
||||
AbstractBinaryFormula b = (AbstractBinaryFormula) f;
|
||||
if (b.getConnective().equals(BinaryConnective.AND)) {
|
||||
if (tautology(b.getF1(), facts) && tautology(b.getF2(), facts)) {
|
||||
return true;
|
||||
}
|
||||
}
|
||||
if (b.getConnective().equals(BinaryConnective.OR)) {
|
||||
if (tautology(b.getF1(), facts) || tautology(b.getF2(), facts)) {
|
||||
return true;
|
||||
} else if (b.getF1().equals(normalize(NotFormula.make(b.getF2())))) {
|
||||
return true;
|
||||
}
|
||||
}
|
||||
break;
|
||||
case CONSTANT:
|
||||
return f.equals(BooleanConstantFormula.TRUE);
|
||||
case NEGATION:
|
||||
NotFormula n = (NotFormula) f;
|
||||
return isContradiction(n.getFormula(), facts);
|
||||
case QUANTIFIED:
|
||||
return false;
|
||||
case RELATION:
|
||||
RelationFormula r = (RelationFormula) f;
|
||||
if (r.getRelation().equals(BinaryRelation.EQUALS)) {
|
||||
ITerm lhs = r.getTerms().get(0);
|
||||
ITerm rhs = r.getTerms().get(1);
|
||||
if (lhs.equals(rhs)) {
|
||||
return true;
|
||||
}
|
||||
} else if (r.getRelation().equals(BinaryRelation.NE)) {
|
||||
ITerm lhs = r.getTerms().get(0);
|
||||
ITerm rhs = r.getTerms().get(1);
|
||||
if (lhs.getKind().equals(ITerm.Kind.CONSTANT) && rhs.getKind().equals(ITerm.Kind.CONSTANT)) {
|
||||
if (!lhs.equals(rhs)) {
|
||||
return true;
|
||||
}
|
||||
}
|
||||
} else if (r.getRelation().equals(BinaryRelation.GE)) {
|
||||
ITerm lhs = r.getTerms().get(0);
|
||||
ITerm rhs = r.getTerms().get(1);
|
||||
if (isLE(rhs, lhs)) {
|
||||
return true;
|
||||
}
|
||||
} else if (r.getRelation().equals(BinaryRelation.LT)) {
|
||||
ITerm lhs = r.getTerms().get(0);
|
||||
ITerm rhs = r.getTerms().get(1);
|
||||
if (lhs instanceof IntConstant && rhs instanceof IntConstant) {
|
||||
IntConstant x = (IntConstant) lhs;
|
||||
IntConstant y = (IntConstant) rhs;
|
||||
return x.getVal().intValue() < y.getVal().intValue();
|
||||
}
|
||||
} else if (r.getRelation().equals(BinaryRelation.LE)) {
|
||||
ITerm lhs = r.getTerms().get(0);
|
||||
ITerm rhs = r.getTerms().get(1);
|
||||
if (isLE(lhs, rhs)) {
|
||||
return true;
|
||||
}
|
||||
}
|
||||
break;
|
||||
}
|
||||
return false;
|
||||
}
|
||||
|
||||
/**
|
||||
* do we know a <= b ?
|
||||
*
|
||||
* @return false if no or maybe
|
||||
*/
|
||||
public boolean isLE(ITerm a, ITerm b) {
|
||||
|
||||
if (a.equals(b)) {
|
||||
return true;
|
||||
}
|
||||
|
||||
if (a instanceof IntConstant && b instanceof IntConstant) {
|
||||
IntConstant ac = (IntConstant) a;
|
||||
IntConstant bc = (IntConstant) b;
|
||||
return ac.getVal().intValue() <= bc.getVal().intValue();
|
||||
}
|
||||
if (a instanceof LongConstant && b instanceof LongConstant) {
|
||||
LongConstant ac = (LongConstant) a;
|
||||
LongConstant bc = (LongConstant) b;
|
||||
return ac.getVal().longValue() <= bc.getVal().longValue();
|
||||
}
|
||||
if (a instanceof DoubleConstant && b instanceof DoubleConstant) {
|
||||
DoubleConstant ac = (DoubleConstant) a;
|
||||
DoubleConstant bc = (DoubleConstant) b;
|
||||
return ac.getVal().doubleValue() <= bc.getVal().doubleValue();
|
||||
}
|
||||
if (a instanceof FloatConstant && b instanceof FloatConstant) {
|
||||
FloatConstant ac = (FloatConstant) a;
|
||||
FloatConstant bc = (FloatConstant) b;
|
||||
return ac.getVal().floatValue() <= bc.getVal().floatValue();
|
||||
}
|
||||
|
||||
return false;
|
||||
}
|
||||
|
||||
}
|
||||
|
|
@ -1,37 +0,0 @@
|
|||
/*******************************************************************************
|
||||
* Copyright (c) 2007 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 java.util.Collection;
|
||||
|
||||
public class BasicTheory extends AbstractTheory {
|
||||
|
||||
private final IVocabulary vocab;
|
||||
private final Collection<IFormula> sentences;
|
||||
|
||||
protected BasicTheory(IVocabulary vocab, Collection<IFormula> sentences) {
|
||||
this.vocab = vocab;
|
||||
this.sentences = sentences;
|
||||
}
|
||||
|
||||
public static BasicTheory make(IVocabulary vocab, Collection<IFormula> sentences) {
|
||||
return new BasicTheory(vocab, sentences);
|
||||
}
|
||||
|
||||
public Collection<IFormula> getSentences() {
|
||||
return sentences;
|
||||
}
|
||||
|
||||
public IVocabulary getVocabulary() {
|
||||
return vocab;
|
||||
}
|
||||
|
||||
}
|
||||
|
|
@ -1,71 +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 java.util.Collection;
|
||||
import java.util.Collections;
|
||||
|
||||
/**
|
||||
* A simple class to define a simple vocabulary of functions and relations
|
||||
*
|
||||
* @author sjfink
|
||||
*
|
||||
*/
|
||||
public class BasicVocabulary<T extends IConstant> extends AbstractVocabulary<T> {
|
||||
|
||||
private final Collection<? extends IFunction> functions;
|
||||
|
||||
private final Collection<? extends IRelation> relations;
|
||||
|
||||
private final Collection<AbstractVariable> variables;
|
||||
|
||||
protected BasicVocabulary(final Collection<? extends IFunction> functions, final Collection<? extends IRelation> relations,
|
||||
final Collection<AbstractVariable> variables) {
|
||||
super();
|
||||
this.functions = functions;
|
||||
this.relations = relations;
|
||||
this.variables = variables;
|
||||
}
|
||||
|
||||
public Collection<? extends IFunction> getFunctions() {
|
||||
return Collections.unmodifiableCollection(functions);
|
||||
}
|
||||
|
||||
public Collection<? extends IRelation> getRelations() {
|
||||
return Collections.unmodifiableCollection(relations);
|
||||
}
|
||||
|
||||
public Collection<AbstractVariable> getVariables() {
|
||||
return Collections.unmodifiableCollection(variables);
|
||||
}
|
||||
|
||||
public static <T extends IConstant> BasicVocabulary<T> make(IFunction f) {
|
||||
Collection<IRelation> empty = Collections.emptySet();
|
||||
Collection<AbstractVariable> emptyV = Collections.emptySet();
|
||||
return new BasicVocabulary<T>(Collections.singleton(f), empty, emptyV);
|
||||
}
|
||||
|
||||
public static <T extends IConstant> BasicVocabulary<T> make(Collection<IFunction> f) {
|
||||
Collection<IRelation> empty = Collections.emptySet();
|
||||
Collection<AbstractVariable> emptyV = Collections.emptySet();
|
||||
return new BasicVocabulary<T>(f, empty, emptyV);
|
||||
}
|
||||
|
||||
public static <T extends IConstant> BasicVocabulary<T> make(Collection<? extends IFunction> f, Collection<IRelation> r) {
|
||||
Collection<AbstractVariable> emptyV = Collections.emptySet();
|
||||
return new BasicVocabulary<T>(f, r, emptyV);
|
||||
}
|
||||
|
||||
public Collection<T> getConstants() {
|
||||
return Collections.emptySet();
|
||||
}
|
||||
|
||||
}
|
||||
|
|
@ -1,192 +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 java.util.ArrayList;
|
||||
import java.util.Collection;
|
||||
import java.util.Iterator;
|
||||
|
||||
import com.ibm.wala.logic.ILogicConstants.BinaryConnective;
|
||||
import com.ibm.wala.util.collections.HashSetFactory;
|
||||
|
||||
public class BinaryFormula extends AbstractBinaryFormula {
|
||||
private final IFormula f1;
|
||||
|
||||
private final IFormula f2;
|
||||
|
||||
private final BinaryConnective b;
|
||||
|
||||
private BinaryFormula(BinaryConnective b, IFormula f1, IFormula f2) {
|
||||
super();
|
||||
this.b = b;
|
||||
this.f1 = f1;
|
||||
this.f2 = f2;
|
||||
}
|
||||
|
||||
public static IFormula and(Collection<IFormula> clauses) throws IllegalArgumentException {
|
||||
if (clauses == null) {
|
||||
throw new IllegalArgumentException("clauses is null");
|
||||
}
|
||||
if (clauses.isEmpty()) {
|
||||
throw new IllegalArgumentException("cannot and empty collection");
|
||||
}
|
||||
Iterator<IFormula> it = clauses.iterator();
|
||||
IFormula result = it.next();
|
||||
while (it.hasNext()) {
|
||||
result = and(result, it.next());
|
||||
}
|
||||
return result;
|
||||
}
|
||||
|
||||
public static IFormula and(IFormula f1, IFormula f2) throws IllegalArgumentException {
|
||||
if (f1 == null) {
|
||||
throw new IllegalArgumentException("f1 == null");
|
||||
}
|
||||
if (f1.equals(BooleanConstantFormula.TRUE)) {
|
||||
return f2;
|
||||
} else if (f2.equals(BooleanConstantFormula.TRUE)) {
|
||||
return f1;
|
||||
} else if (f1.equals(BooleanConstantFormula.FALSE) || f2.equals(BooleanConstantFormula.FALSE)) {
|
||||
return BooleanConstantFormula.FALSE;
|
||||
} else {
|
||||
if (f1 instanceof IMaxTerm && f2 instanceof IMaxTerm) {
|
||||
Collection<IMaxTerm> c = new ArrayList<IMaxTerm>(2);
|
||||
c.add((IMaxTerm) f1);
|
||||
c.add((IMaxTerm) f2);
|
||||
return CNFFormula.make(c);
|
||||
} else if (f1 instanceof ICNFFormula && f2 instanceof IMaxTerm) {
|
||||
return CNFFormula.make((ICNFFormula) f1, (IMaxTerm) f2);
|
||||
} else if (f1 instanceof IMaxTerm && f2 instanceof ICNFFormula) {
|
||||
return CNFFormula.make((ICNFFormula) f2, (IMaxTerm) f1);
|
||||
} else if (f1 instanceof ICNFFormula && f2 instanceof ICNFFormula) {
|
||||
return CNFFormula.make((ICNFFormula) f1, (ICNFFormula) f2);
|
||||
}else {
|
||||
return new BinaryFormula(BinaryConnective.AND, f1, f2);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
public static BinaryFormula biconditional(IFormula f1, IFormula f2) {
|
||||
return new BinaryFormula(BinaryConnective.BICONDITIONAL, f1, f2);
|
||||
}
|
||||
|
||||
public static IFormula make(BinaryConnective connective, IFormula f1, IFormula f2) {
|
||||
if (connective.equals(BinaryConnective.AND)) {
|
||||
return and(f1, f2);
|
||||
} else {
|
||||
return new BinaryFormula(connective, f1, f2);
|
||||
}
|
||||
}
|
||||
|
||||
public static IFormula or(IFormula f1, IFormula f2) throws IllegalArgumentException {
|
||||
if (f1 == null) {
|
||||
throw new IllegalArgumentException("f1 == null");
|
||||
}
|
||||
if (f1.equals(BooleanConstantFormula.FALSE)) {
|
||||
return f2;
|
||||
} else if (f2.equals(BooleanConstantFormula.FALSE)) {
|
||||
return f1;
|
||||
} else if (f1.equals(BooleanConstantFormula.TRUE) || f2.equals(BooleanConstantFormula.TRUE)) {
|
||||
return BooleanConstantFormula.TRUE;
|
||||
} else {
|
||||
return new BinaryFormula(BinaryConnective.OR, f1, f2);
|
||||
}
|
||||
}
|
||||
|
||||
public static BinaryFormula implies(IFormula f1, IFormula f2) {
|
||||
return new BinaryFormula(BinaryConnective.IMPLIES, f1, f2);
|
||||
}
|
||||
|
||||
@Override
|
||||
public BinaryConnective getConnective() {
|
||||
return b;
|
||||
}
|
||||
|
||||
@Override
|
||||
public IFormula getF1() {
|
||||
return f1;
|
||||
}
|
||||
|
||||
@Override
|
||||
public IFormula getF2() {
|
||||
return f2;
|
||||
}
|
||||
|
||||
public Collection<AbstractVariable> getFreeVariables() {
|
||||
Collection<AbstractVariable> result = HashSetFactory.make();
|
||||
result.addAll(f1.getFreeVariables());
|
||||
result.addAll(f2.getFreeVariables());
|
||||
return result;
|
||||
}
|
||||
|
||||
public Collection<? extends ITerm> getAllTerms() {
|
||||
Collection<ITerm> result = HashSetFactory.make();
|
||||
result.addAll(f1.getAllTerms());
|
||||
result.addAll(f2.getAllTerms());
|
||||
return result;
|
||||
}
|
||||
|
||||
public Collection<IConstant> getConstants() {
|
||||
Collection<IConstant> result = HashSetFactory.make();
|
||||
result.addAll(f1.getConstants());
|
||||
result.addAll(f2.getConstants());
|
||||
return result;
|
||||
}
|
||||
|
||||
public String prettyPrint(ILogicDecorator d) throws IllegalArgumentException {
|
||||
if (d == null) {
|
||||
throw new IllegalArgumentException("d == null");
|
||||
}
|
||||
return d.prettyPrint(this);
|
||||
}
|
||||
|
||||
@Override
|
||||
public String toString() {
|
||||
return prettyPrint(DefaultDecorator.instance());
|
||||
}
|
||||
|
||||
@Override
|
||||
public int hashCode() {
|
||||
final int PRIME = 31;
|
||||
int result = 1;
|
||||
result = PRIME * result + ((b == null) ? 0 : b.hashCode());
|
||||
result = PRIME * result + ((f1 == null) ? 0 : f1.hashCode());
|
||||
result = PRIME * result + ((f2 == null) ? 0 : f2.hashCode());
|
||||
return result;
|
||||
}
|
||||
|
||||
@Override
|
||||
public boolean equals(Object obj) {
|
||||
if (this == obj)
|
||||
return true;
|
||||
if (obj == null)
|
||||
return false;
|
||||
if (getClass() != obj.getClass())
|
||||
return false;
|
||||
final BinaryFormula other = (BinaryFormula) obj;
|
||||
if (b == null) {
|
||||
if (other.b != null)
|
||||
return false;
|
||||
} else if (!b.equals(other.b))
|
||||
return false;
|
||||
if (f1 == null) {
|
||||
if (other.f1 != null)
|
||||
return false;
|
||||
} else if (!f1.equals(other.f1))
|
||||
return false;
|
||||
if (f2 == null) {
|
||||
if (other.f2 != null)
|
||||
return false;
|
||||
} else if (!f2.equals(other.f2))
|
||||
return false;
|
||||
return true;
|
||||
}
|
||||
}
|
||||
|
|
@ -1,64 +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;
|
||||
|
||||
|
||||
public class BinaryFunction implements IFunction {
|
||||
|
||||
private final String symbol;
|
||||
|
||||
protected BinaryFunction(String symbol) {
|
||||
this.symbol = symbol;
|
||||
}
|
||||
|
||||
public static BinaryFunction make(String symbol) {
|
||||
return new BinaryFunction(symbol);
|
||||
}
|
||||
|
||||
public int getNumberOfParameters() {
|
||||
return 2;
|
||||
}
|
||||
|
||||
public String getSymbol() {
|
||||
return symbol;
|
||||
}
|
||||
|
||||
@Override
|
||||
public String toString() {
|
||||
return getSymbol() + " : int x int -> int";
|
||||
}
|
||||
|
||||
@Override
|
||||
public int hashCode() {
|
||||
final int prime = 31;
|
||||
int result = 1;
|
||||
result = prime * result + ((symbol == null) ? 0 : symbol.hashCode());
|
||||
return result;
|
||||
}
|
||||
|
||||
@Override
|
||||
public boolean equals(Object obj) {
|
||||
if (this == obj)
|
||||
return true;
|
||||
if (obj == null)
|
||||
return false;
|
||||
if (getClass() != obj.getClass())
|
||||
return false;
|
||||
final BinaryFunction other = (BinaryFunction) obj;
|
||||
if (symbol == null) {
|
||||
if (other.symbol != null)
|
||||
return false;
|
||||
} else if (!symbol.equals(other.symbol))
|
||||
return false;
|
||||
return true;
|
||||
}
|
||||
|
||||
}
|
||||
|
|
@ -1,112 +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 java.util.Map;
|
||||
|
||||
import com.ibm.wala.util.collections.HashMapFactory;
|
||||
|
||||
public class BinaryRelation implements IRelation {
|
||||
|
||||
public final static BinaryRelation EQUALS = new BinaryRelation("=");
|
||||
|
||||
public final static BinaryRelation NE = new BinaryRelation("/=");
|
||||
|
||||
public final static BinaryRelation LT = new BinaryRelation("<");
|
||||
|
||||
public final static BinaryRelation LE = new BinaryRelation("<=");
|
||||
|
||||
public final static BinaryRelation GT = new BinaryRelation(">");
|
||||
|
||||
public final static BinaryRelation GE = new BinaryRelation(">=");
|
||||
|
||||
private final static Map<BinaryRelation, BinaryRelation> negations = HashMapFactory.make();
|
||||
static {
|
||||
negations.put(EQUALS, NE);
|
||||
negations.put(NE, EQUALS);
|
||||
negations.put(LT, GE);
|
||||
negations.put(GE, LT);
|
||||
negations.put(GT, LE);
|
||||
negations.put(LE, GT);
|
||||
}
|
||||
|
||||
private final static Map<BinaryRelation, BinaryRelation> swap = HashMapFactory.make();
|
||||
static {
|
||||
swap.put(LT, GT);
|
||||
swap.put(GE, LE);
|
||||
swap.put(GT, LT);
|
||||
swap.put(LE, GE);
|
||||
}
|
||||
|
||||
private final String symbol;
|
||||
|
||||
protected BinaryRelation(String symbol) {
|
||||
this.symbol = symbol;
|
||||
}
|
||||
|
||||
public int getValence() {
|
||||
return 2;
|
||||
}
|
||||
|
||||
@Override
|
||||
public String toString() {
|
||||
return getSymbol() + " : int x int";
|
||||
}
|
||||
|
||||
@Override
|
||||
public int hashCode() {
|
||||
final int PRIME = 31;
|
||||
int result = 1;
|
||||
result = PRIME * result + ((symbol == null) ? 0 : symbol.hashCode());
|
||||
return result;
|
||||
}
|
||||
|
||||
@Override
|
||||
public boolean equals(Object obj) {
|
||||
if (this == obj)
|
||||
return true;
|
||||
if (obj == null)
|
||||
return false;
|
||||
if (getClass() != obj.getClass())
|
||||
return false;
|
||||
final BinaryRelation other = (BinaryRelation) obj;
|
||||
if (symbol == null) {
|
||||
if (other.symbol != null)
|
||||
return false;
|
||||
} else if (!symbol.equals(other.symbol))
|
||||
return false;
|
||||
return true;
|
||||
}
|
||||
|
||||
public String getSymbol() {
|
||||
return symbol;
|
||||
}
|
||||
|
||||
public static BinaryRelation make(String symbol) {
|
||||
return new BinaryRelation(symbol);
|
||||
}
|
||||
|
||||
/**
|
||||
* Attempt to negate a relation symbol. Return null if unsuccessful.
|
||||
*/
|
||||
public static BinaryRelation negate(IRelation relation) {
|
||||
return negations.get(relation);
|
||||
}
|
||||
|
||||
/**
|
||||
* Return the relation which is the "swap" of the original relation. Return
|
||||
* null if unsuccessful.
|
||||
*/
|
||||
public static BinaryRelation swap(IRelation relation) {
|
||||
return swap.get(relation);
|
||||
}
|
||||
|
||||
}
|
||||
|
|
@ -1,41 +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;
|
||||
|
||||
|
||||
public class BooleanConstant extends AbstractConstant {
|
||||
|
||||
public static final BooleanConstant TRUE = new BooleanConstant(true);
|
||||
public static final BooleanConstant FALSE = new BooleanConstant(false);
|
||||
|
||||
final private boolean val;
|
||||
|
||||
private BooleanConstant(boolean val) {
|
||||
this.val = val;
|
||||
}
|
||||
|
||||
@Override
|
||||
public String toString() {
|
||||
return Boolean.toString(val);
|
||||
}
|
||||
|
||||
@Override
|
||||
public boolean equals(Object obj) {
|
||||
// note that these are canonical
|
||||
return this == obj;
|
||||
}
|
||||
|
||||
@Override
|
||||
public int hashCode() {
|
||||
return val ? 11 : 13;
|
||||
}
|
||||
|
||||
}
|
||||
|
|
@ -1,76 +0,0 @@
|
|||
/*******************************************************************************
|
||||
* Copyright (c) 2007 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 java.util.Collection;
|
||||
import java.util.Collections;
|
||||
|
||||
public class BooleanConstantFormula implements IMaxTerm {
|
||||
|
||||
public static final BooleanConstantFormula TRUE = new BooleanConstantFormula(BooleanConstant.TRUE);
|
||||
|
||||
public static final BooleanConstantFormula FALSE = new BooleanConstantFormula(BooleanConstant.FALSE);
|
||||
|
||||
private final BooleanConstant c;
|
||||
|
||||
private BooleanConstantFormula(BooleanConstant c) {
|
||||
this.c = c;
|
||||
}
|
||||
|
||||
public Collection<AbstractVariable> getFreeVariables() {
|
||||
return Collections.emptySet();
|
||||
}
|
||||
|
||||
public Collection<? extends IConstant> getConstants() {
|
||||
Collection<? extends IConstant> result = Collections.singleton(c);
|
||||
return result;
|
||||
}
|
||||
|
||||
public Collection<? extends ITerm> getTerms() {
|
||||
return getConstants();
|
||||
}
|
||||
|
||||
public Kind getKind() {
|
||||
return Kind.CONSTANT;
|
||||
}
|
||||
|
||||
@Override
|
||||
public String toString() {
|
||||
return prettyPrint(DefaultDecorator.instance());
|
||||
}
|
||||
|
||||
public String prettyPrint(ILogicDecorator d) throws IllegalArgumentException {
|
||||
if (d == null) {
|
||||
throw new IllegalArgumentException("d == null");
|
||||
}
|
||||
return d.prettyPrint(c);
|
||||
}
|
||||
|
||||
@Override
|
||||
public boolean equals(Object obj) {
|
||||
// note that these are canonical
|
||||
return this == obj;
|
||||
}
|
||||
|
||||
@Override
|
||||
public int hashCode() {
|
||||
return 163 * c.hashCode();
|
||||
}
|
||||
|
||||
public Collection<? extends ITerm> getAllTerms() {
|
||||
return Collections.singleton(c);
|
||||
}
|
||||
|
||||
public Collection<? extends IMaxTerm> getMaxTerms() {
|
||||
return Collections.singleton(this);
|
||||
}
|
||||
|
||||
}
|
||||
|
|
@ -1,442 +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 java.util.Collection;
|
||||
import java.util.Collections;
|
||||
|
||||
import com.ibm.wala.logic.ILogicConstants.BinaryConnective;
|
||||
import com.ibm.wala.util.collections.HashSetFactory;
|
||||
import com.ibm.wala.util.debug.Assertions;
|
||||
|
||||
/**
|
||||
* A formula in conjunctive normal form.
|
||||
*
|
||||
* @author sjfink
|
||||
*/
|
||||
public class CNFFormula extends AbstractBinaryFormula implements ICNFFormula {
|
||||
|
||||
private static final boolean DEBUG = false;
|
||||
|
||||
// invariant: size >= 2
|
||||
final Collection<? extends IMaxTerm> maxTerms;
|
||||
|
||||
private CNFFormula(Collection<? extends IMaxTerm> maxTerms) {
|
||||
assert maxTerms.size() >= 2;
|
||||
this.maxTerms = maxTerms;
|
||||
}
|
||||
|
||||
private CNFFormula(IMaxTerm single) {
|
||||
this.maxTerms = Collections.singleton(single);
|
||||
}
|
||||
|
||||
public Collection<? extends IConstant> getConstants() {
|
||||
Collection<IConstant> result = HashSetFactory.make();
|
||||
for (IFormula f : maxTerms) {
|
||||
result.addAll(f.getConstants());
|
||||
}
|
||||
return result;
|
||||
}
|
||||
|
||||
public Collection<? extends ITerm> getAllTerms() {
|
||||
Collection<ITerm> result = HashSetFactory.make();
|
||||
for (IFormula f : maxTerms) {
|
||||
result.addAll(f.getAllTerms());
|
||||
}
|
||||
return result;
|
||||
}
|
||||
|
||||
public Collection<AbstractVariable> getFreeVariables() {
|
||||
Collection<AbstractVariable> result = HashSetFactory.make();
|
||||
for (IFormula f : maxTerms) {
|
||||
result.addAll(f.getFreeVariables());
|
||||
}
|
||||
return result;
|
||||
}
|
||||
|
||||
public String prettyPrint(ILogicDecorator d) throws IllegalArgumentException {
|
||||
if (d == null) {
|
||||
throw new IllegalArgumentException("d == null");
|
||||
}
|
||||
return d.prettyPrint(this);
|
||||
}
|
||||
|
||||
public static ICNFFormula make(IFormula f) throws IllegalArgumentException {
|
||||
if (f == null) {
|
||||
throw new IllegalArgumentException("f == null");
|
||||
}
|
||||
if (DEBUG) {
|
||||
System.err.println("make CNF " + f);
|
||||
}
|
||||
if (f instanceof ICNFFormula) {
|
||||
return (ICNFFormula) f;
|
||||
} else {
|
||||
switch (f.getKind()) {
|
||||
case RELATION:
|
||||
case QUANTIFIED:
|
||||
case CONSTANT:
|
||||
return (IMaxTerm) f;
|
||||
case BINARY:
|
||||
case NEGATION: {
|
||||
f = trivialCleanup(f);
|
||||
if (DEBUG) {
|
||||
System.err.println("after trivial cleanup " + f);
|
||||
}
|
||||
|
||||
f = eliminateArrows(f);
|
||||
if (DEBUG) {
|
||||
System.err.println("after eliminate arrows " + f);
|
||||
}
|
||||
|
||||
f = pushNegations(f);
|
||||
if (DEBUG) {
|
||||
System.err.println("after pushNegations " + f);
|
||||
}
|
||||
|
||||
f = distribute(f);
|
||||
if (DEBUG) {
|
||||
System.err.println("after distribute " + f);
|
||||
}
|
||||
|
||||
if (f instanceof AbstractBinaryFormula || f instanceof NotFormula) {
|
||||
Collection<IMaxTerm> c = collectMaxTerms(f);
|
||||
c.remove(BooleanConstantFormula.TRUE);
|
||||
return CNFFormula.make(c);
|
||||
} else {
|
||||
return CNFFormula.make(f);
|
||||
}
|
||||
}
|
||||
default:
|
||||
Assertions.UNREACHABLE(f + " " + f.getKind());
|
||||
return null;
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
private static Collection<IMaxTerm> collectMaxTerms(IFormula f) {
|
||||
switch (f.getKind()) {
|
||||
case CONSTANT:
|
||||
case QUANTIFIED:
|
||||
case RELATION:
|
||||
return Collections.singleton((IMaxTerm) f);
|
||||
case BINARY:
|
||||
AbstractBinaryFormula b = (AbstractBinaryFormula) f;
|
||||
if (b.getConnective().equals(BinaryConnective.AND)) {
|
||||
Collection<IMaxTerm> result = HashSetFactory.make();
|
||||
result.addAll(collectMaxTerms(b.getF1()));
|
||||
result.addAll(collectMaxTerms(b.getF2()));
|
||||
return result;
|
||||
} else if (b.getConnective().equals(BinaryConnective.OR)) {
|
||||
return Collections.singleton(orToMaxTerm(b));
|
||||
} else {
|
||||
Assertions.UNREACHABLE();
|
||||
return null;
|
||||
}
|
||||
case NEGATION:
|
||||
NotFormula n = (NotFormula) f;
|
||||
if (n.getFormula() instanceof RelationFormula) {
|
||||
IMaxTerm t = NotFormulaMaxTerm.createNotFormulaMaxTerm((RelationFormula)n.getFormula());
|
||||
return Collections.singleton(t);
|
||||
} else {
|
||||
// should not get here if other logic is working.
|
||||
Assertions.UNREACHABLE(n.getFormula());
|
||||
return null;
|
||||
}
|
||||
default:
|
||||
Assertions.UNREACHABLE(f);
|
||||
return null;
|
||||
}
|
||||
}
|
||||
|
||||
private static IMaxTerm orToMaxTerm(AbstractBinaryFormula b) {
|
||||
assert b.getConnective().equals(BinaryConnective.OR);
|
||||
Collection<IMaxTerm> clauses = HashSetFactory.make();
|
||||
clauses.addAll(collectMaxTerms(b.getF1()));
|
||||
clauses.addAll(collectMaxTerms(b.getF2()));
|
||||
if (clauses.size() == 1) {
|
||||
return clauses.iterator().next();
|
||||
} else {
|
||||
return Disjunction.make(clauses);
|
||||
}
|
||||
}
|
||||
|
||||
private static IFormula trivialCleanup(IFormula f) {
|
||||
if (AdHocSemiDecisionProcedure.singleton().isTautology(f)) {
|
||||
return BooleanConstantFormula.TRUE;
|
||||
} else if (AdHocSemiDecisionProcedure.singleton().isContradiction(f)) {
|
||||
return BooleanConstantFormula.FALSE;
|
||||
} else {
|
||||
switch (f.getKind()) {
|
||||
case BINARY:
|
||||
AbstractBinaryFormula b = (AbstractBinaryFormula) f;
|
||||
return BinaryFormula.make(b.getConnective(), trivialCleanup(b.getF1()), trivialCleanup(b.getF2()));
|
||||
case RELATION:
|
||||
RelationFormula r = (RelationFormula) f;
|
||||
if (r.getRelation().equals(BinaryRelation.NE)) {
|
||||
if (r.getTerms().get(1).equals(BooleanConstant.FALSE)) {
|
||||
return RelationFormula.makeEquals(r.getTerms().get(0), BooleanConstant.TRUE);
|
||||
}
|
||||
}
|
||||
return f;
|
||||
case CONSTANT:
|
||||
case NEGATION:
|
||||
case QUANTIFIED:
|
||||
default:
|
||||
return f;
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
/**
|
||||
* move all conjunctions outside disjunctions using distributive laws.
|
||||
*
|
||||
* (a AND b) OR c -> (a OR c) AND (b OR c)
|
||||
*
|
||||
* a OR (b AND c) -> (a OR b) AND (a OR c)
|
||||
*/
|
||||
private static IFormula distribute(IFormula f) {
|
||||
switch (f.getKind()) {
|
||||
case BINARY:
|
||||
return distribute((AbstractBinaryFormula) f);
|
||||
case CONSTANT:
|
||||
case QUANTIFIED:
|
||||
case RELATION:
|
||||
case NEGATION:
|
||||
return f;
|
||||
default:
|
||||
Assertions.UNREACHABLE(f.getKind());
|
||||
return null;
|
||||
}
|
||||
}
|
||||
|
||||
/**
|
||||
* move all conjunctions outside disjunctions using distributive laws.
|
||||
*
|
||||
* (a AND b) OR c -> (a OR c) AND (b OR c)
|
||||
*
|
||||
* a OR (b AND c) -> (a OR b) AND (a OR c)
|
||||
*/
|
||||
private static IFormula distribute(AbstractBinaryFormula b) {
|
||||
IFormula f1 = b.getF1();
|
||||
IFormula f2 = b.getF2();
|
||||
f1 = distribute(f1);
|
||||
f2 = distribute(f2);
|
||||
switch (b.getConnective()) {
|
||||
case OR:
|
||||
if (f1 instanceof AbstractBinaryFormula && ((AbstractBinaryFormula) f1).getConnective().equals(BinaryConnective.AND)) {
|
||||
AbstractBinaryFormula c1 = (AbstractBinaryFormula) f1;
|
||||
IFormula af = c1.getF1();
|
||||
IFormula bf = c1.getF2();
|
||||
IFormula x = BinaryFormula.and(BinaryFormula.or(af, f2), BinaryFormula.or(bf, f2));
|
||||
// distribute again; case 2 may apply
|
||||
return distribute(x);
|
||||
}
|
||||
if (f2 instanceof AbstractBinaryFormula && ((AbstractBinaryFormula) f2).getConnective().equals(BinaryConnective.AND)) {
|
||||
AbstractBinaryFormula c2 = (AbstractBinaryFormula) f2;
|
||||
IFormula bf = c2.getF1();
|
||||
IFormula cf = c2.getF2();
|
||||
IFormula x = BinaryFormula.and(BinaryFormula.or(f1, bf), BinaryFormula.or(f1, cf));
|
||||
// distribute again; case 1 may apply now
|
||||
return distribute(x);
|
||||
}
|
||||
return BinaryFormula.make(b.getConnective(), f1, f2);
|
||||
case AND:
|
||||
return BinaryFormula.make(b.getConnective(), f1, f2);
|
||||
case BICONDITIONAL:
|
||||
case IMPLIES:
|
||||
default:
|
||||
Assertions.UNREACHABLE(b.getConnective());
|
||||
return null;
|
||||
}
|
||||
}
|
||||
|
||||
/**
|
||||
* push NOT operators into the formula using double complement and De Morgan's
|
||||
* laws.
|
||||
*/
|
||||
private static IFormula pushNegations(IFormula f) {
|
||||
switch (f.getKind()) {
|
||||
case BINARY:
|
||||
AbstractBinaryFormula b = (AbstractBinaryFormula) f;
|
||||
IFormula f1 = b.getF1();
|
||||
IFormula f2 = b.getF2();
|
||||
f1 = pushNegations(f1);
|
||||
f2 = pushNegations(f2);
|
||||
return BinaryFormula.make(b.getConnective(), f1, f2);
|
||||
case CONSTANT:
|
||||
case RELATION:
|
||||
case QUANTIFIED:
|
||||
return f;
|
||||
case NEGATION:
|
||||
NotFormula n = (NotFormula) f;
|
||||
return Simplifier.distributeNot(n);
|
||||
default:
|
||||
return null;
|
||||
}
|
||||
}
|
||||
|
||||
/**
|
||||
* eliminate all IMPLIES and BICONDITIONALS
|
||||
*/
|
||||
private static IFormula eliminateArrows(IFormula f) {
|
||||
switch (f.getKind()) {
|
||||
case BINARY:
|
||||
AbstractBinaryFormula b = (AbstractBinaryFormula) f;
|
||||
return eliminateArrows(b);
|
||||
case CONSTANT:
|
||||
case RELATION:
|
||||
case QUANTIFIED:
|
||||
return f;
|
||||
case NEGATION:
|
||||
NotFormula n = (NotFormula) f;
|
||||
return NotFormula.make(eliminateArrows(n.getFormula()));
|
||||
default:
|
||||
Assertions.UNREACHABLE(f.getKind());
|
||||
return null;
|
||||
}
|
||||
}
|
||||
|
||||
/**
|
||||
* eliminate all IMPLIES and BICONDITIONALS
|
||||
*/
|
||||
private static IFormula eliminateArrows(AbstractBinaryFormula b) {
|
||||
IFormula f1 = b.getF1();
|
||||
IFormula f2 = b.getF2();
|
||||
f1 = eliminateArrows(f1);
|
||||
f2 = eliminateArrows(f2);
|
||||
|
||||
switch (b.getConnective()) {
|
||||
case BICONDITIONAL:
|
||||
if (AdHocSemiDecisionProcedure.singleton().isTautology(f1)) {
|
||||
return f2;
|
||||
} else if (AdHocSemiDecisionProcedure.singleton().isContradiction(f1)) {
|
||||
return BooleanConstantFormula.TRUE;
|
||||
} else {
|
||||
IFormula not1 = NotFormula.make(f1);
|
||||
IFormula not2 = NotFormula.make(f2);
|
||||
return BinaryFormula.or(BinaryFormula.and(f1, f2), BinaryFormula.and(not1, not2));
|
||||
}
|
||||
case AND:
|
||||
case OR:
|
||||
return BinaryFormula.make(b.getConnective(), f1, f2);
|
||||
case IMPLIES:
|
||||
return BinaryFormula.or(NotFormula.make(f1), f2);
|
||||
default:
|
||||
Assertions.UNREACHABLE(b);
|
||||
return null;
|
||||
}
|
||||
}
|
||||
|
||||
@Override
|
||||
public int hashCode() {
|
||||
final int prime = 31;
|
||||
int result = 1;
|
||||
result = prime * result + ((maxTerms == null) ? 0 : maxTerms.hashCode());
|
||||
return result;
|
||||
}
|
||||
|
||||
@Override
|
||||
public boolean equals(Object obj) {
|
||||
if (this == obj)
|
||||
return true;
|
||||
if (obj == null)
|
||||
return false;
|
||||
if (getClass() != obj.getClass())
|
||||
return false;
|
||||
final CNFFormula other = (CNFFormula) obj;
|
||||
if (maxTerms == null) {
|
||||
if (other.maxTerms != null)
|
||||
return false;
|
||||
} else if (!maxTerms.equals(other.maxTerms))
|
||||
return false;
|
||||
return true;
|
||||
}
|
||||
|
||||
@Override
|
||||
public BinaryConnective getConnective() {
|
||||
return BinaryConnective.AND;
|
||||
}
|
||||
|
||||
@Override
|
||||
public IFormula getF1() {
|
||||
return maxTerms.iterator().next();
|
||||
}
|
||||
|
||||
@Override
|
||||
public IFormula getF2() {
|
||||
Collection<? extends IMaxTerm> c = HashSetFactory.make(maxTerms);
|
||||
c.remove(getF1());
|
||||
return CNFFormula.make(c);
|
||||
}
|
||||
|
||||
@Override
|
||||
public String toString() {
|
||||
StringBuffer result = new StringBuffer("CNF\n");
|
||||
int i = 1;
|
||||
for (IMaxTerm t : getMaxTerms()) {
|
||||
result.append(" (" + i + ") " + t.prettyPrint(DefaultDecorator.instance()) + "\n");
|
||||
i++;
|
||||
}
|
||||
return result.toString();
|
||||
}
|
||||
|
||||
public Collection<IMaxTerm> getMaxTerms() {
|
||||
return Collections.unmodifiableCollection(maxTerms);
|
||||
}
|
||||
|
||||
public static ICNFFormula make(Collection<? extends IMaxTerm> d) {
|
||||
Collection<IMaxTerm> c = HashSetFactory.make();
|
||||
for (IMaxTerm x : d) {
|
||||
c.add(normalize(x));
|
||||
}
|
||||
c.remove(BooleanConstantFormula.TRUE);
|
||||
if (c.size() == 0) {
|
||||
return BooleanConstantFormula.TRUE;
|
||||
} else if (c.size() == 1) {
|
||||
return c.iterator().next();
|
||||
} else {
|
||||
return new CNFFormula(c);
|
||||
}
|
||||
}
|
||||
|
||||
public static IFormula make(ICNFFormula cnf, IMaxTerm t) {
|
||||
Collection<IMaxTerm> c = HashSetFactory.make();
|
||||
c.addAll(cnf.getMaxTerms());
|
||||
c.add(t);
|
||||
return make(c);
|
||||
}
|
||||
|
||||
public static IFormula make(ICNFFormula f1, ICNFFormula f2) {
|
||||
Collection<IMaxTerm> c = HashSetFactory.make();
|
||||
c.addAll(f1.getMaxTerms());
|
||||
c.addAll(f2.getMaxTerms());
|
||||
return make(c);
|
||||
}
|
||||
|
||||
// TODO: move this to Simplifier?
|
||||
public static IMaxTerm normalize(IMaxTerm f) throws IllegalArgumentException {
|
||||
if (f == null) {
|
||||
throw new IllegalArgumentException("f == null");
|
||||
}
|
||||
switch (f.getKind()) {
|
||||
case RELATION:
|
||||
RelationFormula r = (RelationFormula) f;
|
||||
if (r.getRelation().equals(BinaryRelation.GE) || r.getRelation().equals(BinaryRelation.GT)) {
|
||||
BinaryRelation swap = BinaryRelation.swap(r.getRelation());
|
||||
return RelationFormula.make(swap, r.getTerms().get(1), r.getTerms().get(0));
|
||||
}
|
||||
return f;
|
||||
default:
|
||||
return f;
|
||||
}
|
||||
}
|
||||
|
||||
}
|
||||
|
|
@ -1,86 +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 java.util.Collection;
|
||||
import java.util.Collections;
|
||||
import java.util.Set;
|
||||
|
||||
import com.ibm.wala.util.collections.HashSetFactory;
|
||||
|
||||
/**
|
||||
* The union of two theories.
|
||||
*
|
||||
* @author sjfink
|
||||
*/
|
||||
public class CombinedTheory extends AbstractTheory {
|
||||
|
||||
private final ITheory a;
|
||||
|
||||
private final ITheory b;
|
||||
|
||||
private CombinedTheory(ITheory a, ITheory b) {
|
||||
this.a = a;
|
||||
this.b = b;
|
||||
}
|
||||
|
||||
public static CombinedTheory make(ITheory a, ITheory b) throws IllegalArgumentException {
|
||||
if (a == null) {
|
||||
throw new IllegalArgumentException("a cannot be null");
|
||||
}
|
||||
if (b == null) {
|
||||
throw new IllegalArgumentException("b cannot be null");
|
||||
}
|
||||
return new CombinedTheory(a, b);
|
||||
}
|
||||
|
||||
public Collection<IFormula> getSentences() {
|
||||
Set<IFormula> union = HashSetFactory.make();
|
||||
union.addAll(a.getSentences());
|
||||
union.addAll(b.getSentences());
|
||||
return union;
|
||||
}
|
||||
|
||||
@Override
|
||||
public Collection<? extends IFormula> getSentencesRelevantToConstraints(Collection<? extends IFormula> constraints) {
|
||||
Set<IFormula> union = HashSetFactory.make();
|
||||
union.addAll(a.getSentencesRelevantToConstraints(constraints));
|
||||
union.addAll(b.getSentencesRelevantToConstraints(constraints));
|
||||
return union;
|
||||
}
|
||||
|
||||
public IVocabulary getVocabulary() {
|
||||
return CombinedVocabulary.make(a.getVocabulary(), b.getVocabulary());
|
||||
}
|
||||
|
||||
public static ITheory make(ITheory t, IVocabulary<?> v) {
|
||||
return make(t, new JustVocabulary(v));
|
||||
}
|
||||
|
||||
private final static class JustVocabulary extends AbstractTheory {
|
||||
|
||||
private final IVocabulary v;
|
||||
|
||||
public JustVocabulary(IVocabulary v) {
|
||||
this.v = v;
|
||||
}
|
||||
|
||||
public Collection<IFormula> getSentences() {
|
||||
return Collections.emptySet();
|
||||
}
|
||||
|
||||
public IVocabulary getVocabulary() {
|
||||
return v;
|
||||
}
|
||||
|
||||
}
|
||||
|
||||
}
|
||||
|
|
@ -1,73 +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 java.util.Collection;
|
||||
|
||||
import com.ibm.wala.util.collections.HashSetFactory;
|
||||
|
||||
public class CombinedVocabulary extends AbstractVocabulary<IConstant> {
|
||||
|
||||
private final IVocabulary a;
|
||||
private final IVocabulary b;
|
||||
|
||||
private CombinedVocabulary(IVocabulary a, IVocabulary b) {
|
||||
this.a = a;
|
||||
this.b = b;
|
||||
if (b.getRelations() == null) {
|
||||
throw new IllegalArgumentException("b relations are null " + b.getClass());
|
||||
}
|
||||
}
|
||||
|
||||
public static CombinedVocabulary make(IVocabulary a, IVocabulary b) throws IllegalArgumentException {
|
||||
if (b == null) {
|
||||
throw new IllegalArgumentException("b == null");
|
||||
}
|
||||
return new CombinedVocabulary(a,b);
|
||||
}
|
||||
|
||||
|
||||
@SuppressWarnings("unchecked")
|
||||
public Collection<? extends IFunction> getFunctions() {
|
||||
Collection<? extends IFunction> s = HashSetFactory.make();
|
||||
s.addAll(a.getFunctions());
|
||||
s.addAll(b.getFunctions());
|
||||
return s;
|
||||
}
|
||||
|
||||
@SuppressWarnings("unchecked")
|
||||
public Collection<? extends IRelation> getRelations() {
|
||||
Collection<? extends IRelation> s = HashSetFactory.make();
|
||||
s.addAll(a.getRelations());
|
||||
s.addAll(b.getRelations());
|
||||
return s;
|
||||
}
|
||||
|
||||
@SuppressWarnings("unchecked")
|
||||
public Collection<AbstractVariable> getVariables() {
|
||||
Collection<AbstractVariable> s = HashSetFactory.make();
|
||||
s.addAll(a.getVariables());
|
||||
s.addAll(b.getVariables());
|
||||
return s;
|
||||
}
|
||||
|
||||
@SuppressWarnings("unchecked")
|
||||
public Collection<IConstant> getConstants() {
|
||||
Collection<IConstant> ma = a.getConstants();
|
||||
Collection<IConstant> mb = b.getConstants();
|
||||
assert ma != null;
|
||||
assert mb != null;
|
||||
Collection<IConstant> result = HashSetFactory.make();
|
||||
result.addAll(ma);
|
||||
result.addAll(mb);
|
||||
return result;
|
||||
}
|
||||
}
|
||||
|
|
@ -1,150 +0,0 @@
|
|||
/*******************************************************************************
|
||||
* Copyright (c) 2007 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.logic.ILogicConstants.BinaryConnective;
|
||||
import com.ibm.wala.logic.ILogicConstants.Quantifier;
|
||||
|
||||
public class DefaultDecorator implements ILogicDecorator {
|
||||
|
||||
private final static DefaultDecorator INSTANCE = new DefaultDecorator();
|
||||
|
||||
protected DefaultDecorator() {
|
||||
}
|
||||
|
||||
public static DefaultDecorator instance() {
|
||||
return INSTANCE;
|
||||
}
|
||||
|
||||
public String prettyPrint(BinaryConnective b) throws IllegalArgumentException {
|
||||
if (b == null) {
|
||||
throw new IllegalArgumentException("b == null");
|
||||
}
|
||||
return b.toString();
|
||||
}
|
||||
|
||||
public String prettyPrint(BooleanConstant c) throws IllegalArgumentException {
|
||||
if (c == null) {
|
||||
throw new IllegalArgumentException("c == null");
|
||||
}
|
||||
return c.toString();
|
||||
}
|
||||
|
||||
public String prettyPrint(AbstractVariable v) throws IllegalArgumentException {
|
||||
if (v == null) {
|
||||
throw new IllegalArgumentException("v == null");
|
||||
}
|
||||
return v.toString();
|
||||
}
|
||||
|
||||
public String prettyPrint(Quantifier q) throws IllegalArgumentException {
|
||||
if (q == null) {
|
||||
throw new IllegalArgumentException("q == null");
|
||||
}
|
||||
return q.toString();
|
||||
}
|
||||
|
||||
public String prettyPrint(IConstant constant) throws IllegalArgumentException {
|
||||
if (constant == null) {
|
||||
throw new IllegalArgumentException("constant == null");
|
||||
}
|
||||
return constant.toString();
|
||||
}
|
||||
|
||||
public String prettyPrint(FunctionTerm term) throws IllegalArgumentException {
|
||||
if (term == null) {
|
||||
throw new IllegalArgumentException("term == null");
|
||||
}
|
||||
StringBuffer result = new StringBuffer(term.getFunction().getSymbol());
|
||||
result.append("(");
|
||||
for (int i = 0; i < term.getFunction().getNumberOfParameters() - 1; i++) {
|
||||
result.append(term.getParameters().get(i).prettyPrint(this));
|
||||
result.append(",");
|
||||
}
|
||||
if (term.getFunction().getNumberOfParameters() > 0) {
|
||||
result.append(term.getParameters().get(term.getFunction().getNumberOfParameters() - 1).prettyPrint(this));
|
||||
}
|
||||
result.append(")");
|
||||
return result.toString();
|
||||
}
|
||||
|
||||
public String prettyPrint(RelationFormula r) throws IllegalArgumentException {
|
||||
if (r == null) {
|
||||
throw new IllegalArgumentException("r == null");
|
||||
}
|
||||
if (r.getRelation().getValence() == 2) {
|
||||
return infixNotation(r);
|
||||
} else {
|
||||
return prefixNotation(r);
|
||||
}
|
||||
}
|
||||
|
||||
public String prefixNotation(RelationFormula r) throws IllegalArgumentException {
|
||||
if (r == null) {
|
||||
throw new IllegalArgumentException("r == null");
|
||||
}
|
||||
StringBuffer result = new StringBuffer(prettyPrint(r.getRelation()));
|
||||
result.append("(");
|
||||
for (int i = 0; i < r.getRelation().getValence() - 1; i++) {
|
||||
result.append(r.getTerms().get(i).prettyPrint(this));
|
||||
result.append(",");
|
||||
}
|
||||
if (r.getRelation().getValence() > 0) {
|
||||
result.append(r.getTerms().get(r.getRelation().getValence() - 1).prettyPrint(this));
|
||||
}
|
||||
result.append(")");
|
||||
return result.toString();
|
||||
}
|
||||
|
||||
public String infixNotation(RelationFormula r) {
|
||||
assert r.getRelation().getValence() == 2;
|
||||
StringBuffer result = new StringBuffer();
|
||||
result.append(r.getTerms().get(0).prettyPrint(this));
|
||||
result.append(" ");
|
||||
result.append(prettyPrint(r.getRelation()));
|
||||
result.append(" ");
|
||||
result.append(r.getTerms().get(1).prettyPrint(this));
|
||||
return result.toString();
|
||||
}
|
||||
|
||||
public String prettyPrint(IRelation r) throws IllegalArgumentException {
|
||||
if (r == null) {
|
||||
throw new IllegalArgumentException("r == null");
|
||||
}
|
||||
return r.getSymbol();
|
||||
}
|
||||
|
||||
public String prettyPrint(AbstractBinaryFormula f) throws IllegalArgumentException {
|
||||
if (f == null) {
|
||||
throw new IllegalArgumentException("f == null");
|
||||
}
|
||||
StringBuffer result = new StringBuffer();
|
||||
result.append(" ( ");
|
||||
result.append(f.getF1().prettyPrint(this));
|
||||
result.append(" ) ");
|
||||
result.append(prettyPrint(f.getConnective()));
|
||||
result.append(" ( ");
|
||||
result.append(f.getF2().prettyPrint(this));
|
||||
result.append(" )");
|
||||
return result.toString();
|
||||
}
|
||||
|
||||
public String prettyPrint(NotFormula n) throws IllegalArgumentException {
|
||||
if (n == null) {
|
||||
throw new IllegalArgumentException("n == null");
|
||||
}
|
||||
StringBuffer result = new StringBuffer();
|
||||
result.append("not ( ");
|
||||
result.append(n.getFormula().prettyPrint(this));
|
||||
result.append(" ) ");
|
||||
return result.toString();
|
||||
}
|
||||
}
|
||||
|
|
@ -1,150 +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 java.util.Collection;
|
||||
import java.util.Collections;
|
||||
|
||||
import com.ibm.wala.logic.ILogicConstants.BinaryConnective;
|
||||
import com.ibm.wala.util.collections.HashSetFactory;
|
||||
|
||||
/**
|
||||
* A disjunction of formulae
|
||||
*
|
||||
* @author sjfink
|
||||
*/
|
||||
public class Disjunction extends AbstractBinaryFormula implements IMaxTerm {
|
||||
|
||||
// invariant: size >= 2
|
||||
private final Collection<? extends IFormula> clauses;
|
||||
|
||||
private Disjunction(Collection<? extends IFormula> clauses) {
|
||||
assert clauses.size() >= 2;
|
||||
this.clauses = clauses;
|
||||
}
|
||||
|
||||
public Collection<? extends IConstant> getConstants() {
|
||||
Collection<IConstant> result = HashSetFactory.make();
|
||||
for (IFormula f : clauses) {
|
||||
result.addAll(f.getConstants());
|
||||
}
|
||||
return result;
|
||||
}
|
||||
|
||||
public Collection<? extends ITerm> getAllTerms() {
|
||||
Collection<ITerm> result = HashSetFactory.make();
|
||||
for (IFormula f : clauses) {
|
||||
result.addAll(f.getAllTerms());
|
||||
}
|
||||
return result;
|
||||
}
|
||||
|
||||
public Collection<AbstractVariable> getFreeVariables() {
|
||||
Collection<AbstractVariable> result = HashSetFactory.make();
|
||||
for (IFormula f : clauses) {
|
||||
result.addAll(f.getFreeVariables());
|
||||
}
|
||||
return result;
|
||||
}
|
||||
|
||||
public String prettyPrint(ILogicDecorator d) {
|
||||
if (d == null) {
|
||||
throw new IllegalArgumentException("d == null");
|
||||
}
|
||||
return d.prettyPrint(this);
|
||||
}
|
||||
|
||||
@Override
|
||||
public int hashCode() {
|
||||
final int prime = 31;
|
||||
int result = 1;
|
||||
result = prime * result + ((clauses == null) ? 0 : clauses.hashCode());
|
||||
return result;
|
||||
}
|
||||
|
||||
@Override
|
||||
public boolean equals(Object obj) {
|
||||
if (this == obj)
|
||||
return true;
|
||||
if (obj == null)
|
||||
return false;
|
||||
if (getClass() != obj.getClass())
|
||||
return false;
|
||||
final Disjunction other = (Disjunction) obj;
|
||||
if (clauses == null) {
|
||||
if (other.clauses != null)
|
||||
return false;
|
||||
} else if (!clauses.equals(other.clauses))
|
||||
return false;
|
||||
return true;
|
||||
}
|
||||
|
||||
@Override
|
||||
public BinaryConnective getConnective() {
|
||||
return BinaryConnective.OR;
|
||||
}
|
||||
|
||||
@Override
|
||||
public IFormula getF1() {
|
||||
return clauses.iterator().next();
|
||||
}
|
||||
|
||||
@Override
|
||||
public IFormula getF2() {
|
||||
Collection<? extends IFormula> c = HashSetFactory.make(clauses);
|
||||
c.remove(getF1());
|
||||
if (c.size() == 1) {
|
||||
return c.iterator().next();
|
||||
} else {
|
||||
return make(c);
|
||||
}
|
||||
}
|
||||
|
||||
public static IMaxTerm make(Collection<? extends IFormula> clauses) {
|
||||
assert clauses.size() >= 2;
|
||||
Collection<IFormula> newClauses = HashSetFactory.make();
|
||||
for (IFormula c : clauses) {
|
||||
if (c instanceof Disjunction) {
|
||||
Disjunction d = (Disjunction) c;
|
||||
newClauses.addAll(d.clauses);
|
||||
} else {
|
||||
if (AdHocSemiDecisionProcedure.singleton().isTautology(c)) {
|
||||
return BooleanConstantFormula.TRUE;
|
||||
} else if (!AdHocSemiDecisionProcedure.singleton().isContradiction(c)) {
|
||||
newClauses.add(AdHocSemiDecisionProcedure.normalize(c));
|
||||
}
|
||||
}
|
||||
}
|
||||
if (newClauses.isEmpty()) {
|
||||
return (BooleanConstantFormula.FALSE);
|
||||
} else if (newClauses.size() == 1) {
|
||||
IFormula f = newClauses.iterator().next();
|
||||
assert f instanceof IMaxTerm;
|
||||
return (IMaxTerm) f;
|
||||
} else {
|
||||
return new Disjunction(newClauses);
|
||||
}
|
||||
}
|
||||
|
||||
public Collection<? extends IFormula> getClauses() {
|
||||
return Collections.unmodifiableCollection(clauses);
|
||||
}
|
||||
|
||||
@Override
|
||||
public String toString() {
|
||||
return prettyPrint(DefaultDecorator.instance());
|
||||
}
|
||||
|
||||
public Collection<? extends IMaxTerm> getMaxTerms() {
|
||||
return Collections.singleton(this);
|
||||
}
|
||||
|
||||
}
|
||||
|
|
@ -1,58 +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;
|
||||
|
||||
public class DoubleConstant extends NumberConstant {
|
||||
private final double val;
|
||||
|
||||
protected DoubleConstant(double val) {
|
||||
this.val = val;
|
||||
}
|
||||
|
||||
public static DoubleConstant make(double val) {
|
||||
return new DoubleConstant(val);
|
||||
}
|
||||
|
||||
@Override
|
||||
public Number getVal() {
|
||||
return val;
|
||||
}
|
||||
|
||||
@Override
|
||||
public String toString() {
|
||||
return String.valueOf(val);
|
||||
}
|
||||
|
||||
@Override
|
||||
public int hashCode() {
|
||||
final int prime = 31;
|
||||
int result = 1;
|
||||
long temp;
|
||||
temp = Double.doubleToLongBits(val);
|
||||
result = prime * result + (int) (temp ^ (temp >>> 32));
|
||||
return result;
|
||||
}
|
||||
|
||||
@Override
|
||||
public boolean equals(Object obj) {
|
||||
if (this == obj)
|
||||
return true;
|
||||
if (obj == null)
|
||||
return false;
|
||||
if (getClass() != obj.getClass())
|
||||
return false;
|
||||
final DoubleConstant other = (DoubleConstant) obj;
|
||||
if (Double.doubleToLongBits(val) != Double.doubleToLongBits(other.val))
|
||||
return false;
|
||||
return true;
|
||||
}
|
||||
|
||||
}
|
||||
|
|
@ -1,34 +0,0 @@
|
|||
/*******************************************************************************
|
||||
* Copyright (c) 2007 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 java.util.Collection;
|
||||
import java.util.Collections;
|
||||
|
||||
public class EmptyTheory extends AbstractTheory {
|
||||
|
||||
private final static EmptyTheory INSTANCE = new EmptyTheory();
|
||||
|
||||
public static EmptyTheory singleton() {
|
||||
return INSTANCE;
|
||||
}
|
||||
|
||||
private EmptyTheory() {}
|
||||
|
||||
public Collection<? extends IFormula> getSentences() {
|
||||
return Collections.emptySet();
|
||||
}
|
||||
|
||||
public IVocabulary getVocabulary() {
|
||||
return BasicVocabulary.make(Collections.<IFunction>emptySet());
|
||||
}
|
||||
|
||||
}
|
||||
|
|
@ -1,57 +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;
|
||||
|
||||
public class FloatConstant extends NumberConstant {
|
||||
private final float val;
|
||||
|
||||
protected FloatConstant(float val) {
|
||||
this.val = val;
|
||||
}
|
||||
|
||||
public static FloatConstant make(float val) {
|
||||
return new FloatConstant(val);
|
||||
}
|
||||
|
||||
@Override
|
||||
public Number getVal() {
|
||||
return val;
|
||||
}
|
||||
|
||||
@Override
|
||||
public String toString() {
|
||||
return String.valueOf(val);
|
||||
}
|
||||
|
||||
@Override
|
||||
public int hashCode() {
|
||||
final int prime = 31;
|
||||
int result = 1;
|
||||
result = prime * result + Float.floatToIntBits(val);
|
||||
return result;
|
||||
}
|
||||
|
||||
@Override
|
||||
public boolean equals(Object obj) {
|
||||
if (this == obj)
|
||||
return true;
|
||||
if (obj == null)
|
||||
return false;
|
||||
if (getClass() != obj.getClass())
|
||||
return false;
|
||||
final FloatConstant other = (FloatConstant) obj;
|
||||
if (Float.floatToIntBits(val) != Float.floatToIntBits(other.val))
|
||||
return false;
|
||||
return true;
|
||||
}
|
||||
|
||||
|
||||
}
|
||||
|
|
@ -1,172 +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 java.util.ArrayList;
|
||||
import java.util.Collection;
|
||||
import java.util.Collections;
|
||||
import java.util.List;
|
||||
|
||||
import com.ibm.wala.util.collections.HashSetFactory;
|
||||
|
||||
public class FunctionTerm extends AbstractTerm {
|
||||
|
||||
private static final boolean PARANOID = false;
|
||||
|
||||
private final List<ITerm> parameters;
|
||||
|
||||
private final IFunction f;
|
||||
|
||||
|
||||
private FunctionTerm(IFunction f, List<ITerm> parameters) throws IllegalArgumentException {
|
||||
this.f = f;
|
||||
this.parameters = parameters;
|
||||
if (f == null) {
|
||||
throw new IllegalArgumentException("f cannot be null");
|
||||
}
|
||||
if (parameters == null) {
|
||||
throw new IllegalArgumentException("parameters cannot be null");
|
||||
}
|
||||
for (ITerm t : parameters) {
|
||||
if (t == null) {
|
||||
throw new IllegalArgumentException("cannot have a null parameter");
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
public Kind getKind() {
|
||||
return Kind.FUNCTION;
|
||||
}
|
||||
|
||||
@Override
|
||||
public String toString() {
|
||||
return prettyPrint(DefaultDecorator.instance());
|
||||
}
|
||||
|
||||
public String prettyPrint(ILogicDecorator d) throws IllegalArgumentException {
|
||||
if (d == null) {
|
||||
throw new IllegalArgumentException("d == null");
|
||||
}
|
||||
return d.prettyPrint(this);
|
||||
|
||||
}
|
||||
|
||||
public static FunctionTerm make(UnaryFunction f, int i) {
|
||||
List<ITerm> p = new ArrayList<ITerm>(1);
|
||||
p.add(IntConstant.make(i));
|
||||
return new FunctionTerm(f, p);
|
||||
}
|
||||
|
||||
public static FunctionTerm make(BinaryFunction f, int i, int j) {
|
||||
List<ITerm> p = new ArrayList<ITerm>(2);
|
||||
p.add(IntConstant.make(i));
|
||||
p.add(IntConstant.make(j));
|
||||
return new FunctionTerm(f, p);
|
||||
}
|
||||
|
||||
public static FunctionTerm make(IFunction f, List<ITerm> terms) {
|
||||
assert f.getNumberOfParameters() == terms.size();
|
||||
return new FunctionTerm(f, terms);
|
||||
}
|
||||
|
||||
public static FunctionTerm make(BinaryFunction f, ITerm i, int j) {
|
||||
List<ITerm> p = new ArrayList<ITerm>(2);
|
||||
p.add(i);
|
||||
p.add(IntConstant.make(j));
|
||||
return new FunctionTerm(f, p);
|
||||
}
|
||||
|
||||
public static FunctionTerm make(BinaryFunction f, ITerm i, ITerm j) {
|
||||
List<ITerm> p = new ArrayList<ITerm>(2);
|
||||
p.add(i);
|
||||
p.add(j);
|
||||
return new FunctionTerm(f, p);
|
||||
}
|
||||
|
||||
public static FunctionTerm make(NullaryFunction f) {
|
||||
List<ITerm> empty = Collections.emptyList();
|
||||
return new FunctionTerm(f, empty);
|
||||
}
|
||||
|
||||
public static FunctionTerm make(UnaryFunction f, ITerm t) {
|
||||
List<ITerm> p = new ArrayList<ITerm>(1);
|
||||
p.add(t);
|
||||
return new FunctionTerm(f, p);
|
||||
}
|
||||
|
||||
public IFunction getFunction() {
|
||||
return f;
|
||||
}
|
||||
|
||||
public List<ITerm> getParameters() {
|
||||
return PARANOID ? Collections.unmodifiableList(parameters) : parameters;
|
||||
}
|
||||
|
||||
public Collection<AbstractVariable> getFreeVariables() {
|
||||
Collection<AbstractVariable> result = HashSetFactory.make();
|
||||
for (ITerm t : parameters) {
|
||||
result.addAll(t.getFreeVariables());
|
||||
}
|
||||
return result;
|
||||
}
|
||||
|
||||
public Collection<? extends IConstant> getConstants() {
|
||||
Collection<IConstant> result = HashSetFactory.make();
|
||||
for (ITerm t : parameters) {
|
||||
result.addAll(t.getConstants());
|
||||
}
|
||||
return result;
|
||||
}
|
||||
|
||||
@Override
|
||||
public int hashCode() {
|
||||
final int PRIME = 31;
|
||||
int result = 1;
|
||||
result = PRIME * result + f.hashCode();
|
||||
result = PRIME * result + parameters.hashCode();
|
||||
return result;
|
||||
}
|
||||
|
||||
@Override
|
||||
public boolean equals(Object obj) {
|
||||
if (this == obj)
|
||||
return true;
|
||||
if (obj == null)
|
||||
return false;
|
||||
if (getClass() != obj.getClass())
|
||||
return false;
|
||||
final FunctionTerm other = (FunctionTerm) obj;
|
||||
if (!f.equals(other.f)) {
|
||||
return false;
|
||||
}
|
||||
if (!parameters.equals(other.parameters)) {
|
||||
return false;
|
||||
}
|
||||
return true;
|
||||
}
|
||||
|
||||
public Collection<? extends ITerm> getAllTerms() {
|
||||
Collection<ITerm> result = HashSetFactory.make();
|
||||
result.add(this);
|
||||
for (ITerm t : parameters) {
|
||||
result.addAll(t.getAllTerms());
|
||||
}
|
||||
return result;
|
||||
}
|
||||
|
||||
public static FunctionTerm make(NaryFunction f, ITerm t1, ITerm t2, ITerm t3) {
|
||||
List<ITerm> l = new ArrayList<ITerm>(3);
|
||||
l.add(t1);
|
||||
l.add(t2);
|
||||
l.add(t3);
|
||||
return make(f, l);
|
||||
}
|
||||
}
|
||||
|
|
@ -1,25 +0,0 @@
|
|||
/*******************************************************************************
|
||||
* Copyright (c) 2007 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 java.util.Collection;
|
||||
|
||||
/**
|
||||
* A formula in conjunctive normal form
|
||||
*
|
||||
* @author sjfink
|
||||
*
|
||||
*/
|
||||
public interface ICNFFormula extends IFormula {
|
||||
|
||||
public Collection<? extends IMaxTerm> getMaxTerms();
|
||||
|
||||
}
|
||||
|
|
@ -1,15 +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;
|
||||
|
||||
public interface IConstant extends ITerm {
|
||||
|
||||
}
|
||||
|
|
@ -1,50 +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 java.util.Collection;
|
||||
|
||||
/**
|
||||
* Formula := P(Term, ....)
|
||||
* | NOT(Formula)
|
||||
* | Formula CONNECTIVE Formula
|
||||
* | QUANTIFIER Formula
|
||||
* | TRUE
|
||||
* | FALSE
|
||||
*
|
||||
* @author sjfink
|
||||
*
|
||||
*/
|
||||
public interface IFormula {
|
||||
static enum Kind {
|
||||
RELATION, NEGATION, BINARY, QUANTIFIED, CONSTANT
|
||||
}
|
||||
|
||||
public Kind getKind();
|
||||
|
||||
/**
|
||||
* @return the free variables in this formula
|
||||
*/
|
||||
public Collection<AbstractVariable> getFreeVariables();
|
||||
|
||||
/**
|
||||
* @return the constants that appear in this formula
|
||||
*/
|
||||
public Collection<? extends IConstant> getConstants();
|
||||
|
||||
/**
|
||||
* @return all terms that appear in this formula, including recursive descent non on-atomic terms
|
||||
*/
|
||||
public Collection<? extends ITerm> getAllTerms();
|
||||
|
||||
public String prettyPrint(ILogicDecorator d);
|
||||
|
||||
}
|
||||
|
|
@ -1,31 +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;
|
||||
|
||||
/**
|
||||
* An n-ary function
|
||||
*
|
||||
* @author sjfink
|
||||
*
|
||||
*/
|
||||
public interface IFunction {
|
||||
/**
|
||||
* @return the number of parameters to this function
|
||||
*/
|
||||
int getNumberOfParameters();
|
||||
|
||||
/**
|
||||
* @return a string which uniquely identifies this relation
|
||||
*/
|
||||
String getSymbol();
|
||||
|
||||
|
||||
}
|
||||
|
|
@ -1,29 +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;
|
||||
|
||||
/**
|
||||
* Constants used to build up formulae
|
||||
*
|
||||
* @author sjfink
|
||||
*
|
||||
*/
|
||||
public interface ILogicConstants {
|
||||
|
||||
public enum BinaryConnective {
|
||||
AND, OR, IMPLIES, BICONDITIONAL
|
||||
}
|
||||
|
||||
public enum Quantifier {
|
||||
FORALL, EXISTS
|
||||
}
|
||||
|
||||
}
|
||||
|
|
@ -1,38 +0,0 @@
|
|||
/*******************************************************************************
|
||||
* Copyright (c) 2007 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.logic.ILogicConstants.BinaryConnective;
|
||||
import com.ibm.wala.logic.ILogicConstants.Quantifier;
|
||||
|
||||
public interface ILogicDecorator {
|
||||
|
||||
String prettyPrint(BinaryConnective b);
|
||||
|
||||
String prettyPrint(BooleanConstant c);
|
||||
|
||||
String prettyPrint(AbstractVariable v);
|
||||
|
||||
String prettyPrint(Quantifier quantifier);
|
||||
|
||||
String prettyPrint(IConstant constant);
|
||||
|
||||
String prettyPrint(FunctionTerm term);
|
||||
|
||||
String prettyPrint(RelationFormula formula);
|
||||
|
||||
String prettyPrint(IRelation r);
|
||||
|
||||
String prettyPrint(AbstractBinaryFormula binaryFormula);
|
||||
|
||||
String prettyPrint(NotFormula notFormula);
|
||||
|
||||
}
|
||||
|
|
@ -1,21 +0,0 @@
|
|||
/*******************************************************************************
|
||||
* Copyright (c) 2007 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;
|
||||
|
||||
/**
|
||||
* A maxterm is a sum (disjunction) of atomic formulae (constants, relations, or quantified).
|
||||
*
|
||||
* @author sjfink
|
||||
*
|
||||
*/
|
||||
public interface IMaxTerm extends ICNFFormula {
|
||||
|
||||
}
|
||||
|
|
@ -1,31 +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;
|
||||
|
||||
/**
|
||||
* an n-ary relational predicate symbol
|
||||
*
|
||||
* @author sjfink
|
||||
*
|
||||
*/
|
||||
public interface IRelation {
|
||||
|
||||
/**
|
||||
* @return the arity, or valence of this relation
|
||||
*/
|
||||
int getValence();
|
||||
|
||||
/**
|
||||
* @return a string which uniquely identifies this relation
|
||||
*/
|
||||
String getSymbol();
|
||||
|
||||
}
|
||||
|
|
@ -1,48 +0,0 @@
|
|||
/*******************************************************************************
|
||||
* Copyright (c) 2007 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 java.util.Collection;
|
||||
|
||||
/**
|
||||
* @author sjfink
|
||||
*/
|
||||
public interface ISemiDecisionProcedure {
|
||||
|
||||
/**
|
||||
* @return true if we can prove f is a contradiction
|
||||
*/
|
||||
public boolean isContradiction(IFormula f);
|
||||
|
||||
/**
|
||||
* @return true if we can prove f is a tautology
|
||||
*/
|
||||
public boolean isTautology(IFormula f);
|
||||
|
||||
/**
|
||||
* @param facts
|
||||
* formulae that can be treated as axioms
|
||||
* @return true if we can prove f is a tautology
|
||||
* @throws IllegalArgumentException
|
||||
* if facts == null
|
||||
*/
|
||||
public boolean isTautology(IFormula f, Collection<IMaxTerm> facts) throws IllegalArgumentException;
|
||||
|
||||
/**
|
||||
* @param facts
|
||||
* formulae that can be treated as axioms
|
||||
* @return true if we can prove f is a contradiction
|
||||
* @throws IllegalArgumentException
|
||||
* if facts == null
|
||||
*/
|
||||
public boolean isContradiction(IFormula f, Collection<IMaxTerm> facts) throws IllegalArgumentException;
|
||||
|
||||
}
|
||||
|
|
@ -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 java.util.Collection;
|
||||
|
||||
/**
|
||||
* Term := Constant
|
||||
* | Variable
|
||||
* | f(Term,...)
|
||||
*
|
||||
* @author sjfink
|
||||
*
|
||||
*/
|
||||
public interface ITerm {
|
||||
static enum Kind {
|
||||
CONSTANT, VARIABLE, FUNCTION
|
||||
}
|
||||
|
||||
public Kind getKind();
|
||||
|
||||
public Collection<? extends AbstractVariable> getFreeVariables();
|
||||
|
||||
public String prettyPrint(ILogicDecorator d);
|
||||
|
||||
public Collection<? extends IConstant> getConstants();
|
||||
|
||||
/**
|
||||
* Collect all terms that appear in this term, including subterms if this is a function term
|
||||
*/
|
||||
public Collection<? extends ITerm> getAllTerms();
|
||||
}
|
||||
|
|
@ -1,39 +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 java.util.Collection;
|
||||
|
||||
/**
|
||||
* A theory is a set of sentences
|
||||
*
|
||||
* @author sjfink
|
||||
*
|
||||
*/
|
||||
public interface ITheory {
|
||||
|
||||
public IVocabulary getVocabulary();
|
||||
|
||||
/**
|
||||
* get all sentences in theory
|
||||
* TODO: remove this, replace with getSentencesRelevantToConstraints(empty)? MS
|
||||
* @return the sentences
|
||||
*/
|
||||
public Collection<? extends IFormula> getSentences();
|
||||
|
||||
/**
|
||||
*
|
||||
* @param constraints
|
||||
* @return those sentences in this theory relevant to constraints
|
||||
*/
|
||||
public Collection<? extends IFormula> getSentencesRelevantToConstraints(Collection<? extends IFormula> constraints);
|
||||
|
||||
}
|
||||
|
|
@ -1,32 +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 java.util.Collection;
|
||||
|
||||
/**
|
||||
* Vocabulary of a calculus
|
||||
*
|
||||
* @param <T> the type of constants in this vocabulary
|
||||
*
|
||||
* @author sjfink
|
||||
*
|
||||
*/
|
||||
public interface IVocabulary<T extends IConstant> {
|
||||
|
||||
Collection<AbstractVariable> getVariables();
|
||||
|
||||
Collection<T> getConstants();
|
||||
|
||||
Collection<? extends IRelation> getRelations();
|
||||
|
||||
Collection<? extends IFunction> getFunctions();
|
||||
}
|
||||
|
|
@ -1,56 +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;
|
||||
|
||||
public class IntConstant extends NumberConstant {
|
||||
private final int val;
|
||||
|
||||
protected IntConstant(int val) {
|
||||
this.val = val;
|
||||
}
|
||||
|
||||
public static IntConstant make(int val) {
|
||||
return new IntConstant(val);
|
||||
}
|
||||
|
||||
@Override
|
||||
public Number getVal() {
|
||||
return val;
|
||||
}
|
||||
|
||||
@Override
|
||||
public String toString() {
|
||||
return String.valueOf(val);
|
||||
}
|
||||
|
||||
|
||||
@Override
|
||||
public int hashCode() {
|
||||
final int PRIME = 31;
|
||||
int result = 1;
|
||||
result = PRIME * result + val;
|
||||
return result;
|
||||
}
|
||||
|
||||
@Override
|
||||
public boolean equals(Object obj) {
|
||||
if (this == obj)
|
||||
return true;
|
||||
if (obj == null)
|
||||
return false;
|
||||
if (getClass() != obj.getClass())
|
||||
return false;
|
||||
final IntConstant other = (IntConstant) obj;
|
||||
if (val != other.val)
|
||||
return false;
|
||||
return true;
|
||||
}
|
||||
}
|
||||
|
|
@ -1,28 +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;
|
||||
|
||||
|
||||
/**
|
||||
* A term that represents an unconstrained integer variable in a formula
|
||||
*
|
||||
* @author sjfink
|
||||
*/
|
||||
public class IntVariable extends AbstractNumberedVariable {
|
||||
|
||||
protected IntVariable(int number) {
|
||||
super(number);
|
||||
}
|
||||
|
||||
public static IntVariable make(int number) {
|
||||
return new IntVariable(number);
|
||||
}
|
||||
}
|
||||
|
|
@ -1,56 +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;
|
||||
|
||||
public class LongConstant extends NumberConstant {
|
||||
private final long val;
|
||||
|
||||
protected LongConstant(long val) {
|
||||
this.val = val;
|
||||
}
|
||||
|
||||
public static LongConstant make(long val) {
|
||||
return new LongConstant(val);
|
||||
}
|
||||
|
||||
@Override
|
||||
public Number getVal() {
|
||||
return val;
|
||||
}
|
||||
|
||||
@Override
|
||||
public String toString() {
|
||||
return String.valueOf(val);
|
||||
}
|
||||
|
||||
|
||||
@Override
|
||||
public int hashCode() {
|
||||
final int PRIME = 31;
|
||||
int result = 1;
|
||||
result = (int) (PRIME * result + val);
|
||||
return result;
|
||||
}
|
||||
|
||||
@Override
|
||||
public boolean equals(Object obj) {
|
||||
if (this == obj)
|
||||
return true;
|
||||
if (obj == null)
|
||||
return false;
|
||||
if (getClass() != obj.getClass())
|
||||
return false;
|
||||
final LongConstant other = (LongConstant) obj;
|
||||
if (val != other.val)
|
||||
return false;
|
||||
return true;
|
||||
}
|
||||
}
|
||||
|
|
@ -1,70 +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;
|
||||
|
||||
/**
|
||||
* @author schandra_sf
|
||||
*/
|
||||
public class NaryFunction implements IFunction {
|
||||
|
||||
private final String symbol;
|
||||
|
||||
private final int k;
|
||||
|
||||
private NaryFunction(String symbol, int k) {
|
||||
this.symbol = symbol;
|
||||
this.k = k;
|
||||
}
|
||||
|
||||
public static NaryFunction make(String symbol, int k) {
|
||||
return new NaryFunction(symbol, k);
|
||||
}
|
||||
|
||||
public int getNumberOfParameters() {
|
||||
return k;
|
||||
}
|
||||
|
||||
public String getSymbol() {
|
||||
return symbol;
|
||||
}
|
||||
|
||||
@Override
|
||||
public String toString() {
|
||||
return getSymbol() + " : int ^ k -> int";
|
||||
}
|
||||
|
||||
@Override
|
||||
public int hashCode() {
|
||||
final int prime = 31;
|
||||
int result = 1;
|
||||
result = prime * result + ((symbol == null) ? 0 : symbol.hashCode());
|
||||
return result;
|
||||
}
|
||||
|
||||
@Override
|
||||
public boolean equals(Object obj) {
|
||||
if (this == obj)
|
||||
return true;
|
||||
if (obj == null)
|
||||
return false;
|
||||
if (getClass() != obj.getClass())
|
||||
return false;
|
||||
final NaryFunction other = (NaryFunction) obj;
|
||||
if (symbol == null) {
|
||||
if (other.symbol != null)
|
||||
return false;
|
||||
} else if (!symbol.equals(other.symbol))
|
||||
return false;
|
||||
return true;
|
||||
}
|
||||
|
||||
}
|
||||
|
|
@ -1,132 +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 java.util.Collection;
|
||||
|
||||
/**
|
||||
* A formula of the form not(f)
|
||||
*
|
||||
* @author sjfink
|
||||
*/
|
||||
public class NotFormula implements IFormula {
|
||||
|
||||
private final IFormula f;
|
||||
|
||||
protected NotFormula(final IFormula f) throws IllegalArgumentException {
|
||||
super();
|
||||
this.f = f;
|
||||
if (f == null) {
|
||||
throw new IllegalArgumentException("f cannot be null");
|
||||
}
|
||||
}
|
||||
|
||||
public static IFormula make(IFormula f) throws IllegalArgumentException {
|
||||
if (f == null) {
|
||||
throw new IllegalArgumentException("f == null");
|
||||
}
|
||||
switch (f.getKind()) {
|
||||
case RELATION:
|
||||
RelationFormula r = (RelationFormula) f;
|
||||
if (r.getRelation().equals(BinaryRelation.EQUALS)) {
|
||||
return RelationFormula.make(BinaryRelation.NE, r.getTerms());
|
||||
}
|
||||
if (r.getRelation().equals(BinaryRelation.NE)) {
|
||||
return RelationFormula.make(BinaryRelation.EQUALS, r.getTerms());
|
||||
}
|
||||
if (r.getRelation().equals(BinaryRelation.GE)) {
|
||||
return RelationFormula.make(BinaryRelation.LT, r.getTerms());
|
||||
}
|
||||
if (r.getRelation().equals(BinaryRelation.GT)) {
|
||||
return RelationFormula.make(BinaryRelation.LE, r.getTerms());
|
||||
}
|
||||
if (r.getRelation().equals(BinaryRelation.LE)) {
|
||||
return RelationFormula.make(BinaryRelation.GT, r.getTerms());
|
||||
}
|
||||
if (r.getRelation().equals(BinaryRelation.LT)) {
|
||||
return RelationFormula.make(BinaryRelation.GE, r.getTerms());
|
||||
}
|
||||
return NotFormulaMaxTerm.createNotFormulaMaxTerm(r);
|
||||
case CONSTANT:
|
||||
if (f.equals(BooleanConstantFormula.TRUE)) {
|
||||
return BooleanConstantFormula.FALSE;
|
||||
} else {
|
||||
assert f.equals(BooleanConstantFormula.FALSE);
|
||||
return BooleanConstantFormula.TRUE;
|
||||
}
|
||||
case NEGATION:
|
||||
// NOT(NOT(g)) == g
|
||||
NotFormula n = (NotFormula)f;
|
||||
return n.getFormula();
|
||||
case BINARY:
|
||||
case QUANTIFIED:
|
||||
default:
|
||||
return new NotFormula(f);
|
||||
}
|
||||
}
|
||||
|
||||
public Kind getKind() {
|
||||
return Kind.NEGATION;
|
||||
}
|
||||
|
||||
public IFormula getFormula() {
|
||||
return f;
|
||||
}
|
||||
|
||||
public Collection<AbstractVariable> getFreeVariables() {
|
||||
return f.getFreeVariables();
|
||||
}
|
||||
|
||||
public Collection<? extends IConstant> getConstants() {
|
||||
return f.getConstants();
|
||||
}
|
||||
|
||||
public Collection<? extends ITerm> getAllTerms() {
|
||||
return f.getAllTerms();
|
||||
}
|
||||
|
||||
@Override
|
||||
public String toString() {
|
||||
return prettyPrint(DefaultDecorator.instance());
|
||||
}
|
||||
|
||||
public String prettyPrint(ILogicDecorator d) throws IllegalArgumentException {
|
||||
if (d == null) {
|
||||
throw new IllegalArgumentException("d == null");
|
||||
}
|
||||
return d.prettyPrint(this);
|
||||
}
|
||||
|
||||
@Override
|
||||
public int hashCode() {
|
||||
final int prime = 31;
|
||||
int result = 1;
|
||||
result = prime * result + ((f == null) ? 0 : f.hashCode());
|
||||
return result;
|
||||
}
|
||||
|
||||
@Override
|
||||
public boolean equals(Object obj) {
|
||||
if (this == obj)
|
||||
return true;
|
||||
if (obj == null)
|
||||
return false;
|
||||
if (getClass() != obj.getClass())
|
||||
return false;
|
||||
final NotFormula other = (NotFormula) obj;
|
||||
if (f == null) {
|
||||
if (other.f != null)
|
||||
return false;
|
||||
} else if (!f.equals(other.f))
|
||||
return false;
|
||||
return true;
|
||||
}
|
||||
}
|
||||
|
|
@ -1,39 +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 java.util.Collection;
|
||||
import java.util.Collections;
|
||||
|
||||
|
||||
/**
|
||||
* An irreducible Not Formula.
|
||||
*
|
||||
* use carefully.
|
||||
*
|
||||
* @author sjfink
|
||||
*/
|
||||
public class NotFormulaMaxTerm extends NotFormula implements IMaxTerm {
|
||||
|
||||
public static NotFormulaMaxTerm createNotFormulaMaxTerm(RelationFormula f) {
|
||||
return new NotFormulaMaxTerm(f);
|
||||
}
|
||||
|
||||
private NotFormulaMaxTerm(IFormula f) {
|
||||
super(f);
|
||||
}
|
||||
|
||||
public Collection<? extends IMaxTerm> getMaxTerms() {
|
||||
return Collections.singleton(this);
|
||||
}
|
||||
|
||||
|
||||
}
|
||||
|
|
@ -1,71 +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;
|
||||
|
||||
|
||||
/**
|
||||
* a function that takes no parameters.
|
||||
*
|
||||
* @author sjfink
|
||||
*
|
||||
*/
|
||||
public class NullaryFunction implements IFunction {
|
||||
|
||||
private final String symbol;
|
||||
|
||||
|
||||
|
||||
private NullaryFunction(String symbol) {
|
||||
this.symbol = symbol;
|
||||
}
|
||||
|
||||
public static NullaryFunction make(String symbol) {
|
||||
return new NullaryFunction(symbol);
|
||||
}
|
||||
|
||||
public int getNumberOfParameters() {
|
||||
return 0;
|
||||
}
|
||||
|
||||
public String getSymbol() {
|
||||
return symbol;
|
||||
}
|
||||
|
||||
@Override
|
||||
public String toString() {
|
||||
return getSymbol() + "()";
|
||||
}
|
||||
|
||||
@Override
|
||||
public int hashCode() {
|
||||
final int PRIME = 31;
|
||||
int result = 1;
|
||||
result = PRIME * result + ((symbol == null) ? 0 : symbol.hashCode());
|
||||
return result;
|
||||
}
|
||||
|
||||
@Override
|
||||
public boolean equals(Object obj) {
|
||||
if (this == obj)
|
||||
return true;
|
||||
if (obj == null)
|
||||
return false;
|
||||
if (getClass() != obj.getClass())
|
||||
return false;
|
||||
final NullaryFunction other = (NullaryFunction) obj;
|
||||
if (symbol == null) {
|
||||
if (other.symbol != null)
|
||||
return false;
|
||||
} else if (!symbol.equals(other.symbol))
|
||||
return false;
|
||||
return true;
|
||||
}
|
||||
}
|
||||
|
|
@ -1,23 +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;
|
||||
|
||||
|
||||
|
||||
/**
|
||||
* @author sjfink
|
||||
*
|
||||
*/
|
||||
public abstract class NumberConstant extends AbstractConstant {
|
||||
|
||||
public abstract Number getVal();
|
||||
|
||||
}
|
||||
|
|
@ -1,131 +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 java.util.Collection;
|
||||
import java.util.Collections;
|
||||
|
||||
import com.ibm.wala.logic.ILogicConstants.Quantifier;
|
||||
|
||||
public class QuantifiedFormula implements IMaxTerm {
|
||||
|
||||
private final IFormula f;
|
||||
|
||||
private final Quantifier q;
|
||||
|
||||
private final AbstractVariable boundV;
|
||||
|
||||
private QuantifiedFormula(final Quantifier q, final AbstractVariable boundV, final IFormula f) {
|
||||
super();
|
||||
this.f = f;
|
||||
this.q = q;
|
||||
this.boundV = boundV;
|
||||
}
|
||||
|
||||
public static QuantifiedFormula forall(AbstractVariable v, IFormula formula) {
|
||||
return new QuantifiedFormula(Quantifier.FORALL, v, formula);
|
||||
}
|
||||
|
||||
public static QuantifiedFormula forall(AbstractVariable v1, AbstractVariable v2, IFormula formula) {
|
||||
return new QuantifiedFormula(Quantifier.FORALL, v1, forall(v2, formula));
|
||||
}
|
||||
|
||||
public static QuantifiedFormula forall(AbstractVariable v1, AbstractVariable v2, AbstractVariable v3, IFormula formula) {
|
||||
return new QuantifiedFormula(Quantifier.FORALL, v1, forall(v2, v3, formula));
|
||||
}
|
||||
|
||||
public static IFormula make(Quantifier q, AbstractVariable v, IFormula f) {
|
||||
return new QuantifiedFormula(q, v, f);
|
||||
}
|
||||
|
||||
public Kind getKind() {
|
||||
return Kind.QUANTIFIED;
|
||||
}
|
||||
|
||||
public AbstractVariable getBoundVar() {
|
||||
return boundV;
|
||||
}
|
||||
|
||||
public IFormula getFormula() {
|
||||
return f;
|
||||
}
|
||||
|
||||
public Quantifier getQuantifier() {
|
||||
return q;
|
||||
}
|
||||
|
||||
@Override
|
||||
public int hashCode() {
|
||||
final int PRIME = 31;
|
||||
int result = 1;
|
||||
result = PRIME * result + ((boundV == null) ? 0 : boundV.hashCode());
|
||||
result = PRIME * result + ((f == null) ? 0 : f.hashCode());
|
||||
result = PRIME * result + ((q == null) ? 0 : q.hashCode());
|
||||
return result;
|
||||
}
|
||||
|
||||
@Override
|
||||
public boolean equals(Object obj) {
|
||||
if (this == obj)
|
||||
return true;
|
||||
if (obj == null)
|
||||
return false;
|
||||
if (getClass() != obj.getClass())
|
||||
return false;
|
||||
final QuantifiedFormula other = (QuantifiedFormula) obj;
|
||||
if (boundV == null) {
|
||||
if (other.boundV != null)
|
||||
return false;
|
||||
} else if (!boundV.equals(other.boundV))
|
||||
return false;
|
||||
if (f == null) {
|
||||
if (other.f != null)
|
||||
return false;
|
||||
} else if (!f.equals(other.f))
|
||||
return false;
|
||||
if (q == null) {
|
||||
if (other.q != null)
|
||||
return false;
|
||||
} else if (!q.equals(other.q))
|
||||
return false;
|
||||
return true;
|
||||
}
|
||||
|
||||
public Collection<AbstractVariable> getFreeVariables() {
|
||||
Collection<AbstractVariable> result = f.getFreeVariables();
|
||||
result.remove(boundV);
|
||||
return result;
|
||||
}
|
||||
|
||||
public Collection<? extends IConstant> getConstants() {
|
||||
return f.getConstants();
|
||||
}
|
||||
|
||||
public Collection<? extends ITerm> getAllTerms() {
|
||||
return f.getAllTerms();
|
||||
}
|
||||
|
||||
@Override
|
||||
public String toString() {
|
||||
return getQuantifier() + " " + getBoundVar() + "." + getFormula();
|
||||
}
|
||||
|
||||
public String prettyPrint(ILogicDecorator d) throws IllegalArgumentException {
|
||||
if (d == null) {
|
||||
throw new IllegalArgumentException("d == null");
|
||||
}
|
||||
return d.prettyPrint(getQuantifier()) + " " + d.prettyPrint(getBoundVar()) + "." + getFormula().prettyPrint(d);
|
||||
}
|
||||
|
||||
public Collection<? extends IMaxTerm> getMaxTerms() {
|
||||
return Collections.singleton(this);
|
||||
}
|
||||
}
|
||||
|
|
@ -1,28 +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;
|
||||
|
||||
|
||||
/**
|
||||
* A term that represents an unconstrained real number variable in a formula
|
||||
*
|
||||
* @author sjfink
|
||||
*/
|
||||
public class RealNumberVariable extends AbstractNumberedVariable {
|
||||
|
||||
protected RealNumberVariable(int number) {
|
||||
super(number);
|
||||
}
|
||||
|
||||
public static RealNumberVariable make(int number) {
|
||||
return new RealNumberVariable(number);
|
||||
}
|
||||
}
|
||||
|
|
@ -1,192 +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 java.util.ArrayList;
|
||||
import java.util.Collection;
|
||||
import java.util.Collections;
|
||||
import java.util.List;
|
||||
|
||||
import com.ibm.wala.util.collections.HashSetFactory;
|
||||
|
||||
/**
|
||||
* An atomic formula of the form R(Term, ... Term)
|
||||
*
|
||||
* @author sjfink
|
||||
*
|
||||
*/
|
||||
public class RelationFormula implements IMaxTerm {
|
||||
|
||||
private final IRelation R;
|
||||
|
||||
private final List<ITerm> terms;
|
||||
|
||||
public IRelation getRelation() {
|
||||
return R;
|
||||
}
|
||||
|
||||
public List<ITerm> getTerms() {
|
||||
return terms;
|
||||
}
|
||||
|
||||
public Collection<? extends ITerm> getAllTerms() {
|
||||
Collection<ITerm> result = HashSetFactory.make();
|
||||
for (ITerm t : terms) {
|
||||
result.addAll(t.getAllTerms());
|
||||
}
|
||||
return result;
|
||||
}
|
||||
|
||||
private RelationFormula(final IRelation R, final List<ITerm> terms) throws IllegalArgumentException {
|
||||
super();
|
||||
this.R = R;
|
||||
this.terms = terms;
|
||||
if (R == null) {
|
||||
throw new IllegalArgumentException("R cannot be null");
|
||||
}
|
||||
}
|
||||
|
||||
public static RelationFormula make(BinaryRelation R, ITerm t1, ITerm t2) {
|
||||
ArrayList<ITerm> l = new ArrayList<ITerm>();
|
||||
l.add(t1);
|
||||
l.add(t2);
|
||||
return new RelationFormula(R, l);
|
||||
}
|
||||
|
||||
public static RelationFormula make(BinaryRelation R, int i, ITerm t2) {
|
||||
return make(R, IntConstant.make(i), t2);
|
||||
}
|
||||
|
||||
public static RelationFormula make(BinaryRelation R, ITerm t1, int j) {
|
||||
return make(R, t1, IntConstant.make(j));
|
||||
}
|
||||
|
||||
public static RelationFormula make(BinaryRelation R, int i, int j) {
|
||||
return make(R, IntConstant.make(i), IntConstant.make(j));
|
||||
}
|
||||
|
||||
public static RelationFormula makeEquals(ITerm t1, ITerm t2) {
|
||||
return make(BinaryRelation.EQUALS, t1, t2);
|
||||
}
|
||||
|
||||
public static RelationFormula makeEquals(ITerm t1, int i) {
|
||||
return make(BinaryRelation.EQUALS, t1, IntConstant.make(i));
|
||||
}
|
||||
|
||||
public static RelationFormula make(UnaryRelation R, ITerm t) {
|
||||
ArrayList<ITerm> l = new ArrayList<ITerm>();
|
||||
l.add(t);
|
||||
return new RelationFormula(R, l);
|
||||
}
|
||||
|
||||
public static RelationFormula make(UnaryRelation R, int i) {
|
||||
ArrayList<ITerm> l = new ArrayList<ITerm>();
|
||||
l.add(IntConstant.make(i));
|
||||
return new RelationFormula(R, l);
|
||||
}
|
||||
|
||||
public static RelationFormula make(IRelation relation, List<ITerm> terms) {
|
||||
return new RelationFormula(relation, terms);
|
||||
}
|
||||
|
||||
@Override
|
||||
public int hashCode() {
|
||||
final int PRIME = 31;
|
||||
int result = 1;
|
||||
result = PRIME * result + ((R == null) ? 0 : R.hashCode());
|
||||
result = PRIME * result + ((terms == null) ? 0 : terms.hashCode());
|
||||
return result;
|
||||
}
|
||||
|
||||
@Override
|
||||
public boolean equals(Object obj) {
|
||||
if (this == obj)
|
||||
return true;
|
||||
if (obj == null)
|
||||
return false;
|
||||
if (getClass() != obj.getClass())
|
||||
return false;
|
||||
final RelationFormula other = (RelationFormula) obj;
|
||||
if (R == null) {
|
||||
if (other.R != null)
|
||||
return false;
|
||||
} else if (!R.equals(other.R))
|
||||
return false;
|
||||
if (terms == null) {
|
||||
if (other.terms != null)
|
||||
return false;
|
||||
} else if (!terms.equals(other.terms))
|
||||
return false;
|
||||
return true;
|
||||
}
|
||||
|
||||
public Kind getKind() {
|
||||
return Kind.RELATION;
|
||||
}
|
||||
|
||||
public Collection<AbstractVariable> getFreeVariables() {
|
||||
Collection<AbstractVariable> result = HashSetFactory.make(terms.size());
|
||||
for (ITerm t : terms) {
|
||||
result.addAll(t.getFreeVariables());
|
||||
}
|
||||
return result;
|
||||
}
|
||||
|
||||
public Collection<? extends IConstant> getConstants() {
|
||||
Collection<IConstant> result = HashSetFactory.make(terms.size());
|
||||
for (ITerm t : terms) {
|
||||
result.addAll(t.getConstants());
|
||||
}
|
||||
return result;
|
||||
}
|
||||
|
||||
@Override
|
||||
public String toString() {
|
||||
return prettyPrint(DefaultDecorator.instance());
|
||||
}
|
||||
|
||||
public String prettyPrint(ILogicDecorator d) throws IllegalArgumentException {
|
||||
if (d == null) {
|
||||
throw new IllegalArgumentException("d == null");
|
||||
}
|
||||
return d.prettyPrint(this);
|
||||
}
|
||||
|
||||
public String prefixNotation(ILogicDecorator d) {
|
||||
StringBuffer result = new StringBuffer(R.getSymbol());
|
||||
result.append("(");
|
||||
for (int i = 0; i < R.getValence() - 1; i++) {
|
||||
result.append(terms.get(i).prettyPrint(d));
|
||||
result.append(",");
|
||||
}
|
||||
if (R.getValence() > 0) {
|
||||
result.append(terms.get(R.getValence() - 1).prettyPrint(d));
|
||||
}
|
||||
result.append(")");
|
||||
return result.toString();
|
||||
}
|
||||
|
||||
public String infixNotation(ILogicDecorator d) {
|
||||
assert R.getValence() == 2;
|
||||
StringBuffer result = new StringBuffer();
|
||||
result.append(terms.get(0).prettyPrint(d));
|
||||
result.append(" ");
|
||||
result.append(R.getSymbol());
|
||||
result.append(" ");
|
||||
result.append(terms.get(1).prettyPrint(d));
|
||||
return result.toString();
|
||||
}
|
||||
|
||||
public Collection<? extends IMaxTerm> getMaxTerms() {
|
||||
return Collections.singleton(this);
|
||||
}
|
||||
|
||||
}
|
||||
|
|
@ -1,722 +0,0 @@
|
|||
/*******************************************************************************
|
||||
* Copyright (c) 2007 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 java.util.ArrayList;
|
||||
import java.util.Collection;
|
||||
import java.util.Collections;
|
||||
import java.util.Comparator;
|
||||
import java.util.List;
|
||||
import java.util.Map;
|
||||
|
||||
import com.ibm.wala.logic.ILogicConstants.BinaryConnective;
|
||||
import com.ibm.wala.util.collections.HashMapFactory;
|
||||
import com.ibm.wala.util.collections.HashSetFactory;
|
||||
import com.ibm.wala.util.debug.Assertions;
|
||||
|
||||
/**
|
||||
* Utilities for simplifying logic expressions
|
||||
*
|
||||
* @author sjfink
|
||||
*/
|
||||
public class Simplifier {
|
||||
|
||||
private final static boolean DEBUG = false;
|
||||
|
||||
/**
|
||||
* Eliminate quantifiers, by substituting every possible constant value for a quantified variable
|
||||
*/
|
||||
public static ITheory eliminateQuantifiers(ITheory t, Collection<? extends IFormula> constraints) {
|
||||
if (t == null) {
|
||||
throw new IllegalArgumentException("t is null");
|
||||
}
|
||||
Collection<IFormula> sentences = HashSetFactory.make();
|
||||
for (IFormula s : t.getSentencesRelevantToConstraints(constraints)) {
|
||||
sentences.addAll(eliminateQuantifiers(s));
|
||||
}
|
||||
return BasicTheory.make(t.getVocabulary(), sentences);
|
||||
}
|
||||
|
||||
/**
|
||||
* Eliminate quantifiers, by substituting every possible constant value for a quantified variable
|
||||
*/
|
||||
private static Collection<? extends IFormula> eliminateQuantifiers(IFormula 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);
|
||||
// }
|
||||
}
|
||||
|
||||
/**
|
||||
* Eliminate quantifiers, by substituting every possible constant value for a quantified variable
|
||||
*/
|
||||
public static Collection<? extends IFormula> eliminateQuantifiers(Collection<? extends IFormula> s) {
|
||||
if (s == null) {
|
||||
throw new IllegalArgumentException("s is null");
|
||||
}
|
||||
Collection<IFormula> result = HashSetFactory.make();
|
||||
for (IFormula f : s) {
|
||||
result.addAll(eliminateQuantifiers(f));
|
||||
}
|
||||
return result;
|
||||
}
|
||||
|
||||
/**
|
||||
* this is uglified a little to avoid tail recursion, which leads to stack overflow.
|
||||
*
|
||||
* This is inefficient.
|
||||
*/
|
||||
public static Collection<IFormula> simplify(Collection<? extends IFormula> s, Collection<? extends IFormula> theory,
|
||||
ISemiDecisionProcedure dec) {
|
||||
// the following is ad hoc and bogus.
|
||||
// boolean changed = true;
|
||||
// while (changed) {
|
||||
// changed = false;
|
||||
// Collection<IFormula> alreadyUsed = HashSetFactory.make();
|
||||
// Pair<ITerm, ITerm> substitution = getNextEqualitySubstitution(s, theory, alreadyUsed);
|
||||
// while (substitution != null) {
|
||||
// Collection<IFormula> temp = HashSetFactory.make();
|
||||
// for (IFormula f : s) {
|
||||
// if (!defines(f, substitution.fst)) {
|
||||
// IFormula f2 = substitute(f, substitution.fst, substitution.snd);
|
||||
// temp.add(f2);
|
||||
// if (!f.equals(f2)) {
|
||||
// changed = true;
|
||||
// }
|
||||
// } else {
|
||||
// temp.add(f);
|
||||
// }
|
||||
// }
|
||||
// s = temp;
|
||||
// substitution = getNextEqualitySubstitution(s, theory, alreadyUsed);
|
||||
// }
|
||||
// }
|
||||
return propositionalSimplify(s, theory, dec);
|
||||
}
|
||||
|
||||
/**
|
||||
* Simplify the set s based on simple propositional logic.
|
||||
*/
|
||||
public static Collection<IFormula> propositionalSimplify(Collection<? extends IFormula> s, Collection<? extends IFormula> t,
|
||||
ISemiDecisionProcedure dec) {
|
||||
debug1(s, t);
|
||||
Collection<ICNFFormula> cs = toCNF(s);
|
||||
Collection<ICNFFormula> ct = toCNF(t);
|
||||
debug2(cs, ct);
|
||||
Collection<IMaxTerm> facts = collectClauses(ct);
|
||||
|
||||
Collection<IFormula> result = HashSetFactory.make();
|
||||
for (ICNFFormula f : cs) {
|
||||
Collection<? extends IMaxTerm> d = simplifyCNF(f, facts, dec);
|
||||
result.add(CNFFormula.make(d));
|
||||
}
|
||||
|
||||
if (DEBUG) {
|
||||
System.err.println("--result--");
|
||||
for (IFormula f : result) {
|
||||
System.err.println(f);
|
||||
}
|
||||
}
|
||||
return result;
|
||||
}
|
||||
|
||||
/**
|
||||
* Simplify the set s based on simple propositional logic.
|
||||
*/
|
||||
public static IFormula propositionalSimplify(IFormula f, Collection<? extends IFormula> t, ISemiDecisionProcedure dec) {
|
||||
Collection<IFormula> result = propositionalSimplify(Collections.singleton(f), t, dec);
|
||||
return result.iterator().next();
|
||||
}
|
||||
|
||||
/**
|
||||
* Assuming a set of facts holds, simplify a CNF formula
|
||||
*/
|
||||
private static Collection<? extends IMaxTerm> simplifyCNF(ICNFFormula f, Collection<IMaxTerm> facts, ISemiDecisionProcedure dec) {
|
||||
Collection<IMaxTerm> result = HashSetFactory.make();
|
||||
Collection<IMaxTerm> removedClauses = HashSetFactory.make();
|
||||
// sort clauses in f, to ensure determinism
|
||||
List<IMaxTerm> sortedMaxTerms = new ArrayList<IMaxTerm>(f.getMaxTerms());
|
||||
Collections.sort(sortedMaxTerms, new Comparator<IMaxTerm>() {
|
||||
|
||||
public int compare(IMaxTerm o1, IMaxTerm o2) {
|
||||
return o1.toString().compareTo(o2.toString());
|
||||
}
|
||||
|
||||
});
|
||||
// for each clause in f ....
|
||||
for (IMaxTerm d : sortedMaxTerms) {
|
||||
// otherFacts := facts U live clauses of f - d
|
||||
Collection<IMaxTerm> otherFacts = HashSetFactory.make(facts);
|
||||
otherFacts.addAll(f.getMaxTerms());
|
||||
otherFacts.remove(d);
|
||||
otherFacts.removeAll(removedClauses);
|
||||
|
||||
IMaxTerm checkD = d;
|
||||
if (d instanceof Disjunction) {
|
||||
checkD = simplifyDisjunction((Disjunction) d, otherFacts, dec);
|
||||
}
|
||||
|
||||
if (dec.isContradiction(checkD, otherFacts)) {
|
||||
return Collections.singleton(BooleanConstantFormula.FALSE);
|
||||
} else if (facts.contains(checkD) || dec.isTautology(checkD, otherFacts)) {
|
||||
removedClauses.add(d);
|
||||
} else {
|
||||
result.add(checkD);
|
||||
}
|
||||
}
|
||||
if (result.isEmpty()) {
|
||||
return Collections.singleton(BooleanConstantFormula.TRUE);
|
||||
}
|
||||
return result;
|
||||
}
|
||||
|
||||
private static IMaxTerm simplifyDisjunction(Disjunction d, Collection<IMaxTerm> otherFacts, ISemiDecisionProcedure dec) {
|
||||
Collection<IFormula> result = HashSetFactory.make();
|
||||
for (IFormula f : d.getClauses()) {
|
||||
if (dec.isContradiction(f, otherFacts)) {
|
||||
result.add(BooleanConstantFormula.FALSE);
|
||||
} else if (dec.isTautology(f, otherFacts)) {
|
||||
result.add(BooleanConstantFormula.TRUE);
|
||||
} else {
|
||||
result.add(f);
|
||||
}
|
||||
}
|
||||
if (result.size() == 1) {
|
||||
IFormula f = result.iterator().next();
|
||||
assert f instanceof IMaxTerm;
|
||||
return (IMaxTerm) f;
|
||||
} else {
|
||||
return Disjunction.make(result);
|
||||
}
|
||||
}
|
||||
|
||||
/**
|
||||
* Collect all {@link IMaxTerm}s that appear in the formulae in s
|
||||
*/
|
||||
private static Collection<IMaxTerm> collectClauses(Collection<ICNFFormula> s) {
|
||||
Collection<IMaxTerm> result = HashSetFactory.make();
|
||||
for (ICNFFormula f : s) {
|
||||
if (f instanceof CNFFormula) {
|
||||
result.addAll(f.getMaxTerms());
|
||||
} else {
|
||||
result.add((IMaxTerm) f);
|
||||
}
|
||||
}
|
||||
return result;
|
||||
}
|
||||
|
||||
private static void debug2(Collection<ICNFFormula> cs, Collection<ICNFFormula> ct) {
|
||||
if (DEBUG) {
|
||||
System.err.println("--cs--");
|
||||
for (IFormula f : cs) {
|
||||
System.err.println(f);
|
||||
}
|
||||
System.err.println("--ct--");
|
||||
for (IFormula f : ct) {
|
||||
System.err.println(f);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
private static void debug1(Collection<? extends IFormula> s, Collection<? extends IFormula> t) {
|
||||
if (DEBUG) {
|
||||
System.err.println("--s--");
|
||||
for (IFormula f : s) {
|
||||
System.err.println(f);
|
||||
}
|
||||
System.err.println("--t--");
|
||||
for (IFormula f : t) {
|
||||
System.err.println(f);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
private static Collection<ICNFFormula> toCNF(Collection<? extends IFormula> s) {
|
||||
Collection<ICNFFormula> result = HashSetFactory.make();
|
||||
for (IFormula f : s) {
|
||||
result.add(CNFFormula.make(f));
|
||||
}
|
||||
return result;
|
||||
}
|
||||
|
||||
static boolean innerStructureMatches(QuantifiedFormula q, IFormula f) {
|
||||
IFormula g = innermost(q);
|
||||
if (!f.getKind().equals(g.getKind())) {
|
||||
return false;
|
||||
} else {
|
||||
// TODO be less conservative
|
||||
return true;
|
||||
}
|
||||
}
|
||||
|
||||
public static IFormula innermost(QuantifiedFormula q) throws IllegalArgumentException {
|
||||
if (q == null) {
|
||||
throw new IllegalArgumentException("q == null");
|
||||
}
|
||||
IFormula g = q.getFormula();
|
||||
if (g.getKind().equals(IFormula.Kind.QUANTIFIED)) {
|
||||
return innermost((QuantifiedFormula) g);
|
||||
} else {
|
||||
return g;
|
||||
}
|
||||
}
|
||||
|
||||
// static AbstractNumberedVariable makeFreshIntVariable(IFormula f, IFormula g) {
|
||||
// int max = 0;
|
||||
// for (AbstractVariable v : f.getFreeVariables()) {
|
||||
// max = Math.max(max, v.getNumber());
|
||||
// }
|
||||
// for (AbstractVariable v : g.getFreeVariables()) {
|
||||
// max = Math.max(max, v.getNumber());
|
||||
// }
|
||||
// return IntVariable.make(max + 1);
|
||||
// }
|
||||
|
||||
// /**
|
||||
// * Is f of the form t = rhs?
|
||||
// */
|
||||
// private static boolean defines(IFormula f, ITerm t) {
|
||||
// if (f.getKind().equals(IFormula.Kind.RELATION)) {
|
||||
// RelationFormula r = (RelationFormula) f;
|
||||
// if (r.getRelation().equals(BinaryRelation.EQUALS)) {
|
||||
// return r.getTerms().get(0).equals(t);
|
||||
// }
|
||||
// }
|
||||
// return false;
|
||||
// }
|
||||
//
|
||||
// /**
|
||||
// * does the structure of some formula f suggest an immediate substitution to
|
||||
// * simplify the system, based on theory of equality?
|
||||
// *
|
||||
// * @return a pair (p1, p2) meaning "substitute p2 for p1"
|
||||
// */
|
||||
// private static Pair<ITerm, ITerm> getNextEqualitySubstitution(Collection<IFormula> s, Collection<? extends
|
||||
// IFormula> theory,
|
||||
// Collection<IFormula> alreadyUsed) {
|
||||
// Collection<IFormula> candidates = HashSetFactory.make();
|
||||
// candidates.addAll(s);
|
||||
// candidates.addAll(theory);
|
||||
// for (IFormula f : candidates) {
|
||||
// if (!alreadyUsed.contains(f)) {
|
||||
// Pair<ITerm, ITerm> substitution = equalitySuggestsSubstitution(f);
|
||||
// if (substitution != null) {
|
||||
// alreadyUsed.add(f);
|
||||
// return substitution;
|
||||
// }
|
||||
// }
|
||||
// }
|
||||
// return null;
|
||||
// }
|
||||
|
||||
// /**
|
||||
// * does the structure of formula f suggest an immediate substitution to
|
||||
// * simplify the system, based on theory of equality?
|
||||
// *
|
||||
// * @return a pair (p1, p2) meaning "substitute p2 for p1"
|
||||
// */
|
||||
// private static Pair<ITerm, ITerm> equalitySuggestsSubstitution(IFormula f) {
|
||||
// switch (f.getKind()) {
|
||||
// case RELATION:
|
||||
// // it's not clear at this level that a constant or variable is "simpler" than
|
||||
// // e.g. a function term. so, don't do anything.
|
||||
// return null;
|
||||
// // RelationFormula r = (RelationFormula) f;
|
||||
// // if (r.getRelation().equals(BinaryRelation.EQUALS)) {
|
||||
// // ITerm lhs = r.getTerms().get(0);
|
||||
// // ITerm rhs = r.getTerms().get(1);
|
||||
// // if (rhs.getKind().equals(ITerm.Kind.CONSTANT) || rhs.getKind().equals(ITerm.Kind.VARIABLE)) {
|
||||
// // return Pair.make(lhs, rhs);
|
||||
// // } else {
|
||||
// // return null;
|
||||
// // }
|
||||
// // } else {
|
||||
// // return null;
|
||||
// // }
|
||||
// case QUANTIFIED:
|
||||
// QuantifiedFormula q = (QuantifiedFormula) f;
|
||||
// if (q.getQuantifier().equals(Quantifier.FORALL)) {
|
||||
// AbstractVariable bound = q.getBoundVar();
|
||||
// Wildcard w = freshWildcard(q);
|
||||
// IFormula g = substitute(q.getFormula(), bound, w);
|
||||
// return equalitySuggestsSubstitution(g);
|
||||
// } else {
|
||||
// return null;
|
||||
// }
|
||||
// case BINARY:
|
||||
// case CONSTANT:
|
||||
// case NEGATION:
|
||||
// default:
|
||||
// // TODO
|
||||
// return null;
|
||||
// }
|
||||
// }
|
||||
|
||||
// private static Wildcard freshWildcard(QuantifiedFormula q) {
|
||||
// int max = 0;
|
||||
// for (ITerm t : q.getAllTerms()) {
|
||||
// if (t instanceof Wildcard) {
|
||||
// Wildcard w = (Wildcard) t;
|
||||
// max = Math.max(max, w.getNumber());
|
||||
// }
|
||||
// }
|
||||
// return Wildcard.make(max + 1);
|
||||
// }
|
||||
|
||||
/**
|
||||
* in formula f, substitute the term t2 for all free occurrences of t1
|
||||
*
|
||||
* @throws IllegalArgumentException if formula is null
|
||||
*/
|
||||
public static IFormula substituteCNF(ICNFFormula formula, ITerm t1, ITerm t2) {
|
||||
Collection<IMaxTerm> maxTerms = new ArrayList<IMaxTerm>();
|
||||
for (IMaxTerm t : formula.getMaxTerms()) {
|
||||
maxTerms.add(substituteMaxTerm(t, t1, t2));
|
||||
}
|
||||
return CNFFormula.make(maxTerms);
|
||||
}
|
||||
|
||||
/**
|
||||
* in formula f, substitute the term t2 for all free occurrences of t1
|
||||
*
|
||||
* @throws IllegalArgumentException if formula is null
|
||||
*/
|
||||
public static IMaxTerm substituteMaxTerm(IMaxTerm formula, ITerm t1, ITerm t2) {
|
||||
if (formula == null) {
|
||||
throw new IllegalArgumentException("formula is null");
|
||||
}
|
||||
switch (formula.getKind()) {
|
||||
case BINARY:
|
||||
Disjunction d = (Disjunction)formula;
|
||||
Collection<IFormula> c = HashSetFactory.make();
|
||||
for (IFormula clause : d.getClauses()) {
|
||||
c.add(substitute(clause, t1, t2));
|
||||
}
|
||||
return Disjunction.make(c);
|
||||
case NEGATION:
|
||||
NotFormulaMaxTerm n = (NotFormulaMaxTerm) formula;
|
||||
RelationFormula F = (RelationFormula) n.getFormula();
|
||||
RelationFormula subF = (RelationFormula)substitute(F, t1, t2);
|
||||
return (F != subF ? NotFormulaMaxTerm.createNotFormulaMaxTerm(subF) : formula);
|
||||
case QUANTIFIED:
|
||||
Assertions.UNREACHABLE();
|
||||
return null;
|
||||
case RELATION:
|
||||
RelationFormula r = (RelationFormula) formula;
|
||||
List<ITerm> rTerms = r.getTerms();
|
||||
List<ITerm> terms = new ArrayList<ITerm>(rTerms.size());
|
||||
boolean someChange = false;
|
||||
for (ITerm t : rTerms) {
|
||||
Map<Wildcard, ITerm> binding = HashMapFactory.make();
|
||||
ITerm subTerm = substituteInTerm(t, t1, t2, binding);
|
||||
terms.add(subTerm);
|
||||
someChange = someChange || t != subTerm;
|
||||
}
|
||||
if (someChange) {
|
||||
return RelationFormula.make(r.getRelation(), terms);
|
||||
} else {
|
||||
return formula;
|
||||
}
|
||||
case CONSTANT:
|
||||
return formula;
|
||||
default:
|
||||
Assertions.UNREACHABLE();
|
||||
return null;
|
||||
}
|
||||
}
|
||||
|
||||
/**
|
||||
* in formula f, substitute the term t2 for all free occurrences of t1
|
||||
*
|
||||
* @throws IllegalArgumentException if formula is null
|
||||
*/
|
||||
public static IFormula substitute(IFormula formula, ITerm t1, ITerm t2) {
|
||||
if (formula == null) {
|
||||
throw new IllegalArgumentException("formula is null");
|
||||
}
|
||||
if (formula instanceof ICNFFormula) {
|
||||
return substituteCNF((ICNFFormula) formula, t1, t2);
|
||||
} else {
|
||||
switch (formula.getKind()) {
|
||||
case BINARY:
|
||||
AbstractBinaryFormula b = (AbstractBinaryFormula) formula;
|
||||
// TODO separate out cases for CNFFormula and Disjunction?
|
||||
IFormula F1 = b.getF1();
|
||||
IFormula subF1 = substitute(F1, t1, t2);
|
||||
IFormula F2 = b.getF2();
|
||||
IFormula subF2 = substitute(F2, t1, t2);
|
||||
if (F1 != subF1 || F2 != subF2) {
|
||||
return BinaryFormula.make(b.getConnective(), subF1, subF2);
|
||||
} else {
|
||||
return formula;
|
||||
}
|
||||
case NEGATION:
|
||||
NotFormula n = (NotFormula) formula;
|
||||
IFormula F = n.getFormula();
|
||||
IFormula subF = substitute(F, t1, t2);
|
||||
return F != subF ? NotFormula.make(subF) : formula;
|
||||
case QUANTIFIED:
|
||||
QuantifiedFormula q = (QuantifiedFormula) formula;
|
||||
if (q.getBoundVar().equals(t1)) {
|
||||
return q;
|
||||
} else {
|
||||
IFormula body = q.getFormula();
|
||||
IFormula subBody = substitute(body, t1, t2);
|
||||
if (body != subBody) {
|
||||
return QuantifiedFormula.make(q.getQuantifier(), q.getBoundVar(), subBody);
|
||||
} else {
|
||||
return formula;
|
||||
}
|
||||
}
|
||||
case RELATION:
|
||||
RelationFormula r = (RelationFormula) formula;
|
||||
List<ITerm> rTerms = r.getTerms();
|
||||
List<ITerm> terms = new ArrayList<ITerm>(rTerms.size());
|
||||
boolean someChange = false;
|
||||
for (ITerm t : rTerms) {
|
||||
Map<Wildcard, ITerm> binding = HashMapFactory.make();
|
||||
ITerm subTerm = substituteInTerm(t, t1, t2, binding);
|
||||
terms.add(subTerm);
|
||||
someChange = someChange || t != subTerm;
|
||||
}
|
||||
if (someChange) {
|
||||
return RelationFormula.make(r.getRelation(), terms);
|
||||
} else {
|
||||
return formula;
|
||||
}
|
||||
case CONSTANT:
|
||||
return formula;
|
||||
default:
|
||||
Assertions.UNREACHABLE();
|
||||
return null;
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
/**
|
||||
* in term t, substitute t2 for free occurrences of t1
|
||||
*/
|
||||
public static ITerm substituteInTerm(ITerm t, ITerm t1, ITerm t2, Map<Wildcard, ITerm> binding) {
|
||||
assert t != null;
|
||||
assert t1 != null;
|
||||
assert t2 != null;
|
||||
if (termsMatch(t, t1, binding)) {
|
||||
ITerm result = bindingOf(t2, binding);
|
||||
assert result != null;
|
||||
return result;
|
||||
}
|
||||
switch (t.getKind()) {
|
||||
case CONSTANT:
|
||||
return t;
|
||||
case FUNCTION:
|
||||
FunctionTerm f = (FunctionTerm) t;
|
||||
List<ITerm> parameters = f.getParameters();
|
||||
List<ITerm> terms = new ArrayList<ITerm>(parameters.size());
|
||||
boolean someChange = false;
|
||||
for (ITerm p : parameters) {
|
||||
ITerm subTerm = substituteInTerm(p, t1, t2, binding);
|
||||
terms.add(subTerm);
|
||||
someChange = someChange || p != subTerm;
|
||||
}
|
||||
if (someChange) {
|
||||
return FunctionTerm.make(f.getFunction(), terms);
|
||||
} else {
|
||||
return t;
|
||||
}
|
||||
case VARIABLE:
|
||||
if (t1.equals(t)) {
|
||||
return t2;
|
||||
} else {
|
||||
return t;
|
||||
}
|
||||
default:
|
||||
Assertions.UNREACHABLE();
|
||||
return null;
|
||||
}
|
||||
}
|
||||
|
||||
private static ITerm bindingOf(ITerm t, Map<Wildcard, ITerm> binding) {
|
||||
assert t != null;
|
||||
switch (t.getKind()) {
|
||||
case CONSTANT:
|
||||
if (t instanceof Wildcard) {
|
||||
ITerm result = binding.get(t);
|
||||
if (result == null) {
|
||||
return t;
|
||||
} else {
|
||||
return result;
|
||||
}
|
||||
} else {
|
||||
return t;
|
||||
}
|
||||
case VARIABLE:
|
||||
return t;
|
||||
case FUNCTION:
|
||||
FunctionTerm ft = (FunctionTerm) t;
|
||||
List<ITerm> terms = new ArrayList<ITerm>();
|
||||
boolean someChange = false;
|
||||
for (ITerm p : ft.getParameters()) {
|
||||
ITerm bindingOfP = bindingOf(p, binding);
|
||||
terms.add(bindingOfP);
|
||||
someChange = someChange || p != bindingOfP;
|
||||
}
|
||||
if (someChange) {
|
||||
return FunctionTerm.make(ft.getFunction(), terms);
|
||||
} else {
|
||||
return t;
|
||||
}
|
||||
default:
|
||||
Assertions.UNREACHABLE(t);
|
||||
return null;
|
||||
}
|
||||
}
|
||||
|
||||
/**
|
||||
* Does the term t1 match the pattern t2? Note that this deals with wildcards. Records bindings from Wildcards to
|
||||
* Terms in the binding map ... modified as a side effect.
|
||||
*/
|
||||
private static boolean termsMatch(ITerm t1, ITerm t2, Map<Wildcard, ITerm> binding) {
|
||||
if (t1.equals(t2)) {
|
||||
return true;
|
||||
}
|
||||
if (t2 instanceof Wildcard) {
|
||||
Wildcard w = (Wildcard) t2;
|
||||
ITerm b = binding.get(w);
|
||||
if (b != null) {
|
||||
return b.equals(t1);
|
||||
} else {
|
||||
binding.put(w, t1);
|
||||
return true;
|
||||
}
|
||||
}
|
||||
|
||||
switch (t1.getKind()) {
|
||||
case CONSTANT:
|
||||
case VARIABLE:
|
||||
return false;
|
||||
case FUNCTION:
|
||||
if (t2 instanceof FunctionTerm) {
|
||||
FunctionTerm f1 = (FunctionTerm) t1;
|
||||
FunctionTerm f2 = (FunctionTerm) t2;
|
||||
if (f1.getFunction().equals(f2.getFunction())) {
|
||||
for (int i = 0; i < f1.getParameters().size(); i++) {
|
||||
ITerm x = f1.getParameters().get(i);
|
||||
ITerm y = f2.getParameters().get(i);
|
||||
if (!termsMatch(x, y, binding)) {
|
||||
return false;
|
||||
}
|
||||
}
|
||||
return true;
|
||||
}
|
||||
}
|
||||
return false;
|
||||
default:
|
||||
Assertions.UNREACHABLE();
|
||||
return false;
|
||||
}
|
||||
}
|
||||
|
||||
public static Collection<AbstractVariable> getFreeVariables(Collection<? extends IFormula> constraints) {
|
||||
if (constraints == null) {
|
||||
throw new IllegalArgumentException("constraints is null");
|
||||
}
|
||||
Collection<AbstractVariable> free = HashSetFactory.make();
|
||||
for (IFormula f : constraints) {
|
||||
free.addAll(f.getFreeVariables());
|
||||
}
|
||||
return free;
|
||||
}
|
||||
|
||||
/**
|
||||
* Attempt to distribute the NOT from a NotFormula
|
||||
*
|
||||
* @return the original formula if the distribution is unsuccessful
|
||||
* @throws IllegalArgumentException if f == null
|
||||
*/
|
||||
public static IFormula distributeNot(NotFormula f) throws IllegalArgumentException {
|
||||
if (f == null) {
|
||||
throw new IllegalArgumentException("f == null");
|
||||
}
|
||||
IFormula f1 = f.getFormula();
|
||||
if (f1 instanceof RelationFormula) {
|
||||
RelationFormula r = (RelationFormula) f1;
|
||||
BinaryRelation negate = BinaryRelation.negate(r.getRelation());
|
||||
if (negate == null) {
|
||||
return f;
|
||||
} else {
|
||||
return RelationFormula.make(negate, r.getTerms());
|
||||
}
|
||||
} else if (f1 instanceof AbstractBinaryFormula) {
|
||||
AbstractBinaryFormula bf = (AbstractBinaryFormula) f1;
|
||||
if (bf.getConnective().equals(BinaryConnective.AND)) {
|
||||
// DeMorgan: not(a and b) = not(a) or not(b)
|
||||
IFormula notA = NotFormula.make(bf.getF1());
|
||||
IFormula notB = NotFormula.make(bf.getF2());
|
||||
if (notA instanceof NotFormula) {
|
||||
notA = distributeNot((NotFormula) notA);
|
||||
}
|
||||
if (notB instanceof NotFormula) {
|
||||
notB = distributeNot((NotFormula) notB);
|
||||
}
|
||||
return BinaryFormula.or(notA, notB);
|
||||
} else if (bf.getConnective().equals(BinaryConnective.OR)) {
|
||||
// DeMorgan: not(a or b) = not(a) and not(b)
|
||||
IFormula notA = NotFormula.make(bf.getF1());
|
||||
IFormula notB = NotFormula.make(bf.getF2());
|
||||
if (notA instanceof NotFormula) {
|
||||
notA = distributeNot((NotFormula) notA);
|
||||
}
|
||||
if (notB instanceof NotFormula) {
|
||||
notB = distributeNot((NotFormula) notB);
|
||||
}
|
||||
return BinaryFormula.and(notA, notB);
|
||||
|
||||
}
|
||||
}
|
||||
return f;
|
||||
}
|
||||
|
||||
public static IFormula simplify(IFormula f, ISemiDecisionProcedure dec) {
|
||||
Collection<Disjunction> emptyTheory = Collections.emptySet();
|
||||
Collection<IFormula> single = Collections.singleton(f);
|
||||
Collection<IFormula> result = propositionalSimplify(single, emptyTheory, dec);
|
||||
assert result.size() == 1;
|
||||
return result.iterator().next();
|
||||
}
|
||||
|
||||
public static IFormula propositionalSimplify(IFormula f, ISemiDecisionProcedure dec) {
|
||||
Collection<IFormula> emptySet = Collections.emptySet();
|
||||
Collection<IFormula> singleton = Collections.singleton(f);
|
||||
Collection<IFormula> result = propositionalSimplify(singleton, emptySet, dec);
|
||||
assert result.size() == 1;
|
||||
return result.iterator().next();
|
||||
}
|
||||
|
||||
public static IFormula simplify(IFormula f, IFormula t, ISemiDecisionProcedure dec) {
|
||||
Collection<IFormula> s = simplify(Collections.singleton(f), Collections.singleton(t), dec);
|
||||
assert s.size() == 1;
|
||||
return s.iterator().next();
|
||||
}
|
||||
|
||||
}
|
||||
|
|
@ -1,93 +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 java.util.Collection;
|
||||
import java.util.Set;
|
||||
|
||||
import com.ibm.wala.util.collections.HashSetFactory;
|
||||
import com.ibm.wala.util.intset.IBinaryNaturalRelation;
|
||||
import com.ibm.wala.util.intset.IntPair;
|
||||
import com.ibm.wala.util.intset.IntSet;
|
||||
|
||||
public class UnaryFunction implements IFunction {
|
||||
|
||||
private final String symbol;
|
||||
|
||||
protected UnaryFunction(String symbol) {
|
||||
this.symbol = symbol;
|
||||
}
|
||||
|
||||
public static UnaryFunction make(String symbol) {
|
||||
return new UnaryFunction(symbol);
|
||||
}
|
||||
|
||||
public int getNumberOfParameters() {
|
||||
return 1;
|
||||
}
|
||||
|
||||
public String getSymbol() {
|
||||
return symbol;
|
||||
}
|
||||
|
||||
/**
|
||||
* Build constraints which ensure that the function f defines the relation R.
|
||||
* @param domain
|
||||
* @throws IllegalArgumentException if domain is null
|
||||
*/
|
||||
public static Collection<IFormula> buildConstraints(IBinaryNaturalRelation R, UnaryFunction f, 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) {
|
||||
assert (s.size() == 1);
|
||||
result.add(RelationFormula.makeEquals(FunctionTerm.make(f, i), s.intIterator().next()));
|
||||
} else {
|
||||
result.add(RelationFormula.makeEquals(FunctionTerm.make(f, i), -1));
|
||||
}
|
||||
}
|
||||
return result;
|
||||
}
|
||||
|
||||
@Override
|
||||
public String toString() {
|
||||
return getSymbol() + " : int -> int";
|
||||
}
|
||||
|
||||
@Override
|
||||
public int hashCode() {
|
||||
final int prime = 31;
|
||||
int result = 1;
|
||||
result = prime * result + ((symbol == null) ? 0 : symbol.hashCode());
|
||||
return result;
|
||||
}
|
||||
|
||||
@Override
|
||||
public boolean equals(Object obj) {
|
||||
if (this == obj)
|
||||
return true;
|
||||
if (obj == null)
|
||||
return false;
|
||||
if (getClass() != obj.getClass())
|
||||
return false;
|
||||
final UnaryFunction other = (UnaryFunction) obj;
|
||||
if (symbol == null) {
|
||||
if (other.symbol != null)
|
||||
return false;
|
||||
} else if (!symbol.equals(other.symbol))
|
||||
return false;
|
||||
return true;
|
||||
}
|
||||
|
||||
}
|
||||
|
|
@ -1,65 +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;
|
||||
|
||||
|
||||
public class UnaryRelation implements IRelation {
|
||||
|
||||
private final String symbol;
|
||||
|
||||
protected UnaryRelation(String symbol) {
|
||||
this.symbol = symbol;
|
||||
}
|
||||
|
||||
public int getValence() {
|
||||
return 1;
|
||||
}
|
||||
|
||||
@Override
|
||||
public String toString() {
|
||||
return getSymbol() + " : int ";
|
||||
}
|
||||
|
||||
@Override
|
||||
public int hashCode() {
|
||||
final int PRIME = 31;
|
||||
int result = 1;
|
||||
result = PRIME * result + ((symbol == null) ? 0 : symbol.hashCode());
|
||||
return result;
|
||||
}
|
||||
|
||||
@Override
|
||||
public boolean equals(Object obj) {
|
||||
if (this == obj)
|
||||
return true;
|
||||
if (obj == null)
|
||||
return false;
|
||||
if (getClass() != obj.getClass())
|
||||
return false;
|
||||
final UnaryRelation other = (UnaryRelation) obj;
|
||||
if (symbol == null) {
|
||||
if (other.symbol != null)
|
||||
return false;
|
||||
} else if (!symbol.equals(other.symbol))
|
||||
return false;
|
||||
return true;
|
||||
}
|
||||
|
||||
public String getSymbol() {
|
||||
return symbol;
|
||||
}
|
||||
|
||||
|
||||
public static UnaryRelation make(String symbol) {
|
||||
return new UnaryRelation(symbol);
|
||||
}
|
||||
|
||||
}
|
||||
|
|
@ -1,60 +0,0 @@
|
|||
/*******************************************************************************
|
||||
* Copyright (c) 2007 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;
|
||||
|
||||
/**
|
||||
* A special constant used for pattern matching during substitution.
|
||||
*
|
||||
* @author sjfink
|
||||
*/
|
||||
public class Wildcard extends AbstractConstant {
|
||||
|
||||
private final int number;
|
||||
private Wildcard(int number) {
|
||||
this.number = number;
|
||||
}
|
||||
|
||||
@Override
|
||||
public String toString() {
|
||||
return "?" + number + "?";
|
||||
}
|
||||
|
||||
@Override
|
||||
public int hashCode() {
|
||||
final int prime = 31;
|
||||
int result = 1;
|
||||
result = prime * result + number;
|
||||
return result;
|
||||
}
|
||||
|
||||
@Override
|
||||
public boolean equals(Object obj) {
|
||||
if (this == obj)
|
||||
return true;
|
||||
if (obj == null)
|
||||
return false;
|
||||
if (getClass() != obj.getClass())
|
||||
return false;
|
||||
final Wildcard other = (Wildcard) obj;
|
||||
if (number != other.number)
|
||||
return false;
|
||||
return true;
|
||||
}
|
||||
|
||||
public int getNumber() {
|
||||
return number;
|
||||
}
|
||||
|
||||
public static Wildcard make(int i) {
|
||||
return new Wildcard(i);
|
||||
}
|
||||
|
||||
}
|
||||
Loading…
Reference in New Issue