org.evosuite.symbolic.solver

Class SmtExprBuilder

java.lang.Object

org.evosuite.symbolic.solver.SmtExprBuilder

public abstract class SmtExprBuilder
extends Object

Field Summary

Fields

Modifier and Type	Field and Description
static SmtBooleanConstant	FALSE
static SmtIntConstant	ONE_INT
static SmtBooleanConstant	TRUE
static SmtIntConstant	ZERO_INT
static SmtRealConstant	ZERO_REAL

Constructor Summary

Constructors

Constructor and Description
SmtExprBuilder()

Method Summary

Modifier and Type	Method and Description
static SmtExpr	mkAbs(SmtExpr arg)
static SmtExpr	mkAdd(SmtExpr left, SmtExpr right)
static SmtExpr	mkBV2Int(SmtExpr arg)
static SmtExpr	mkBV2Nat(SmtExpr arg)
static SmtExpr	mkBVADD(SmtExpr left, SmtExpr right)
static SmtExpr	mkBVAND(SmtExpr left, SmtExpr right)
static SmtExpr	mkBVASHR(SmtExpr left, SmtExpr right)
static SmtExpr	mkBVLSHR(SmtExpr left, SmtExpr right)
static SmtExpr	mkBVOR(SmtExpr left, SmtExpr right)
static SmtExpr	mkBVSHL(SmtExpr left, SmtExpr right)
static SmtExpr	mkBVXOR(SmtExpr left, SmtExpr right)
static SmtExpr	mkCharToInt(SmtExpr arg)
static SmtExpr	mkConcat(SmtExpr left, SmtExpr right)
static SmtExpr	mkContains(SmtExpr left, SmtExpr right)
static SmtExpr	mkEndsWith(SmtExpr left, SmtExpr right)
static SmtExpr	mkEq(SmtExpr left, SmtExpr right)
static SmtExpr	mkGe(SmtExpr left, SmtExpr right)
static SmtExpr	mkGt(SmtExpr left, SmtExpr right)
static SmtExpr	mkIndexOf(SmtExpr left, SmtExpr right)
static SmtExpr	mkInt2BV(int bitwidth, SmtExpr arg)
static SmtExpr	mkInt2Real(SmtExpr intExpr)
static SmtIntConstant	mkIntConstant(long longValue)
static SmtConstantDeclaration	mkIntConstantDeclaration(String constName)
static SmtExpr	mkIntDiv(SmtExpr left, SmtExpr right)
static SmtFunctionDeclaration	mkIntFunctionDeclaration(String funcName)
static SmtExpr	mkIntToChar(SmtExpr arg)
static SmtExpr	mkIntToStr(SmtExpr arg)
static SmtIntVariable	mkIntVariable(String varName)
static SmtExpr	mkITE(SmtExpr condExpr, SmtExpr thenExpr, SmtExpr elseExpr)
static SmtExpr	mkLe(SmtExpr left, SmtExpr right)
static SmtExpr	mkLength(SmtExpr stringExpr)
static SmtExpr	mkLoop(SmtExpr regExpr, SmtIntConstant minExpr)
static SmtExpr	mkLoop(SmtExpr regExpr, SmtIntConstant minExpr, SmtIntConstant maxExpr)
static SmtExpr	mkLt(SmtExpr left, SmtExpr right)
static SmtExpr	mkMod(SmtExpr left, SmtExpr right)
static SmtExpr	mkMul(SmtExpr left, SmtExpr right)
static SmtExpr	mkNeg(SmtExpr expr)
static SmtExpr	mkNot(SmtExpr arg)
static SmtExpr	mkReal2Int(SmtExpr realExpr)
static SmtRealConstant	mkRealConstant(double doubleValue)
static SmtConstantDeclaration	mkRealConstantDeclaration(String constName)
static SmtExpr	mkRealDiv(SmtExpr left, SmtExpr right)
static SmtFunctionDeclaration	mkRealFunctionDeclaration(String funcName)
static SmtRealVariable	mkRealVariable(String varName)
static SmtExpr	mkRegExpAllChar()
static SmtExpr	mkRegExpConcat(SmtExpr left, SmtExpr right)
static SmtExpr	mkRegExpKleeCross(SmtExpr regExpr)
static SmtExpr	mkRegExpOptional(SmtExpr e)
static SmtExpr	mkRegExpRange(SmtExpr fromExpr, SmtExpr toExpr)
static SmtExpr	mkRegExpUnion(SmtExpr left, SmtExpr right)
static SmtExpr	mkReKleeneStar(SmtExpr expr)
static SmtExpr	mkRem(SmtExpr left, SmtExpr right)
static SmtExpr	mkReplace(SmtExpr strExpr, SmtExpr targetExpr, SmtExpr replacementExpr)
static SmtExpr	mkStartsWith(SmtExpr left, SmtExpr right)
static SmtExpr	mkStrAt(SmtExpr left, SmtExpr right)
static SmtExpr	mkStrConcat(SmtExpr left, SmtExpr right)
static SmtExpr	mkStrContains(SmtExpr left, SmtExpr right)
static SmtExpr	mkStrIndexOf(SmtExpr stringExpr, SmtExpr termExpr, SmtExpr indexExpr)
static SmtStringConstant	mkStringConstant(String stringValue)
static SmtConstantDeclaration	mkStringConstantDeclaration(String constName)
static SmtFunctionDeclaration	mkStringFunctionDeclaration(String funcName)
static SmtExpr	mkStringVariable(String varName)
static SmtExpr	mkStrInRegExp(SmtExpr left, SmtExpr right)
static SmtExpr	mkStrLen(SmtExpr arg)
static SmtExpr	mkStrPrefixOf(SmtExpr stringExpr, SmtExpr termExpr)
static SmtExpr	mkStrReplace(SmtExpr stringExpr, SmtExpr targetExpr, SmtExpr replacementExpr)
static SmtExpr	mkStrSubstring(SmtExpr stringExpr, SmtExpr startIndex, SmtExpr offset)
static SmtExpr	mkStrSuffixOf(SmtExpr left, SmtExpr right)
static SmtExpr	mkStrToInt(SmtExpr arg)
static SmtExpr	mkStrToRegExp(SmtStringConstant strConstant)
static SmtExpr	mkSub(SmtExpr left, SmtExpr right)
static SmtExpr	mkSubstring(SmtExpr string, SmtExpr fromExpr, SmtExpr toExpr)

