Class RuleBasedSolver
java.lang.Object
tools.refinery.store.reasoning.smt.internal.solver.RuleBasedSolver
-
Field Summary
Fields -
Constructor Summary
ConstructorsConstructorDescriptionRuleBasedSolver(ModelContext context, Concreteness concreteness, List<PreparedSmtRule> rules, com.microsoft.z3.Solver solver) -
Method Summary
Modifier and TypeMethodDescriptionvoidchangeRef(AnyPartialFunction partialFunction, Tuple tuple, boolean add) checkSatisfiable(Object reason) concretize(Object reason) booleanvoid
-
Field Details
-
REJECTION_UNSAT
- See Also:
-
REJECTION_UNKNOWN
- See Also:
-
REJECTION_NO_MODEL
- See Also:
-
-
Constructor Details
-
RuleBasedSolver
public RuleBasedSolver(ModelContext context, Concreteness concreteness, List<PreparedSmtRule> rules, com.microsoft.z3.Solver solver)
-
-
Method Details
-
getContext
-
getConcreteness
-
isChanged
public boolean isChanged() -
markChanged
public void markChanged() -
changeRef
-
checkSatisfiable
-
concretize
-