added getSentencesRelevantToConstraints() to ITheory
git-svn-id: https://wala.svn.sourceforge.net/svnroot/wala/trunk@2568 f5eafffb-2e1d-0410-98e4-8ec43c5233c4
This commit is contained in:
parent
245ec9c7d5
commit
4eba933775
|
@ -10,6 +10,7 @@
|
||||||
*******************************************************************************/
|
*******************************************************************************/
|
||||||
package com.ibm.wala.logic;
|
package com.ibm.wala.logic;
|
||||||
|
|
||||||
|
import java.util.Collection;
|
||||||
import java.util.TreeSet;
|
import java.util.TreeSet;
|
||||||
|
|
||||||
public abstract class AbstractTheory extends DefaultDecorator implements ITheory {
|
public abstract class AbstractTheory extends DefaultDecorator implements ITheory {
|
||||||
|
@ -31,4 +32,12 @@ public abstract class AbstractTheory extends DefaultDecorator implements ITheory
|
||||||
return result.toString();
|
return result.toString();
|
||||||
}
|
}
|
||||||
|
|
||||||
|
/**
|
||||||
|
* by default, just return all sentences
|
||||||
|
*/
|
||||||
|
public Collection<? extends IFormula> getSentencesRelevantToConstraints(Collection<? extends IFormula> constraints) {
|
||||||
|
return getSentences();
|
||||||
|
}
|
||||||
|
|
||||||
|
|
||||||
}
|
}
|
||||||
|
|
|
@ -49,6 +49,14 @@ public class CombinedTheory extends AbstractTheory {
|
||||||
return union;
|
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() {
|
public IVocabulary getVocabulary() {
|
||||||
return CombinedVocabulary.make(a.getVocabulary(), b.getVocabulary());
|
return CombinedVocabulary.make(a.getVocabulary(), b.getVocabulary());
|
||||||
}
|
}
|
||||||
|
|
|
@ -41,7 +41,7 @@ public interface IFormula {
|
||||||
public Collection<? extends IConstant> getConstants();
|
public Collection<? extends IConstant> getConstants();
|
||||||
|
|
||||||
/**
|
/**
|
||||||
* @return all terms that appear in this formula, including recursive descent on on-atomic terms
|
* @return all terms that appear in this formula, including recursive descent non on-atomic terms
|
||||||
*/
|
*/
|
||||||
public Collection<? extends ITerm> getAllTerms();
|
public Collection<? extends ITerm> getAllTerms();
|
||||||
|
|
||||||
|
|
|
@ -22,6 +22,18 @@ public interface ITheory {
|
||||||
|
|
||||||
public IVocabulary getVocabulary();
|
public IVocabulary getVocabulary();
|
||||||
|
|
||||||
|
/**
|
||||||
|
* get all sentences in theory
|
||||||
|
* TODO: remove this, replace with getSentencesRelevantToConstraints(empty)? MS
|
||||||
|
* @return the sentences
|
||||||
|
*/
|
||||||
public Collection<? extends IFormula> getSentences();
|
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);
|
||||||
|
|
||||||
}
|
}
|
||||||
|
|
|
@ -35,12 +35,12 @@ public class Simplifier {
|
||||||
* Eliminate quantifiers, by substituting every possible constant value for a
|
* Eliminate quantifiers, by substituting every possible constant value for a
|
||||||
* quantified variable
|
* quantified variable
|
||||||
*/
|
*/
|
||||||
public static ITheory eliminateQuantifiers(ITheory t) {
|
public static ITheory eliminateQuantifiers(ITheory t, Collection<? extends IFormula> constraints) {
|
||||||
if (t == null) {
|
if (t == null) {
|
||||||
throw new IllegalArgumentException("t is null");
|
throw new IllegalArgumentException("t is null");
|
||||||
}
|
}
|
||||||
Collection<IFormula> sentences = HashSetFactory.make();
|
Collection<IFormula> sentences = HashSetFactory.make();
|
||||||
for (IFormula s : t.getSentences()) {
|
for (IFormula s : t.getSentencesRelevantToConstraints(constraints)) {
|
||||||
sentences.addAll(eliminateQuantifiers(s));
|
sentences.addAll(eliminateQuantifiers(s));
|
||||||
}
|
}
|
||||||
return BasicTheory.make(t.getVocabulary(), sentences);
|
return BasicTheory.make(t.getVocabulary(), sentences);
|
||||||
|
|
Loading…
Reference in New Issue