Re: [Haskell-cafe] Installing Z3 on OS X 10.8.4 ( Off topic )
SBV should be able to pick up Z3 from your path; make sure the "z3" executable is in it and you can invoke it from your shell. Alternatively, you can use the SBV_Z3 environment variable to point to the executable itself, if adding it to your path is not desirable for whatever reason. Let me know if you still have issues. -Levent. On Mon, Jul 1, 2013 at 5:34 AM, Johannes Waldmann < waldm...@imn.htwk-leipzig.de> wrote: > > Unable to locate executable for z3 > > well, do you really have z3 in the $PATH? > what does 'which z3' answer? > > I used this for installation of z3: > python scripts/mk_make.py --prefix=/usr/local > > and note that the install script says: > > Z3 shared libraries were installed at /usr/local/lib, make sure this > directory is in your LD_LIBRARY_PATH environment variable. > > - J.W. > > > > ___ > Haskell-Cafe mailing list > Haskell-Cafe@haskell.org > http://www.haskell.org/mailman/listinfo/haskell-cafe > ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Formal Methods/Functional programming job position at Intel
Our formal methods team at Intel has a full-time position available that I think would be a good fit for functional programming and formal methods enthusiasts. I'm including the description below. Do not hesitate to contact me if you've any questions, or just want to talk about it in general. To apply for the position, please visit: http://www.intel.com/jobs/jobsearch/index.htm, and in the "advanced search" area enter the job number: 709631. Thanks, -Levent. Job Description *Formal Methods & Validation Architect* *-* *709631* Description If you're interested in products going into future super computer markets then the Intel® Many Integrated Core (Intel® MIC) Hardware Engineering Group is the place for you! We design and validate silicon chips with many Intel cores integrated inside being used in high performance computing architectures. In this position you will work as part of the pre-silicon formal methods, tools, and verification team to support a continued high quality of the future Intel many core processor products. You will work together with Intel's formal verification and validation community, the Formal Verification Center of Expertise (FV CoE) in a team of experts in formal methods and AV Validation. Your specific responsibilities will include defining formal verification (FV) test plans as well as Cluster Test Environment (CTE) based test plans for dynamic simulation validation (DV). The goal is to help optimize a combined use of FV and CTE based validation techniques (DV) and contribute to an increasing use of formal methods at Intel. Based on the test plans you will write properties in formal language, and prove the properties using our model checkers and theorem proving tools. You will also write CTE based test cases and coverage plans. Your area of strength may currently lie within either FV or DV with strong skills rooted in software development. But through your skills and work, you will become an expert in both formal methods and validation technologies. You will interact very closely with design teams, and other validation teams, as well as with Intel's internal R&D groups that continue to improve and develop formal method and verification tools. You must be able to communicate effectively with various technical groups and coordinate activities amongst those groups. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] NaN as Integer value
For better or worse; IEEE-754 settled many of these questions. I personally think the standard is a good compromise of what's practical, efficiently implementable, and mathematically sensible. I find the following paper by Rummer and Wahl an especially good read: http://www.ccs.neu.edu/home/wahl/Publications/rw10.pdf The paper focuses on how to formalize floating-point in SMT-solvers; but section 3 is a great read for understanding how floating-point semantics work, regardless whether you care for SMT-solving or not. It could be the basis for a nice software implementation of floating-point, for instance. -Levent. On Wed, Apr 17, 2013 at 10:11 AM, wren ng thornton wrote: > On 4/14/13 8:53 PM, Kim-Ee Yeoh wrote: > > On Sun, Apr 14, 2013 at 3:28 PM, wren ng thornton > wrote: > >> Whereas the problematic > >> values due to infinities are overspecified, so no matter which answer > you > >> pick it's guaranteed to be the wrong answer half the time. > >> > >> Part of this whole problem comes from the fact that floats *do* decide > to > >> give a meaning to 1/0 (namely Infinity). > > > > I'm not sure what you mean about overspecification here, but in > > setting 1/0 as +infinity (as opposed to -infinity), there's an easily > > overlooked assumption that the limit is obtained "from above" as > > opposed to "from below." > > Setting 1/0 = +inf isn't the problem, or at least not the main one. Of > course, there's always the question about which completion of the reals to > use--- i.e., whether we have +inf vs -inf, or whether we just have a > single point infinity. > > Rather, the NaN problem comes from trying to resolve things like: > > inf - inf > inf * 0 > inf / inf > 0 / 0 > > The overspecification problem I mentioned is that each of these > expressions has "too many" solutions. For example, we have the following > equations: > > x * 0 == 0 -- where x is finite > inf * y == inf * signum y -- where y /= 0 > inf * 0 == ?? > > x - inf == -inf -- where x is finite > inf - y == inf -- where y is finite > inf - inf == ?? > > x / 0 == inf * signum x -- where x /= 0 > 0 / y == 0 -- where y /= 0 > 0 / 0 == ?? > > -- > Live well, > ~wren > > > ___ > Haskell-Cafe mailing list > Haskell-Cafe@haskell.org > http://www.haskell.org/mailman/listinfo/haskell-cafe > ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] [Announcement] Sparse matrix Conjugate Gradient Solver
I'm happy to announce the first release of conjugateGradient, implementing the Conjugate Gradient algorithm for solving linear systems of equations over sparse matrices: http://hackage.haskell.org/package/conjugateGradient The conjugate gradient algorithm only applies to the cases when the input matrix is symmetric and positive definite. See: http://en.wikipedia.org/wiki/Conjugate_gradient_method The advantage of this method is that it can handle really large sparse systems quite well, when other direct methods (such as LU decomposition) are just not practical due to algorithmic complexity. Such large and sparse systems naturally arise in engineering applications, such as in ASIC placement algorithms and when solving partial differential equations. Bug reports, feedback, and improvements are always welcome. -Levent. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] abs on Float/Doubles
It was pointed out to me that the precise issue came up before in the libraries list in January 2011 as well: http://www.haskell.org/pipermail/libraries/2011-January/015761.html >From the archives; it appears that proposal didn't generate much discussion either. I think everyone is agreed on the currently non-compliant behavior should be changed, but there just isn't enough number of people who care about it to make it actually happen. I'll follow up on the libraries list to freshen-up that proposal; if interested please post there. Thanks, -Levent. On Sun, Apr 7, 2013 at 5:11 PM, Richard A. O'Keefe wrote: > > On 8/04/2013, at 11:21 AM, Levent Erkok wrote: > > It appears that the consensus is that this is a historical definition > dating back to the times when IEEE754 itself wasn't quite clear on the > topic itself, and "so nobody thought that hard about negative zeroes." (The > quote is from a comment from Lennart.) > > I would expect abs(f) to be identical to copysign(f, 1.0). > > > ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] abs on Float/Doubles
Hello all, I definitely do not want to create a yet another thread on handling of floating-point values in Haskell. My intention is only to see what can be done to make it more "compilant" with IEEE754. (Also, my interest is not a theoretical one, but rather entirely practical: I'm interested in using SMT solvers for reasoning about Haskell programs, in particular using the new SMT logics that cover IEEE-754 semantics. So, any discrepancy between Haskell and IEEE-754 is a cause for concern as we strive to build powerful tools around the Haskell eco-system.) In IEEE-754, there are two zero values: +0, and -0; inhabiting all floating point types. IEEE-754 requires these two compare equal, but be distinguished when used as arguments to functions as they can produce different results. (Unfortunately the standard is not freely available, but there's a nice discussion in wikipedia: http://en.wikipedia.org/wiki/Negative_zero.) As far as I know, Haskell's floating-point handling does *not* explicitly claim to be IEEE-754 compliant, but I think it's safe to assume that any serious implementation will take advantage of the underlying CPU's floating-point facilities; and thus will use IEEE-754 semantics. In particular, Haskell supports both +0 and -0; and you can distinguish them using the isNegativeZero function of the RealFloat class. Furthermore, the show instance for Float/Double will turn these two values to strings differently, preserving the minus sign if it receives a negative-zero. Comparisons follow the IEEE rules; so all these behaviors seem to be in accordance with IEEE754. Unfortunately, the same isn't true for the abs function. In Haskell, the call: "isNegativeZero (abs (-0::Double))" evaluates to "True". IEEE754 requires abs to always return "+0" in this case. The same also holds for the semantics of the newly proposed SMT-Lib logic for IEEE754: See section 3.3.1 (page 8) of: http://www.philipp.ruemmer.org/publications/smt-fpa.pdf The fix is easy. A one line change in the Double/Float instances of the Num class in the Prelude would guarantee the IEEE754 semantics. The reason I'm not simply posting this as a "library" issue is that it appears the topic came up in stack-overflow a while ago; without any clear resolution: http://stackoverflow.com/questions/10395761/absolute-value-of-negative-zero-bug-or-a-part-of-the-floating-point-standard It appears that the consensus is that this is a historical definition dating back to the times when IEEE754 itself wasn't quite clear on the topic itself, and "so nobody thought that hard about negative zeroes." (The quote is from a comment from Lennart.) I think it's a safe bet to assume IEEE754 semantics (for better or worse) is here to stay, and it would be nice to reduce any discrepancy we have in the Haskell libraries with respect to it. So, if there's consensus, I'd like to propose a library change to implement the proper IEEE754 semantics for the abs function for Double and Float types. Note that the argument is not really about semantics here, but rather with compliance to the accepted industrial standard. So, it would be best if we kept the discussion purely to the IEEE-compliance here, as opposed to relative merits of the semantics as defined. -Levent. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Functional Programming Internship @ Intel
[I'm posting on behalf of my colleague Jesse Bingham. While Jesse and I work for different groups at Intel, we collaborate quite often, and I do expect to work with the intern to an extent as well. To that end, I'm happy to answer any questions you might have. Otherwise, direct all correspondence to Jesse as indicated below. -Levent.] = Hi, we are looking to hire an intern to fill the below position. If interested, please send your resume to jesse.d.bing...@intel.com. Thanks Intern SW Engr. Formal Verification - 708053 Description Design and Technology Solutions (DTS) creates the software that caters to Intel's insatiable appetite for innovating silicon technology. Through our CAD solutions and engineering services, we enable Intel's process engineers to achieve the technical breakthroughs required to deliver tomorrows technology, and we help Intel's architects and chip designers develop products that change the world. To us, Moore's law is the imperative that drives our work to continuously improve the ways we explore technology options, so we can deliver better products, faster. As a software engineer in DTS, you will work as part of a multi-disciplinary team to create software tools that meet Intel's specific, rapidly evolving requirements for designing, manufacturing, testing, and packaging silicon products. We work very closely with process engineers and chip designers (our internal customers) around the world, to understand their technical challenges, and to create proprietary CAD solutions. We help them apply our software to answer critical questions, and to address their design and manufacturing objectives. The daily work in DTS spans the complete software life cycle, from early research to mature production code with industrial robustness and quality. To deliver critical new features in our established solutions, or to create new CAD capabilities beyond the state of art in the industry, our teams frequently go through all steps in software development - problem analysis, requirements definition, design, coding, test, and deployment. As a member of our team, you are expected to participate actively in all these steps. Success in this fast-paced, results-oriented environment requires strong analytical skills and the ability to perform productive teamwork, which depends on very good communication skills. In this particular job opening, you will join DTS's Formal Verification Center of Expertise (FVCoE) for a three month placement in Hillsboro, Oregon, in the timeframe of fall 2013. A primary responsibility of FVCoE is the maintenance of a large code base used for formal verification of Intel's core datapath designs; you will help rework several key aspects of this code to make it more robust and user-friendly. This will involve strict software engineering discipline to deliver robust, quality code that must perform reliably and predictably, The code is written in an in-house functional language called reflect. Reflect is similar to the popular functional languages Ocaml and Haskell; hence you should have considerable experience with one of these. Experience with formal verification is preferred but not necessarily required. Applicants will ideally be working towards a graduate degree in Computer Science or a related discipline. Qualifications Minimum Requirements Skills: Functional programming coding skills; experience with one or more scripting languages; analytical skills for problem abstraction; broad theoretical knowledge in computer science, including algorithms and data structures; familiarity with standard software engineering practices. Experience: acquired through coursework, internships, or personal projects. Experience in applied computer programming in a functional language. Education: working toward an MS or Ph.D. degree in Computer Science, Applied Mathematics, or in an Engineering field related to silicon technology. Strong senior undergraduates will also be considered. Preferred Requirements Skills: Familiarity with: hardware formal verification techniques (especially symbolic simulation, binary decision diagrams, parametric substitutions, case splitting), arithmetic/floating point computer hardware designs, IEEE 754 floating point standard, Intel x86 instruction set. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Haskell SBV Package with Z3
Jun Jie: A SymArray is an abstraction of an array that can contain symbolic values, as well as being indexed by a symbolic value. I'm not sure how the example you picked relates. There's a sample program in the SBV distribution that shows how to use SymArray's, maybe looking at that might help: http://hackage.haskell.org/packages/archive/sbv/2.10/doc/html/Data-SBV-Examples-Uninterpreted-AUF.html Feel free to e-mail me privately for further questions on SBV; the mailing list might not be quite appropriate for detailed discussions. -Levent. On Sun, Mar 31, 2013 at 7:12 AM, J. J. W. wrote: > Dear L. Erkok, > > First I would like to wish you happy easter and I would like to thank you > for your help. > > I have a couple of more questions. I am now playing with SBV package, > however I am not sure if I understand the use of arrays, maybe you can give > me some pointers. For example I want to prove the following (note: this > example is only used to illustrate my question, I thought I've read > somewhere in Haddock that this method only support functions with 7 > parameters?) > > prove $ \(a :: SWord8) b c -> a .> b &&& b .> c ==> a .> c > Q.E.D. > > how should I express this using SymArray? > > Thanks in advance! > > Yours sincerely, > > Jun Jie > > > 2013/3/29 Levent Erkok > >> Sorry, there were a couple of typos in the last example. It should read: >> >> allSat $ \(x::SWord8) -> x `shiftL` 2 ./= x >> >> Note that this will return all 255 values that satisfy this property; >> i.e., everything except 0. (Here, we're using "sat/allSat" as opposed to >> "prove," and hence the inversion of equality in the property.) >> >> -Levent. >> >> >> On Fri, Mar 29, 2013 at 6:49 AM, Levent Erkok wrote: >> >>> You're welcome Jun Jie. >>> >>> Regarding getting a different counter example: That's perfectly normal. >>> When SMT solvers build models they use random seeds. Furthermore, different >>> versions of the same solver can use different algorithms/heuristics to >>> arrive at the falsifying model. So, it's entirely expected that you get a >>> different counter-example. You can turn the question around, and ask the >>> solver to give you all counter-examples like this: >>> >>> allSat $ \x -> \(x::SWord8) -> x `shiftL` 2 .!= x >>> >>> -Levent. >>> >>> On Mar 29, 2013, at 1:42 AM, "J. J. W." wrote: >>> >>> Dear Levent, >>> >>> Thank you for your support. I am very honoured to have the developer of >>> the SBV package to solve my elementary problem. I noticed that the >>> counter-example given by my Z3 differs from the one said on HackageDB: >>> sbv-2.10. >>> >>> Code that is on Hackage: >>> >>> Prelude Data.SBV> prove $ forAll ["x"] $ \(x::SWord8) -> x `shiftL` 2 >>> .== x >>>Falsifiable. Counter-example: >>> x = 128 :: SWord8 >>> >>> My current GHCi output: >>> >>> Prelude Data.SBV> prove $ forAll ["x"] $ \(x::SWord8) -> x `shiftL` 2 >>> .== x >>> Falsifiable. Counter-example: >>> x = 51 :: SWord8 >>> (0.02 secs, 1196468 bytes) >>> >>> Thank you for your help! >>> >>> Yours sincerely, >>> >>> Jun Jie >>> >>> >>> 2013/3/29 Levent Erkok >>> >>>> Hi Jun Jie: >>>> >>>> SBV uses some of the not-yet-officially-released features in Z3. The >>>> version you have, while it's the latest official Z3 release, will not work. >>>> >>>> To resolve, you need to install the "development" version of Z3 >>>> (something that is at least 4.3.2 or better). Here're instructions from the >>>> Microsoft folks explaining how to get these builds: >>>> http://research.microsoft.com/en-us/um/people/leonardo/blog/2013/02/15/precompiled.html >>>> >>>> Let me know if you find any issues after you get the latest-development >>>> version of Z3 installed. >>>> >>>> -Levent. >>>> >>>> >>>> On Thu, Mar 28, 2013 at 10:22 PM, J. J. W. wrote: >>>> >>>>> Dear all, >>>>> >>>>> I have a small question regarding the installation of the SBV package. >>>>> I first installed the SBV 2.10 package with cabal with the following >>&
Re: [Haskell-cafe] Haskell SBV Package with Z3
Sorry, there were a couple of typos in the last example. It should read: allSat $ \(x::SWord8) -> x `shiftL` 2 ./= x Note that this will return all 255 values that satisfy this property; i.e., everything except 0. (Here, we're using "sat/allSat" as opposed to "prove," and hence the inversion of equality in the property.) -Levent. On Fri, Mar 29, 2013 at 6:49 AM, Levent Erkok wrote: > You're welcome Jun Jie. > > Regarding getting a different counter example: That's perfectly normal. > When SMT solvers build models they use random seeds. Furthermore, different > versions of the same solver can use different algorithms/heuristics to > arrive at the falsifying model. So, it's entirely expected that you get a > different counter-example. You can turn the question around, and ask the > solver to give you all counter-examples like this: > > allSat $ \x -> \(x::SWord8) -> x `shiftL` 2 .!= x > > -Levent. > > On Mar 29, 2013, at 1:42 AM, "J. J. W." wrote: > > Dear Levent, > > Thank you for your support. I am very honoured to have the developer of > the SBV package to solve my elementary problem. I noticed that the > counter-example given by my Z3 differs from the one said on HackageDB: > sbv-2.10. > > Code that is on Hackage: > > Prelude Data.SBV> prove $ forAll ["x"] $ \(x::SWord8) -> x `shiftL` 2 .== > x >Falsifiable. Counter-example: > x = 128 :: SWord8 > > My current GHCi output: > > Prelude Data.SBV> prove $ forAll ["x"] $ \(x::SWord8) -> x `shiftL` 2 .== x > Falsifiable. Counter-example: > x = 51 :: SWord8 > (0.02 secs, 1196468 bytes) > > Thank you for your help! > > Yours sincerely, > > Jun Jie > > > 2013/3/29 Levent Erkok > >> Hi Jun Jie: >> >> SBV uses some of the not-yet-officially-released features in Z3. The >> version you have, while it's the latest official Z3 release, will not work. >> >> To resolve, you need to install the "development" version of Z3 >> (something that is at least 4.3.2 or better). Here're instructions from the >> Microsoft folks explaining how to get these builds: >> http://research.microsoft.com/en-us/um/people/leonardo/blog/2013/02/15/precompiled.html >> >> Let me know if you find any issues after you get the latest-development >> version of Z3 installed. >> >> -Levent. >> >> >> On Thu, Mar 28, 2013 at 10:22 PM, J. J. W. wrote: >> >>> Dear all, >>> >>> I have a small question regarding the installation of the SBV package. I >>> first installed the SBV 2.10 package with cabal with the following >>> instructions: >>> >>> cabal install sbv >>> >>> Next I installed the Z3 theorem prover and adding the path to my system >>> variables (Windows 7 x64). Next I tested whether I could find it by opening >>> cmd.exe and then typing z3, I get an error message of Z3, so I can safely >>> assume the system can find it. (I added the path to the bin of Z3, I have >>> not included the include directory, I see no reason why I should add a path >>> to this directory, but maybe I am wrong). >>> >>> I ran the program: SBVUnitTests. However it had some errors in the >>> beginning and afterwards a few failures. Having no idea how to fix this, I >>> continued to check whether I can get the SBV to work. So I started to >>> execute the SBV package: >>> >>> ghci -XScopedTypeVariables >>> ghci> :m Data.SBV >>> ghci> prove $ \(x::SWord8) -> x `shiftL` 2 .== 4*x >>> >>> Now this should return Q.E.D., however it returned the following: >>> >>> An error occured. >>> Failed to complete the call to z3 >>> Executable: "C:\\Program Files\\z3-4.3.0-x64\\bin\\z3.exe >>> Options: /in /smt2 >>> Exit code: 0 >>> Solver output: >>> === >>> ; :smt.mbqi >>> ; :pp.decimal_precision >>> === >>> >>> Giving up.. >>> >>> It does seems like that the Z3 has a normal output, however not a >>> result. Can someone help me to figure out what I actually did wrong? >>> >>> I am using Z3 version 4.3.0, SBV 2.10 and GHCi 7.4.2 >>> >>> Thank you for your help! >>> >>> Yours sincerely, >>> >>> Jun Jie >>> >>> >>> ___ >>> Haskell-Cafe mailing list >>> Haskell-Cafe@haskell.org >>> http://www.haskell.org/mailman/listinfo/haskell-cafe >>> >>> >> > ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Haskell SBV Package with Z3
You're welcome Jun Jie. Regarding getting a different counter example: That's perfectly normal. When SMT solvers build models they use random seeds. Furthermore, different versions of the same solver can use different algorithms/heuristics to arrive at the falsifying model. So, it's entirely expected that you get a different counter-example. You can turn the question around, and ask the solver to give you all counter-examples like this: allSat $ \x -> \(x::SWord8) -> x `shiftL` 2 .!= x -Levent. On Mar 29, 2013, at 1:42 AM, "J. J. W." wrote: > Dear Levent, > > Thank you for your support. I am very honoured to have the developer of the > SBV package to solve my elementary problem. I noticed that the > counter-example given by my Z3 differs from the one said on HackageDB: > sbv-2.10. > > Code that is on Hackage: > > Prelude Data.SBV> prove $ forAll ["x"] $ \(x::SWord8) -> x `shiftL` 2 .== x >Falsifiable. Counter-example: > x = 128 :: SWord8 > > My current GHCi output: > > Prelude Data.SBV> prove $ forAll ["x"] $ \(x::SWord8) -> x `shiftL` 2 .== x > Falsifiable. Counter-example: > x = 51 :: SWord8 > (0.02 secs, 1196468 bytes) > > Thank you for your help! > > Yours sincerely, > > Jun Jie > > > 2013/3/29 Levent Erkok >> Hi Jun Jie: >> >> SBV uses some of the not-yet-officially-released features in Z3. The version >> you have, while it's the latest official Z3 release, will not work. >> >> To resolve, you need to install the "development" version of Z3 (something >> that is at least 4.3.2 or better). Here're instructions from the Microsoft >> folks explaining how to get these builds: >> http://research.microsoft.com/en-us/um/people/leonardo/blog/2013/02/15/precompiled.html >> >> Let me know if you find any issues after you get the latest-development >> version of Z3 installed. >> >> -Levent. >> >> >> On Thu, Mar 28, 2013 at 10:22 PM, J. J. W. wrote: >>> Dear all, >>> >>> I have a small question regarding the installation of the SBV package. I >>> first installed the SBV 2.10 package with cabal with the following >>> instructions: >>> >>> cabal install sbv >>> >>> Next I installed the Z3 theorem prover and adding the path to my system >>> variables (Windows 7 x64). Next I tested whether I could find it by opening >>> cmd.exe and then typing z3, I get an error message of Z3, so I can safely >>> assume the system can find it. (I added the path to the bin of Z3, I have >>> not included the include directory, I see no reason why I should add a path >>> to this directory, but maybe I am wrong). >>> >>> I ran the program: SBVUnitTests. However it had some errors in the >>> beginning and afterwards a few failures. Having no idea how to fix this, I >>> continued to check whether I can get the SBV to work. So I started to >>> execute the SBV package: >>> >>> ghci -XScopedTypeVariables >>> ghci> :m Data.SBV >>> ghci> prove $ \(x::SWord8) -> x `shiftL` 2 .== 4*x >>> >>> Now this should return Q.E.D., however it returned the following: >>> >>> An error occured. >>> Failed to complete the call to z3 >>> Executable: "C:\\Program Files\\z3-4.3.0-x64\\bin\\z3.exe >>> Options: /in /smt2 >>> Exit code: 0 >>> Solver output: >>> === >>> ; :smt.mbqi >>> ; :pp.decimal_precision >>> === >>> >>> Giving up.. >>> >>> It does seems like that the Z3 has a normal output, however not a result. >>> Can someone help me to figure out what I actually did wrong? >>> >>> I am using Z3 version 4.3.0, SBV 2.10 and GHCi 7.4.2 >>> >>> Thank you for your help! >>> >>> Yours sincerely, >>> >>> Jun Jie >>> >>> >>> ___ >>> Haskell-Cafe mailing list >>> Haskell-Cafe@haskell.org >>> http://www.haskell.org/mailman/listinfo/haskell-cafe > ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Haskell SBV Package with Z3
Hi Jun Jie: SBV uses some of the not-yet-officially-released features in Z3. The version you have, while it's the latest official Z3 release, will not work. To resolve, you need to install the "development" version of Z3 (something that is at least 4.3.2 or better). Here're instructions from the Microsoft folks explaining how to get these builds: http://research.microsoft.com/en-us/um/people/leonardo/blog/2013/02/15/precompiled.html Let me know if you find any issues after you get the latest-development version of Z3 installed. -Levent. On Thu, Mar 28, 2013 at 10:22 PM, J. J. W. wrote: > Dear all, > > I have a small question regarding the installation of the SBV package. I > first installed the SBV 2.10 package with cabal with the following > instructions: > > cabal install sbv > > Next I installed the Z3 theorem prover and adding the path to my system > variables (Windows 7 x64). Next I tested whether I could find it by opening > cmd.exe and then typing z3, I get an error message of Z3, so I can safely > assume the system can find it. (I added the path to the bin of Z3, I have > not included the include directory, I see no reason why I should add a path > to this directory, but maybe I am wrong). > > I ran the program: SBVUnitTests. However it had some errors in the > beginning and afterwards a few failures. Having no idea how to fix this, I > continued to check whether I can get the SBV to work. So I started to > execute the SBV package: > > ghci -XScopedTypeVariables > ghci> :m Data.SBV > ghci> prove $ \(x::SWord8) -> x `shiftL` 2 .== 4*x > > Now this should return Q.E.D., however it returned the following: > > An error occured. > Failed to complete the call to z3 > Executable: "C:\\Program Files\\z3-4.3.0-x64\\bin\\z3.exe > Options: /in /smt2 > Exit code: 0 > Solver output: > === > ; :smt.mbqi > ; :pp.decimal_precision > === > > Giving up.. > > It does seems like that the Z3 has a normal output, however not a result. > Can someone help me to figure out what I actually did wrong? > > I am using Z3 version 4.3.0, SBV 2.10 and GHCi 7.4.2 > > Thank you for your help! > > Yours sincerely, > > Jun Jie > > > ___ > Haskell-Cafe mailing list > Haskell-Cafe@haskell.org > http://www.haskell.org/mailman/listinfo/haskell-cafe > > ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] [Announcement] New release of hArduino: Control your Arduino board from Haskell
A new release (v0.5) of hArduno is out, now supporting servo-motors, shift-registers, seven-segment displays, and distance sensors. Comes with a bunch of examples to play around with: http://leventerkok.github.com/hArduino/ On Hackage: http://hackage.haskell.org/package/hArduino -Levent. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] [Announcement] hArduino: Control your Arduino board from Haskell
I'm happy to announce hArduino: a library that allows Arduino boards to be controlled directly from Haskell. hArduino uses the Firmata protocol ( http://firmata.org), to communicate with and control Arduino boards, making it possible to implement many controller projects directly in Haskell. Home page: http://leventerkok.github.com/hArduino/ Hackage: http://hackage.haskell.org/package/hArduino Some example programs: Blink the led: http://hackage.haskell.org/packages/archive/hArduino/latest/doc/html/System-Hardware-Arduino-SamplePrograms-Blink.html Digital counter: http://hackage.haskell.org/packages/archive/hArduino/latest/doc/html/System-Hardware-Arduino-SamplePrograms-Counter.html Control an LCD: http://hackage.haskell.org/packages/archive/hArduino/latest/doc/html/System-Hardware-Arduino-SamplePrograms-LCD.html Short (4.5 mins) youtube video of the blink example: http://www.youtube.com/watch?v=PPa3im44t2g hArduino is work-in-progress: Patches, bug-reports, and feedback is most welcome. -Levent. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] [Announcement] New SBV release
I'm happy to announce v2.9 release of the Haskell SBV library: http://leventerkok.github.com/sbv/ SBV (SMT Based Verification) is a library that allows Haskell programs to take advantage of modern SMT solvers, by providing a symbolic simulation engine that can invoke 3rd party SMT solvers to prove/falsify properties about (a certain class of) Haskell programs. New in this release is the support for the CVC4 SMT solver: http://cvc4.cs.nyu.edu/web/ If you were planning to use SMT solvers before, but were worried about the not-so-commercial-friendly licenses of Yices and Z3, then this is a great opportunity: *CVC4 comes with essentially no limit on its use for research or commercial purposes*! Feedback, patches and bug reports are always welcome. -Levent. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] ANNOUNCE: pretty-tree
Iavor's pretty-show package is quite handy for these kind of tasks as well. Highly recommended: http://hackage.haskell.org/package/pretty-show Since Iavor package is not tree-centric, it'll probably not generate as nice output as you can for real tree-like-data. However, since it works on arbitrary Show instances, it's much more readily usable: It's (almost) a drop-in replacement for show. I find it to be extremely valuable in debugging tasks. -Levent. On Fri, Oct 26, 2012 at 5:58 AM, Ivan Lazar Miljenovic < ivan.miljeno...@gmail.com> wrote: > For a project I'm working on, I got sick of writing out trees by hand. > Data.Tree has a drawTree function, but whilst it's better than > nothing, I prefer a more top-down "traditional" approach to drawing > trees. > > So I wrote a package to do just that: > http://hackage.haskell.org/package/pretty-tree > > (I didn't think to check whether diagrams had capabilities to do so > until after I finished, though in this case I prefer a textual > approach anyway.) > > I'm more than happy to consider adding other forms of drawing trees > (though off-hand I can't think of any), or of course you can send me > patches since I'm taking advantage of the nice new shiny hub.darcs.net > (thanks Darcs team!). > > I was going to put an example here but it only really comes out nicely > if you're using a monospaced font, so have a look at the Haddock docs > for the module once Hackage builds it (in hindsight, I should probably > have come up with better labels before releasing the package... oh > well :) > > -- > Ivan Lazar Miljenovic > ivan.miljeno...@gmail.com > http://IvanMiljenovic.wordpress.com > > ___ > Haskell-Cafe mailing list > Haskell-Cafe@haskell.org > http://www.haskell.org/mailman/listinfo/haskell-cafe > ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Solving integer equations in Haskell
On Oct 17, 2012, at 3:35 AM, Justin Paston-Cooper wrote: > Thanks for all the informative replies. SBV seems the simplest solution right > now, and speed isn't too much of an issue here. Anything under 20 seconds per > solution should be bearable. I'm happy to announce the SMT based linear equation solver library: http://hackage.haskell.org/package/linearEqSolver You can use it get solutions over Integers only, or over Rationals if so needed. Functions are provided to extract one solution, or all possible solutions (as a lazy list). The latter variant is useful for underspecified systems. Regarding performance: SMT solvers are very good at solving such equations, so aside from the overhead of calling out to an external program, it should be fairly fast. I'd expect no practical instance to come to anywhere near the 20 second limit you've mentioned. For most practical instances, the process switch overhead would dominate computation time, which should be negligible. Let me know if you find otherwise. -Levent. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Solving integer equations in Haskell
On Mon, Oct 15, 2012 at 9:00 AM, Johannes Waldmann wrote: > Justin Paston-Cooper gmail.com> writes: > >> Can anyone suggest a library written in Haskell which can solve equations >> of the form xM(transpose(x)) = y, where x should be an integer vector, >> M is an integer matrix and y is an integer? > > when in doubt, use brute force: > > write this as a constraint system > (in QF_NIA or QF_BV logics) and solve with Z3. As Johannes mentioned, you can indeed use SBV/Z3 to solve such problems. Indeed, there's an existing example for showing how to solve Diophantine equations this way: http://hackage.haskell.org/packages/archive/sbv/2.3/doc/html/Data-SBV-Examples-Existentials-Diophantine.html The technique described there can be used to solve the problem you've described; or systems of arbitrary constraint equations in general with minor tweaks. Having said that, using an SMT solver for this problem may not necessarily be the fastest route. The general purpose nature of SMT solving, while sound and complete for this class of problems, are not necessarily the most efficient when there are existing fast algorithms. In particular, you should check out John Ramsdell's cmu package: http://hackage.haskell.org/package/cmu. In particular see: http://hackage.haskell.org/packages/archive/cmu/1.8/doc/html/Algebra-CommutativeMonoid-LinDiophEq.html While the approach here only applies to linear diophantine equations, you might be able to adapt it to your particular needs. -Levent. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Fwd: hackage compile failure with QuickCheck 2.5
Ah, that explains why the hackage page mysteriously got fixed. Thanks for looking into this Ross. It still feels like this'll start biting more folks down the road. I've created the following cabal ticket so it can be tracked: https://github.com/haskell/cabal/issues/978 However, my understanding of the problem is rather incomplete; please feel free to add comments to the ticket. -Levent. On Tue, Jul 17, 2012 at 10:26 AM, Ross Paterson wrote: > With ghc 7.4.1, cabal-install 0.13.3 and Cabal 1.14.0, > > % cabal install --avoid-reinstalls sbv-2.2 > > fails to find a plan without reinstalls, and recommends --solver=modular. > > % cabal install --solver=modular --avoid-reinstalls sbv-2.2 > > reinstalls template-haskell-2.6.0.0, which breaks the GHC installation. > > I've added the suggested --constraint='template-haskell==2.7.0.0' > option as a workaround, but it seems the --avoid-reinstalls option is > being ignored. > > ___ > Haskell-Cafe mailing list > Haskell-Cafe@haskell.org > http://www.haskell.org/mailman/listinfo/haskell-cafe > ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Fwd: hackage compile failure with QuickCheck 2.5
Thanks Alexander.. Here's the shocker: I just checked that page again ( http://hackage.haskell.org/package/sbv) and now it's mysteriously fine! Hackage must've recompiled the package somehow. Someone watching this thread must've fixed something on the server and triggered a new compile. While I'm happy the problem is now gone, the mystery behind the hackage recompile remains.. Maybe someone can shed some light on how hackage goes about managing the uploads. -Levent. On Tue, Jul 17, 2012 at 9:43 AM, Alexander Foremny < alexanderfore...@gmail.com> wrote: > Dear Levent, > > unfortunately I am at a loss here. As far as I understand it this > should be fixed in QuickCheck's .cabal file or on Hackage. But I am > not experienced enough to decide. > > You best wait for someone else to comment on this. Depending on > template-haskell in your .cabal file is not the way to go as far as I > understand it. But maybe it's a possible work-around in case you > depend on the package being available on Hackage timely. > > Regards, > Alexander Foremny > > 2012/7/17 Levent Erkok : > > It builds fine locally on my box; but not on hackage. Here's the page: > > http://hackage.haskell.org/package/sbv-2.2 > > > > Thanks for looking into this Alexander, I appreciate your help. > > > > -Levent. > > > > > > On Tue, Jul 17, 2012 at 9:09 AM, Alexander Foremny > > wrote: > >> > >> Which package are you trying to build? Is it a local package that > >> fails to build or something on Hackage? Its .cabal file or at least > >> full dependencies would be of interest. > >> > >> Regards, > >> Alexander Foremny > >> > >> 2012/7/17 Levent Erkok : > >> > Thanks Alexander. However, I'm not sure how to use the workaround > >> > described > >> > so I can get hackage to properly compile my package. It sounds like I > >> > have > >> > to add a "template-haskell >= 2.7.0.0" dependency to my own cabal > file, > >> > which sounds like the wrong thing to do in the long-run. > >> > > >> > Is there something that can be done on the hackage/ghc side to avoid > >> > this > >> > issue? Or something less drastic than adding a template-haskell > >> > dependency > >> > on my own package's cabal file? > >> > > >> > Thanks, > >> > > >> > -Levent. > >> > > >> > > >> > On Tue, Jul 17, 2012 at 7:31 AM, Alexander Foremny > >> > wrote: > >> >> > >> >> Dear Levent, > >> >> > >> >> I think this [1] could be related. > >> >> > >> >> Regards, > >> >> Alexander Foremny > >> >> > >> >> PS. Sent this to Levent directly. Here's a copy for the mailing list. > >> >> Sorry for the noise. > >> >> > >> >> [1] > >> >> > >> >> > http://haskell.1045720.n5.nabble.com/Bad-interface-problem-td5714184.html > >> >> > >> >> -- Forwarded message -- > >> >> From: Alexander Foremny > >> >> Date: 2012/7/17 > >> >> Subject: Re: [Haskell-cafe] hackage compile failure with QuickCheck > 2.5 > >> >> To: Levent Erkok > >> >> > >> >> > >> >> Dear Levent, > >> >> > >> >> I think this [1] could be related. > >> >> > >> >> Regards, > >> >> Alexander Foremny > >> >> > >> >> [1] > >> >> > >> >> > http://haskell.1045720.n5.nabble.com/Bad-interface-problem-td5714184.html > >> >> > >> >> 2012/7/17 Levent Erkok : > >> >> > [This message is more appropriate for a hackage mailing list I > >> >> > presume, > >> >> > but > >> >> > that doesn't seem to exist. Let me know if there's a better place > to > >> >> > send > >> >> > it.] > >> >> > > >> >> > I'm having a hackage compile failure for a newly uplodaded package > >> >> > that > >> >> > has > >> >> > a QuickCheck 2.5 dependence. The error message is: > >> >> > > >> >> > [13 of 13] Compiling Test.QuickCheck.All ( Test/QuickCheck/All.hs, > >> >> > dist/build/Test/
Re: [Haskell-cafe] Fwd: hackage compile failure with QuickCheck 2.5
Thanks Alexander. However, I'm not sure how to use the workaround described so I can get hackage to properly compile my package. It sounds like I have to add a "template-haskell >= 2.7.0.0" dependency to my own cabal file, which sounds like the wrong thing to do in the long-run. Is there something that can be done on the hackage/ghc side to avoid this issue? Or something less drastic than adding a template-haskell dependency on my own package's cabal file? Thanks, -Levent. On Tue, Jul 17, 2012 at 7:31 AM, Alexander Foremny < alexanderfore...@gmail.com> wrote: > Dear Levent, > > I think this [1] could be related. > > Regards, > Alexander Foremny > > PS. Sent this to Levent directly. Here's a copy for the mailing list. > Sorry for the noise. > > [1] > http://haskell.1045720.n5.nabble.com/Bad-interface-problem-td5714184.html > > -- Forwarded message -- > From: Alexander Foremny > Date: 2012/7/17 > Subject: Re: [Haskell-cafe] hackage compile failure with QuickCheck 2.5 > To: Levent Erkok > > > Dear Levent, > > I think this [1] could be related. > > Regards, > Alexander Foremny > > [1] > http://haskell.1045720.n5.nabble.com/Bad-interface-problem-td5714184.html > > 2012/7/17 Levent Erkok : > > [This message is more appropriate for a hackage mailing list I presume, > but > > that doesn't seem to exist. Let me know if there's a better place to send > > it.] > > > > I'm having a hackage compile failure for a newly uplodaded package that > has > > a QuickCheck 2.5 dependence. The error message is: > > > > [13 of 13] Compiling Test.QuickCheck.All ( Test/QuickCheck/All.hs, > > dist/build/Test/QuickCheck/All.o ) > > > > Test/QuickCheck/All.hs:15:1: > > Bad interface file: > > > /usr/local/tmp/archive/install/lib/template-haskell-2.6.0.0/ghc-7.4.1/Language/Haskell/TH.hi > > Something is amiss; requested module > > template-haskell-2.6.0.0:Language.Haskell.TH differs from name found in > the > > interface file template-haskell:Language.Haskell.TH > > > > > > The full log file is at (search for "Something is a miss" in it): > > http://hackage.haskell.org/packages/archive/sbv/2.2/logs/failure/ghc-7.4 > > > > Needless to say, I don't see this problem when I compile this package at > > home with the same compiler (ghc 7.4.1) as hackage is using; also Hackage > > has a successfully compiled QuickCheck 2.5 package. > > > > Could it be something related to the particular cabal/ghc installation on > > the hackage server? In particular, I don't understand why it picks > > template-haskell 2.6.0.0 when there's a newer version (2.7.0.0). As far > as I > > can see, QuickCheck doesn't put an upper limit on its template haskell > > version dependency. > > > > I'd appreciate any pointers with this. (Googling and questions on the > > #haskell irc channel didn't help much, unfortunately.) > > > > -Levent. > > > > > > ___ > > Haskell-Cafe mailing list > > Haskell-Cafe@haskell.org > > http://www.haskell.org/mailman/listinfo/haskell-cafe > > > > ___ > Haskell-Cafe mailing list > Haskell-Cafe@haskell.org > http://www.haskell.org/mailman/listinfo/haskell-cafe > ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] hackage compile failure with QuickCheck 2.5
[This message is more appropriate for a hackage mailing list I presume, but that doesn't seem to exist. Let me know if there's a better place to send it.] I'm having a hackage compile failure for a newly uplodaded package that has a QuickCheck 2.5 dependence. The error message is: [13 of 13] Compiling Test.QuickCheck.All ( Test/QuickCheck/All.hs, dist/build/Test/QuickCheck/All.o ) Test/QuickCheck/All.hs:15:1: Bad interface file: /usr/local/tmp/archive/install/lib/template-haskell-2.6.0.0/ghc-7.4.1/Language/Haskell/TH.hi Something is amiss; requested module template-haskell-2.6.0.0:Language.Haskell.TH differs from name found in the interface file template-haskell:Language.Haskell.TH The full log file is at (search for "Something is a miss" in it): http://hackage.haskell.org/packages/archive/sbv/2.2/logs/failure/ghc-7.4 Needless to say, I don't see this problem when I compile this package at home with the same compiler (ghc 7.4.1) as hackage is using; also Hackage has a successfully compiled QuickCheck 2.5 package. Could it be something related to the particular cabal/ghc installation on the hackage server? In particular, I don't understand why it picks template-haskell 2.6.0.0 when there's a newer version (2.7.0.0). As far as I can see, QuickCheck doesn't put an upper limit on its template haskell version dependency. I'd appreciate any pointers with this. (Googling and questions on the #haskell irc channel didn't help much, unfortunately.) -Levent. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] ANNOUNCE: fast-tags-0.0.1
Chris: You might be experiencing this issue: http://hackage.haskell.org/trac/ghc/ticket/5783 Upgrading text and recompiling fast-tags should take care of this problem. -Levent. On Sun, Apr 1, 2012 at 10:12 AM, Christopher Done wrote: > By the way, I'm assuming that this library isn't an April Fools joke > by making a library called “fast” with explosive O(n²) time problems. > :-P > > ___ > Haskell-Cafe mailing list > Haskell-Cafe@haskell.org > http://www.haskell.org/mailman/listinfo/haskell-cafe ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] generating parens for pretty-printing code in haskell-src-exts
Neil Mitchell's HLint (http://community.haskell.org/~ndm/hlint/) warns about "extra parens" in Haskell code. So, it must have code for detecting those. I wonder if you can just insert parens liberally in a first run, and then use his algorithm to remove those that are unnecessary. The two passes can probably be fused, if you're willing to use haskell-stc-exts and do a bit of bookkeeping.. -Levent. On Sat, Jan 21, 2012 at 10:39 AM, Niklas Broberg wrote: > Hi Conal, > > On Sun, Jan 15, 2012 at 6:45 AM, Conal Elliott wrote: >> >> I'm using haskell-src-exts together with SYB for a code-rewriting project, >> and I'm having difficulty with parenthesization. I naïvely expected that >> parentheses would be absent from the abstract syntax, being removed during >> parsing and inserted during pretty-printing. It's easy for me to remove them >> myself, but harder to add them (minimally) after transformation. Rather than >> re-inventing the wheel, I thought I'd ask for help. > > > It's not at all straight-forward to properly insert minimal parentheses > during pretty-printing, since "minimal" is a semantic notion. For that to > work, we would need the pretty-printer to take a set of known fixities as an > argument, just like the parser currently does. I'm not opposed to the idea > in principle, but it's not how it currently works. > >> >> Has anyone written automatic minimal parens insertion for >> haskell-src-exts? > > > ... or we could do it this way, in a two-stage modular process which gives > even more flexibility. I'm not aware of any such functionality, currently, > but if it exists (or happens to come into existence) then I would be > interested in including it in haskell-src-exts. > > Best regards, > > /Niklas > > ___ > Haskell-Cafe mailing list > Haskell-Cafe@haskell.org > http://www.haskell.org/mailman/listinfo/haskell-cafe > ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] [ANNOUNCEMENT] SBV 0.9.24 is out
Hello all, SBV 0.9.24 is out: http://hackage.haskell.org/package/sbv In short, SBV allows for scripting SMT solvers directly within Haskell, with built-in support for bit-vectors and unbounded integers. (Microsoft's Z3 SMT solver, and SRI's Yices can be used as backends.) New in this release are SMT based optimization (both quantified and iterative), and support for explicit domain constraints with vacuity check. Full release notes: http://github.com/LeventErkok/sbv/blob/master/RELEASENOTES Happy new year! -Levent. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] smt solver bindings
Dimitrios: The SBV library (http://hackage.haskell.org/package/sbv) can indeed use Z3 as a backend SBV solver. However, it uses Z3 via SMT-Lib2, not via it's C-API. It aims to provide a much higher level interface, integrating with Haskell as smoothly as possible, keeping the SMT-solver transparent to the user. I'm actively developing and using SBV (http://github.com/LeventErkok/sbv), so any comments/feedback would be most welcome. Do let me know if you decide to use it and see any issues.. -Levent. On Thu, Dec 15, 2011 at 12:17 PM, Josef Svenningsson wrote: > On Thu, Dec 15, 2011 at 7:04 PM, Dimitrios Vytiniotis > wrote: >> >> >> I've a quick question: >> >> Are there Haskell wrappers for the Z3 C API around? >> > I believe sbv recently got support for Z3 but I don't know if it uses the C > API. Neither have I tried the Z3 backend, I only played with the Yices > backend. If you contact Levent Erkök, the author of sbv, he should be able > to give you more information. > > https://github.com/LeventErkok/sbv > > Thanks, > > Josef > > ___ > Haskell-Cafe mailing list > Haskell-Cafe@haskell.org > http://www.haskell.org/mailman/listinfo/haskell-cafe > ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] [Announcement] New release of SBV (0.9.22)
New release of SBV (0.9.22) is out: http://hackage.haskell.org/package/sbv Major changes in this release are: - Support for explicit quantification (including alternating existentials and universals) - Ability to use Microsoft's Z3 SMT solver (in addition to Yices). Full release notes: http://github.com/LeventErkok/sbv/blob/b75fb082c013ae9612ef09b90d5feeaec6527a47/RELEASENOTES Thanks, -Levent. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] library on common sub-expression elimination?
On 8/12/2011 10:30 AM, Conal Elliott wrote:
Note that data-reify will only find *some* common/equal sub-expressions,
namely the pointer-equal ones. In all of my code-generating ("deep")
DSLs, it's been very important for efficiency to also pull out
equal-but-pointer-unequal expressions.
- Conal
data-reify-cse (http://hackage.haskell.org/package/data-reify-cse) by
Sebastiaan Visser performs cse for graphs generated by Andy's data-reify.
-Levent.
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] pointer equality
On Jul 19, 2011, at 11:34 PM, Levent Erkok wrote: > import System.Mem.StableName > > areEqual :: Eq a => a -> a -> IO Bool > areEqual x y = do > sx <- hashStableName `fmap` (x `seq` makeStableName x) > sy <- hashStableName `fmap` (y `seq` makeStableName y) > return $ (sx == sy) || x == y One correction to the above code: Since we're actually comparing hashes, there's a non-zero chance that we might get a hash-collision; thus incorrectly identifying two different objects to be the same even though they have different stable names. To accommodate for that, you can use the hashes to index into a look-up table and then do a linear-scan to make sure it's an object that you've seen before. So the above code is *not* going to work for your purposes in general, but it can be extended to handle such equalities if you can afford to carry around the hash-table with you and be disciplined in how you perform your equality tests. Again, see Andy's paper (section 11) for further details on how he this problem can be handled in general. -Levent. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] pointer equality
> Is there any way of getting the following code to immediately return > True without performing the element-by-element comparison? Essentially > this boils down to checking whether pointers are equal before > comparing the contents. > >> main = print $ f == f >> where f = [1..10^9] Nikhil, As others pointed out, what you're asking for is not possible in Haskell, and for good reasons. However, this is an important problem, and it comes up quite often in practice when implementing DSLs: Detecting sharing. So, it's no surprise that people developed different ways of dealing with it in various forms. In my mind, Andy Gill came up with the nicest solution in his "Type-Safe Observable Sharing in Haskell" paper, published in the 2009 Haskell Symposium. Andy's paper traces the technique back to a 1999 paper by Simon Peyton Jones, Simon Marlow, and Conal Elliott. Probably few others came up with the same idea as well over the years. Andy's paper is a joy to read and I'd highly recommend it, you can get a copy at his web site: http://www.ittc.ku.edu/csdl/fpg/sites/default/files/Gill-09-TypeSafeReification.pdf. Andy's fundamental observation is that while you cannot check for "pointer-equality" in the pure world for obvious reasons, it's perfectly fine to do so when you're in the IO monad. He further observes that for almost all most practical use cases, this is really not an issue: You're probably in some sort of a monad wrapped over IO anyhow: This has certainly been my experience, for instance. While the paper has all the details, the "trick" is to use GHC's StableName abstraction. If you define: import System.Mem.StableName areEqual :: Eq a => a -> a -> IO Bool areEqual x y = do sx <- hashStableName `fmap` (x `seq` makeStableName x) sy <- hashStableName `fmap` (y `seq` makeStableName y) return $ (sx == sy) || x == y then areEqual will run quite fast if it indeed receives the same object twice, no matter how large it is. In fact, it might even be cyclic! (See Andy's paper for details.) However, if the stable-name equality fails, then you are *not* guaranteed that the objects are different, hence you further need to run the usual "==" on them, which can be quite costly. (Of course "==" can go in loops if the objects happen to have cycles in them.) You can also change the last line of areEqual to read: return $ sx == sy In this case, if it returns True then you're guaranteed that the objects are equal. If the result is False, then you just don't know. However it's guaranteed that the function will run fast in either case. Client code can decide on how to proceed based on that information. I hope this helps. Reading Andy's paper, and the papers he's cited can further elucidate the technique. In fact, Andy uses this idea to turn cyclic structures to graphs with explicit back-edges that can be processed much more easily in the pure world, something that comes up quite often in practice as well. -Levent. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Reference monad
On Mar 11, 2011, at 7:37 PM, Luke Palmer wrote: > On Fri, Mar 11, 2011 at 8:18 PM, Joshua Ball wrote: >> Suppose I want the following functions: >> >> newRef :: a -> RefMonad (Ref a) >> readRef :: Ref a -> RefMonad a >> writeRef :: Ref a -> a -> RefMonad () > > I would be delighted to see a pure, unsafe*-free implementation of > your interface. I have never seen one, and I don't really expect it > to exist. Likewise I would love to see a proof that it doesn't. This message from Koen Claessen, dating back to 2001, discusses precisely this issue: http://www.mail-archive.com/haskell@haskell.org/msg09207.html Quoting Koen: "I conjecture this functionality cannot be implemented in Haskell 98, nor in any of the known safe extensions of Haskell." I think the folk consensus in the community is that Koen was right. While a proof along the lines of "doing so would violate parametricity" seems plausible, I can't recall anybody attempting a rigorous proof so far. -Levent. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] writing graphs with do-notation
Andy Gill wrote a very nice recent paper on this topic which can serve
as the basis for a generic implementation:
http://www.ittc.ku.edu/~andygill/paper.php?label=DSLExtract09
As long as you do your "reification" in the IO monad, Andy's library
gives you the graph conversion for (almost-) free.
-Levent.
On Dec 13, 2009, at 10:48 PM, Emil Axelsson wrote:
Hi!
This technique has been used to define netlists in hardware
description languages. The original Lava [1] used a monad, but later
switched to using observable sharing [2]. Wired [3] uses a monad
similar to yours (but more complicated).
I think it would be nice to have a single library for defining such
graphs (or maybe there is one already?). The graph structure in
Wired could probably be divided into a purely structural part and a
hardware-specific part.
[1] http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.46.5221
[2] http://www.cs.chalmers.se/~dave/papers/observable-sharing.pdf
[3] http://hackage.haskell.org/package/Wired
/ Emil
Soenke Hahn skrev:
Hi!
Some time ago, i needed to write down graphs in Haskell. I wanted
to be able to write them down without to much noise, to make them
easily maintainable. I came up with a way to define graphs using
monads and the do notation. I thought this might be interesting to
someone, so i wrote a small script to illustrate the idea. Here's
an example:
example :: Graph String
example = buildGraph $ do
a <- mkNode "A" []
b <- mkNode "B" [a]
mkNode "C" [a, b]
In this graph there are three nodes identified by ["A", "B", "C"]
and three edges ([("A", "B"), ("A", "C"), ("B", "C")]). Think of
the variables a and b as outputs of the nodes "A" and "B". Note
that each node identifier needs to be mentioned only once. Also the
definition of edges (references to other nodes via the outputs) can
be checked at compile time.
The attachment is a little script that defines a Graph-type
(nothing elaborate), the "buildGraph" function and an example graph
that is a little more complex than the above. The main function of
the script prints the example graph to stdout to be read by dot (or
similar).
By the way, it is possible to define cyclic graphs using mdo
(RecursiveDo).
I haven't come across something similar, so i thought, i'd share
it. What do you think?
Sönke
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] There can be only one fix? Pondering Bekic's lemma
On 3/19/07, Nicolas Frisby <[EMAIL PROTECTED]> wrote: Nope, but I believe the two are equipotent. This usage of "believe" is one of those "I think I remember reading it somewhere" usages. On 3/19/07, Henning Thielemann <[EMAIL PROTECTED]> wrote: > > On Sat, 17 Mar 2007, Nicolas Frisby wrote: > > > Bekic's lemma [1], allows us to transform nested fixed points into a > > single fixed point, such as: > > > > fix (\x -> fix (\y -> f (x, y))) = fix f where f :: (a, a) -> a > > The 'fix' on the right hand side is not the standard one (e.g. > Control.Monad.Fix), is it? Yes, it is the standard "fix". The Bekic lemma actually reads: fix (\x -> fix (\y -> f (x, y))) = fix (\x -> f (x, x)) which should explain the confusion here. -Levent. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] ReadP and MonadFix
Gracjan:To declare "ReadP" an instance of MonadFix; you'll first have to make the P monad into a MonadFix instance. That can be done using existing techniques in the literature.ReadP is essentially the continuation monad transformer wrapped around P. It's well known in the value-recursion literature that continuation monad is too "strong" to have a value-recursion operator. I am not aware of any "simple" solutions in that space. Hence, ReadP is beyond the realm of current theories of value recursion. Having said that, I'd also like to point out that Amr Sabry and Eugenio Moggi, and independently Magnus Carlsson has done some interesting work to extend value recursion to the world of continuations; which might help with your particular problem. Essentially, you end up adding some extra infrastructure to your monad, and then forgo some of the basic axioms of value recursion. But you can get running examples! Maybe all you'll need is a MonadFix instance of P; which is definitely doable with the current techniques. Anything further would actually make a nice research paper...-Levent. (I could provide references to above work if needed; all is available on the net freely, anyhow.) On 6/23/06, Gracjan Polak <[EMAIL PROTECTED]> wrote: Hi all,A question for hot summer day: Text.ParserCombinators.ReadP.ReadP isan instance of Monad. Could it be an instance of MonadFix too?I'm not that sharp in Haskell to write it myself, but it seems I could make use of such a beast. :) Anybody willing to share?This will also present the advantage of Lazy over Eager ParserCombinators, mentioned in some other thread.--Gracjan___ Haskell-Cafe mailing listHaskell-Cafe@haskell.orghttp://www.haskell.org/mailman/listinfo/haskell-cafe ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: Question about typing
Tom Pledger wrote: > > Toby Watson writes: > | Intuitively the following scenarios seem to be related, can anyone > | point my in the direction of formal work on this, or give me the > | formal terms I need to search around? > | > | 1. Adding two integers together: Int -> Int -> Int > | > | 2. Adding two lists of Integers together: [Int] -> [Int] -> [Int] > > If you're adding each element of the first list to the element in the > corresponding position in the second list, it's usually called > zipping. The zipWith function in the prelude takes as its parameter a > function of type a->b->c (your scenario 1) and returns a function of > type [a]->[b]->[c] (your scenario 2). Jeff Lewis implemented zip comprehensions in the latest versions of both GHC and Hugs. This notation provides special syntax to deal with the second case above nicely. You can say: [x + y | x <- [1,2,3,4,5] | y <- [5,6,7,8]] to get: [6,8,10,12] The shorther list determines the final length (could of course be infinite.) It's an extension of the usual syntax, so multiple generators are OK too: [x + y | x <- [1,2,3,4,5], z <- [3, 4, 5], (x+z) `mod`2 == 1 | y <- [5,6,7,8], y `mod` 2 == 0] gives: [7, 10] It's a great notation that avoids zipWith's. (You need to start hugs with -98 and GHC needs -fglasgow-exts for zip comprehensions to be recognized.) -Levent. ___ Haskell-Cafe mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell-cafe
