CNF and related support
git-svn-id: https://wala.svn.sourceforge.net/svnroot/wala/trunk@1404 f5eafffb-2e1d-0410-98e4-8ec43c5233c4
This commit is contained in:
sjfink
parent
56cda5a9e2
commit
078deea908
|
|
@ -0,0 +1,30 @@
|
|||
/*******************************************************************************
|
||||
* 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();
|
||||
}
|
||||
|
|
@ -16,7 +16,7 @@ import java.util.Iterator;
|
|||
import com.ibm.wala.logic.ILogicConstants.BinaryConnective;
|
||||
import com.ibm.wala.util.collections.HashSetFactory;
|
||||
|
||||
public class BinaryFormula implements IFormula {
|
||||
public class BinaryFormula extends AbstractBinaryFormula {
|
||||
private final IFormula f1;
|
||||
|
||||
private final IFormula f2;
|
||||
|
|
@ -30,10 +30,6 @@ public class BinaryFormula implements IFormula {
|
|||
this.f2 = f2;
|
||||
}
|
||||
|
||||
public Kind getKind() {
|
||||
return Kind.BINARY;
|
||||
}
|
||||
|
||||
public static IFormula and(Collection<IFormula> clauses) throws IllegalArgumentException {
|
||||
if (clauses == null) {
|
||||
throw new IllegalArgumentException("clauses is null");
|
||||
|
|
@ -85,14 +81,17 @@ public class BinaryFormula implements IFormula {
|
|||
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;
|
||||
}
|
||||
|
|
@ -113,13 +112,13 @@ public class BinaryFormula implements IFormula {
|
|||
|
||||
public String prettyPrint(ILogicDecorator d) {
|
||||
StringBuffer result = new StringBuffer();
|
||||
result.append("(");
|
||||
result.append(" ( ");
|
||||
result.append(f1.prettyPrint(d));
|
||||
result.append(") ");
|
||||
result.append(" ) ");
|
||||
result.append(d.prettyPrint(b));
|
||||
result.append(" (");
|
||||
result.append(" ( ");
|
||||
result.append(f2.prettyPrint(d));
|
||||
result.append(")");
|
||||
result.append(" )");
|
||||
return result.toString();
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -0,0 +1,367 @@
|
|||
/*******************************************************************************
|
||||
* 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.HashSet;
|
||||
|
||||
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 {
|
||||
|
||||
private static final boolean DEBUG = true;
|
||||
|
||||
// invariant: size >= 1
|
||||
private final Collection<Disjunction> disjunctions;
|
||||
|
||||
private CNFFormula(Collection<Disjunction> clauses) {
|
||||
assert !clauses.isEmpty();
|
||||
this.disjunctions = clauses;
|
||||
}
|
||||
|
||||
public Collection<? extends IConstant> getConstants() {
|
||||
Collection<IConstant> result = HashSetFactory.make();
|
||||
for (IFormula f : disjunctions) {
|
||||
result.addAll(f.getConstants());
|
||||
}
|
||||
return result;
|
||||
}
|
||||
|
||||
public Collection<Variable> getFreeVariables() {
|
||||
Collection<Variable> result = HashSetFactory.make();
|
||||
for (IFormula f : disjunctions) {
|
||||
result.addAll(f.getFreeVariables());
|
||||
}
|
||||
return result;
|
||||
}
|
||||
|
||||
public boolean isAtomic() {
|
||||
return false;
|
||||
}
|
||||
|
||||
public String prettyPrint(ILogicDecorator d) {
|
||||
if (disjunctions.size() == 1) {
|
||||
return getF1().prettyPrint(d);
|
||||
} else {
|
||||
StringBuffer result = new StringBuffer();
|
||||
result.append(" ( ");
|
||||
result.append(getF1().prettyPrint(d));
|
||||
result.append(" ) ");
|
||||
result.append(d.prettyPrint(getConnective()));
|
||||
result.append(" ( ");
|
||||
result.append(getF2().prettyPrint(d));
|
||||
result.append(" )");
|
||||
return result.toString();
|
||||
}
|
||||
}
|
||||
|
||||
public static CNFFormula make(IFormula f) {
|
||||
if (DEBUG) {
|
||||
System.err.println("make CNF " + f);
|
||||
}
|
||||
if (f instanceof CNFFormula) {
|
||||
return (CNFFormula) f;
|
||||
} else {
|
||||
switch (f.getKind()) {
|
||||
case RELATION:
|
||||
case QUANTIFIED:
|
||||
case CONSTANT:
|
||||
Disjunction single = Disjunction.make(Collections.singleton(f));
|
||||
Collection<Disjunction> clauses = Collections.singleton(single);
|
||||
return new CNFFormula(clauses);
|
||||
case BINARY:
|
||||
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) {
|
||||
AbstractBinaryFormula b = (AbstractBinaryFormula) f;
|
||||
assert (b.getConnective().equals(BinaryConnective.AND));
|
||||
return new CNFFormula(collectClauses(b));
|
||||
} else {
|
||||
return CNFFormula.make(f);
|
||||
}
|
||||
case NEGATION:
|
||||
default:
|
||||
Assertions.UNREACHABLE(f + " " + f.getKind());
|
||||
return null;
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
private static Collection<Disjunction> collectClauses(AbstractBinaryFormula b) {
|
||||
assert (b.getConnective().equals(BinaryConnective.AND));
|
||||
Collection<Disjunction> result = HashSetFactory.make();
|
||||
IFormula f1 = b.getF1();
|
||||
if (f1 instanceof AbstractBinaryFormula) {
|
||||
AbstractBinaryFormula b1 = (AbstractBinaryFormula) f1;
|
||||
if (b1.getConnective().equals(BinaryConnective.AND)) {
|
||||
result.addAll(collectClauses(b1));
|
||||
} else {
|
||||
result.add(toDisjunction(b1));
|
||||
}
|
||||
} else {
|
||||
result.add(toDisjunction(f1));
|
||||
}
|
||||
|
||||
IFormula f2 = b.getF2();
|
||||
if (f2 instanceof AbstractBinaryFormula) {
|
||||
AbstractBinaryFormula b2 = (AbstractBinaryFormula) f2;
|
||||
if (b2.getConnective().equals(BinaryConnective.AND)) {
|
||||
result.addAll(collectClauses(b2));
|
||||
} else {
|
||||
result.add(toDisjunction(b2));
|
||||
}
|
||||
} else {
|
||||
result.add(toDisjunction(f2));
|
||||
}
|
||||
return result;
|
||||
}
|
||||
|
||||
private static Disjunction toDisjunction(IFormula f) {
|
||||
switch (f.getKind()) {
|
||||
case BINARY:
|
||||
AbstractBinaryFormula b = (AbstractBinaryFormula) f;
|
||||
if (b.getConnective().equals(BinaryConnective.OR)) {
|
||||
IFormula f1 = b.getF1();
|
||||
Disjunction d2 = toDisjunction(b.getF2());
|
||||
Collection<IFormula> c = HashSetFactory.make();
|
||||
c.add(f1);
|
||||
c.addAll(d2.getClauses());
|
||||
return Disjunction.make(c);
|
||||
} else {
|
||||
Assertions.UNREACHABLE(b);
|
||||
return null;
|
||||
}
|
||||
case CONSTANT:
|
||||
case QUANTIFIED:
|
||||
case RELATION:
|
||||
return Disjunction.make(Collections.singleton(f));
|
||||
case NEGATION:
|
||||
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(IFormula f) {
|
||||
switch (f.getKind()) {
|
||||
case BINARY:
|
||||
return distribute((AbstractBinaryFormula) f);
|
||||
case CONSTANT:
|
||||
case QUANTIFIED:
|
||||
case RELATION:
|
||||
return f;
|
||||
case NEGATION:
|
||||
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));
|
||||
return 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:
|
||||
default:
|
||||
Assertions.UNREACHABLE(f.getKind());
|
||||
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:
|
||||
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);
|
||||
Collection<Disjunction> emptyTheory = Collections.emptySet();
|
||||
|
||||
switch (b.getConnective()) {
|
||||
case BICONDITIONAL:
|
||||
if (Simplifier.isTautology(f1, emptyTheory)) {
|
||||
return f2;
|
||||
} else if (Simplifier.isContradiction(f1, emptyTheory)) {
|
||||
return BooleanConstantFormula.FALSE;
|
||||
} 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:
|
||||
default:
|
||||
Assertions.UNREACHABLE(b);
|
||||
return null;
|
||||
}
|
||||
}
|
||||
|
||||
@Override
|
||||
public int hashCode() {
|
||||
final int prime = 31;
|
||||
int result = 1;
|
||||
result = prime * result + ((disjunctions == null) ? 0 : disjunctions.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 (disjunctions == null) {
|
||||
if (other.disjunctions != null)
|
||||
return false;
|
||||
} else if (!disjunctions.equals(other.disjunctions))
|
||||
return false;
|
||||
return true;
|
||||
}
|
||||
|
||||
@Override
|
||||
public BinaryConnective getConnective() {
|
||||
return BinaryConnective.AND;
|
||||
}
|
||||
|
||||
@Override
|
||||
public IFormula getF1() {
|
||||
return disjunctions.iterator().next();
|
||||
}
|
||||
|
||||
@Override
|
||||
public IFormula getF2() {
|
||||
// if clauses.size() == 1, we fake this by saying we are getF1() AND true
|
||||
if (disjunctions.size() == 1) {
|
||||
return BooleanConstantFormula.TRUE;
|
||||
} else {
|
||||
Collection<Disjunction> c = new HashSet<Disjunction>(disjunctions);
|
||||
c.remove(getF1());
|
||||
return new CNFFormula(c);
|
||||
}
|
||||
}
|
||||
|
||||
@Override
|
||||
public String toString() {
|
||||
return prettyPrint(DefaultDecorator.instance());
|
||||
}
|
||||
|
||||
public Collection<? extends Disjunction> getDisjunctions() {
|
||||
return Collections.unmodifiableCollection(disjunctions);
|
||||
}
|
||||
|
||||
public static CNFFormula make(Collection<Disjunction> d) {
|
||||
return new CNFFormula(d);
|
||||
}
|
||||
|
||||
}
|
||||
|
|
@ -0,0 +1,139 @@
|
|||
/*******************************************************************************
|
||||
* 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.HashSet;
|
||||
|
||||
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 {
|
||||
|
||||
// invariant: size >= 1
|
||||
private final Collection<? extends IFormula> clauses;
|
||||
|
||||
private Disjunction(Collection<? extends IFormula> clauses) {
|
||||
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<Variable> getFreeVariables() {
|
||||
Collection<Variable> result = HashSetFactory.make();
|
||||
for (IFormula f : clauses) {
|
||||
result.addAll(f.getFreeVariables());
|
||||
}
|
||||
return result;
|
||||
}
|
||||
|
||||
public boolean isAtomic() {
|
||||
return false;
|
||||
}
|
||||
|
||||
public String prettyPrint(ILogicDecorator d) {
|
||||
if (clauses.size() == 1) {
|
||||
return getF1().prettyPrint(d);
|
||||
} else {
|
||||
StringBuffer result = new StringBuffer();
|
||||
result.append(" ( ");
|
||||
result.append(getF1().prettyPrint(d));
|
||||
result.append(" ) ");
|
||||
result.append(d.prettyPrint(getConnective()));
|
||||
result.append(" ( ");
|
||||
result.append(getF2().prettyPrint(d));
|
||||
result.append(" )");
|
||||
return result.toString();
|
||||
}
|
||||
}
|
||||
|
||||
@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() {
|
||||
// if clauses.size() == 1, we fake this by saying we are getF1() OR false
|
||||
if (clauses.size() == 1) {
|
||||
return BooleanConstantFormula.FALSE;
|
||||
} else {
|
||||
Collection<IFormula> c = new HashSet<IFormula>(clauses);
|
||||
c.remove(getF1());
|
||||
return make(c);
|
||||
}
|
||||
}
|
||||
|
||||
public static Disjunction make(Collection<? extends IFormula> clauses) {
|
||||
for (IFormula c: clauses) {
|
||||
assert !(c instanceof Disjunction);
|
||||
}
|
||||
return new Disjunction(clauses);
|
||||
}
|
||||
|
||||
public Collection<? extends IFormula> getClauses() {
|
||||
return Collections.unmodifiableCollection(clauses);
|
||||
}
|
||||
|
||||
public static Disjunction make(BooleanConstantFormula f) {
|
||||
Collection<? extends IFormula> c = Collections.singleton(f);
|
||||
return new Disjunction(c);
|
||||
}
|
||||
|
||||
|
||||
@Override
|
||||
public String toString() {
|
||||
return prettyPrint(DefaultDecorator.instance());
|
||||
}
|
||||
|
||||
}
|
||||
|
|
@ -29,6 +29,12 @@ import com.ibm.wala.util.intset.IntPair;
|
|||
*/
|
||||
public class Simplifier {
|
||||
|
||||
private final static boolean DEBUG = true;
|
||||
|
||||
/**
|
||||
* Eliminate quantifiers, by substituting every possible constant value for a
|
||||
* quantified variable
|
||||
*/
|
||||
public static ITheory eliminateQuantifiers(ITheory t) {
|
||||
if (t == null) {
|
||||
throw new IllegalArgumentException("t is null");
|
||||
|
|
@ -40,6 +46,10 @@ public class Simplifier {
|
|||
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) {
|
||||
if (s.getKind().equals(IFormula.Kind.QUANTIFIED)) {
|
||||
Collection<IFormula> result = HashSetFactory.make();
|
||||
|
|
@ -79,7 +89,7 @@ public class Simplifier {
|
|||
while (changed) {
|
||||
changed = false;
|
||||
Collection<IFormula> alreadyUsed = HashSetFactory.make();
|
||||
Pair<ITerm, ITerm> substitution = getNextSubCandidate(s, t, alreadyUsed);
|
||||
Pair<ITerm, ITerm> substitution = getNextEqualitySubstitution(s, t, alreadyUsed);
|
||||
while (substitution != null) {
|
||||
Collection<IFormula> temp = HashSetFactory.make();
|
||||
for (IFormula f : s) {
|
||||
|
|
@ -94,35 +104,129 @@ public class Simplifier {
|
|||
}
|
||||
}
|
||||
s = temp;
|
||||
substitution = getNextSubCandidate(s, t, alreadyUsed);
|
||||
substitution = getNextEqualitySubstitution(s, t, alreadyUsed);
|
||||
}
|
||||
}
|
||||
return trivialDecision(s);
|
||||
return propositionalSimplify(s, t.getSentences());
|
||||
}
|
||||
|
||||
/**
|
||||
* Check simple satisfiability rules for each formula in a collection. Replace
|
||||
* tautologies with "true" and contradictions with false.
|
||||
* Simplify the set s based on simple propositional logic.
|
||||
*/
|
||||
private static Collection<IFormula> trivialDecision(Collection<IFormula> s) {
|
||||
public static Collection<IFormula> propositionalSimplify(Collection<IFormula> s, Collection<? extends IFormula> t) {
|
||||
debug1(s, t);
|
||||
Collection<CNFFormula> cs = toCNF(s);
|
||||
Collection<CNFFormula> ct = toCNF(t);
|
||||
debug2(cs, ct);
|
||||
Collection<Disjunction> facts = collectClauses(ct);
|
||||
|
||||
Collection<IFormula> result = HashSetFactory.make();
|
||||
for (IFormula f : s) {
|
||||
if (isTautology(f)) {
|
||||
result.add(BooleanConstantFormula.TRUE);
|
||||
} else if (isContradiction(f)) {
|
||||
result.add(BooleanConstantFormula.FALSE);
|
||||
for (CNFFormula f : cs) {
|
||||
Collection<Disjunction> d = simplifyCNF(f.getDisjunctions(), facts);
|
||||
if (d.size() == 1) {
|
||||
Disjunction x = d.iterator().next();
|
||||
Collection<? extends IFormula> y = x.getClauses();
|
||||
if (y.size() == 1) {
|
||||
result.add(y.iterator().next());
|
||||
} else {
|
||||
result.add(CNFFormula.make(d));
|
||||
}
|
||||
} else {
|
||||
result.add(f);
|
||||
result.add(CNFFormula.make(d));
|
||||
}
|
||||
}
|
||||
return result;
|
||||
}
|
||||
|
||||
private static Collection<Disjunction> simplifyCNF(Collection<? extends Disjunction> s, Collection<Disjunction> facts) {
|
||||
Collection<Disjunction> result = HashSetFactory.make();
|
||||
for (Disjunction d : s) {
|
||||
if (isContradiction(d, facts)) {
|
||||
return Collections.singleton(Disjunction.make(BooleanConstantFormula.FALSE));
|
||||
} else if (isTautology(d, facts)) {
|
||||
// do nothing.
|
||||
} else {
|
||||
result.add(d);
|
||||
}
|
||||
}
|
||||
if (result.isEmpty()) {
|
||||
return Collections.singleton(Disjunction.make(BooleanConstantFormula.TRUE));
|
||||
}
|
||||
return result;
|
||||
}
|
||||
|
||||
private static Collection<Disjunction> collectClauses(Collection<CNFFormula> s) {
|
||||
Collection<Disjunction> result = HashSetFactory.make();
|
||||
for (CNFFormula f : s) {
|
||||
result.addAll(f.getDisjunctions());
|
||||
}
|
||||
return result;
|
||||
}
|
||||
|
||||
private static void debug2(Collection<CNFFormula> cs, Collection<CNFFormula> 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<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<CNFFormula> toCNF(Collection<? extends IFormula> s) {
|
||||
Collection<CNFFormula> result = HashSetFactory.make();
|
||||
for (IFormula f : s) {
|
||||
result.add(CNFFormula.make(f));
|
||||
}
|
||||
return result;
|
||||
}
|
||||
|
||||
/**
|
||||
* @param facts
|
||||
* formulae that can be treated as axioms
|
||||
* @return true if we can easily prove f is a contradiction
|
||||
*/
|
||||
private static boolean isContradiction(IFormula f) {
|
||||
if (f.getKind().equals(IFormula.Kind.RELATION)) {
|
||||
public static boolean isContradiction(IFormula f, Collection<Disjunction> facts) {
|
||||
for (Disjunction d : facts) {
|
||||
if (contradicts(d, f)) {
|
||||
return true;
|
||||
}
|
||||
}
|
||||
switch (f.getKind()) {
|
||||
case BINARY:
|
||||
AbstractBinaryFormula b = (AbstractBinaryFormula) f;
|
||||
if (b.getConnective().equals(BinaryConnective.AND)) {
|
||||
if (isContradiction(b.getF1(), facts) || isContradiction(b.getF2(), facts)) {
|
||||
return true;
|
||||
}
|
||||
} else if (b.getConnective().equals(BinaryConnective.OR)) {
|
||||
if (isContradiction(b.getF1(), facts) && isContradiction(b.getF2(), facts)) {
|
||||
return true;
|
||||
}
|
||||
}
|
||||
break;
|
||||
case CONSTANT:
|
||||
BooleanConstantFormula bc = (BooleanConstantFormula) f;
|
||||
return bc.equals(BooleanConstantFormula.FALSE);
|
||||
case NEGATION:
|
||||
case QUANTIFIED:
|
||||
case RELATION:
|
||||
RelationFormula r = (RelationFormula) f;
|
||||
if (r.getRelation().equals(BinaryRelation.EQUALS)) {
|
||||
ITerm lhs = r.getTerms().get(0);
|
||||
|
|
@ -133,22 +237,76 @@ public class Simplifier {
|
|||
}
|
||||
}
|
||||
}
|
||||
} else if (f.getKind().equals(IFormula.Kind.BINARY)) {
|
||||
BinaryFormula b = (BinaryFormula) f;
|
||||
if (b.getConnective().equals(BinaryConnective.AND)) {
|
||||
if (isContradiction(b.getF1()) || isContradiction(b.getF2())) {
|
||||
return true;
|
||||
}
|
||||
break;
|
||||
}
|
||||
return false;
|
||||
}
|
||||
|
||||
private static boolean contradicts(Disjunction axiom, IFormula f) {
|
||||
IFormula notF = NotFormula.make(f);
|
||||
return implies(axiom, notF);
|
||||
}
|
||||
|
||||
private static boolean implies(Disjunction axiom, IFormula f) {
|
||||
Collection<? extends IFormula> c = axiom.getClauses();
|
||||
if (c.size() == 1) {
|
||||
IFormula a = c.iterator().next();
|
||||
if (a.equals(f)) {
|
||||
return true;
|
||||
}
|
||||
}
|
||||
if (f instanceof Disjunction) {
|
||||
Disjunction d = (Disjunction) f;
|
||||
Collection<? extends IFormula> dc = d.getClauses();
|
||||
if (sameValue(c, dc)) {
|
||||
return true;
|
||||
}
|
||||
}
|
||||
return false;
|
||||
}
|
||||
|
||||
private static boolean sameValue(Collection<?> a, Collection<?> b) {
|
||||
if (a.size() != b.size()) {
|
||||
return false;
|
||||
}
|
||||
for (Object x : a) {
|
||||
if (!b.contains(x)) {
|
||||
return false;
|
||||
}
|
||||
}
|
||||
return true;
|
||||
}
|
||||
|
||||
/**
|
||||
* @param facts
|
||||
* formulae that can be treated as axioms
|
||||
* @return true if we can easily prove f is a tautology
|
||||
*/
|
||||
private static boolean isTautology(IFormula f) {
|
||||
if (f.getKind().equals(IFormula.Kind.RELATION)) {
|
||||
public static boolean isTautology(IFormula f, Collection<Disjunction> facts) {
|
||||
for (Disjunction d : facts) {
|
||||
if (implies(d, f)) {
|
||||
return true;
|
||||
}
|
||||
}
|
||||
switch (f.getKind()) {
|
||||
case BINARY:
|
||||
AbstractBinaryFormula b = (AbstractBinaryFormula) f;
|
||||
if (b.getConnective().equals(BinaryConnective.AND)) {
|
||||
if (isTautology(b.getF1(), facts) && isTautology(b.getF2(), facts)) {
|
||||
return true;
|
||||
}
|
||||
}
|
||||
break;
|
||||
case CONSTANT:
|
||||
Assertions.UNREACHABLE();
|
||||
break;
|
||||
case NEGATION:
|
||||
Assertions.UNREACHABLE();
|
||||
break;
|
||||
case QUANTIFIED:
|
||||
Assertions.UNREACHABLE();
|
||||
break;
|
||||
case RELATION:
|
||||
RelationFormula r = (RelationFormula) f;
|
||||
if (r.getRelation().equals(BinaryRelation.EQUALS)) {
|
||||
ITerm lhs = r.getTerms().get(0);
|
||||
|
|
@ -159,17 +317,14 @@ public class Simplifier {
|
|||
}
|
||||
}
|
||||
}
|
||||
} else if (f.getKind().equals(IFormula.Kind.BINARY)) {
|
||||
BinaryFormula b = (BinaryFormula) f;
|
||||
if (b.getConnective().equals(BinaryConnective.AND)) {
|
||||
if (isTautology(b.getF1()) && isTautology(b.getF2())) {
|
||||
return true;
|
||||
}
|
||||
}
|
||||
break;
|
||||
}
|
||||
return false;
|
||||
}
|
||||
|
||||
/**
|
||||
* 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;
|
||||
|
|
@ -180,13 +335,19 @@ public class Simplifier {
|
|||
return false;
|
||||
}
|
||||
|
||||
private static Pair<ITerm, ITerm> getNextSubCandidate(Collection<IFormula> s, ITheory t, Collection<IFormula> alreadyUsed) {
|
||||
/**
|
||||
* 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, ITheory t, Collection<IFormula> alreadyUsed) {
|
||||
Collection<IFormula> candidates = HashSetFactory.make();
|
||||
candidates.addAll(s);
|
||||
candidates.addAll(t.getSentences());
|
||||
for (IFormula f : candidates) {
|
||||
if (!alreadyUsed.contains(f)) {
|
||||
Pair<ITerm, ITerm> substitution = suggestsSubstitution(f);
|
||||
Pair<ITerm, ITerm> substitution = equalitySuggestsSubsitution(f);
|
||||
if (substitution != null) {
|
||||
alreadyUsed.add(f);
|
||||
return substitution;
|
||||
|
|
@ -198,11 +359,11 @@ public class Simplifier {
|
|||
|
||||
/**
|
||||
* does the structure of formula f suggest an immediate substitution to
|
||||
* simplify the system?
|
||||
* simplify the system, based on theory of equality?
|
||||
*
|
||||
* @return a pair (p1, p2) meaning "substitute p2 for p1"
|
||||
*/
|
||||
private static Pair<ITerm, ITerm> suggestsSubstitution(IFormula f) {
|
||||
private static Pair<ITerm, ITerm> equalitySuggestsSubsitution(IFormula f) {
|
||||
switch (f.getKind()) {
|
||||
case RELATION:
|
||||
RelationFormula r = (RelationFormula) f;
|
||||
|
|
@ -239,7 +400,7 @@ public class Simplifier {
|
|||
}
|
||||
switch (formula.getKind()) {
|
||||
case BINARY:
|
||||
BinaryFormula b = (BinaryFormula) formula;
|
||||
AbstractBinaryFormula b = (AbstractBinaryFormula) formula;
|
||||
return BinaryFormula.make(b.getConnective(), substitute(b.getF1(), t1, t2), substitute(b.getF2(), t1, t2));
|
||||
case NEGATION:
|
||||
NotFormula n = (NotFormula) formula;
|
||||
|
|
|
|||
Loading…
Reference in New Issue