Class ModelContext

java.lang.Object

tools.refinery.store.reasoning.smt.internal.context.ModelContext

All Implemented Interfaces:

AutoCloseable

public class ModelContext
extends Object
implements AutoCloseable

Constructor Summary

Constructors

Constructor	Description
ModelContext(Model model, Collection<PreparedSmtRule> rules, int timeout, int rlimit)

Method Summary

Modifier and Type	Method	Description
<T> T	callWithInterrupt(Callable<T> callable)
void	close()
RuleBasedSolver	createSolver(Concreteness concreteness)
com.microsoft.z3.Expr<com.microsoft.z3.BoolSort>	getExpr(PreparedSmtRule rule, Tuple input)
<A extends AbstractValue<A,C>, C> PartialInterpretation<A,C>	getPartialInterpretation(Concreteness concreteness, PartialSymbol<A,C> partialSymbol)
<A extends AbstractValue<A,C>, C> PartialInterpretationRefiner<A,C>	getRefiner(PartialSymbol<A,C> partialSymbol)
<T> ResultSet<T>	getResultSet(Query<T> query)
com.microsoft.z3.FuncDecl<?>	getVariable(AnyPartialFunction partialFunction, Tuple input)
com.microsoft.z3.Context	getZ3Context()

Methods inherited from class Object

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

Constructor Details

ModelContext

public ModelContext(Model model,
 Collection<PreparedSmtRule> rules,
 int timeout,
 int rlimit)

Method Details

getZ3Context

public com.microsoft.z3.Context getZ3Context()

getResultSet

public <T> ResultSet<T> getResultSet(Query<T> query)

getPartialInterpretation

public <A extends AbstractValue<A,C>, C>
PartialInterpretation<A,C> getPartialInterpretation(Concreteness concreteness,
 PartialSymbol<A,C> partialSymbol)

getRefiner

public <A extends AbstractValue<A,C>, C>
PartialInterpretationRefiner<A,C> getRefiner(PartialSymbol<A,C> partialSymbol)

createSolver

public RuleBasedSolver createSolver(Concreteness concreteness)

getVariable

public com.microsoft.z3.FuncDecl<?> getVariable(AnyPartialFunction partialFunction,
 Tuple input)

getExpr

public com.microsoft.z3.Expr<com.microsoft.z3.BoolSort> getExpr(PreparedSmtRule rule,
 Tuple input)

callWithInterrupt

public <T> T callWithInterrupt(Callable<T> callable)

close

public void close()

Specified by:

close in interface AutoCloseable