Methods inherited from class java.lang.Object

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

Field Detail

ZERO_INT

public static final SmtIntConstant ZERO_INT

ZERO_REAL

public static final SmtRealConstant ZERO_REAL

ONE_INT

public static final SmtIntConstant ONE_INT

TRUE

public static final SmtBooleanConstant TRUE

FALSE

public static final SmtBooleanConstant FALSE

Constructor Detail

SmtExprBuilder

public SmtExprBuilder()

Method Detail

mkIntDiv

public static SmtExpr mkIntDiv(SmtExpr left,
                               SmtExpr right)

mkRealDiv

public static SmtExpr mkRealDiv(SmtExpr left,
                                SmtExpr right)

mkMul

public static SmtExpr mkMul(SmtExpr left,
                            SmtExpr right)

mkSub

public static SmtExpr mkSub(SmtExpr left,
                            SmtExpr right)

mkAdd

public static SmtExpr mkAdd(SmtExpr left,
                            SmtExpr right)

mkMod

public static SmtExpr mkMod(SmtExpr left,
                            SmtExpr right)

mkInt2BV

public static SmtExpr mkInt2BV(int bitwidth,
                               SmtExpr arg)

mkBVOR

public static SmtExpr mkBVOR(SmtExpr left,
                             SmtExpr right)

mkBV2Nat

public static SmtExpr mkBV2Nat(SmtExpr arg)

mkBVAND

public static SmtExpr mkBVAND(SmtExpr left,
                              SmtExpr right)

mkBVXOR

public static SmtExpr mkBVXOR(SmtExpr left,
                              SmtExpr right)

mkBV2Int

public static SmtExpr mkBV2Int(SmtExpr arg)

mkBVSHL

public static SmtExpr mkBVSHL(SmtExpr left,
                              SmtExpr right)

mkBVASHR

public static SmtExpr mkBVASHR(SmtExpr left,
                               SmtExpr right)

mkBVLSHR

public static SmtExpr mkBVLSHR(SmtExpr left,
                               SmtExpr right)

mkGt

public static SmtExpr mkGt(SmtExpr left,
                           SmtExpr right)

mkITE

public static SmtExpr mkITE(SmtExpr condExpr,
                            SmtExpr thenExpr,
                            SmtExpr elseExpr)

mkLt

public static SmtExpr mkLt(SmtExpr left,
                           SmtExpr right)

mkIntConstant

public static SmtIntConstant mkIntConstant(long longValue)

mkRealConstant

public static SmtRealConstant mkRealConstant(double doubleValue)

mkGe

public static SmtExpr mkGe(SmtExpr left,
                           SmtExpr right)

mkNeg

public static SmtExpr mkNeg(SmtExpr expr)

mkReal2Int

public static SmtExpr mkReal2Int(SmtExpr realExpr)

mkInt2Real

public static SmtExpr mkInt2Real(SmtExpr intExpr)

mkRealVariable

public static SmtRealVariable mkRealVariable(String varName)

mkIntVariable

public static SmtIntVariable mkIntVariable(String varName)

mkStrSubstring

public static SmtExpr mkStrSubstring(SmtExpr stringExpr,
                                     SmtExpr startIndex,
                                     SmtExpr offset)

mkStringConstant

public static SmtStringConstant mkStringConstant(String stringValue)

