abau / co4 Goto Github PK
View Code? Open in Web Editor NEWCOmplexity COncerned COnstraint COmpiler
License: GNU General Public License v3.0
COmplexity COncerned COnstraint COmpiler
License: GNU General Public License v3.0
commit c5eaecd
leads to stack overflows during abstract evaluation, which should not happen, since resursion is on known list shapes only (the contents of the lists is unknown but it should not influence the control flow)
./CO4/CSPlib/Prob006/Main 2 1 +RTS -xc
Start producing CNF
*** Exception (reporting due to +RTS -xc): (THUNK_STATIC), stack trace:
CO4.EncodedAdt.isDefined,
called from CO4.EncodedAdt.isUndefined,
called from CO4.EncodedAdt.isConstantlyUndefined,
called from CO4.EncodedAdt.flags.\,
called from CO4.EncodedAdt.flags,
called from CO4.EncodedAdt.constantConstructorIndex,
called from CO4.EncodedAdt.constructorArgument,
called from Main.encDistribute.\.encXs'_31,
called from Main.encDistribute.\,
called from Main.encDistribute,
called from Main.encOesort.\,
called from Main.encOesort,
called from Main.encAlldifferent_sorting.\,
called from Main.encAlldifferent_sorting,
called from Main.encConstraint.\,
called from Main.encConstraint,
called from CO4.Monad.runCO4,
called from CO4.Solve.solveP,
called from CO4.Solve.solveAndTestP,
called from Main.run,
called from Main.main,
called from :Main.CAF:main
...
Stack space overflow: current size 8388608 bytes.
in order to be able to use *.standalone.hs in ghci, data declarations must contain deriving (Eq,Show)
. These should just be ignored by CO4.
for debugging the space/time behaviour I want to know, for each case
, how often it was happening on known data, and how often on unknown data. Of course "known" is better since it does not require encoding and merging.
case
should ONLY be executed on known data"as long as we don't have the "modes" system, if such an annotation is present, CO4 does not generate code for matching unknown data and merging the results, but instead emits code that will throw an exception.
a nice modelling test case:
https://en.wikipedia.org/wiki/Costas_array
https://github.com/apunktbau/co4/tree/master/CO4/Test/Costas
at the moment, it's plain Haskell. How much do we need to rewrite so that CO4 can accept it? Can we then find a Costas array of size 32?
We should provide an easy way to use an externally defined (and optimized) binary encoding for data types, like those in https://github.com/jwaldmann/satchmo/blob/master/Satchmo/Binary/Op/Times.hs#L21
Suggestion: for abstract objects for types Integer (arbitrary width), Int8, Int16 (fixed width) (actually, Natural, Nat8, ... ) we use the type EncodedAdt that we already have:
we put the binary encoding in the list of flags, and there are no arguments. Then:
Using (==) in polymorphic code, like
ord :: Eq a => a -> ...
, results in ambiguous types in the compiled code (here: encOrd
)
Could not deduce (EncEq a0 e p)
arising from the ambiguity check for `encOrd'
from the context (CO4.Cache.MonadCache (e p) m,
CO4.Profiling.MonadProfiling m,
EncEq a e p)
bound by the inferred type for `encOrd':
(CO4.Cache.MonadCache (e p) m, CO4.Profiling.MonadProfiling m,
EncEq a e p) =>
e p -> e p -> e p -> m (e p)
as it is unclear which EncEq
instance to choose. Ghci suggests
Possible fix: add a type signature that fixes these type variable(s)
but this requires to explicitly annotate type signatures in the compiled program.
this does not work:
monotone xs =
and (zipWith gtNat8 xs (tail xs) )
...
CO4/Test/Assert.hs:25:4:
Could not deduce (p ~ (e p -> m (e p)))
but this does:
monotone xs =
and (zipWith gt xs (tail xs) )
gt = gtNat8
I am getting stack overflows when generating CNFs of moderate (I think) size.
It would be good to know the reason. Perhaps something is too strict,
e.g., foldr
with a strict combining function (so it has to traverse the whole list before producing a result)? The following trace (with cache, with profiling) shows nothing unusual.
commit 7a4284f ,
./CO4/Test/WCB '(((......)))' +RTS -xc
Start producing CNF
*** Exception (reporting due to +RTS -xc): (THUNK_STATIC), stack trace:
CO4.Profiling.onCurrentInner,
called from CO4.Profiling.emit,
called from Satchmo.Core.Boolean.assert,
called from Satchmo.Core.Primitive.assertOr,
called from Satchmo.Core.Boolean.and,
called from Satchmo.Core.Primitive.xor.xor2,
called from Satchmo.Core.Primitive.xor,
called from CO4.PreludeNat.encComparePrimitives,
called from CO4.PreludeNat.encLtNat8.\,
called from CO4.PreludeNat.onFlags,
called from CO4.PreludeNat.encLtNat8,
called from CO4.PreludeNat.encGtNat8,
called from CO4.PreludeNat.encMaxNat8.\,
called from CO4.PreludeNat.encMaxNat8,
called from CO4.Cache.withCache.\,
called from CO4.Cache.withCache,
called from Satchmo.Core.SAT.Minisat.>>=.\.(...),
called from Satchmo.Core.SAT.Minisat.>>=.\,
called from Satchmo.Core.SAT.Minisat.>>=,
called from Satchmo.Core.SAT.Minisat.solve'.\,
called from Satchmo.Core.SAT.Minisat.solve',
called from CO4.Algorithms.Eitherize.Solve.solve,
called from CO4.Algorithms.Eitherize.Solve.solveAndTestP,
called from CO4.Algorithms.Eitherize.Solve.solveAndTestBooleanP,
called from Main.result_for,
called from Main.mainz
for the definition of equality on
data T = A | B | C
it would be nice if we had '_' for writing
eqT x y = case x of A -> case y of A -> True ; _ -> False ...
simple proposal (for satchmo backend):
status :: SAT (Int, Int)
should give current number of variables, clauses (we can count this on our own, or ask minisat-API)
then, simple version of "call with profile" (in the compiled program)
traced :: String -> SAT a -> SAT a
traced msg action = do
s0 <- status
x <- action
s1 <- status
print (msg, s1 - s0)
return x
but the semantics in the constraint system is:
traced :: String -> a -> a ; traced msg x = x
for all user-defined algebraic data types, equalitiy would be nice:
(Note: We don't want the full type class machinery, just '=='.)
A design question is whether
Writing might be better: then the constraint program is a correctly typed Haskell program
it would be nice to allow nested patterns, for example
case xs of Cons x Nil -> ...
They should be translated to nested cases with flat patterns like
case xs of Cons x xs' -> case xs' of Nil -> ...
make available numbers similar to Satchmo.Unary
https://github.com/jwaldmann/satchmo/tree/master/Satchmo/Unary
the main problem is a reasonable naming scheme for types and operations
(ultimately, need some form of a numeric type class?)
in publications, also cite Sugar http://bach.istc.kobe-u.ac.jp/sugar/ which seems to be quite successful at using such encodings for CSP.
Allow users to turn off optimizations like 6615963.
(this is not a bug) Following example shows an exponential blowup
due to recursive merging (which I think will produce a full binary tree)
data T = A | B Bool T | C T Bool
build xs = case xs of
[] -> A
x : xs' ->
let t' = build xs'
in case x of
False -> B x t'
True -> C t' x
data from running the test program (#vars is doubled each time)
depth #vars
5 188
6 380
7 764
8 1532
9 3068
10 6140
I think this could be avoided if the arguments of constructor C
are swapped in the abstract value,
effectively using
data T = A | B Bool T | C Bool T
but I am not sure whether CO4 should look for such kind of optimisation.
could we replace Nat8
by Nat
in the sense that:
the concrete program is terminating (for all arguments)
but the abstract program (currently) is not.
with incremental feasibility checking, abstract evaluation should detect
that "case u of True ..." cannot happen in the inner call.
constraint k u = case u of
False -> k
True -> constraint (not k) False
This doesn't compile
data Bool = False | True
data List a = Nil | Cons a (List a)
main x = all (\c -> c x) (Cons not Nil)
all f = foldr (\x -> and (f x)) True
foldr k z xs = case xs of
Nil -> z
Cons y ys -> k y ( foldr k z ys )
and x y = case x of
False -> False
True -> y
not x = case x of False -> True
True -> False
Maybe passing around top level functions in the compiled system isn't handled correctly?
this occurs often in CSP, both in educational problems (sendmoremoney to N-queens to Golomb rulers) an in real ones (scheduling).
see https://github.com/apunktbau/co4/blob/master/CO4/Test/Merge.hs#L14
constraint :: Bool -> Either [Bool] [Bool] -> Bool
constraint p u = case u of
Left xs -> p == and (assertKnown xs)
Right ys -> p == or ys
allocator for u:
( constructors [ Just [ kList 2 uBool ], Just [ kList 2 uBool ] ] )
so the moded type of u
is
Unknown-Either (Known-List (Unknown-Bool)) (Known-List (Unknown-Bool))
I expect that assertKnown xs
holds, but it does not.
it would be nice to have data Bool = False | True
and some basic operations ( not, ||, && )
and also if-then-else (translated to case).
Note: data Bool is needed anyway for the result type
of the top-level constraint.
just the data declarations, as in the prelude, and the canonical functions
maybe :: b -> (a -> b) -> Maybe a -> b
either :: (a -> c) -> (b -> c) -> Either a b -> c
the programmer should be able to write (e.g., for the maybe monad)
infixl 1 >>, >>=
m >>= f = case m of ...
the problem seems to be that Template Haskell parses the application of >>=
as http://hackage.haskell.org/packages/archive/template-haskell/2.8.0.0/doc/html/Language-Haskell-TH-Syntax.html#v:UInfixE
commit f3c98ba
file CO4/Test/SL.hs
execute example
, gives
(RULES a -> b)
[([[]],[[True]])]
fromList [(b,[True]),(a,[])]
Start producing CNF
Cache call hits: 61 (18%), call misses: 267 (81%)
Cache case hits: 29 (16%), case misses: 149 (83%)
Assertion: 196
CNF finished (#variables: 99, #clauses: 221)
Starting solver
Solver finished in 0.0 seconds (result: True)
Starting decoder
Decoder finished
Solution: Step [([],[[Finite [False]]]),([True],[[Finite [True]]])] []
Test: *** Exception: Prelude.undefined
instead it should print True
?
otherwise it conflicts with the "main" function (of type IO()) that ghc expects when compiling an executable.
there are work-arounds like
so it is probably not that important.
Test case: https://github.com/apunktbau/co4/blob/master/CO4/Test/Factor.hs
constains simple binary multiplication.
Obeserved behaviour: eats huge amount of space (try replacing 24 by 32 also).
This seems terribly wrong: https://github.com/apunktbau/co4/blob/master/CO4/PreludeNat.hs#L50
instance Encodeable Nat where
encode n = encodedConstructor (value n) (2^(width n)) []
since it seems to iterate over 2^24 values.
This inefficiency is hidden for the lower bit widths that we usually have (<= 8)
but it should be fixed.
at the moment, CO4 is configurable like this
$( runIO $ configurable [ Verbose
, ImportPrelude
-- , DumpAll "/tmp/sl"
-- , Profile
, Cache
]
$ compileFile "CO4/Test/SL.standalone.hs" )
This means I have to know all the options at compile-time.
There should be a way to set some of these options at run-time (Verbose
,Profile
, maybe Cache
)
Simplify import of prelude when this issue is solved.
commit ac8e7ec
this is fine:
ghci CO4/Test/WCB_Matrix.standalone.hs
but this fails:
ghci CO4/Test/WCB_Matrix.hs
CO4/Test/WCB_Matrix.hs:73:8:
Couldn't match type `e0 p0
-> CO4.EncodedAdt.Overlapping.Overlapping
Satchmo.Core.Boolean.Boolean'
with `Satchmo.Core.SAT.Minisat.SAT
(EncodedAdt Satchmo.Core.Boolean.Boolean)'
Expected type: ParamConstraintSystem
Satchmo.Core.SAT.Minisat.SAT Satchmo.Core.Boolean.Boolean
Actual type: CO4.EncodedAdt.Overlapping.Overlapping
Satchmo.Core.Boolean.Boolean
-> CO4.EncodedAdt.Overlapping.Overlapping
Satchmo.Core.Boolean.Boolean
-> e0 p0
-> CO4.EncodedAdt.Overlapping.Overlapping
Satchmo.Core.Boolean.Boolean
In the fourth argument of `solveAndTestBooleanP', namely
`encConstraint'
now ParamConstraintSystem SAT Boolean
expands to
Overlapping Boolean
-> Overlapping Boolean
-> SAT (Overlapping Boolean)
and this looks like encConstraint
somehow got one extra argument (of type e p
)
strange thing is: if I comment out the second clause (after &&
) of
simple s (p, t) =
( geEnergy (bound p s) (get t (leftmostI p) (rightmostI p)) )
&& ( maxboundOk mi zero plus times eqEnergy cost p t )
then it works fine.
the new assertKnown
is great help in debugging.
I found that x == y
is not assertKnown when x and y both are,
but the explicit definition is fine
eqBool x y = case x of
False -> not y
True -> y
CSPLIB ( http://www.csplib.org/ ) contains combinatorial problems that are standard in the constraints community. It would be good to have at least some of them encoded in CO4, to compare encoding (does it look nice?) and performance. (I started in CO4/CSPLIB/ ) One recurring building block seems to be the alldifferent constraint (cf. Issue #44 )
it would be nice to have
data [a] = [] | a : [a]
and some standard operations from the Prelude like (++), concat, reverse, map, foldr, and, or.
commit 064eb31
ghci CO4/Test/SL
example
(RULES a a -> a b a)
[([[False],[False]],[[False],[True],[False]])]
fromList [(b,[True]),(a,[False])]
Start producing CNF
*** Exception: CO4/EncodedAdt.hs:64:5-20: Assertion failed
even with data Bool built-in, there's (probably) a difference between
x && y = case x of { False -> False; True -> y }
and Satchmo.Boolean.&&
Is there indeed? This should be investigated. Perhaps Minisat's simplifier removes the difference already.
the current profiler accumulates costs
(everything "in and under" a function, is attributed to that function).
it would be nice to have, in addition, the cost "in" the function
(without the cost "under" the function).
possible realisation: global variables with the meanings:
and each time where name-of-current-function changes, a new snapshot is taken, and the difference to the previous snapshot is attributed to the previous function.
how to compile and execute with ghc's profiler (commit 60351a6)
ghc -O2 CO4/Test/WCB.hs -main-is mainz -rtsopts
ghc -O2 CO4/Test/WCB.hs -main-is mainz -rtsopts -prof -auto-all -osuf oprof
./CO4/Test/WCB '((...))' +RTS -K1G -M7G -P -h
then look at WCB.prof
COST CENTRE MODULE %time %alloc ticks bytes
solve CO4.Algorithms.Eitherize.Solve 20.0 0.0 1050 125088
emit CO4.Profiling 14.2 22.1 746 392602912
caseOfBits.caseOf2Bits.merge2 CO4.EncodedAdt 10.8 20.3 565 360866736
is this expected?
commit 7ad6117
at present it seems plusNat8 etc. are ingnored for profiling:
constraint s xs =
eqNat8 s ( summe xs )
summe xs = case xs of
[] -> nat8 0
x:xs' -> plusNat8 x (summe xs')
Profiling (inner):
("summe",ProfileData {numCalls = 12, numVariables = 633, numClauses = 1878})
("constraint",ProfileData {numCalls = 1, numVariables = 17, numClauses = 41})
("__init",ProfileData {numCalls = 0, numVariables = 0, numClauses = 0})
this gives the wrong impression that summe
allocates variables. Work-around:
constraint s xs =
eqNat8 s ( summe xs )
summe xs = case xs of
[] -> nat8 0
x:xs' -> plus x (summe xs')
plus = plusNat8
Profiling (inner):
("plus",ProfileData {numCalls = 11, numVariables = 633, numClauses = 1878})
("constraint",ProfileData {numCalls = 1, numVariables = 17, numClauses = 41})
("summe",ProfileData {numCalls = 12, numVariables = 0, numClauses = 0})
("__init",ProfileData {numCalls = 0, numVariables = 0, numClauses = 0})
For optimized memoization we need an ideal (collision-free) hash function, so we can find an item in the cache in one step (and avoid the traversal of the item).
The "easy" (brute force) solution is to memoize constructor calls. To each node, we attach a globally unique Identifier (a number). Then all terms are reduced (as in "reduced BDDs").
by "built-in" I mean: it should be available to the user, not necessarily: it should be treated in a special way by the compiler (only Bool is special).
It is more like reading a module with definitions that the Haskell programmer expects (it should be a subset of the official Haskell Prelude).
Add typed allocators to statically guarantee that an allocator matches an ADT.
as I understand, currently
these decisions are ok for a prototype, but the point of this bug report is that the ordering restriction is not enforced. My suggestion:
Support type synonyms, so we can write:
type Foo = Bar
data Spam = Spam Foo
Possible implementation: expand type synonyms in Template Haskell frontend.
it seems that currently the type ()
is not supported
Example: for termination tools, it is required that stdout contains just the final proof (starting with YES) so everything that happens before, must be silent.
In general, CO4 applications expect to have control over any output.
They want to enable/disable, and also to direct it to some handle.
Or, instead of printing, it could be collected into some structured data type so it can be analysed programmatically later.
it would be nice to be able to declare
data T = C { foo :: T1, bar :: T2 }
and then have
For the sake of testability we should introduce an Example/ directory that includes working examples. New versions of co4 must solve these examples in order to get released.
The existing Test directory should contain drafts and tests that may not work with the latest version of co4.
(mini)zinc is (planned to be) the standard CSP modelling language. We should compare CO4 encodings to minizinc encodings, for standard/interesting/challenging problems. Cf. http://www.minizinc.org/challenge2013/
The programming models are still different: minizinc does have only limited forms of abstraction, and no pattern matching. So we should not directly translate the minizinc encoding, but rewrite to more idiomatic Haskell.
See http://article.gmane.org/gmane.comp.lang.haskell.cafe/106293
Here's a simple way to do it:
but it should of course be done automatically inside compileFile
.
It would be really really helpful to have some data that is never encoded.
An important use case is indices for collections (e.g., lists, maps).
We do want caching for non-encoded data.
For monomorphic Prelude types, we could just take
data Overlapping p = Overlapping p [p] [ Overlapping p ]
| Bottom
| Known_Int Int
but the problem is in
A declarative, efficient, and flexible JavaScript library for building user interfaces.
๐ Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
An Open Source Machine Learning Framework for Everyone
The Web framework for perfectionists with deadlines.
A PHP framework for web artisans
Bring data to life with SVG, Canvas and HTML. ๐๐๐
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
Some thing interesting about web. New door for the world.
A server is a program made to process requests and deliver data to clients.
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
Some thing interesting about visualization, use data art
Some thing interesting about game, make everyone happy.
We are working to build community through open source technology. NB: members must have two-factor auth.
Open source projects and samples from Microsoft.
Google โค๏ธ Open Source for everyone.
Alibaba Open Source for everyone
Data-Driven Documents codes.
China tencent open source team.