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?
<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_>
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)]