Class TermToExpr

java.lang.Object

tools.refinery.store.reasoning.smt.expr.TermToExpr

public class TermToExpr
extends Object

Constructor Summary

Constructors

Constructor	Description
TermToExpr(ModelContext modelContext)

Method Summary

Modifier and Type	Method	Description
com.microsoft.z3.Expr<?>	toExpr(ConstantTerm<?> term)
com.microsoft.z3.Expr<?>	toExpr(Term<?> term, Tuple parameterTuple, org.eclipse.collections.api.map.primitive.ObjectIntMap<NodeVariable> parameterMap)
com.microsoft.z3.Expr<?>	toExpr(PartialFunctionCallTerm<?,?> partialFunctionCallTerm, Tuple parameterTuple, org.eclipse.collections.api.map.primitive.ObjectIntMap<NodeVariable> parameterMap)

Methods inherited from class Object

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

Constructor Details

TermToExpr

public TermToExpr(ModelContext modelContext)

Method Details

toExpr

public com.microsoft.z3.Expr<?> toExpr(Term<?> term,
 Tuple parameterTuple,
 org.eclipse.collections.api.map.primitive.ObjectIntMap<NodeVariable> parameterMap)

toExpr

public com.microsoft.z3.Expr<?> toExpr(ConstantTerm<?> term)

toExpr

public com.microsoft.z3.Expr<?> toExpr(PartialFunctionCallTerm<?,?> partialFunctionCallTerm,
 Tuple parameterTuple,
 org.eclipse.collections.api.map.primitive.ObjectIntMap<NodeVariable> parameterMap)