Commit bbdf3b20 authored by Jan Rasmus Tikovsky 's avatar Jan Rasmus Tikovsky
Browse files

Merge remote-tracking branch 'origin' into newConstraints

Conflicts:
	External_Prelude.hs
	External_ValueSequence.hs
parents 43c59209 189e2aa2
......@@ -3,7 +3,8 @@
.curry
Curry_Main_Goal.curry
dist
kics2-libraries.cabal
*.cabal
AllLibraries.curry
# documentation
CDOC
------------------------------------------------------------------------------
--- 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,
getOneSolution,getOneValue,
getAllFailures,
getSearchTree,SearchTree(..)) where
import Findall
--- 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>
......@@ -3,7 +3,7 @@
--- Curry module tester "currytest".
---
--- @author Michael Hanus
--- @version June 2012
--- @version May 2014
------------------------------------------------------------------------------
module Assertion(-- for writing test cases:
......@@ -20,6 +20,7 @@ import AllSolutions
import List((\\))
import Socket -- for sending results to test GUI
import IO(hPutStrLn,hClose)
import Distribution(curryCompiler)
infixl 1 `seqStrActions`
......@@ -91,8 +92,7 @@ seqStrActions a1 a2 =
--- @return a protocol string and a flag whether the test was successful
checkAssertion :: String -> ((String,Bool) -> IO (String,Bool)) -> Assertion _
-> IO (String,Bool)
checkAssertion asrtfname prot assrt =
catchNDIO asrtfname prot (execAsrt assrt)
checkAssertion asrtop prot assrt = catchNDIO asrtop prot (execAsrt assrt)
where
execAsrt (AssertTrue name cond) =
catch (checkAssertTrue name cond) (returnError name) >>= prot
......@@ -113,47 +113,35 @@ checkAssertion asrtfname prot assrt =
-- 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
-> IO (String,Bool) -> IO (String,Bool)
catchNDIO fname prot a =
if curryCompiler == "kics2"
then -- specific handling for KiCS2 since it might report non-det errors
-- even if there is only one result value, e.g., in functional patterns
getAllValues a >>= checkIOActions
else catch a (\e -> prot ("ERROR in "++fname++": "++showError e++"\n",False))
where
checkIOActions results
| null results
= prot ("ERROR in operation "++fname++": computation failed\n",False)
= prot ("ERROR in "++fname++": computation failed\n",False)
| not (null (tail results))
= prot ("ERROR in operation "++fname++
= prot ("ERROR in "++fname++
": computation is non-deterministic\n",False)
| otherwise = head results
-- Checks Boolean assertion.
checkAssertTrue :: String -> Bool -> IO (String,Bool)
checkAssertTrue name cond =
getAllValues cond >>= checkResults
where
checkResults results
| null results
= return ("FAILURE of "++name++": computation of assertion failed\n",False)
| not (null (tail results))
= return ("FAILURE of "++name++
": computation of assertion is non-deterministic\n",False)
| head results = return ("OK: "++name++"\n",True)
| otherwise
= return ("FAILURE of "++name++": assertion not satisfied:\n",False)
checkAssertTrue name cond = catchNDIO name return $
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 =
getAllValues (call==result) >>= checkResults
where
checkResults results
| null results
= return ("FAILURE of "++name++
": computation of equality assertion failed\n",False)
| not (null (tail results))
= return ("FAILURE of "++name++
": computation of equality assertion is non-deterministic\n",False)
| head results = return ("OK: "++name++"\n",True)
| otherwise
= return ("FAILURE of "++name++": equality assertion not satisfied:\n"++
checkAssertEqual name call result = catchNDIO name return $
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)
......
--- 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
--- Reifyable "less than" constraint on FD variables.
(#<#) :: Int -> Int -> Constraint
x #<# y = FDLess x y
--- Reifyable "less than or equal" constraint on FD variables.
(#<=#) :: Int -> Int -> Constraint
x #<=# y = FDLessOrEqual x y
--- Reifyable "greater than" constraint on FD variables.
(#>#) :: Int -> Int -> Constraint
x #># y = FDGreater x y
--- Reifyable "greater than or equal" constraint on FD variables.
(#>=#) :: Int -> Int -> Constraint
x #>=# y = FDGreaterOrEqual x y
--- The resulting constraint is satisfied if both argument constraints
--- are satisfied.
neg :: Constraint -> Constraint
neg x = FDNeg x
--- The resulting constraint is satisfied if both argument constraints
--- are satisfied.
(#/\#) :: Constraint -> Constraint -> Constraint
x #/\# y = FDAnd x y
--- The resulting constraint is satisfied if both argument constraints
--- are satisfied.
(#\/#) :: Constraint -> Constraint -> Constraint
x #\/# y = FDOr x y
--- The resulting constraint is satisfied if the first argument constraint
--- do not hold or both argument constraints are satisfied.
(#=>#) :: Constraint -> Constraint -> Constraint
x #=># y = FDImply x y
--- The resulting constraint is satisfied if both argument constraint
--- are either satisfied and do not hold.
(#<=>#) :: Constraint -> Constraint -> Constraint
x #<=># y = FDEquiv x y
--- Solves a reified constraint.
solve :: Constraint -> Success
solve c = prim_solve_reify $!! c
prim_solve_reify :: Constraint -> Success
prim_solve_reify external
---------------------------------------------------------------------------
-- Complex constraints.
--- Relates the sum of FD variables with some integer of FD variable.
sum :: [Int] -> (Int -> Int -> Success) -> Int -> Success
sum vs rel v = seq (normalForm (ensureSpine vs))
(seq (ensureNotFree rel) (seq v (prim_sum vs rel v)))
prim_sum :: [Int] -> (Int -> Int -> Success) -> Int -> Success
prim_sum external
--- (scalarProduct cs vs relop v) is satisfied if ((cs*vs) relop v) is satisfied.
--- The first argument must be a list of integers. The other arguments are as
--- in <code>sum</code>.
scalarProduct :: [Int] -> [Int] -> (Int -> Int -> Success) -> Int -> Success
scalarProduct cs vs rel v =
seq (groundNormalForm cs)
(seq (normalForm (ensureSpine vs))
(seq (ensureNotFree rel) (seq v (prim_scalarProduct cs vs rel v))))
prim_scalarProduct :: [Int] -> [Int] -> (Int -> Int -> Success) -> Int -> Success
prim_scalarProduct external
--- (count v vs relop c) is satisfied if (n relop c), where n is the number of
--- elements in the list of FD variables vs that are equal to v, is satisfied.
--- The first argument must be an integer. The other arguments are as
--- in <code>sum</code>.
count :: Int -> [Int] -> (Int -> Int -> Success) -> Int -> Success
count v vs rel c =
seq (ensureNotFree v)
(seq (normalForm (ensureSpine vs))
(seq (ensureNotFree rel) (seq c (prim_count v vs rel c))))
prim_count :: Int -> [Int] -> (Int -> Int -> Success) -> Int -> Success
prim_count external
--- "All different" constraint on FD variables.
--- @param xs - list of FD variables
--- @return satisfied if the FD variables in the argument list xs
--- have pairwise different values.
allDifferent :: [Int] -> Success
allDifferent vs = seq (normalForm (ensureSpine vs)) (prim_allDifferent vs)
--- For backward compatibility. Use <code>allDifferent</code>.
all_different :: [Int] -> Success
all_different = allDifferent
prim_allDifferent :: [Int] -> Success
prim_allDifferent external
--- Instantiate a single FD variable to its values in the specified domain.
indomain :: Int -> Success
indomain x = seq x (prim_indomain x)
prim_indomain :: Int -> Success
prim_indomain external
---------------------------------------------------------------------------
-- Labeling.
--- Instantiate FD variables to their values in the specified domain.
--- @param options - list of option to control the instantiation of FD variables
--- @param xs - list of FD variables that are non-deterministically
--- instantiated to their possible values.
labeling :: [LabelingOption] -> [Int] -> Success
labeling options vs = seq (normalForm (map ensureNotFree (ensureSpine options)))
(seq (normalForm (ensureSpine vs))
(prim_labeling options vs))
prim_labeling :: [LabelingOption] -> [Int] -> Success
prim_labeling external
--- This datatype contains all options to control the instantiated of FD variables
--- with the enumeration constraint <code>labeling</code>.
--- @cons LeftMost - The leftmost variable is selected for instantiation (default)
--- @cons FirstFail - The leftmost variable with the smallest domain is selected
--- (also known as first-fail principle)
--- @cons FirstFailConstrained - The leftmost variable with the smallest domain
--- and the most constraints on it is selected.
--- @cons Min - The leftmost variable with the smalled lower bound is selected.