Class ModelContext
java.lang.Object
tools.refinery.store.reasoning.smt.internal.context.ModelContext
- All Implemented Interfaces:
AutoCloseable
-
Constructor Summary
ConstructorsConstructorDescriptionModelContext(Model model, Collection<PreparedSmtRule> rules, int timeout, int rlimit) -
Method Summary
Modifier and TypeMethodDescription<T> TcallWithInterrupt(Callable<T> callable) voidclose()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
-
Constructor Details
-
ModelContext
-
-
Method Details
-
getZ3Context
public com.microsoft.z3.Context getZ3Context() -
getResultSet
-
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
-
getVariable
-
getExpr
-
callWithInterrupt
-
close
public void close()- Specified by:
closein interfaceAutoCloseable
-