packages feed

toysolver-0.10.0: test/Test/SMTLIB2Solver.hs

{-# OPTIONS_GHC -Wall #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TemplateHaskell #-}
module Test.SMTLIB2Solver (smtlib2SolverTestGroup) where

import Control.Monad
import Data.List (sort)
import qualified Data.Map as Map
import qualified Data.Set as Set
import qualified Data.Text as T

import Test.Tasty
import Test.Tasty.HUnit
import Test.Tasty.TH

import ToySolver.SMT.SMTLIB2Solver as SMTLIB2

case_assertionStackLevels :: Assertion
case_assertionStackLevels = do
  solver <- SMTLIB2.newSolver
  SMTLIB2.setLogic solver "QF_UF"
  lv1 <- SMTLIB2.getInfo solver (AssertionStackLevels ())
  lv1 @?= [IRAssertionStackLevels 0]
  SMTLIB2.push solver 1
  lv2 <- SMTLIB2.getInfo solver (AssertionStackLevels ())
  lv2 @?= [IRAssertionStackLevels 1]
  SMTLIB2.pop solver 1
  lv3 <- SMTLIB2.getInfo solver (AssertionStackLevels ())
  lv3 @?= [IRAssertionStackLevels 0]

case_getUnsatAssumptions :: Assertion
case_getUnsatAssumptions = do
  solver <- SMTLIB2.newSolver
  SMTLIB2.setOption solver (ProduceUnsatAssumptions True ())
  o <- SMTLIB2.getOption solver ":produce-unsat-assumptions"
  o @?= AVSymbol "true" ()
  SMTLIB2.setLogic solver "QF_UF"
  SMTLIB2.declareFun solver "a" [] (Sort (Symbol "Bool") [] ())
  SMTLIB2.declareFun solver "b" [] (Sort (Symbol "Bool") [] ())
  _ <- SMTLIB2.runCommandString solver "(assert (or a b))"
  r <- SMTLIB2.runCommandString solver "(check-sat-assuming ((not a) (not b)))"
  r @?= RCheckSat Unsat
  r2 <- SMTLIB2.getUnsatAssumptions solver
  let expected =
       [ TApp (QIdentifier (Symbol "not") ()) [TQualIdent (QIdentifier (Symbol "a") ()) ()] ()
       , TApp (QIdentifier (Symbol "not") ()) [TQualIdent (QIdentifier (Symbol "b") ()) ()] ()
       ]
  Set.fromList r2 @?= Set.fromList expected

case_declareConst :: Assertion
case_declareConst = do
  solver <- SMTLIB2.newSolver
  SMTLIB2.setLogic solver "QF_LRA"
  assertSuccess =<< SMTLIB2.runCommandString solver "(declare-const b Bool)"
  assertSuccess =<< SMTLIB2.runCommandString solver "(declare-const x Bool)"
  assertSuccess =<< SMTLIB2.runCommandString solver "(declare-const y Bool)"

case_defineConst :: Assertion
case_defineConst = do
  solver <- SMTLIB2.newSolver
  SMTLIB2.setLogic solver "QF_LRA"
  assertSuccess =<< SMTLIB2.runCommandString solver "(define-const x Real 3)"
  assertSuccess =<< SMTLIB2.runCommandString solver "(assert (not (= x 3)))"
  r <- SMTLIB2.checkSat solver
  r @?= Unsat

case_divisionByZero :: Assertion
case_divisionByZero = do
  solver <- SMTLIB2.newSolver
  SMTLIB2.setOption solver (ProduceUnsatAssumptions True ())
  SMTLIB2.setLogic solver "QF_LRA"
  assertSuccess =<< SMTLIB2.runCommandString solver "(declare-const x1 Real)"
  assertSuccess =<< SMTLIB2.runCommandString solver "(declare-const x2 Real)"

  assertSuccess =<< SMTLIB2.runCommandString solver "(define-fun y1 () Real (/ x1 0))"
  assertSuccess =<< SMTLIB2.runCommandString solver "(define-fun y2 () Real (/ x2 0))"
  r <- SMTLIB2.checkSat solver
  r @?= Sat

  assertSuccess =<< SMTLIB2.runCommandString solver "(assert (not (= y1 y2)))"
  r2 <- SMTLIB2.checkSat solver
  r2 @?= Sat

  assertSuccess =<< SMTLIB2.runCommandString solver "(assert (= x1 x2))"
  r3 <- SMTLIB2.checkSat solver
  r3 @?= Unsat

case_getAssertions :: Assertion
case_getAssertions = do
  solver <- SMTLIB2.newSolver
  SMTLIB2.setOption solver (ProduceAssertions True ())
  o <- SMTLIB2.getOption solver ":produce-assertions"
  o @?= AVSymbol "true" ()
  SMTLIB2.setLogic solver "QF_UF"
  assertSuccess =<< SMTLIB2.runCommandString solver "(declare-fun a () Bool)"
  assertSuccess =<< SMTLIB2.runCommandString solver "(declare-fun b () Bool)"
  assertSuccess =<< SMTLIB2.runCommandString solver "(assert (or (! a :named aa) (! b :named bb)))"
  r <- SMTLIB2.runCommandString solver "(get-assertions)"
  showSL r @?= "((or (! a :named aa) (! b :named bb)))"
  SMTLIB2.push solver 1
  assertSuccess =<< SMTLIB2.runCommandString solver "(assert (not (and a bb)))"
  r2 <- SMTLIB2.runCommandString solver "(get-assertions)"
  showSL r2 @?= "((or (! a :named aa) (! b :named bb)) (not (and a bb)))"
  SMTLIB2.pop solver 1
  r3 <- SMTLIB2.runCommandString solver "(get-assertions)"
  showSL r3 @?= "((or (! a :named aa) (! b :named bb)))"

case_getAssignment :: Assertion
case_getAssignment = do
  solver <- SMTLIB2.newSolver
  SMTLIB2.setOption solver (ProduceAssignments True ())
  o <- SMTLIB2.getOption solver ":produce-assignments"
  o @?= AVSymbol "true" ()
  SMTLIB2.setLogic solver "QF_UFLRA"
  assertSuccess =<< SMTLIB2.runCommandString solver "(declare-fun a () Bool)"
  assertSuccess =<< SMTLIB2.runCommandString solver "(declare-fun b () Bool)"
  assertSuccess =<< SMTLIB2.runCommandString solver "(declare-fun c () Real)"
  assertSuccess =<< SMTLIB2.runCommandString solver "(assert (or (! a :named aa) (! b :named bb)))"
  assertSuccess =<< SMTLIB2.runCommandString solver "(assert (>= (! c :named cc) 0))"
  assertSuccess =<< SMTLIB2.runCommandString solver "(assert (not (and a bb)))"
  _ <- SMTLIB2.checkSat solver
  r <- SMTLIB2.getAssignment solver
  let m = Map.fromList r
  unless (m == Map.fromList [("aa",True), ("bb",False)] || m == Map.fromList [("aa",False), ("bb",True)]) $ do
    assertFailure (show r)

case_getModel :: Assertion
case_getModel = do
  solver <- SMTLIB2.newSolver
  SMTLIB2.setOption solver (ProduceModels True ())
  o <- SMTLIB2.getOption solver ":produce-models"
  o @?= AVSymbol "true" ()
  SMTLIB2.setLogic solver "QF_UF"
  assertSuccess =<< SMTLIB2.runCommandString solver "(declare-fun a () Bool)"
  assertSuccess =<< SMTLIB2.runCommandString solver "(declare-fun b () Bool)"
  assertSuccess =<< SMTLIB2.runCommandString solver "(assert (or a b))"
  assertSuccess =<< SMTLIB2.runCommandString solver "(assert (not (and a b)))"
  _ <- SMTLIB2.checkSat solver
  r <- SMTLIB2.getModel solver
  let m = sort $ map showSL r
  unless (m == ["(define-fun a () Bool true)", "(define-fun b () Bool false)"] ||
          m == ["(define-fun a () Bool false)", "(define-fun b () Bool true)"]) $ do
    assertFailure (show r)

case_getModel_division_by_zero :: Assertion
case_getModel_division_by_zero = do
  solver <- SMTLIB2.newSolver
  SMTLIB2.setOption solver (ProduceModels True ())
  SMTLIB2.setLogic solver "QF_LRA"

  assertSuccess =<< SMTLIB2.runCommandString solver "(declare-fun x1 () Real)"
  assertSuccess =<< SMTLIB2.runCommandString solver "(declare-fun x2 () Real)"
  status1 <- SMTLIB2.checkSat solver
  status1 @?= Sat
  RGetModel model1 <- SMTLIB2.runCommandString solver "(get-model)"
  assertBool ("/0 should not be in the model: " ++ showSL (RGetModel model1))
    (null [() | MRDefineFun (FunctionDef "/0" _ _ _ _) <- model1])

  assertSuccess =<< SMTLIB2.runCommandString solver "(define-fun y1 () Real (/ x1 0))"
  assertSuccess =<< SMTLIB2.runCommandString solver "(define-fun y2 () Real (/ x2 0))"
  assertSuccess =<< SMTLIB2.runCommandString solver "(assert (not (= y1 y2)))"
  status2 <- SMTLIB2.checkSat solver
  status2 @?= Sat
  RGetModel model2 <- SMTLIB2.runCommandString solver "(get-model)"
  assertBool ("/0 should be in the model: " ++ showSL (RGetModel model2))
    (not (null [() | MRDefineFun (FunctionDef "/0" _ _ _ _) <- model2]))

  assertSuccess =<< SMTLIB2.runCommandString solver "(assert (= x1 x2))"
  status3 <- SMTLIB2.checkSat solver
  status3 @?= Unsat

case_getValue :: Assertion
case_getValue = do
  solver <- SMTLIB2.newSolver
  SMTLIB2.setOption solver (ProduceModels True ())
  o <- SMTLIB2.getOption solver ":produce-models"
  o @?= AVSymbol "true" ()
  SMTLIB2.setLogic solver "QF_UF"
  assertSuccess =<< SMTLIB2.runCommandString solver "(declare-sort U 0)"
  assertSuccess =<< SMTLIB2.runCommandString solver "(declare-fun f (U) U)"
  assertSuccess =<< SMTLIB2.runCommandString solver "(declare-fun g (U) U)"
  assertSuccess =<< SMTLIB2.runCommandString solver "(declare-fun A () Bool)"
  assertSuccess =<< SMTLIB2.runCommandString solver "(declare-fun x () U)"
  assertSuccess =<< SMTLIB2.runCommandString solver "(declare-fun y () U)"
  _ <- SMTLIB2.checkSat solver
  r <- SMTLIB2.runCommandString solver "(get-value (x A (f x) (g y)))"
  case r of
    RGetValue _xs -> return () -- fixme
    _ -> assertFailure (show r)

case_GlobalDeclarations :: Assertion
case_GlobalDeclarations = do
  solver <- SMTLIB2.newSolver

  SMTLIB2.setOption solver (GlobalDeclarations False ())
  o <- SMTLIB2.getOption solver ":global-declarations"
  o @?= AVSymbol "false" ()
  SMTLIB2.setLogic solver "QF_UFLRA"
  SMTLIB2.push solver 1
  assertSuccess =<< SMTLIB2.runCommandString solver "(declare-const x1 Bool)"
  SMTLIB2.pop solver 1
  assertSuccess =<< SMTLIB2.runCommandString solver "(declare-const x1 Real)"

  SMTLIB2.reset solver

  SMTLIB2.setOption solver (GlobalDeclarations True ())
  o2 <- SMTLIB2.getOption solver ":global-declarations"
  o2 @?= AVSymbol "true" ()
  SMTLIB2.setLogic solver "QF_UFLRA"
  SMTLIB2.push solver 1
  assertSuccess =<< SMTLIB2.runCommandString solver "(define-fun x2 () Real 1.0)"
  SMTLIB2.pop solver 1
  assertSuccess =<< SMTLIB2.runCommandString solver "(assert (= x2 1.0))"
  _ <- SMTLIB2.checkSat solver

  return ()

case_quoted_symbols :: Assertion
case_quoted_symbols = do
  solver <- SMTLIB2.newSolver
  SMTLIB2.setLogic solver "QF_LRA"
  assertSuccess =<< SMTLIB2.runCommandString solver "(declare-fun abc () Real)"
  assertSuccess =<< SMTLIB2.runCommandString solver "(assert (= abc 0))"
  assertSuccess =<< SMTLIB2.runCommandString solver "(assert (= |abc| 1))"
  r <- SMTLIB2.checkSat solver
  r @?= Unsat

case_reset :: Assertion
case_reset = do
  solver <- SMTLIB2.newSolver

  SMTLIB2.setLogic solver "QF_UF"
  assertSuccess =<< SMTLIB2.runCommandString solver "(declare-fun x1 () Bool)"
  assertSuccess =<< SMTLIB2.runCommandString solver "(declare-fun x2 () Bool)"
  assertSuccess =<< SMTLIB2.runCommandString solver "(declare-fun x3 () Bool)"
  assertSuccess =<< SMTLIB2.runCommandString solver "(assert (! x1 :named C1))"
  assertSuccess =<< SMTLIB2.runCommandString solver "(assert (! (not x1) :named C2))"
  assertSuccess =<< SMTLIB2.runCommandString solver "(assert (! (or (not x1) x2) :named C3))"
  assertSuccess =<< SMTLIB2.runCommandString solver "(assert (! (not x2) :named C4))"
  assertSuccess =<< SMTLIB2.runCommandString solver "(assert (! (or (not x1) x3) :named C5))"
  assertSuccess =<< SMTLIB2.runCommandString solver "(assert (! (not x3) :named C6))"

  r <- SMTLIB2.checkSat solver
  r @?= Unsat

  SMTLIB2.reset solver

  r2 <- SMTLIB2.checkSat solver
  r2 @?= Sat

case_resetAssertions :: Assertion
case_resetAssertions = do
  solver <- SMTLIB2.newSolver

  SMTLIB2.setLogic solver "QF_UF"
  assertSuccess =<< SMTLIB2.runCommandString solver "(declare-fun x1 () Bool)"
  assertSuccess =<< SMTLIB2.runCommandString solver "(declare-fun x2 () Bool)"
  assertSuccess =<< SMTLIB2.runCommandString solver "(declare-fun x3 () Bool)"
  SMTLIB2.push solver 1
  assertSuccess =<< SMTLIB2.runCommandString solver "(assert (! x1 :named C1))"
  assertSuccess =<< SMTLIB2.runCommandString solver "(assert (! (not x1) :named C2))"
  assertSuccess =<< SMTLIB2.runCommandString solver "(assert (! (or (not x1) x2) :named C3))"
  assertSuccess =<< SMTLIB2.runCommandString solver "(assert (! (not x2) :named C4))"
  assertSuccess =<< SMTLIB2.runCommandString solver "(assert (! (or (not x1) x3) :named C5))"
  assertSuccess =<< SMTLIB2.runCommandString solver "(assert (! (not x3) :named C6))"

  r <- SMTLIB2.checkSat solver
  r @?= Unsat

  SMTLIB2.resetAssertions solver

  r2 <- SMTLIB2.checkSat solver
  r2 @?= Sat

-- http://sun.iwu.edu/~mliffito/publications/jar_liffiton_CAMUS.pdf
-- φ= (x1) ∧ (¬x1) ∧ (¬x1∨x2) ∧ (¬x2) ∧ (¬x1∨x3) ∧ (¬x3)
-- MUSes(φ) = {{C1, C2}, {C1, C3, C4}, {C1, C5, C6}}
-- MCSes(φ) = {{C1}, {C2, C3, C5}, {C2, C3, C6}, {C2, C4, C5}, {C2, C4, C6}}
case_getUnsatCore :: Assertion
case_getUnsatCore = do
  solver <- SMTLIB2.newSolver

  SMTLIB2.setOption solver (ProduceUnsatCores True ())
  o <- SMTLIB2.getOption solver ":produce-unsat-cores"
  o @?= AVSymbol "true" ()

  SMTLIB2.setLogic solver "QF_UF"
  assertSuccess =<< SMTLIB2.runCommandString solver "(declare-fun x1 () Bool)"
  assertSuccess =<< SMTLIB2.runCommandString solver "(declare-fun x2 () Bool)"
  assertSuccess =<< SMTLIB2.runCommandString solver "(declare-fun x3 () Bool)"
  assertSuccess =<< SMTLIB2.runCommandString solver "(assert (! x1 :named C1))"
  assertSuccess =<< SMTLIB2.runCommandString solver "(assert (! (not x1) :named C2))"
  assertSuccess =<< SMTLIB2.runCommandString solver "(assert (! (or (not x1) x2) :named C3))"
  assertSuccess =<< SMTLIB2.runCommandString solver "(assert (! (not x2) :named C4))"
  assertSuccess =<< SMTLIB2.runCommandString solver "(assert (! (or (not x1) x3) :named C5))"
  assertSuccess =<< SMTLIB2.runCommandString solver "(assert (! (not x3) :named C6))"
  r <- SMTLIB2.checkSat solver
  r @?= Unsat
  r2 <- SMTLIB2.getUnsatCore solver
  let expected = map Set.fromList [["C1", "C2"], ["C1", "C3", "C4"], ["C1", "C5", "C6"]]
  Set.fromList r2 `elem` expected @?= True

case_echo :: Assertion
case_echo = do
  solver <- SMTLIB2.newSolver
  r <- SMTLIB2.runCommandString solver "(echo \"hello\")"
  showSL r @?= "\"hello\""

case_let :: Assertion
case_let = do
  solver <- SMTLIB2.newSolver
  SMTLIB2.setLogic solver "QF_LRA"
  assertSuccess =<< SMTLIB2.runCommandString solver "(define-fun x () Real (let ((y 1)) (+ y 2)))"
  assertSuccess =<< SMTLIB2.runCommandString solver "(assert (not (= x 3)))"
  r <- SMTLIB2.checkSat solver
  r @?= Unsat

case_delcareSort :: Assertion
case_delcareSort = do
  solver <- SMTLIB2.newSolver
  SMTLIB2.setLogic solver "QF_UFLRA"
  assertSuccess =<< SMTLIB2.runCommandString solver "(declare-sort U 1)"
  assertSuccess =<< SMTLIB2.runCommandString solver "(declare-const x1 (U Real))"
  assertSuccess =<< SMTLIB2.runCommandString solver "(declare-const x2 (U Bool))"

case_defineSort :: Assertion
case_defineSort = do
  solver <- SMTLIB2.newSolver
  SMTLIB2.setLogic solver "QF_UFLRA"
  assertSuccess =<< SMTLIB2.runCommandString solver "(declare-sort U 1)"
  assertSuccess =<< SMTLIB2.runCommandString solver "(define-sort T (X) (U X))"
  assertSuccess =<< SMTLIB2.runCommandString solver "(declare-const x1 (T Real))"
  assertSuccess =<< SMTLIB2.runCommandString solver "(declare-const x2 (T Bool))"

case_defineFun :: Assertion
case_defineFun = do
  solver <- SMTLIB2.newSolver
  SMTLIB2.setOption solver (ProduceModels True ())
  SMTLIB2.setLogic solver "QF_UFLRA"
  assertSuccess =<< SMTLIB2.runCommandString solver "(define-fun f ((b Bool) (x Real)) Bool (ite b (>= x 0) (>= 0 x)))"
  assertSuccess =<< SMTLIB2.runCommandString solver "(declare-const bb Bool)"
  assertSuccess =<< SMTLIB2.runCommandString solver "(declare-const xx Real)"
  assertSuccess =<< SMTLIB2.runCommandString solver "(assert (>= xx 100))"
  assertSuccess =<< SMTLIB2.runCommandString solver "(assert (f bb xx))"
  r <- SMTLIB2.checkSat solver
  r @?= Sat
  r2 <- SMTLIB2.runCommandString solver "(get-value (bb))"
  showSL r2 @?= "((bb true))"

case_getInfo :: Assertion
case_getInfo = do
  solver <- SMTLIB2.newSolver
  _ <- SMTLIB2.getInfo solver (ErrorBehaviorFlag ())
  _ <- SMTLIB2.getInfo solver (InfoName ())
  _ <- SMTLIB2.getInfo solver (Authors ())
  _ <- SMTLIB2.getInfo solver (InfoVersion ())
  return ()

case_setInfo :: Assertion
case_setInfo = do
  solver <- SMTLIB2.newSolver
  assertSuccess =<< SMTLIB2.runCommandString solver "(set-info :status sat)"
  assertSuccess =<< SMTLIB2.runCommandString solver "(set-info :status unsat)"
  assertSuccess =<< SMTLIB2.runCommandString solver "(set-info :status unknown)"
  return ()

-- ---------------------------------------------------------------------

assertSuccess :: CommandResponse () -> Assertion
assertSuccess RSuccess = return ()
assertSuccess RUnsupported = assertFailure "unsupported"
assertSuccess (RError str) = assertFailure ("(error " ++ T.unpack str ++ ")")
assertSuccess r = assertFailure (showSL r)

-- ---------------------------------------------------------------------
-- Test harness

smtlib2SolverTestGroup :: TestTree
smtlib2SolverTestGroup = $(testGroupGenerator)