Safe Haskell | None |
---|---|
Language | Haskell98 |
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
- data Verbosity
- data CHRGlobState cnstr guard bprio prio subst env m = CHRGlobState {
- _chrgstStore :: !(CHRStore cnstr guard bprio prio)
- _chrgstNextFreeRuleInx :: !CHRInx
- _chrgstWorkStore :: !(WorkStore cnstr)
- _chrgstNextFreeWorkInx :: !WorkTime
- _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 = CHRBackState {
- _chrbstBacktrackPrio :: !(CHRPrioEvaluatableVal bprio)
- _chrbstRuleWorkQueue :: !WorkQueue
- _chrbstSolveQueue :: !WorkQueue
- _chrbstResidualQueue :: [WorkInx]
- _chrbstMatchedCombis :: !(Set MatchedCombi)
- _chrbstFreshVar :: !Int
- _chrbstSolveSubst :: !subst
- _chrbstWaitForVar :: !(Map (VarLookupKey subst) [WaitForVar subst])
- _chrbstReductionSteps :: [SolverReductionStep]
- 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
- 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
- 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]
- addRule :: MonoBacktrackPrio c g bp p s e m => Rule c g bp p -> CHRMonoBacktrackPrioT c g bp p s e m ()
- addConstraintAsWork :: MonoBacktrackPrio c g bp p s e m => c -> CHRMonoBacktrackPrioT c g bp p s e m (ConstraintSolvesVia, WorkInx)
- data SolverResult subst = SolverResult {
- slvresSubst :: subst
- slvresResidualCnstr :: [WorkInx]
- slvresWorkCnstr :: [WorkInx]
- slvresWaitVarCnstr :: [WorkInx]
- slvresReductionSteps :: [SolverReductionStep]
- 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
- data CHRSolveOpts = CHRSolveOpts {}
- defaultCHRSolveOpts :: CHRSolveOpts
- data StoredCHR c g bp p
- 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)
- 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
- 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
Documentation
data CHRGlobState cnstr guard bprio prio subst env m Source #
Global state
CHRGlobState | |
|
emptyCHRGlobState :: CHRGlobState c g b p s e m Source #
data CHRBackState cnstr bprio subst env Source #
Backtrackable state
CHRBackState | |
|
emptyCHRBackState :: (CHREmptySubstitution s, Bounded (CHRPrioEvaluatableVal bp)) => CHRBackState c bp s e Source #
emptyCHRStore :: CHRStore cnstr guard bprio prio Source #
type CHRMonoBacktrackPrioT cnstr guard bprio prio subst env m = LogicStateT (CHRGlobState cnstr guard bprio prio subst env m) (CHRBackState cnstr bprio subst env) m Source #
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 Source #
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] Source #
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 () Source #
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) Source #
Add a constraint to be solved or residualised
data SolverResult subst Source #
Solver solution
SolverResult | |
|
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 Source #
PP result
data CHRSolveOpts Source #
Solve specific options
CHRSolveOpts | |
|
data StoredCHR c g bp p Source #
A CHR as stored in a CHRStore, requiring additional info for efficiency
storedChrRule' :: StoredCHR c g bp p -> Rule c g bp p Source #
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) Source #
(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 Source #
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 Source #
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 Source #
(Class alias) API for solving requirements