search

LeventErkok / sbv

SMT Based Verification in Haskell. Express properties about Haskell programs and automatically prove them using SMT solvers.
https://github.com/LeventErkok/sbv
Other
240 stars 33 forks source link

Axioms for uninterpreted functions cross language boundaries #64

Closed TomMD closed 11 years ago

TomMD commented 11 years ago

Borrowing from one of the examples, axioms require the user to enter "raw" SMT-lib strings to be passed through SBV:

ax2 :: [String]
ax2 = [ "(assert (forall ((p B) (q B))"
      , "   (= (NOT (OR p q))"
      , "      (AND (NOT p) (NOT q)))))"
      ]

It would be convenient if we could reuse some of the SBV grammar and symbols:

addAxiom ::  Axiom -> Symbolic ()
ax2 :: Axiom
ax2 = forall2_ $ \p q -> (bnot $ p ||| q) === (bnot p &&& bnot q)

Or perhaps build on Iavor's SMTlib ADT (pseudo code follows, not based on SMTlib at all):

addAxiom :: Axiom -> Symbolic ()
ax2 :: Axiom
ax2 = toAxiom $ Forall "p" "q" $ Eq (Not (Or "p" "q")) (And (Not "p") (Not "q"))

I note the SBV source already agrees some cleaner interface would be beneficial, saying "A separate formalization of SMT-Lib would be very useful here." wrt addAxiom.

LeventErkok commented 11 years ago

Yeah, this is a nuisance indeed. I tried to do something along the lines you suggested before, but it just didn't work out: You almost end-up adding a whole new layer of constructs, which just complicates things. Also, the SMT-Lib axiom syntax is fairly rich; with quantifiers, patterns for e-matching etc.; so it's not quite clear what precisely one should support.

I'll ponder this a bit more; but I'm not sure if there's a good design out there that's both cheap-to-implement, and has considerable ROI. The reason is that SMT solvers typically choke in the presence of quantified axioms: They hardly can make effective use of them; at least for the time being. Z3 has a notion of "tactics" that can help in this regard; but then we'd have to build a way in SBV to specify those tactics as well; adding to the complexity.

I'll leave this ticket open in case someone else chimes in with an idea; but given the state of affairs it's really really low ROI to pursue this any further. If your use case really involves serious axiomatic reasoning, then an SMT solver is probably not the right tool to use to start with. (A better choice would be to use automated theorem proving with SMT solver tactics; like our earlier work on Yices-Isabelle connection: http://corp.galois.com/isabelle-ismt/; or any of the new SMT tactics that pretty much come with every theorem prover out there these days.)

LeventErkok commented 11 years ago

Pondering this a bit more, it's really a can-of-worms with no clear ROI. Maybe we can revisit once SMT solvers and SBV really start ruling the world.. :-) More seriously, if there comes a time when there's really a huge demand and obvious gains to be had from it. For the time being, the restructuring that would be needed to support this properly seems to be way too costly, given the state of affairs for axiomatic reasoning support in existing SMT solvers.