UHC.Util.CHR.Solve.TreeTrie.MonoBacktrackPrio

Under development (as of 20160218).

Solver is: - Monomorphic, i.e. the solver is polymorph but therefore can only work on 1 type of constraints, rules, etc. - Knows about variables for which substitutions can be found, substitutions are part of found solutions. - Backtracking (on variable bindings/substitutions), multiple solution alternatives are explored. - Found rules are applied in an order described by priorities associated with rules. Priorities can be dynamic, i.e. depend on terms in rules.

See

"A Flexible Search Framework for CHR", Leslie De Koninck, Tom Schrijvers, and Bart Demoen. http:/link.springer.com10.1007/978-3-540-92243-8_2

Documentation

data Verbosity

Constructors

Verbosity_Quiet

Verbosity_Normal

Verbosity_ALot

Instances

Enum Verbosity

Eq Verbosity

Ord Verbosity

Show Verbosity

data CHRGlobState cnstr guard bprio prio subst env m

Global state

Constructors

CHRGlobState

Fields

_chrgstStore :: !(CHRStore cnstr guard bprio prio)

Actual database of rules, to be searched

_chrgstNextFreeRuleInx :: !CHRInx

Next free rule identification, used by solving to identify whether a rule has been used for a constraint. The numbering is applied to constraints inside a rule which can be matched.

_chrgstWorkStore :: !(WorkStore cnstr)

Actual database of solvable constraints

_chrgstNextFreeWorkInx :: !WorkTime

Next free work/constraint identification, used by solving to identify whether a rule has been used for a constraint.

_chrgstScheduleQueue :: !(MinPQueue (CHRPrioEvaluatableVal bprio) (CHRMonoBacktrackPrioT cnstr guard bprio prio subst env m (SolverResult subst)))

_chrgstTrace :: SolveTrace' cnstr (StoredCHR cnstr guard bprio prio) subst

_chrgstStatNrSolveSteps :: !Int

emptyCHRGlobState :: CHRGlobState c g b p s e m

data CHRBackState cnstr bprio subst env

Backtrackable state

Constructors

CHRBackState

Fields

_chrbstBacktrackPrio :: !(CHRPrioEvaluatableVal bprio)

the current backtrack prio the solver runs on

_chrbstRuleWorkQueue :: !WorkQueue

work queue for rule matching

_chrbstSolveQueue :: !WorkQueue

solve queue, constraints which are not solved by rule matching but with some domain specific solver, yielding variable subst constributing to backtrackable bindings

_chrbstResidualQueue :: [WorkInx]

residual queue, constraints which are residual, no need to solve, etc

_chrbstMatchedCombis :: !(Set MatchedCombi)

all combis of chr + work which were reduced, to prevent this from happening a second time (when propagating)

_chrbstFreshVar :: !Int

for fresh var

_chrbstSolveSubst :: !subst

subst for variable bindings found during solving, not for the ones binding rule metavars during matching but for the user ones (in to be solved constraints)

_chrbstWaitForVar :: !(Map (VarLookupKey subst) [WaitForVar subst])

work waiting for a var to be bound

_chrbstReductionSteps :: [SolverReductionStep]

trace of reduction steps taken (excluding solve steps)

emptyCHRBackState :: (CHREmptySubstitution s, Bounded (CHRPrioEvaluatableVal bp)) => CHRBackState c bp s e

emptyCHRStore :: CHRStore cnstr guard bprio prio

type CHRMonoBacktrackPrioT cnstr guard bprio prio subst env m = LogicStateT (CHRGlobState cnstr guard bprio prio subst env m) (CHRBackState cnstr bprio subst env) m

Monad for CHR, taking from LogicStateT the state and backtracking behavior

class (IsCHRSolvable env cnstr guard bprio prio subst, Monad m, VarLookup subst, Fresh Int (ExtrValVarKey (VarLookupVal subst)), ExtrValVarKey (VarLookupVal subst) ~ VarLookupKey subst, VarTerm (VarLookupVal subst)) => MonoBacktrackPrio cnstr guard bprio prio subst env m

All required behavior, as class alias

runCHRMonoBacktrackPrioT :: MonoBacktrackPrio cnstr guard bprio prio subst env m => CHRGlobState cnstr guard bprio prio subst env m -> CHRBackState cnstr bprio subst env -> CHRMonoBacktrackPrioT cnstr guard bprio prio subst env m (SolverResult subst) -> m [SolverResult subst]

Run and observe results

addRule :: MonoBacktrackPrio c g bp p s e m => Rule c g bp p -> CHRMonoBacktrackPrioT c g bp p s e m ()

Add a rule as a CHR

addConstraintAsWork :: MonoBacktrackPrio c g bp p s e m => c -> CHRMonoBacktrackPrioT c g bp p s e m (ConstraintSolvesVia, WorkInx)

Add a constraint to be solved or residualised

data SolverResult subst

Solver solution

Constructors

SolverResult

Fields

slvresSubst :: subst

global found variable bindings

slvresResidualCnstr :: [WorkInx]

constraints which are residual, no need to solve, etc, leftover when ready, taken from backtrack state

slvresWorkCnstr :: [WorkInx]

constraints which are still unsolved, taken from backtrack state

slvresWaitVarCnstr :: [WorkInx]

constraints which are still unsolved, waiting for variable resolution

slvresReductionSteps :: [SolverReductionStep]

how did we get to the result (taken from the backtrack state when a result is given back)

ppSolverResult :: (MonoBacktrackPrio c g bp p s e m, VarUpdatable s s, PP s) => Verbosity -> SolverResult s -> CHRMonoBacktrackPrioT c g bp p s e m PP_Doc

PP result

data CHRSolveOpts

Solve specific options

Constructors

CHRSolveOpts

Fields

chrslvOptSucceedOnLeftoverWork :: !Bool

left over unresolvable (non residue) work is also a successful result

chrslvOptSucceedOnFailedSolve :: !Bool

failed solve is considered also a successful result, with the failed constraint as a residue

defaultCHRSolveOpts :: CHRSolveOpts

chrSolve :: forall c g bp p s e m. (MonoBacktrackPrio c g bp p s e m, PP s) => CHRSolveOpts -> e -> CHRMonoBacktrackPrioT c g bp p s e m (SolverResult s)

(Under dev) solve

slvFreshSubst :: forall c g bp p s e m x. (MonoBacktrackPrio c g bp p s e m, ExtrValVarKey x ~ ExtrValVarKey (VarLookupVal s), VarExtractable x) => Set (ExtrValVarKey x) -> x -> CHRMonoBacktrackPrioT c g bp p s e m s

Fresh variables in the form of a subst

getSolveTrace :: (PP c, PP g, PP bp, MonoBacktrackPrio c g bp p s e m) => CHRMonoBacktrackPrioT c g bp p s e m PP_Doc

class (IsCHRConstraint env c s, IsCHRGuard env g s, IsCHRBacktrackPrio env bp s, IsCHRPrio env p s, TrTrKey c ~ TTKey c, PP (VarLookupKey s)) => IsCHRSolvable env c g bp p s

(Class alias) API for solving requirements