Banana changed the topic of #ocaml to: OCaml 3.08.1 available! | Archive of Caml Weekly News: http://sardes.inrialpes.fr/~aschmitt/cwn/ | A tutorial: http://merjis.com/richj/computers/ocaml/tutorial/ | A free book: http://cristal.inria.fr/~remy/cours/appsem/ | Mailing List: http://caml.inria.fr/bin/wilma/caml-list/ | Cookbook: http://pleac.sourceforge.net/
vezenchio has quit ["None of you understand. I'm not locked up in here with you. YOU are locked up in here with ME!"]
melchus has quit ["leaving"]
GreyLensman has quit [Read error: 110 (Connection timed out)]
tewk has joined #ocaml
<mrvn_> pretty quiet here
kinners has joined #ocaml
ianxek has quit ["Leaving"]
<judge> yep
m3ga has joined #ocaml
tautologico has joined #ocaml
avlondono has quit ["leaving"]
monochrom has joined #ocaml
m3ga has left #ocaml []
kinners has quit ["leaving"]
monochrom has quit ["Don't talk to those who talk to themselves."]
tautologico has quit []
mrsolo has quit [Read error: 104 (Connection reset by peer)]
mrsolo has joined #ocaml
mrsolo has quit [Read error: 232 (Connection reset by peer)]
Hipo has quit [Read error: 238 (Connection timed out)]
velco has joined #ocaml
mrsolo has joined #ocaml
velco has quit ["I'm outta here ..."]
ejt has joined #ocaml
ejt has quit [Remote closed the connection]
Submarine has joined #ocaml
Submarine has quit ["ChatZilla 0.8.31 [Mozilla rv:1.4.1/20031114]"]
velco has joined #ocaml
Hipo has joined #ocaml
_JusSx_ has joined #ocaml
_fab has quit []
velco has quit ["I'm outta here ..."]
_fab has joined #ocaml
ianxek has joined #ocaml
Submarine has joined #ocaml
<Submarine> hi there
<Submarine> Would somebody here know the input syntax for zChaff?
GreyLensman has joined #ocaml
mrvn has joined #ocaml
vezenchio has joined #ocaml
mrvn_ has quit [Read error: 110 (Connection timed out)]
velco has joined #ocaml
Submarine has quit ["ChatZilla 0.8.31 [Mozilla rv:1.4.1/20031114]"]
karryall_ has joined #ocaml
karryall has quit [Read error: 104 (Connection reset by peer)]
Submarine has joined #ocaml
<Submarine> hi there
<Submarine> what would one advise for conversion of arbitrary logical formulas to SAT?
velco has quit ["I'm outta here ..."]
menace has joined #ocaml
<Smerdyakov> Submarine, what logica are the inputs expressed in?
<Submarine> Smerdyakov, let us say propositional logic with /\, \/, negation, equality
<Submarine> the idea would be to compile programming constructs into propositional logic
<Smerdyakov> I mean the original inputs. The ones you want to "convert to sat."
<Submarine> propositional logic with /\, \/, negation, equality
<Smerdyakov> That's already in the input format of SAT....
<Submarine> chaff needs some CNF input
<Submarine> I have misexplained myself.
<Submarine> I have a propositional logic formula and want to see if it's satisfiable.
<Submarine> Most SAT solvers take CNF input.
<Smerdyakov> For that, look at any book on theory of computation.
<Submarine> so it's a 3-step process: program to propositional formulas (I'll handle this), then formulas to CNF
<Submarine> er...
<Submarine> I'm not asking for an actual algorithm (I can do it).
<Submarine> i'm asking for an efficient implementation :-)
<Smerdyakov> What could be more efficient than theory? These guys do so little work and they still get tenured!
<Smerdyakov> The procedures for conversation to 3-CNF tend to be linear time, right? Is your application hard realtime theorem proving? :D
<Submarine> exponential time you mean
<Submarine> no it's not realtime
<Smerdyakov> No, linear time.
<Smerdyakov> I do truly believe that any procedure found in a book on theory of computation will be fast enough for you.
<Smerdyakov> I just don't remember the details of one.
<Submarine> mmmh
<Submarine> "What would you suggest as a C compiler?" - "Take the Dragon Book and Appel's book, and the ISO norm."
<Smerdyakov> Ridiculous analysis. This is a trivial problem.
<Smerdyakov> Half a page of ML code.
<Submarine> However, in some cases conversion to CNF can lead to an exponential explosion of the formula.
<Smerdyakov> Hm. I may have confused this with CNF -> 3CNF. :)
<GreyLensman> I think I know of one in C. Give me a moment to think where I saw it / have it.
<Submarine> Of course, I can code SAT to CNF quite fast... but 1/ will it give small formulas as output on reasonable inputs 2/ will it not trash memory?
<Submarine> I mean, if you consider the problem of converting a convex polyhedron between representations, there can be a 20x blowup from a smart to a naive implementation.
* Submarine won't make a comment about tenured people who allegedly don't work
<Smerdyakov> Why? You're afraid of reprisals from their union?
<Submarine> union?
<GreyLensman> I believe there is a utility called COMPILE associated with this book. Its been a LONG time. But I think its what you are looking for. Sorry don't have more info.http://www.compman.co.uk/htmlcat/0387950753_Automated_Theorem_Proving.asp
<Submarine> thank you very much
avlondono has joined #ocaml
deknos has joined #ocaml
GreyLensman has quit ["Leaving"]
menace has quit [Connection timed out]
deknos is now known as menace
mrsolo has quit [Read error: 110 (Connection timed out)]
Excedrin has quit [Read error: 238 (Connection timed out)]
pango has quit [Nick collision from services.]
pango_ has joined #ocaml
Submarine has quit ["ChatZilla 0.8.31 [Mozilla rv:1.4.1/20031114]"]
GreyLensman has joined #ocaml
menace has quit [" WOW! This IRC Client ownz! HydraIRC -> http://www.hydrairc.com <-"]
Kevin_ has joined #ocaml
drz has joined #ocaml
<drz> is there a function ('a -> unit)? (so I can ignore the result of Unix.write)
<Kevin_> yep : val ignore 'a -> unit
<drz> thanks :-)
<Smerdyakov> Ignoring the result of Unix.write is a bad idea.
<Smerdyakov> It's not guaranteed to write your whole message. The return value tells you how much was written.
<drz> smerd: I know, but I'm just trying to get things to work for now.
<Kevin_> Some time user have extra information of why is program crash or not...
<pango_> partial writes aren't an error condition
<Smerdyakov> Hm, actually, the man page says that the OCaml version keeps trying until the whole thing is written or an error occurs. It's fishy that the return value doesn't show you _which_ error occurred, though.
<Smerdyakov> If errors are indicated by exceptions, then the return value is useless.
<mflux> but other endpoint exiting isn't an error?
<mflux> which would return 0 from the write
<Kevin_> Only the final user can decide if it is an error or not.
<pango_> partial write can happen because the syscall was interrupted, nothing /wrong/ happened, the app just has to try again
<pango_> or rather, has to go on
<Kevin_> The new function "single_write" look interresting int his context.
<pango_> looking at the code, the only value Unix.write can return is len...
<Kevin_> IMHO when a syscall is interrupted the final user know that there is a problem on is PC :-)
<pango_> Kevin_: no
<pango_> Kevin_: again, it's not an error condition, it can happen in normal conditions
<pango_> Kevin_: when it can happen is implementation dependant, through
<mflux> kevin_, let's say you've requested writing 10 megabytes to a 9600 bps serial link and user presses ctrl-c.. wait until the 10 megabytes are written or stop?-)
<drz> I believe that if you suspend your an in-progerss syscall will get interrupted
<drz> your program
<Kevin_> mflux: I think it stop, no ?
<drz> anyway, gotta run
<mflux> kevin_, well, I haven't tried but I would heavily suspect in that case the serial driver would bail out from the write and return partial write
<Kevin_> yep, but we don't care because, user stop the program.
<pango_> Kevin_: SIGTERM doesn't end programs, that depends what the signal handled chooses to do
<pango_> s/handled/handler/
<pango_> http://www.jwz.org/doc/worse-is-better.html starting from "Two famous people..."
<Kevin_> I juste speak for simple case ...
<pango_> Kevin_: you pick a specific case to put the question under a carped
<pango_> s/carped/carpet/ (damn, I'm tired)
<Kevin_> Sorry I don't understand.
<pango_> Kevin_: more things are up to the application that what you think
<pango_> s/that/than/ (maybe I should stop now ;) )
velco has joined #ocaml
avlondono has quit [Read error: 104 (Connection reset by peer)]
* Kevin_ is away: Away
lus|wazz has joined #ocaml
vezenchio has quit [Read error: 110 (Connection timed out)]
mrsolo has joined #ocaml
Excedrin has joined #ocaml
lodewijk has joined #ocaml
lodewijk has quit []
ml has joined #ocaml
ml has left #ocaml []
GreyLensman has quit ["Leaving"]
Kevin_ has quit ["Quit"]
monochrom has joined #ocaml
cjohnson has joined #ocaml
velco has quit ["I'm outta here ..."]
kinners has joined #ocaml
nrb23 has joined #ocaml
<nrb23> hello
<nrb23> does anyone know where I can find more information about the type-inference algorithm used by OCaml?
<drz> what's the best way to append a character to a mutable string? String.concat and just make a new one?
<pango_> drz: string's lengths aren't mutable
<pango_> nrb23: google for "Hindley-Milner"
<drz> pango: OK, so what's the best way to make a new string out of a string and a character? String.concat is the only thing I found, but it seems like overkill.
<drz> pango: Not like I really care about performance, but I'm trying to learn the language.
<mrvn> drz: If you need that a few times better use a Buffer.t
<pango_> drz: what about using a Buffer instead ?
<mrvn> Otherwise let s = s^(String.create 1 c) in
<mrvn> or similar.
<pango_> let add_char s c = let l = String.length s in let s2 = S
<pango_> tring.create (l+1) in String.blit s 0 s2 0 l; s2.[l] <- c; s2
<nrb23> pango_: thankks
<pango_> etc.
<drz> mrvn,pango: OK, thanks. Somehow I missed the ^ operator
CosmicRay has joined #ocaml
cjohnson has quit [Read error: 60 (Operation timed out)]
tautologico has joined #ocaml
<tautologico> anyone using tuareg-mode on windows ?
_JusSx_ has quit ["[BX] Reserve your copy of BitchX-1.1-final for the PalmPilot today!"]
mrvn_ has joined #ocaml
goomba has joined #ocaml
mrvn has quit [Read error: 110 (Connection timed out)]
menace has joined #ocaml
cjohnson has joined #ocaml