Commit f4e24f91 authored by Michael Hanus's avatar Michael Hanus
Browse files

PAKCS libraries integrated into KiCS2 branch

parent ecd1fe65
------------------------------------------------------------------------------
--- This module contains a collection of functions for
--- obtaining lists of solutions to constraints.
--- These operations are useful to encapsulate
--- non-deterministic operations between I/O actions in
--- order to connects 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.
------------------------------------------------------------------------------
module AllSolutions(getAllSolutions,--getAllValues, -- already in the prelude
getOneSolution,getOneValue,
getAllFailures,
getSearchTree,SearchTree(..)) where
--- 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.
getAllSolutions :: (a->Success) -> IO [a]
getAllSolutions c = return (findall c)
{-
-- In principle, getAllSolutions can be defined by getSearchTree as follows:
getAllSolutions c =
do (Solutions sols) <- getSearchTree [] c
return sols
-- However, our above definition is slightly more efficient.
-}
--- Gets all values of an expression. Since this is based on
--- <code>getAllSolutions</code>, it inherits the same restrictions.
getAllValues :: a -> IO [a]
getAllValues e = return (findall (=:=e))
--- Gets one solution to a constraint (currently, via an incomplete
--- left-to-right strategy). Returns Nothing if the search space
--- is finitely failed.
getOneSolution :: (a->Success) -> IO (Maybe a)
getOneSolution c =
do sols <- getAllSolutions c
return (if null sols then Nothing else Just (head sols))
--- Gets one value of an expression (currently, via an incomplete
--- left-to-right strategy). Returns Nothing if the search space
--- is finitely failed.
getOneValue :: a -> IO (Maybe a)
getOneValue x = getOneSolution (x=:=)
--- Returns a list of values that do not satisfy a given constraint.
--- @param x - an expression (a generator evaluable to various values)
--- @param c - a constraint that should not be satisfied
--- @return A list of all values of e such that (c e) is not provable
getAllFailures :: a -> (a->Success) -> IO [a]
getAllFailures generator test =
do xs <- getAllSolutions (=:=generator)
failures <- mapIO (naf test) xs
return $ concat failures
where
-- (naf c x) returns [x] if (c x) fails, and [] otherwise.
naf :: (a->Success) -> a -> IO [a]
naf c x = getOneSolution (\_->c x) >>= \mbl->
return (maybe [x] (const []) mbl)
--- A search tree for representing search structures.
data SearchTree a b = SearchBranch [(b,SearchTree a b)] | Solutions [a]
--- 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.
getSearchTree :: [a] -> (b -> Success) -> IO (SearchTree b a)
getSearchTree cs goal = return (getSearchTreeUnsafe cs goal)
getSearchTreeUnsafe :: [a] -> (b -> Success) -> (SearchTree b a)
getSearchTreeUnsafe [] goal = Solutions (findall goal)
getSearchTreeUnsafe (c:cs) goal =
SearchBranch (findall (=:=(solve c cs goal)))
solve :: a -> [a] -> (b -> Success) -> (a,SearchTree b a)
solve c cs goal | c=:=y = (y, getSearchTreeUnsafe cs goal) where y free
<?xml version="1.0" standalone="no"?>
<!DOCTYPE primitives SYSTEM "http://www.informatik.uni-kiel.de/~pakcs/primitives.dtd">
<primitives>
<primitive name="getOneSolution" arity="1">
<library>prim_standard</library>
<entry>prim_getOneSolution[raw]</entry>
</primitive>
</primitives>
------------------------------------------------------------------------------
--- This module defines the datatype and operations for the
--- Curry module tester "currytest".
---
--- @author Michael Hanus
--- @version June 2012
------------------------------------------------------------------------------
module Assertion(-- for writing test cases:
Assertion,assertTrue,assertEqual,
assertValues,assertSolutions,assertIO,assertEqualIO,
-- the remaining entities are only used by the test tool:
checkAssertion,
seqStrActions,writeAssertResult,
ProtocolMsg(..),
showTestMod,showTestCase,showTestEnd,showTestCompileError)
where
import AllSolutions
import List((\\))
import Socket -- for sending results to test GUI
import IO(hPutStrLn,hClose)
infixl 1 `seqStrActions`
--- Datatype for defining test cases.
--- @cons AssertTrue s b - assert (with name s) that b must be true
--- @cons AssertEqual s e1 e2 - assert (with name s) that e1 and e2 must
--- be equal (w.r.t. ==)
--- @cons AssertValues s e vs - assert (with name s) that vs is the multiset
--- of all values of e (i.e., all values of e are
--- compared with the elements in vs w.r.t. ==)
--- @cons AssertSolutions s c vs - assert (with name s) that constraint
--- abstraction c has the multiset of solutions vs
--- (i.e., the solutions of c are compared with the elements in vs w.r.t. ==)
--- @cons AssertIO s a r - assert (with name s) that I/O action a
--- yields the result value r
--- @cons AssertEqualIO s a1 a2 - assert (with name s) that I/O actions a1 and
--- a2 yield equal (w.r.t. ==) results
data Assertion a = AssertTrue String Bool
| AssertEqual String a a
| AssertValues String a [a]
| AssertSolutions String (a->Success) [a]
| AssertIO String (IO a) a
| AssertEqualIO String (IO a) (IO a)
--- `(assertTrue s b)` asserts (with name `s`) that `b` must be true.
assertTrue :: String -> Bool -> Assertion ()
assertTrue s b = AssertTrue s b
--- `(assertEqual s e1 e2)` asserts (with name `s`) that `e1` and `e2`
--- must be equal (w.r.t. `==`).
assertEqual :: String -> a -> a -> Assertion a
assertEqual s x y = AssertEqual s x y
--- `(assertValues s e vs)` asserts (with name `s`) that `vs` is the multiset
--- of all values of `e`. All values of `e` are
--- compared with the elements in `vs` w.r.t. `==`.
assertValues :: String -> a -> [a] -> Assertion a
assertValues s x y = AssertValues s x y
--- `(assertSolutions s c vs)` asserts (with name `s`) that constraint
--- abstraction `c` has the multiset of solutions `vs`.
--- The solutions of `c` are compared with the elements in `vs` w.r.t. `==`.
assertSolutions :: String -> (a->Success) -> [a] -> Assertion a
assertSolutions s x y = AssertSolutions s x y
--- `(assertIO s a r)` asserts (with name `s`) that I/O action `a`
--- yields the result value `r`.
assertIO :: String -> IO a -> a -> Assertion a
assertIO s x y = AssertIO s x y
--- `(assertEqualIO s a1 a2)` asserts (with name `s`) that I/O actions `a1`
--- and `a2` yield equal (w.r.t. `==`) results.
assertEqualIO :: String -> IO a -> IO a -> Assertion a
assertEqualIO s x y = AssertEqualIO s x y
--- Combines two actions and combines their results.
--- Used by the currytest tool.
seqStrActions :: IO (String,Bool) -> IO (String,Bool) -> IO (String,Bool)
seqStrActions a1 a2 =
do (s1,b1) <- a1
(s2,b2) <- a2
return (s1++s2,b1&&b2)
--- Executes and checks an assertion, and process the result
--- by an I/O action.
--- Used by the currytest tool.
--- @param protocol - an action to be applied after test execution
--- @param assertion - an assertion to be tested
--- @return a protocol string and a flag whether the test was successful
checkAssertion :: String -> ((String,Bool) -> IO (String,Bool)) -> Assertion _
-> IO (String,Bool)
checkAssertion _ prot assrt =
--catchNDIO asrtfname prot
(execAsrt assrt)
where
execAsrt (AssertTrue name cond) =
catch (checkAssertTrue name cond) (returnError name) >>= prot
execAsrt (AssertEqual name call result) =
catch (checkAssertEqual name call result) (returnError name) >>= prot
execAsrt (AssertValues name expr results) =
catch (checkAssertValues name expr results) (returnError name) >>= prot
execAsrt (AssertSolutions name constr results) =
catch (checkAssertSolutions name constr results) (returnError name) >>= prot
execAsrt (AssertIO name action result) =
catch (checkAssertIO name action result) (returnError name) >>= prot
execAsrt (AssertEqualIO name action1 action2) =
catch (checkAssertEqualIO name action1 action2) (returnError name) >>= prot
returnError name err =
return ("FAILURE of "++name++": "++showError err++"\n",False)
-- Execute I/O action for assertion checking and report any failure
-- or non-determinism.
catchNDIO :: String -> ((String,Bool) -> IO (String,Bool))
-> IO ((String,Bool)) -> IO ((String,Bool))
catchNDIO fname prot a = getAllValues a >>= checkIOActions
where
checkIOActions results
| null results
= prot ("ERROR in operation "++fname++": computation failed\n",False)
| not (null (tail results))
= prot ("ERROR in operation "++fname++
": computation is non-deterministic\n",False)
| otherwise = head results
-- Checks Boolean assertion.
checkAssertTrue :: String -> Bool -> IO (String,Bool)
checkAssertTrue name cond =
if cond
then return ("OK: "++name++"\n",True)
else return ("FAILURE of "++name++": assertion not satisfied:\n",False)
-- Checks equality assertion.
checkAssertEqual :: String -> a -> a -> IO (String,Bool)
checkAssertEqual name call result =
if call==result
then return ("OK: "++name++"\n",True)
else return ("FAILURE of "++name++": equality assertion not satisfied:\n"++
"Computed answer: "++show call++"\n"++
"Expected answer: "++show result++"\n",False)
-- Checks all values assertion.
checkAssertValues :: String -> a -> [a] -> IO (String,Bool)
checkAssertValues name call results = do
rs <- getAllValues call
if null (rs \\ results) && null (results \\ rs)
then return ("OK: "++name++"\n",True)
else return ("FAILURE of "++name++": values assertion not satisfied:\n"++
"Computed values: "++show rs++"\n"++
"Expected values: "++show results++"\n",False)
-- Checks all solutions of a constraint abstraction.
checkAssertSolutions :: String -> (a->Success) -> [a] -> IO (String,Bool)
checkAssertSolutions name constr results = do
rs <- getAllSolutions constr
if null (rs \\ results) && null (results \\ rs)
then return ("OK: "++name++"\n",True)
else return ("FAILURE of "++name++": solutions assertion not satisfied:\n"++
"Computed values: "++show rs++"\n"++
"Expected values: "++show results++"\n",False)
-- Checks an IO assertion.
checkAssertIO :: String -> IO a -> a -> IO (String,Bool)
checkAssertIO name action result = do
r <- action
if r==result
then return ("OK: "++name++"\n",True)
else return ("FAILURE of "++name++": IO assertion not satisfied:\n"++
"Computed answer: "++show r++"\n"++
"Expected answer: "++show result++"\n\n",False)
-- Checks equality of results of two IO assertions.
checkAssertEqualIO :: String -> IO a -> IO a -> IO (String,Bool)
checkAssertEqualIO name action1 action2 = do
r1 <- action1
r2 <- action2
if r1==r2
then return ("OK: "++name++"\n",True)
else return ("FAILURE of "++name++": IO equality assertion not satisfied:\n"++
"Computed answer 1: "++show r1++"\n"++
"Computed answer 2: "++show r2++"\n\n",False)
--- Prints the results of assertion checking.
--- If failures occurred, the return code is positive.
--- Used by the currytest tool.
writeAssertResult :: (String,Bool) -> IO Int
writeAssertResult (result,flag) =
if flag
then putStrLn (result++"All tests successfully passed.") >> return 0
else putStrLn (result++"FAILURE occurred in some assertions!\n") >> return 1
----------------------------------------------------------------------------
-- The following entities are used to implement the test GUI:
--- The messages sent to the test GUI.
--- Used by the currytest tool.
data ProtocolMsg = TestModule String | TestCase String Bool | TestFinished
| TestCompileError
--- Sends message to GUI for showing test of a module.
--- Used by the currytest tool.
showTestMod :: Int -> String -> IO ()
showTestMod portnum modname = sendToLocalSocket portnum (TestModule modname)
--- Sends message to GUI for showing result of executing a test case.
--- Used by the currytest tool.
showTestCase :: Int -> (String,Bool) -> IO (String,Bool)
showTestCase portnum (s,b) = do
sendToLocalSocket portnum (TestCase s b)
return (s,b)
--- Sends message to GUI for showing end of module test.
--- Used by the currytest tool.
showTestEnd :: Int -> IO ()
showTestEnd portnum = sendToLocalSocket portnum TestFinished
--- Sends message to GUI for showing compilation errors in a module test.
--- Used by the currytest tool.
showTestCompileError :: Int -> IO ()
showTestCompileError portnum = sendToLocalSocket portnum TestCompileError
--- Sends protocol message to local socket.
sendToLocalSocket :: Int -> ProtocolMsg -> IO ()
sendToLocalSocket portnum msg = do
h <- connectToSocket "localhost" portnum
hPutStrLn h (show msg)
hClose h
-- end of module Assertion
--- This library provides a Boolean Constraint Solver based on BDDs.
---
--- @author Sebastian Fischer
--- @version May 2006
module CLPB (
Boolean, true, false,
neg, (.&&), (.||), (./=), (.==), (.<=), (.>=), (.<), (.>), count, exists,
satisfied, check, bound, simplify, evaluate
) where
infixr 3 .&&
infixr 2 .||
infix 1 ./=, .==
data Boolean = B Int -- abstract
--- The always satisfied constraint
true :: Boolean
true = B 1
--- The never satisfied constraint
false :: Boolean
false = B 0
--- Result is true iff argument is false.
neg :: Boolean -> Boolean
neg (B x) = B (prim_neg $! x)
prim_neg :: Int -> Int
prim_neg external
--- Result is true iff both arguments are true.
(.&&) :: Boolean -> Boolean -> Boolean
(B x) .&& (B y) = B ((prim_and $!y) $! x)
prim_and :: Int -> Int -> Int
prim_and external
--- Result is true iff at least one argument is true.
(.||) :: Boolean -> Boolean -> Boolean
(B x) .|| (B y) = B ((prim_or $!y) $! x)
prim_or :: Int -> Int -> Int
prim_or external
--- Result is true iff exactly one argument is true.
(./=) :: Boolean -> Boolean -> Boolean
(B x) ./= (B y) = B ((prim_xor $!y) $! x)
prim_xor :: Int -> Int -> Int
prim_xor external
--- Result is true iff both arguments are equal.
(.==) :: Boolean -> Boolean -> Boolean
x .== y = neg x ./= y
--- Result is true iff the first argument implies the second.
(.<=) :: Boolean -> Boolean -> Boolean
x .<= y = neg x .|| y
--- Result is true iff the second argument implies the first.
(.>=) :: Boolean -> Boolean -> Boolean
x .>= y = y .<= x
--- Result is true iff the first argument is false and the second is true.
(.<) :: Boolean -> Boolean -> Boolean
x .< y = neg x .&& y
--- Result is true iff the first argument is true and the second is false.
(.>) :: Boolean -> Boolean -> Boolean
x .> y = y .< x
--- Result is true iff the count of valid constraints in the first list
--- is an element of the second list.
count :: [Boolean] -> [Int] -> Boolean
count bs ns = B ((card $!! map ensureNotFree (ensureSpine ns))
$!! map int (ensureSpine bs))
card :: [Int] -> [Int] -> Int
card external
--- Result is true, if the first argument is a variable which can be
--- instantiated such that the second argument is true.
exists :: Boolean -> Boolean -> Boolean
exists (B v) (B b) = B ((prim_exists $!! v) $!! b)
prim_exists :: Int -> Int -> Int
prim_exists external
--- Checks the consistency of the constraint with regard to the accumulated
--- constraints, and, if the check succeeds, tells the constraint.
satisfied :: Boolean -> Success
satisfied (B b) = sat $!! b
sat :: Int -> Success
sat external
--- Asks whether the argument (or its negation) is now entailed by the
--- accumulated constraints. Fails if it is not.
check :: Boolean -> Bool
check (B b) = (prim_check $!! b) == 1
prim_check :: Int -> Int
prim_check external
--- Instantiates given variables with regard to the accumulated constraints.
bound :: [Boolean] -> Success
bound bs = labeling $!! map int (ensureSpine bs)
labeling :: [Int] -> Success
labeling external
--- Simplifies the argument with regard to the accumulated constraints.
simplify :: Boolean -> Boolean
simplify b | satisfied (a .== b) = a where a free
--- Evaluates the argument with regard to the accumulated constraints.
evaluate :: Boolean -> Bool
evaluate x | bound [y] = int y == 1
where
y = simplify x
-- private
int :: Boolean -> Int
int (B x) = x
<?xml version="1.0" standalone="no"?>
<!DOCTYPE primitives SYSTEM "http://www.informatik.uni-kiel.de/~pakcs/primitives.dtd">
<primitives>
<primitive name="prim_neg" arity="1">
<library>prim_clpb</library>
<entry>clpb_neg</entry>
</primitive>
<primitive name="prim_and" arity="2">
<library>prim_clpb</library>
<entry>clpb_and</entry>
</primitive>
<primitive name="prim_or" arity="2">
<library>prim_clpb</library>
<entry>clpb_or</entry>
</primitive>
<primitive name="prim_xor" arity="2">
<library>prim_clpb</library>
<entry>clpb_xor</entry>
</primitive>
<primitive name="card" arity="2">
<library>prim_clpb</library>
<entry>clpb_card</entry>
</primitive>
<primitive name="prim_exists" arity="2">
<library>prim_clpb</library>
<entry>clpb_exists</entry>
</primitive>
<primitive name="sat" arity="1">
<library>prim_clpb</library>
<entry>clpb_sat</entry>
</primitive>
<primitive name="prim_check" arity="1">
<library>prim_clpb</library>
<entry>clpb_check</entry>
</primitive>
<primitive name="labeling" arity="1">
<library>prim_clpb</library>
<entry>clpb_labeling</entry>
</primitive>
</primitives>
------------------------------------------------------------------------------
--- Library for finite domain constraint solving.
--- <p>
--- The general structure of a specification of an FD problem is as follows:
---
--- <code>domain_constraint & fd_constraint & labeling</code>
---
--- where:
---
--- <code>domain_constraint</code>
--- specifies the possible range of the FD variables (see constraint <code>domain</code>)
---
--- <code>fd_constraint</code>
--- specifies the constraint to be satisfied by a valid solution
--- (see constraints #+, #-, allDifferent, etc below)
---
--- <code>labeling</code>
--- is a labeling function to search for a concrete solution.
---
--- Note: This library is based on the corresponding library of Sicstus-Prolog
--- but does not implement the complete functionality of the
--- Sicstus-Prolog library.
--- However, using the PAKCS interface for external functions, it is relatively
--- easy to provide the complete functionality.
---
--- @author Michael Hanus
--- @version June 2012
------------------------------------------------------------------------------
module CLPFD(domain, (+#), (-#), (*#), (=#), (/=#), (<#), (<=#), (>#), (>=#),
Constraint, (#=#), (#/=#), (#<#), (#<=#), (#>#), (#>=#),
neg, (#/\#), (#\/#), (#=>#), (#<=>#), solve,
sum, scalarProduct, allDifferent, all_different, count,
indomain, labeling, LabelingOption(..)) where
-- The operator declarations are similar to the standard arithmetic
-- and relational operators.
infixl 7 *#
infixl 6 +#, -#
infix 4 =#, /=#, <#, <=#, >#, >=#
infix 4 #=#, #/=#, #<#, #<=#, #>#, #>=#
infixr 3 #/\#
infixr 2 #\/#
infixr 1 #=>#, #<=>#
--- Constraint to specify the domain of all finite domain variables.
--- @param xs - list of finite domain variables
--- @param min - minimum value for all variables in xs
--- @param max - maximum value for all variables in xs
domain :: [Int] -> Int -> Int -> Success
domain vs l u = ((prim_domain $!! (ensureSpine vs)) $# l) $# u
prim_domain :: [Int] -> Int -> Int -> Success
prim_domain external
--- Addition of FD variables.
(+#) :: Int -> Int -> Int
x +# y = (prim_FD_plus $! y) $! x
prim_FD_plus :: Int -> Int -> Int
prim_FD_plus external
--- Subtraction of FD variables.
(-#) :: Int -> Int -> Int
x -# y = (prim_FD_minus $! y) $! x
prim_FD_minus :: Int -> Int -> Int
prim_FD_minus external
--- Multiplication of FD variables.
(*#) :: Int -> Int -> Int
x *# y = (prim_FD_times $! y) $! x
prim_FD_times :: Int -> Int -> Int
prim_FD_times external
--- Equality of FD variables.
(=#) :: Int -> Int -> Success
x =# y = (prim_FD_equal $! y) $! x
prim_FD_equal :: Int -> Int -> Success
prim_FD_equal external
--- Disequality of FD variables.
(/=#) :: Int -> Int -> Success
x /=# y = (prim_FD_notequal $! y) $! x
prim_FD_notequal :: Int -> Int -> Success
prim_FD_notequal external
--- "Less than" constraint on FD variables.
(<#) :: Int -> Int -> Success
x <# y = (prim_FD_le $! y) $! x
prim_FD_le :: Int -> Int -> Success
prim_FD_le external
--- "Less than or equal" constraint on FD variables.
(<=#) :: Int -> Int -> Success
x <=# y = (prim_FD_leq $! y) $! x
prim_FD_leq :: Int -> Int -> Success
prim_FD_leq external
--- "Greater than" constraint on FD variables.
(>#) :: Int -> Int -> Success
x ># y = (prim_FD_ge $! y) $! x
prim_FD_ge :: Int -> Int -> Success
prim_FD_ge external
--- "Greater than or equal" constraint on FD variables.
(>=#) :: Int -> Int -> Success
x >=# y = (prim_FD_geq $! y) $! x
prim_FD_geq :: Int -> Int -> Success
prim_FD_geq external
---------------------------------------------------------------------------
-- Reifyable constraints.
--- A datatype to represent reifyable constraints.
data Constraint = FDEqual Int Int
| FDNotEqual Int Int
| FDGreater Int Int
| FDGreaterOrEqual Int Int
| FDLess Int Int
| FDLessOrEqual Int Int
| FDNeg Constraint
| FDAnd Constraint Constraint
| FDOr Constraint Constraint
| FDImply Constraint Constraint
| FDEquiv Constraint Constraint
--- Reifyable equality constraint on FD variables.
(#=#) :: Int -> Int -> Constraint
x #=# y = FDEqual x y
--- Reifyable inequality constraint on FD variables.
(#/=#) :: Int -> Int -> Constraint
x #/=# y = FDNotEqual x y