smtlib-backends-tests (empty) → 0.2

raw patch · 6 files changed

+288/−0 lines, 6 filesdep +basedep +smtlib-backendsdep +tastysetup-changed

Dependencies added: base, smtlib-backends, tasty, tasty-hunit

Files

CHANGELOG.md +3/−0
LICENSE +21/−0
Setup.hs +3/−0
smtlib-backends-tests.cabal +39/−0
src/SMTLIB/Backends/Tests.hs +44/−0
src/SMTLIB/Backends/Tests/Sources.hs +178/−0

+ CHANGELOG.md view

@@ -0,0 +1,3 @@+# v0.2+- remove `(exit)` commands at the end of sources+- make library compatible with `smtlib-backends-0.2`

+ LICENSE view

@@ -0,0 +1,21 @@+MIT License++Copyright (c) Tweag I/O Limited.++Permission is hereby granted, free of charge, to any person obtaining a copy+of this software and associated documentation files (the "Software"), to deal+in the Software without restriction, including without limitation the rights+to use, copy, modify, merge, publish, distribute, sublicense, and/or sell+copies of the Software, and to permit persons to whom the Software is+furnished to do so, subject to the following conditions:++The above copyright notice and this permission notice shall be included in all+copies or substantial portions of the Software.++THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR+IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,+FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE+AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER+LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,+OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE+SOFTWARE.

+ Setup.hs view

@@ -0,0 +1,3 @@+import Distribution.Simple++main = defaultMain

+ smtlib-backends-tests.cabal view

@@ -0,0 +1,39 @@+name:               smtlib-backends-tests+version:            0.2+synopsis:           Testing SMT-LIB backends.+description:+  This library provides common functions and values used for testing SMT-LIB+  backends, as provided by the smtlib-backends library.++license:            MIT+license-file:       LICENSE+author:             Quentin Aristote+maintainer:         quentin.aristote@tweag.io+build-type:         Simple+category:           SMT, Testing+cabal-version:      >=1.10+extra-source-files: CHANGELOG.md++source-repository head+  type:     git+  location: https://github.com/tweag/smtlib-backends+  subdir:   smtlib-backends-tests++source-repository this+  type:     git+  location: https://github.com/tweag/smtlib-backends+  tag:      0.2+  subdir:   smtlib-backends-tests++library+  ghc-options:      -Wall -Wunused-packages+  hs-source-dirs:   src+  exposed-modules:  SMTLIB.Backends.Tests+  other-modules:    SMTLIB.Backends.Tests.Sources+  build-depends:+      base             >=4.14   && <4.17.0+    , smtlib-backends  >=0.2    && <0.3+    , tasty            >=1.4.2  && <1.5+    , tasty-hunit      >=0.10.0 && <0.11++  default-language: Haskell2010

+ src/SMTLIB/Backends/Tests.hs view

