smtLib 1.0 → 1.0.1

raw patch · 3 files changed

+1/−79 lines, 3 filesdep −processdep −smtLib

Dependencies removed: process, smtLib

Files

smtLib.cabal +1/−22
test/Test1.hs +0/−32
test/Test2.hs +0/−25

smtLib.cabal view

@@ -1,5 +1,5 @@ Name:           smtLib-Version:        1.0+Version:        1.0.1 License:        BSD3 License-file:   LICENSE Author:         Iavor S. Diatchki@@ -43,24 +43,3 @@   type:     git   location: git://github.com/yav/smtLib.git -executable smtLib-test-1--  hs-source-dirs: test--  main-is: Test1.hs--  build-depends:-    base    < 5,-    smtLib,-    process--executable smtLib-test-2--  hs-source-dirs: test--  main-is: Test2.hs--  build-depends:-    base    < 5,-    smtLib,-    process

− test/Test1.hs

@@ -1,32 +0,0 @@-{-# LANGUAGE OverloadedStrings #-}-import SMTLib1.QF_AUFBV as BV-import System.Process-import System.IO--main :: IO ()-main =-  do let txt = show (pp script)-     putStrLn txt-     putStrLn (replicate 80 '-')-     -- putStrLn =<< readProcess "yices" ["-smt", "-tc"] txt-     putStrLn =<< readProcess "yices" ["-f"] txt---script :: Script-script = Script "Test"-  [ logic "QF_AUFBV"-  , constDef "a" (tBitVec 8)-  , goal (BV.concat (bv 1 8) (bv 3 8) === bv 259 16)-  ]---script1 :: Script-script1 = Script "Test"-  [ logic "QF_BV"-  , constDef "x" (tBitVec 8)-  , assume (c "x" === bv 0 8)-  , goal (c "x" ===  bv 256 8)-  ]--c x = App x []-

− test/Test2.hs

@@ -1,25 +0,0 @@-{-# LANGUAGE OverloadedStrings #-}-import SMTLib2-import SMTLib2.Core-import SMTLib2.BitVector-import System.Process-import System.IO--main :: IO ()-main =-  do let txt = show (pp script)-     putStrLn txt-     putStrLn (replicate 80 '-')-     putStrLn =<< readProcess "stp" ["--SMTLIB2"] txt---script :: Script-script = Script-  [ CmdSetLogic "QF_BV"-  , CmdDeclareFun "x" [] (tBitVec 4)-  , CmdAssert (c "x" === bv 3 4)-  , CmdCheckSat-  , CmdExit-  ]--c x = app x []