Class RuleBasedSolver

java.lang.Object

tools.refinery.store.reasoning.smt.internal.solver.RuleBasedSolver

public class RuleBasedSolver
extends Object

Field Summary

Fields

Modifier and Type	Field	Description
static final String	REJECTION_NO_MODEL
static final String	REJECTION_UNKNOWN
static final String	REJECTION_UNSAT

Constructor Summary

Constructors

Constructor	Description
RuleBasedSolver(ModelContext context, Concreteness concreteness, List<PreparedSmtRule> rules, com.microsoft.z3.Solver solver)

Method Summary

Modifier and Type	Method	Description
void	changeRef(AnyPartialFunction partialFunction, Tuple tuple, boolean add)
PropagationResult	checkSatisfiable(Object reason)
PropagationResult	concretize(Object reason)
Concreteness	getConcreteness()
ModelContext	getContext()
boolean	isChanged()
void	markChanged()

Methods inherited from class Object

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

Field Details

REJECTION_UNSAT

public static final String REJECTION_UNSAT

See Also:

• Constant Field Values

REJECTION_UNKNOWN

public static final String REJECTION_UNKNOWN

See Also:

• Constant Field Values

REJECTION_NO_MODEL

public static final String REJECTION_NO_MODEL

See Also:

• Constant Field Values

Constructor Details

RuleBasedSolver

public RuleBasedSolver(ModelContext context,
 Concreteness concreteness,
 List<PreparedSmtRule> rules,
 com.microsoft.z3.Solver solver)

Method Details

getContext

public ModelContext getContext()

getConcreteness

public Concreteness getConcreteness()

isChanged

public boolean isChanged()

markChanged

public void markChanged()

changeRef

public void changeRef(AnyPartialFunction partialFunction,
 Tuple tuple,
 boolean add)

checkSatisfiable

public PropagationResult checkSatisfiable(Object reason)

concretize

public PropagationResult concretize(Object reason)