yav / simple-smt Goto Github PK
View Code? Open in Web Editor NEWLicense: BSD 3-Clause "New" or "Revised" License
License: BSD 3-Clause "New" or "Revised" License
ghc examples/ex1.hs SimpleSMT.hs
...
examples/ex1.hs:5:11: error:
• Couldn't match expected type: IO Logger
with actual type: Int -> IO Logger
• Probable cause: ‘newLogger’ is applied to too few arguments
In a stmt of a 'do' block: l <- newLogger
I think newLogger
was extended with an argument, but the example was not updated.
The trivial fix is
main =
- do l <- newLogger
+ do l <- newLogger 0
s <- newSolver "cvc4" ["--lang=smt2"] (Just l)
I can do it. Perhaps it should be part of a test suite. But this would probably require that some SMT solver is present. cvc4
is superseeded by cvc5
, and for that, we can simply write
s <- newSolver "cvc5" [] (Just l)
(we don't need the option).
well, it's an edge case, but here goes:
[send->] (get-value (v15))
[<-recv] ((v15 0.0)) -- fine, has decimal point
[send->] (get-value (0.0))
[<-recv] ((0.0 0)) -- not fine
this sometimes happens in my application (some expressions might have been simplified but I do not keep track of it)
cvc5
sends back 0.0
.
It's a bit hard to fix in simple-smt, since getExprs
is not typed. I can fix it in my application https://gitlab.imn.htwk-leipzig.de/waldmann/pure-matchbox/-/commit/a9dd4017030d7992132de745708ebfb2cabd51fb because I have typed expressions there.
I propose to
newLogger :: Int -> IO Logger -- keep the type
newLogger = newLoggerH stdout -- refactor implementation
newLoggerH :: Handle -> Int -> IO Logger -- new function
newLoggerH h l = -- old implementation, with stdout replaced by h
do tab <- newIORef 0
...
(I was originally typing this as a comment on #13 but it's really about getResponse
)
When I terminate
a running solver, I am seeing "Missing response from solver"
errors frequently - in the thread that's blocked on getResponse
.
Well, that's life (there is no value that getResponse
could return) but perhaps life can be made easier by using a different exception - instead of plain fail
(from instance MonadFail IO
, so it's failIO
and it raises mkUserError _
)
In my application code, I'd like to ignore that specific exception, but I want to see all others (because they might indicate problems).
With cvc5, I get this
[send->] (assert (<= (- 1.0) (+ (* (- 1.0) x0))))
[<-recv] (error "Parse Error: <stdin>:85.38: Invalid kind 'ADD', expected Terms with kind ADD must have at least 2 children and at most 67108863 children (the one under construction has 1) ")
In Z3's API there is a function Z3_eval_smtlib2_string
which can be used to interact with Z3 using SMTLib2 commands. Using such a binding is noticeably faster than launching Z3 as an external process and communicating with it through pipes.
I'm thus considering extending simple-smt to support using specific solvers that have this kind of bindings in their API. I'm thinking of something like having a
class Solver a where
init :: IO a
command :: a -> SExpr -> IO SExpr
stop :: a -> IO ExitCode
with a generic instance Solver ExternalProcess
for running solvers as external processes and then some more specific ones such as instance Solver Z3
for using solvers through their SMTLib2-parsing bindings.
If I were to make such a PR here, would it be accepted and actively maintained in the future ? Or I am better off forking this project ?
current implementation has just one branch that builds a Real
sexprToVal :: SExpr -> Value
sexprToVal expr =
case expr of
...
List [ Atom "/", x, y ]
| Int a <- sexprToVal x
, Int b <- sexprToVal y -> Real (a % b)
but solvers also produce other forms: z3 sends
[send->] (get-value (x0))
[<-recv] ((x0 (- (/ 1.0 18000.0))))
[send->] (get-value (x1))
[<-recv] ((x1 0.0))
I added a test case (in my fork)
21571e9
I am starting two solvers concurrently. When one returns with a result, I want to kill the other. Ideally, the following should work
main = do
as <- mapM async
[ main_with "yices-smt2" [ "--smt2-model-format" ]
, main_with "cvc5" []
]
(a,r) <- waitAnyCancel as
print r
main_with :: String -> [String] -> IO [(SExpr,Value)]
main_with solver opts = do
l <- newLogger 0
s <- newSolver solver opts (Just l)
...
print =<< check s
getExprs s [a,b,c,d]
but it does not. yices finds a solution, the program stops, but cvc5 keeps running.
I have this constraint
x <- declare s "x" tReal
assert s (mul (real 3) (add x (real 2)) `eq` real (negate 5))
communicating with cvc5 gives
[send->] (assert (= (* 3.0 (+ x 2.0)) -5.0))
[<-recv] (error "Parse Error: <stdin>:4.33: Symbol -5.0 is not declared. (assert (= (* 3.0 (+ x 2.0)) -5.0)) ^ ")
ex3: user error (Unexpected result from the SMT solver:
Expected: success
Result: (error "Parse Error: <stdin>:4.33: Symbol -5.0 is not declared. (assert (= (* 3.0 (+ x 2.0)) -5.0)) ^ ")
)
I guess they want (- 5.0)
instead of -5.0
.
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.