de.uni_freiburg.informatik.ultimate.logic

Class Util

java.lang.Object

de.uni_freiburg.informatik.ultimate.logic.Util

public final class Util
extends java.lang.Object

This class contains some static methods to help creating terms, checking formulas, etc.

Author:

christ, heizmann, hoenicke

Method Summary

Modifier and Type	Method and Description
static Term	and(Script script, Term... subforms) Return slightly simplified version of (and subforms).
static Script.LBool	checkSat(Script script, Term term) Check if term which may contain free TermVariables is satisfiable with respect to the current assertion stack of script.
static Term	implies(Script script, Term... subforms) Create a slightly simplified implies term.
static Term	ite(Script script, Term cond, Term thenPart, Term elsePart) Create a slightly simplified if-then-else term.
static Term	not(Script script, Term f) Return slightly simplified version of (not f).
static Term	or(Script script, Term... subforms) Return slightly simplified version of (or subforms).

Methods inherited from class java.lang.Object

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

Method Detail

checkSat

public static Script.LBool checkSat(Script script,
                                    Term term)

Check if term which may contain free TermVariables is satisfiable with respect to the current assertion stack of script. Only the result from this function can be used since the assertion stack will be modified after leaving this function.

Parameters:

script - the script used to run the check.

term - the term to check for satisfiability (possibly containing free variables).

Returns:

the satisfiability status (SAT, UNSAT or UNKNOWN).

not

public static Term not(Script script,
                       Term f)

Return slightly simplified version of (not f). It removes double negation and simplifies (not true) and (not false).

Parameters:

script - the Script used to build terms.

f - the term to negate

Returns:

a term logically equivalent to (not f).

and

public static Term and(Script script,
                       Term... subforms)

Return slightly simplified version of (and subforms). It removes parameters occuring multiple times, true and false. It also handles the case where there is only one or zero subformulas.

Parameters:

script - the Script used to build terms.

subforms - the sub formulas that are conjoined.

Returns:

a term logically equivalent to (and subforms).

or

public static Term or(Script script,
                      Term... subforms)

Return slightly simplified version of (or subforms). It removes parameters occuring multiple times, true and false. It also handles the case where there is only one or zero subformulas.

Parameters:

script - the Script used to build terms.

subforms - the sub formulas that are disjoined.

Returns:

a term logically equivalent to (or subforms).

ite

public static Term ite(Script script,
                       Term cond,
                       Term thenPart,
                       Term elsePart)

Create a slightly simplified if-then-else term. This mainly optimizes the special cases where one of the parameters is true or false.

Parameters:

script - the script where the term is created.

cond - the if condition.

thenPart - the then part.

elsePart - the else part.

Returns:

the simplified if-then-else term.

implies

public static Term implies(Script script,
                           Term... subforms)

Create a slightly simplified implies term. This mainly optimizes the special cases where one of the parameters is true or false or if a left-hand-side term occurs more than once. It also handles the case where only one subformula is given.

Parameters:

script - the script where the term is created.

subforms - the sub formulas.

Returns:

A simplified version of (=> subforms...).