# Documentation

class Monad solver => Solver solver whereSource

add :: Constraint solver -> solver BoolSource

add a constraint to the current state, and return whether the resulting state is consistent

run a computation

mark :: solver (Label solver)Source

mark the current state, and return its label

goto :: Label solver -> solver ()Source

go to the state with given label

Solver Prolog | |

Solver CodegenSolver | Helper functions Gecode Solver instance declaration |

Solver OvertonFD | |

HTerm t => Solver (Herbrand t) | Solver instance |

FDSolver s => Solver (FDWrapper s) | |

(Monoid w, Solver s) => Solver (WriterT w s) | WriterT decoration of a solver useful for producing statistics during solving |

(Solver s, HTerm t) => Solver (HerbrandT t s) |

class Solver solver => Term solver term whereSource

produce a fresh constraint variable

Term Prolog PrologTerm | |

Term CodegenSolver BoolTerm | |

Term CodegenSolver IntTerm | CodegenSolver terms |

Term OvertonFD FDVar | |

HTerm t => Term (Herbrand t) t | |

(t ~ Expr (FDTerm s), FDSolver s) => Term (FDWrapper s) t | |

(Monoid w, Term s t) => Term (WriterT w s) t | |

(HTerm t, Solver s, Term s st) => Term (HerbrandT t s) (R st) | |

(HTerm t, Solver s) => Term (HerbrandT t s) (L t) |