Module Control.AllSolutions

This module contains a collection of functions for obtaining lists of solutions to constraints or values of expressions. These operations are useful to encapsulate non-deterministic operations between I/O actions in order to connect the worlds of logic and functional programming and to avoid non-determinism failures on the I/O level.

In contrast the "old" concept of encapsulated search (which could be applied to any subexpression in a computation), the operations to encapsulate search in this module are I/O actions in order to avoid some anomalities in the old concept.

Author: Michael Hanus

Version: June 2021

Summary of exported operations:

getAllValues :: a -> IO [a]  Deterministic 
Gets all values of an expression (currently, via an incomplete depth-first strategy).
getOneValue :: a -> IO (Maybe a)  Deterministic 
Gets one value of an expression (currently, via an incomplete left-to-right strategy).
getAllSolutions :: Data a => (a -> Bool) -> IO [a]  Non-deterministic 
Gets all solutions to a constraint (currently, via an incomplete depth-first left-to-right strategy).
getOneSolution :: Data a => (a -> Bool) -> IO (Maybe a)  Non-deterministic 
Gets one solution to a constraint (currently, via an incomplete left-to-right strategy).
getAllFailures :: a -> (a -> Bool) -> IO [a]  Deterministic 
Returns a list of values that do not satisfy a given constraint.
getSearchTree :: (Data a, Data b) => [a] -> (b -> Bool) -> IO (SearchTree b a)  Deterministic 
Computes a tree of solutions where the first argument determines the branching level of the tree.

Exported datatypes:


SearchTree

A search tree for representing search structures.

Constructors:

  • SearchBranch :: [(b,SearchTree a b)] -> SearchTree a b
  • Solutions :: [a] -> SearchTree a b

Exported operations:

getAllValues :: a -> IO [a]  Deterministic 

Gets all values of an expression (currently, via an incomplete depth-first strategy). Conceptually, all values are computed on a copy of the expression, i.e., the evaluation of the expression does not share any results. Moreover, the evaluation suspends as long as the expression contains unbound variables.

getOneValue :: a -> IO (Maybe a)  Deterministic 

Gets one value of an expression (currently, via an incomplete left-to-right strategy). Returns Nothing if the search space is finitely failed.

getAllSolutions :: Data a => (a -> Bool) -> IO [a]  Non-deterministic 

Gets all solutions to a constraint (currently, via an incomplete depth-first left-to-right strategy). Conceptually, all solutions are computed on a copy of the constraint, i.e., the evaluation of the constraint does not share any results. Moreover, this evaluation suspends if the constraints contain unbound variables. Similar to Prolog's findall.

getOneSolution :: Data a => (a -> Bool) -> IO (Maybe a)  Non-deterministic 

Gets one solution to a constraint (currently, via an incomplete left-to-right strategy). Returns Nothing if the search space is finitely failed.

getAllFailures :: a -> (a -> Bool) -> IO [a]  Deterministic 

Returns a list of values that do not satisfy a given constraint.

Example call:
(getAllFailures x c)
Parameters:
  • x : an expression (a generator evaluable to various values)
  • c : a constraint that should not be satisfied
Returns:
A list of all values of e such that (c e) is not provable

getSearchTree :: (Data a, Data b) => [a] -> (b -> Bool) -> IO (SearchTree b a)  Deterministic 

Computes a tree of solutions where the first argument determines the branching level of the tree. For each element in the list of the first argument, the search tree contains a branch node with a child tree for each value of this element. Moreover, evaluations of elements in the branch list are shared within corresponding subtrees.