mkStrReplace

public static SmtExpr mkStrReplace(SmtExpr stringExpr,
                                   SmtExpr targetExpr,
                                   SmtExpr replacementExpr)

mkStringVariable

public static SmtExpr mkStringVariable(String varName)

mkStrIndexOf

public static SmtExpr mkStrIndexOf(SmtExpr stringExpr,
                                   SmtExpr termExpr,
                                   SmtExpr indexExpr)

mkEq

public static SmtExpr mkEq(SmtExpr left,
                           SmtExpr right)

mkStrConcat

public static SmtExpr mkStrConcat(SmtExpr left,
                                  SmtExpr right)

mkIntToStr

public static SmtExpr mkIntToStr(SmtExpr arg)

mkStrSuffixOf

public static SmtExpr mkStrSuffixOf(SmtExpr left,
                                    SmtExpr right)

mkStrContains

public static SmtExpr mkStrContains(SmtExpr left,
                                    SmtExpr right)

mkStrAt

public static SmtExpr mkStrAt(SmtExpr left,
                              SmtExpr right)

mkCharToInt

public static SmtExpr mkCharToInt(SmtExpr arg)

mkStrPrefixOf

public static SmtExpr mkStrPrefixOf(SmtExpr stringExpr,
                                    SmtExpr termExpr)

mkIntToChar

public static SmtExpr mkIntToChar(SmtExpr arg)

mkStrLen

public static SmtExpr mkStrLen(SmtExpr arg)

mkLe

public static SmtExpr mkLe(SmtExpr left,
                           SmtExpr right)

mkNot

public static SmtExpr mkNot(SmtExpr arg)

mkStrToInt

public static SmtExpr mkStrToInt(SmtExpr arg)

mkAbs

public static SmtExpr mkAbs(SmtExpr arg)

mkBVADD

public static SmtExpr mkBVADD(SmtExpr left,
                              SmtExpr right)

mkRegExpConcat

public static SmtExpr mkRegExpConcat(SmtExpr left,
                                     SmtExpr right)

mkStrToRegExp

public static SmtExpr mkStrToRegExp(SmtStringConstant strConstant)

mkReKleeneStar

public static SmtExpr mkReKleeneStar(SmtExpr expr)

mkStrInRegExp

public static SmtExpr mkStrInRegExp(SmtExpr left,
                                    SmtExpr right)

mkRegExpUnion

public static SmtExpr mkRegExpUnion(SmtExpr left,
                                    SmtExpr right)

mkRegExpOptional

public static SmtExpr mkRegExpOptional(SmtExpr e)

mkRegExpAllChar

public static SmtExpr mkRegExpAllChar()

mkRegExpKleeCross

public static SmtExpr mkRegExpKleeCross(SmtExpr regExpr)

mkLoop

public static SmtExpr mkLoop(SmtExpr regExpr,
                             SmtIntConstant minExpr)

mkLoop

public static SmtExpr mkLoop(SmtExpr regExpr,
                             SmtIntConstant minExpr,
                             SmtIntConstant maxExpr)

mkRegExpRange

public static SmtExpr mkRegExpRange(SmtExpr fromExpr,
                                    SmtExpr toExpr)

mkRem

public static SmtExpr mkRem(SmtExpr left,
                            SmtExpr right)

mkConcat

public static SmtExpr mkConcat(SmtExpr left,
                               SmtExpr right)

mkReplace

public static SmtExpr mkReplace(SmtExpr strExpr,
                                SmtExpr targetExpr,
                                SmtExpr replacementExpr)

mkSubstring

public static SmtExpr mkSubstring(SmtExpr string,
                                  SmtExpr fromExpr,
                                  SmtExpr toExpr)

mkEndsWith

public static SmtExpr mkEndsWith(SmtExpr left,
                                 SmtExpr right)

mkContains

public static SmtExpr mkContains(SmtExpr left,
                                 SmtExpr right)

mkStartsWith

public static SmtExpr mkStartsWith(SmtExpr left,
                                   SmtExpr right)

mkIndexOf

public static SmtExpr mkIndexOf(SmtExpr left,
                                SmtExpr right)

mkLength

public static SmtExpr mkLength(SmtExpr stringExpr)

mkIntConstantDeclaration

public static SmtConstantDeclaration mkIntConstantDeclaration(String constName)

mkRealConstantDeclaration

public static SmtConstantDeclaration mkRealConstantDeclaration(String constName)

mkStringConstantDeclaration

public static SmtConstantDeclaration mkStringConstantDeclaration(String constName)

mkIntFunctionDeclaration

public static SmtFunctionDeclaration mkIntFunctionDeclaration(String funcName)

mkRealFunctionDeclaration

public static SmtFunctionDeclaration mkRealFunctionDeclaration(String funcName)

mkStringFunctionDeclaration

public static SmtFunctionDeclaration mkStringFunctionDeclaration(String funcName)