Source

z3-haskell / examples / monad / ToSMTLib.hs

module Main where

import Control.Applicative
import Control.Monad ( join )
import Control.Monad.Trans
import Data.Maybe
import qualified Data.Traversable as T

import Z3.Monad


script :: Z3 String
script = do
  intSort <- mkIntSort
  q1 <- flip mkConst intSort =<< mkStringSymbol "q1"
  q2 <- flip mkConst intSort =<< mkStringSymbol "q2"
  q3 <- flip mkConst intSort =<< mkStringSymbol "q3"
  q4 <- flip mkConst intSort =<< mkStringSymbol "q4"
  _1 <- mkInt 1
  _4 <- mkInt 4
  -- the ith-queen is in the ith-row.
  -- qi is the column of the ith-queen
  as1 <- mkAnd =<< T.sequence [mkLe _1 q1, mkLe q1 _4]
  as2 <- mkAnd =<< T.sequence [mkLe _1 q2, mkLe q2 _4]
  as3 <- mkAnd =<< T.sequence [mkLe _1 q3, mkLe q3 _4]
  as4 <- mkAnd =<< T.sequence [mkLe _1 q4, mkLe q4 _4]
  -- different columns
  as5 <- mkDistinct [q1,q2,q3,q4]
  -- avoid diagonal attacks
  as6 <- mkNot =<< diagonal 1 q1 q2
  as7 <- mkNot =<< diagonal 2 q1 q3
  as8 <- mkNot =<< diagonal 3 q1 q4
  as9 <- mkNot =<< diagonal 1 q2 q3
  as10 <- mkNot =<< diagonal 2 q2 q4
  as11 <- mkNot =<< diagonal 1 q3 q4
  -- SMTLib script
  _true <- mkTrue
  benchmarkToSMTLibString "queens" "QF_LIA" "unknown" ""
                          [as1,as2,as3,as4,as5,as6,as7,as8,as9,as10,as11]
                          _true
  where mkAbs :: AST -> Z3 AST
        mkAbs x = do
          _0 <- mkInt 0
          join $ mkIte <$> mkLe _0 x <*> pure x <*> mkUnaryMinus x
        diagonal d c c' =
          join $ mkEq <$> (mkAbs =<< mkSub [c',c]) <*> (mkInt d)

main = evalZ3 script >>= putStrLn
Tip: Filter by directory path e.g. /media app.js to search for public/media/app.js.
Tip: Use camelCasing e.g. ProjME to search for ProjectModifiedEvent.java.
Tip: Filter by extension type e.g. /repo .js to search for all .js files in the /repo directory.
Tip: Separate your search with spaces e.g. /ssh pom.xml to search for src/ssh/pom.xml.
Tip: Use ↑ and ↓ arrow keys to navigate and return to view the file.
Tip: You can also navigate files with Ctrl+j (next) and Ctrl+k (previous) and view the file with Ctrl+o.
Tip: You can also navigate files with Alt+j (next) and Alt+k (previous) and view the file with Alt+o.