-
Notifications
You must be signed in to change notification settings - Fork 11
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
cabal install toysolver #60
Comments
Thanks for trying the software and reporting the issue. |
It was indeed the problem of |
Hi, $> cabal install toysolver I forgot to install zlib on ubuntu. $>sudo apt install zlib1g-dev I've tested .lp works now but opb not. ./toyconvert Sudoku.lp -o Sudoku.opb .toysat the same "endOfInput" error. |
This is caused by an empty objective function As a workaround, please remove the |
I released |
Hi Masahiro,
very appreciate that you fixed that. I'm trying to evaluate different
encodings of PB constraints into SAT. Would you be able to help with
another issue with PYPBLIB? rjungbeck/pypblib#1
It's library in python but nobody is maintaining that project I guess and
there should be all encodings available according to documentation.
Thank you
Best regards
Vlasta
st 12. 5. 2021 v 2:21 odesílatel Masahiro Sakai ***@***.***>
napsal:
… I released pseudo-boolean-0.1.10.0 which allow parsing min: ; (and other
occurrences of empty <sum >expression) although it does not conform to
the OPB file grammar define in
http://www.cril.univ-artois.fr/PB11/format.pdf .
—
You are receiving this because you authored the thread.
Reply to this email directly, view it on GitHub
<#60 (comment)>,
or unsubscribe
<https://github.com/notifications/unsubscribe-auth/ANIOX3RMMBIUPD6WNHIBZX3TNHCZBANCNFSM44FVYKTA>
.
|
~/$ cabal install toysolver
~/$ wget https://raw.githubusercontent.com/msakai/toysolver/master/samples/lp/Sudoku.lp
~/.cabal/bin/$ ./toysolver --lp Sudoku.lp
Segmentation fault (core dumped)
basically reading lp file won't work in toysat toysolver or toyconvert
./toysolver --sat aaa.cnf works
./toysat aaa.cnf works
~/.cabal/bin/$ ls -l
lrwxrwxrwx 1 ubuntu ubuntu 114 May 5 19:46 toyconvert -> ../store/ghc-8.8.4/toysolver-0.7.0-a2dd48b3ce6143ea169cfa73d74179abe5e7eeb05444e8361f8dc9863f6bf7c0/bin/toyconvert*
lrwxrwxrwx 1 ubuntu ubuntu 110 May 5 19:46 toyqbf -> ../store/ghc-8.8.4/toysolver-0.7.0-0e1deeee83edf2aa18bd4d7bf0ba4bc82d151ea40cbf44f0f5a25fdf2be1f160/bin/toyqbf*
lrwxrwxrwx 1 ubuntu ubuntu 110 May 5 19:46 toysat -> ../store/ghc-8.8.4/toysolver-0.7.0-82239a3f18744616363cb674ac3ededa4ccfa32e6a5d40a519eaafd95156fd0c/bin/toysat*
lrwxrwxrwx 1 ubuntu ubuntu 110 May 5 19:46 toysmt -> ../store/ghc-8.8.4/toysolver-0.7.0-b4ed3ad055453675c3f24f0a301dc551aa7ff1e1e8bd5e2dc91046bc301d6a84/bin/toysmt*
lrwxrwxrwx 1 ubuntu ubuntu 113 May 5 19:46 toysolver -> ../store/ghc-8.8.4/toysolver-0.7.0-dd1e9520e775b36ced274a980f682220c66a9125c74d89e3e0ef301d9f86a5e4/bin/toysolver*
The text was updated successfully, but these errors were encountered: