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

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]

Eq Verbosity

Methods

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

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

Ord Verbosity

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

Show Verbosity

Methods

showsPrec :: Int -> Verbosity -> ShowS

show :: Verbosity -> String

showList :: [Verbosity] -> ShowS

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

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)

Methods

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

show :: StoredCHR c g bp p -> String

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

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

Methods

pp :: StoredCHR c g bp p -> PP_Doc

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

type TTKey (StoredCHR c g bp p)

type TTKey (StoredCHR c g bp p) = TTKey c

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

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