public class HandlerUtil
extends java.lang.Object
SMTHandler
s are likely to use.Modifier and Type | Field and Description |
---|---|
static java.util.List<? extends SMTHandlerProperty<?>> |
GLOBAL_PROPERTIES
This lists the handler properties that do not belong to a particular
SMT handler.
|
static SMTHandlerProperty.BooleanProperty |
PROPERTY_NO_TYPE_HIERARCHY
A user SMT property to decide whether the type hierarchy is translated
at all.
|
static SMTHandlerProperty.BooleanProperty |
PROPERTY_NOBINDERS
A property that can be used by various handlers that deal with
binders.
|
Modifier and Type | Method and Description |
---|---|
static SExpr |
funDeclaration(SortedOperator op,
java.lang.String name)
Generate a smtlib expression for the smtlib declaration that
represents the operator op.
|
public static final SMTHandlerProperty.BooleanProperty PROPERTY_NOBINDERS
public static final SMTHandlerProperty.BooleanProperty PROPERTY_NO_TYPE_HIERARCHY
public static final java.util.List<? extends SMTHandlerProperty<?>> GLOBAL_PROPERTIES
public static SExpr funDeclaration(SortedOperator op, java.lang.String name)
op
- the operator to be declared in smtlibname
- the name to use on the smt lib side.(declare-fun ...)
Copyright © 2003-2019 The KeY-Project.