de.uka.ilkd.key.strategy.quantifierHeuristics

Class TriggerUtils

java.lang.Object

de.uka.ilkd.key.strategy.quantifierHeuristics.TriggerUtils

class TriggerUtils
extends java.lang.Object

Constructor Summary

Constructors

Constructor and Description
TriggerUtils()

Method Summary

Modifier and Type	Method and Description
static Term	discardQuantifiers(Term qterm) remove all the quantifiable variable bounded in the top level of a given formula.
static ImmutableSet<QuantifiableVariable>	intersect(ImmutableSet<QuantifiableVariable> set0, ImmutableSet<QuantifiableVariable> set1)
static boolean	isTrueOrFalse(Term res)
static java.util.Iterator<Term>	iteratorByOperator(Term term, Operator op)
static ImmutableSet<Term>	setByOperator(Term term, Operator op)

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Constructor Detail

TriggerUtils

TriggerUtils()

Method Detail

discardQuantifiers

public static Term discardQuantifiers(Term qterm)

remove all the quantifiable variable bounded in the top level of a given formula.

iteratorByOperator

public static java.util.Iterator<Term> iteratorByOperator(Term term,
                                                          Operator op)

Returns:

set of terms that are that the term splite d through the operator op

setByOperator

public static ImmutableSet<Term> setByOperator(Term term,
                                               Operator op)

intersect

public static ImmutableSet<QuantifiableVariable> intersect(ImmutableSet<QuantifiableVariable> set0,
                                                           ImmutableSet<QuantifiableVariable> set1)

Parameters:

set0 -

set1 -

Returns:

a set of quantifiableVariable which are belonged to both set0 and set1 have

isTrueOrFalse

public static boolean isTrueOrFalse(Term res)