Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Process: fix tests #17

Merged
merged 2 commits into from
Dec 13, 2022
Merged

Process: fix tests #17

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
3543813
tests: remove (exit) command at the end of sources
qaristote Dec 13, 2022
2f3f219
Merge branch 'master' into qa/tests_fix_exits
qaristote Dec 13, 2022
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
7 changes: 6 additions & 1 deletion tests/src/SMTLIB/Backends/Tests.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,3 +1,5 @@
{-# LANGUAGE OverloadedStrings #-}

-- | A module providing functions useful for testing a backend for SimpleSMT.
module SMTLIB.Backends.Tests
( testBackend,
Expand All @@ -6,7 +8,7 @@ module SMTLIB.Backends.Tests
)
where

import SMTLIB.Backends (Backend, initSolver)
import SMTLIB.Backends (Backend, command, initSolver)
import qualified SMTLIB.Backends.Tests.Sources as Src
import Test.Tasty
import Test.Tasty.HUnit
Expand Down Expand Up @@ -37,3 +39,6 @@ testBackend name sources with =
with $ \backend -> do
solver <- initSolver backend lazyMode
Src.run source solver
-- ensure the sources consisting only of ackCommands also run
_ <- command solver "(get-info :name)"
return ()
22 changes: 11 additions & 11 deletions tests/src/SMTLIB/Backends/Tests/Sources.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -46,7 +46,7 @@ assertions = Source "assertions" $ \solver -> do
_ <- command solver "(get-assertions)"
ackCommand solver "(pop 1)"
_ <- command solver "(get-assertions)"
ackCommand solver "(exit)"
return ()

assignments = Source "assignments" $ \solver -> do
ackCommand solver "(set-option :produce-assignments true)"
Expand All @@ -57,28 +57,28 @@ assignments = Source "assignments" $ \solver -> do
ackCommand solver "(assert (not (=(! (and (! p :named P) q) :named PQ) (! r :named R))))"
_ <- command solver "(check-sat)"
_ <- command solver "(get-assignment)"
ackCommand solver "(exit)"
return ()

boolean = Source "boolean" $ \solver -> do
ackCommand solver "(set-logic QF_UF)"
ackCommand solver "(declare-const p Bool)"
ackCommand solver "(assert (and p (not p)))"
_ <- command solver "(check-sat)"
ackCommand solver "(exit)"
return ()

info = Source "info" $ \solver -> do
_ <- command solver "(get-info :name)"
_ <- command solver "(get-info :version )"
_ <- command solver "(get-info :authors )"
ackCommand solver "(exit)"
return ()

integerArithmetic = Source "integer arithmetic" $ \solver -> do
ackCommand solver "(set-logic QF_LIA)"
ackCommand solver "(declare-const x Int)"
ackCommand solver "(declare-const y Int)"
ackCommand solver "(assert (= (- x y) (+ x (- y) 1)))"
_ <- command solver "(check-sat)"
ackCommand solver "(exit)"
return ()

modelingSequentialCodeSSA = Source "modeling sequential code (SSA)" $ \solver -> do
ackCommand solver "(set-logic QF_UFLIA)"
Expand All @@ -94,7 +94,7 @@ modelingSequentialCodeSSA = Source "modeling sequential code (SSA)" $ \solver ->
_ <- command solver "(check-sat)"
_ <- command solver "(get-value ((x 0) (y 0) (x 1) (y 1)))"
_ <- command solver "(get-model)"
ackCommand solver "(exit)"
return ()

modelingSequentialCodeBitvectors = Source "modeling sequential code (bitvectors)" $
\solver -> do
Expand All @@ -110,7 +110,7 @@ modelingSequentialCodeBitvectors = Source "modeling sequential code (bitvectors)
ackCommand solver "(assert (= x_2 (bvsub x_1 y_1)))"
ackCommand solver "(assert (not (and (= x_2 y_0) (= y_1 x_0))))"
_ <- command solver "(check-sat)"
ackCommand solver "(exit)"
return ()

scopes = Source "scopes" $ \solver -> do
ackCommand solver "(set-logic QF_LIA)"
Expand All @@ -125,7 +125,7 @@ scopes = Source "scopes" $ \solver -> do
ackCommand solver "(assert (= (- x y) 3))"
_ <- command solver "(check-sat)"
ackCommand solver "(pop 1)"
ackCommand solver "(exit)"
return ()

sorts = Source "sorts" $ \solver -> do
ackCommand solver "(set-logic QF_UF)"
Expand All @@ -146,7 +146,7 @@ sorts = Source "sorts" $ \solver -> do
ackCommand solver "(assert (distinct c d e))"
_ <- command solver "(check-sat)"
ackCommand solver "(pop 1)"
ackCommand solver "(exit)"
return ()

unsatCores = Source "unsat cores" $ \solver -> do
ackCommand solver "(set-option :produce-unsat-cores true)"
Expand All @@ -163,7 +163,7 @@ unsatCores = Source "unsat cores" $ \solver -> do
ackCommand solver "(assert (! (not (=> q s)) :named NQS))"
_ <- command solver "(check-sat)"
_ <- command solver "(get-unsat-core)"
ackCommand solver "(exit)"
return ()

valuesOrModels = Source "values or models" $ \solver -> do
ackCommand solver "(set-option :produce-models true)"
Expand All @@ -175,4 +175,4 @@ valuesOrModels = Source "values or models" $ \solver -> do
_ <- command solver "(check-sat)"
_ <- command solver "(get-value (x y))"
_ <- command solver "(get-model)"
ackCommand solver "(exit)"
return ()