CHR.Solve.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_Debug

Verbosity_ALot

Instances

Enum Verbosity

Defined in CHR.Solve.MonoBacktrackPrio

Methods

succ :: Verbosity -> Verbosity

pred :: Verbosity -> Verbosity

toEnum :: Int -> Verbosity

fromEnum :: Verbosity -> Int

enumFrom :: Verbosity -> [Verbosity]

enumFromThen :: Verbosity -> Verbosity -> [Verbosity]

enumFromTo :: Verbosity -> Verbosity -> [Verbosity]

enumFromThenTo :: Verbosity -> Verbosity -> Verbosity -> [Verbosity]

Show Verbosity

Defined in CHR.Solve.MonoBacktrackPrio

Methods

showsPrec :: Int -> Verbosity -> ShowS

show :: Verbosity -> String

showList :: [Verbosity] -> ShowS

Eq Verbosity

Defined in CHR.Solve.MonoBacktrackPrio

Methods

(==) :: Verbosity -> Verbosity -> Bool

(/=) :: Verbosity -> Verbosity -> Bool

Ord Verbosity

Defined in CHR.Solve.MonoBacktrackPrio

Methods

compare :: Verbosity -> Verbosity -> Ordering

(<) :: Verbosity -> Verbosity -> Bool

(<=) :: Verbosity -> Verbosity -> Bool

(>) :: Verbosity -> Verbosity -> Bool

(>=) :: Verbosity -> Verbosity -> Bool

max :: Verbosity -> Verbosity -> Verbosity

min :: Verbosity -> Verbosity -> 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.

• _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
• _chrgstVarToNmMp :: !VarToNmMp

emptyCHRGlobState :: TTCtxt (TrTrKey c) => CHRGlobState c g b p s e m

chrgstVarToNmMp :: forall cnstr guard bprio prio subst env m. Lens' (CHRGlobState cnstr guard bprio prio subst env m) VarToNmMp

chrgstStatNrSolveSteps :: forall cnstr guard bprio prio subst env m. Lens' (CHRGlobState cnstr guard bprio prio subst env m) Int

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

• _chrbstWorkStore :: !(WorkStore cnstr)

  Actual database of solvable constraints

• _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 :: (TTCtxt (TrTrKey c), CHREmptySubstitution s, Bounded (CHRPrioEvaluatableVal bp)) => CHRBackState c bp s e

emptyCHRStore :: TTCtxt (TrTrKey cnstr) => 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

type MonoBacktrackPrio cnstr guard bprio prio subst env m = (IsCHRSolvable env cnstr guard bprio prio subst, Monad m, Lookup subst (VarLookupKey subst) (VarLookupVal subst), LookupApply subst subst, Fresh Int (ExtrValVarKey (VarLookupVal subst)), ExtrValVarKey (VarLookupVal subst) ~ VarLookupKey subst, VarTerm (VarLookupVal subst))

All required behavior, as 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], (CHRGlobState cnstr guard bprio prio subst env m, CHRBackState cnstr bprio subst env))

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

• chrslvOptGatherDebugInfo :: !Bool

  gather debug info

• chrslvOptGatherTraceInfo :: !Bool

  gather trace info

defaultCHRSolveOpts :: CHRSolveOpts

data StoredCHR c g bp p

A CHR as stored in a CHRStore, requiring additional info for efficiency

Instances

Show (StoredCHR c g bp p)

Defined in CHR.Solve.MonoBacktrackPrio

Methods

showsPrec :: Int -> StoredCHR c g bp p -> ShowS

show :: StoredCHR c g bp p -> String

showList :: [StoredCHR c g bp p] -> ShowS

(PP (TrTrKey c), PP c, PP g, PP bp, PP p) => PP (StoredCHR c g bp p)

Defined in CHR.Solve.MonoBacktrackPrio

Methods

pp :: StoredCHR c g bp p -> PP_Doc

ppList :: [StoredCHR c g bp p] -> PP_Doc

storedChrRule' :: StoredCHR c g bp p -> Rule c g bp p

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

type IsCHRSolvable env c g bp p s = (IsCHRConstraint env c s, IsCHRGuard env g s, IsCHRBacktrackPrio env bp s, IsCHRPrio env p s, PP (VarLookupKey s))

Alias API for solving requirements