@@ -0,0 +1,44 @@+{-# LANGUAGE OverloadedStrings #-}++-- | A module providing functions useful for testing a backend for SimpleSMT.+module SMTLIB.Backends.Tests+  ( testBackend,+    Src.Source (..),+    Src.sources,+  )+where++import SMTLIB.Backends (Backend, command, initSolver)+import qualified SMTLIB.Backends.Tests.Sources as Src+import Test.Tasty+import Test.Tasty.HUnit++-- | Test a backend by using it to run a list of examples.+testBackend ::+  -- | The name of the test group.+  String ->+  -- | A list of examples on which to run the backend.+  [Src.Source] ->+  -- | A function that should create a backend, run a given+  -- computation and release the backend's resources.+  ((Backend -> Assertion) -> Assertion) ->+  TestTree+testBackend name sources with =+  testGroup name $ do+    lazyMode <- [False, True]+    return $+      testGroup+        ( if lazyMode+            then "lazy"+            else "eager"+        )+        $ do+          source <- sources+          return $+            testCase (Src.name source) $+              with $ \backend -> do+                solver <- initSolver backend lazyMode+                Src.run source solver+                -- ensure the sources consisting only of queued commands also run+                _ <- command solver "(get-info :name)"+                return ()

+ src/SMTLIB/Backends/Tests/Sources.hs view

@@ -0,0 +1,178 @@+{-# LANGUAGE OverloadedStrings #-}+{-# OPTIONS_GHC -Wno-missing-signatures #-}++module SMTLIB.Backends.Tests.Sources (Source (..), sources) where++import SMTLIB.Backends++-- | A source is a list of SMTLib2 commands, available in several different formats+-- for testing purposes.+data Source = Source+  { -- | The name of the source.+    name :: String,+    -- | A computation equivalent to sending the raw content of the source to the+    -- solver.+    run :: Solver -> IO ()+  }++-- | A list of examples SMT-LIB files. Most of them were taken from the official+-- SMT-LIB website:+-- https://smtlib.cs.uiowa.edu/examples.shtml+sources =+  [ assertions,+    assignments,+    boolean,+    info,+    integerArithmetic,+    modelingSequentialCodeSSA,+    modelingSequentialCodeBitvectors,+    scopes,+    sorts,+    unsatCores,+    valuesOrModels+  ]++assertions = Source "assertions" $ \solver -> do+  command_ solver "(set-option :produce-assertions true)"+  command_ solver "(set-logic QF_UF)"+  command_ solver "(declare-const p Bool)"+  command_ solver "(declare-const q Bool)"+  command_ solver "(push 1)"+  command_ solver "(assert (or p q))"+  command_ solver "(push 1)"+  command_ solver "(assert (not q))"+  _ <- command solver "(get-assertions)"+  command_ solver "(pop 1)"+  _ <- command solver "(get-assertions)"+  command_ solver "(pop 1)"+  _ <- command solver "(get-assertions)"+  return ()++assignments = Source "assignments" $ \solver -> do+  command_ solver "(set-option :produce-assignments true)"+  command_ solver "(set-logic QF_UF)"+  command_ solver "(declare-const p Bool)"+  command_ solver "(declare-const q Bool)"+  command_ solver "(declare-const r Bool)"+  command_ solver "(assert (not (=(! (and (! p :named P) q) :named PQ) (! r :named R))))"+  _ <- command solver "(check-sat)"+  _ <- command solver "(get-assignment)"+  return ()++boolean = Source "boolean" $ \solver -> do+  command_ solver "(set-logic QF_UF)"+  command_ solver "(declare-const p Bool)"+  command_ solver "(assert (and p (not p)))"+  _ <- command solver "(check-sat)"+  return ()++info = Source "info" $ \solver -> do+  _ <- command solver "(get-info :name)"+  _ <- command solver "(get-info :version )"+  _ <- command solver "(get-info :authors )"+  return ()++integerArithmetic = Source "integer arithmetic" $ \solver -> do+  command_ solver "(set-logic QF_LIA)"+  command_ solver "(declare-const x Int)"+  command_ solver "(declare-const y Int)"+  command_ solver "(assert (= (- x y) (+ x (- y) 1)))"+  _ <- command solver "(check-sat)"+  return ()++modelingSequentialCodeSSA = Source "modeling sequential code (SSA)" $ \solver -> do+  command_ solver "(set-logic QF_UFLIA)"+  command_ solver "(set-option :produce-models true)"+  command_ solver "(declare-fun x (Int) Int)"+  command_ solver "(declare-fun y (Int) Int)"+  command_ solver "(declare-fun t (Int) Int)"+  command_ solver "(assert (= (t 0) (x 0)))"+  command_ solver "(assert (= (y 1) (t 0)))"+  command_ solver "(assert (= (x 1) (y 1)))"++  command_ solver "(assert (not (and (= (x 1) (y 0)) (= (y 1) (x 0)))))"+  _ <- command solver "(check-sat)"+  _ <- command solver "(get-value ((x 0) (y 0) (x 1) (y 1)))"+  _ <- command solver "(get-model)"+  return ()++modelingSequentialCodeBitvectors = Source "modeling sequential code (bitvectors)" $+  \solver -> do+    command_ solver "(set-logic QF_BV)"+    command_ solver "(set-option :produce-models true)"+    command_ solver "(declare-const x_0 (_ BitVec 32))"+    command_ solver "(declare-const x_1 (_ BitVec 32))"+    command_ solver "(declare-const x_2 (_ BitVec 32))"+    command_ solver "(declare-const y_0 (_ BitVec 32))"+    command_ solver "(declare-const y_1 (_ BitVec 32))"+    command_ solver "(assert (= x_1 (bvadd x_0 y_0)))"+    command_ solver "(assert (= y_1 (bvsub x_1 y_0)))"+    command_ solver "(assert (= x_2 (bvsub x_1 y_1)))"+    command_ solver "(assert (not (and (= x_2 y_0) (= y_1 x_0))))"+    _ <- command solver "(check-sat)"+    return ()++scopes = Source "scopes" $ \solver -> do+  command_ solver "(set-logic QF_LIA)"+  command_ solver "(declare-const x Int)"+  command_ solver "(declare-const y Int)"+  command_ solver "(assert (= (+ x (* 2 y)) 20))"+  command_ solver "(push 1)"+  command_ solver "(assert (= (- x y) 2))"+  _ <- command solver "(check-sat)"+  command_ solver "(pop 1)"+  command_ solver "(push 1)"+  command_ solver "(assert (= (- x y) 3))"+  _ <- command solver "(check-sat)"+  command_ solver "(pop 1)"+  return ()++sorts = Source "sorts" $ \solver -> do+  command_ solver "(set-logic QF_UF)"+  command_ solver "(declare-sort A 0)"+  command_ solver "(declare-const a A)"+  command_ solver "(declare-const b A)"+  command_ solver "(declare-const c A)"+  command_ solver "(declare-const d A)"+  command_ solver "(declare-const e A)"+  command_ solver "(assert (or (= c a)(= c b)))"+  command_ solver "(assert (or (= d a)(= d b)))"+  command_ solver "(assert (or (= e a)(= e b)))"+  command_ solver "(push 1)"+  command_ solver "(assert (distinct c d))"+  _ <- command solver "(check-sat)"+  command_ solver "(pop 1)"+  command_ solver "(push 1)"+  command_ solver "(assert (distinct c d e))"+  _ <- command solver "(check-sat)"+  command_ solver "(pop 1)"+  return ()++unsatCores = Source "unsat cores" $ \solver -> do+  command_ solver "(set-option :produce-unsat-cores true)"+  command_ solver "(set-logic QF_UF)"+  command_ solver "(declare-const p Bool)"+  command_ solver "(declare-const q Bool)"+  command_ solver "(declare-const r Bool)"+  command_ solver "(declare-const s Bool)"+  command_ solver "(declare-const t Bool)"+  command_ solver "(assert (! (=> p q) :named PQ))"+  command_ solver "(assert (! (=> q r) :named QR))"+  command_ solver "(assert (! (=> r s) :named RS))"+  command_ solver "(assert (! (=> s t) :named ST))"+  command_ solver "(assert (! (not (=> q s)) :named NQS))"+  _ <- command solver "(check-sat)"+  _ <- command solver "(get-unsat-core)"+  return ()++valuesOrModels = Source "values or models" $ \solver -> do+  command_ solver "(set-option :produce-models true)"+  command_ solver "(set-logic QF_LIA)"+  command_ solver "(declare-const x Int)"+  command_ solver "(declare-const y Int)"+  command_ solver "(assert (= (+ x (* 2 y)) 20))"+  command_ solver "(assert (= (- x y) 2))"+  _ <- command solver "(check-sat)"+  _ <- command solver "(get-value (x y))"+  _ <- command solver "(get-model)"+  return ()