-- A pretty-printer for SMTLIB.

{-# LANGUAGE CPP, OverloadedStrings #-}
module Jukebox.SMTLIB where

#include "errors.h"
import Data.Char
import Text.PrettyPrint.HughesPJ
import Jukebox.Form
import qualified Data.Map.Strict as Map
import qualified Data.Set as Set
import Jukebox.Name
import Jukebox.Utils
import Jukebox.TPTP.Print(prettyNames)
import Text.PrettyPrint.HughesPJClass
import Data.Maybe
import Data.Ratio
#if __GLASGOW_HASKELL__ < 710
import Control.Applicative hiding (empty)
#endif

keywords :: [String]
keywords :: [String]
keywords =
    [ String
"ac"
    , String
"and"
    , String
"axiom"
    , String
"inversion"
    , String
"bit0"
    , String
"bit1"
    , String
"bitv"
    , String
"bool"
    , String
"check"
    , String
"cut"
    , String
"distinct"
    , String
"else"
    , String
"exists"
    , String
"false"
    , String
"forall"
    , String
"function"
    , String
"goal"
    , String
"if"
    , String
"in"
    , String
"include"
    , String
"int"
    , String
"let"
    , String
"logic"
    , String
"not"
    , String
"or"
    , String
"predicate"
    , String
"prop"
    , String
"real"
    , String
"rewriting"
    , String
"then"
    , String
"true"
    , String
"type"
    , String
"unit"
    , String
"void"
    , String
"with"
    , String
"assert", String
"check-sat"
    , String
"abs", String
"min", String
"max", String
"const"
    , String
"mod", String
"div"
    , String
"=", String
"=>", String
"+", String
"-", String
"*", String
">", String
">=", String
"<", String
"<=", String
"@", String
"!"
    , String
"as"
    , String
"declare-datatypes"
    , String
"declare-sort"
    , String
"declare-const"
    , String
"declare-const"
    , String
"declare-fun"
    , String
"declare-fun"
    , String
"define-fun"
    , String
"define-fun"
    , String
"define-fun-rec"
    , String
"define-fun-rec"
    , String
"define-funs-rec"
    , String
"check-sat"
    -- TIP:
    , String
"par"
    , String
"case"
    , String
"match"
    , String
"assert"
    , String
"assert-not"
    -- Z3:
    , String
"Bool", String
"Int", String
"Array", String
"List", String
"insert"
    , String
"isZero"
    , String
"map"
    , String
"select"
    , String
"subset", String
"union", String
"intersect"
    -- CVC4:
    , String
"concat", String
"member", String
"singleton", String
"card"
    ] [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ ((String, String) -> String) -> [(String, String)] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (String, String) -> String
forall a b. (a, b) -> b
snd [(String, String)]
renamings

renamings :: [(String, String)]
renamings :: [(String, String)]
renamings =
  [(String
"$i", String
"individual"),
   (String
"$int", String
"Int"),
   (String
"$rat", String
"Real"),
   (String
"$real", String
"Real"),
   (String
"$sum", String
"+"),
   (String
"$product", String
"*"),
   (String
"$quotient", String
"/"),
   (String
"$difference", String
"-"),
   (String
"$uminus", String
"-"),
   (String
"$is_int", String
"IsInt"),
   (String
"$to_int", String
"to_int"),
   (String
"$to_real", String
"to_real"),
   (String
"$less", String
"<"),
   (String
"$lesseq", String
"<="),
   (String
"$greater", String
">"),
   (String
"$greatereq", String
">=")]

-- Both the following functions expect prettyNames to have been used first
-- (no Unique names).
renameAvoidingKeywords :: Symbolic a => a -> NameM a
renameAvoidingKeywords :: a -> NameM a
renameAvoidingKeywords a
x = do
  -- Allocate a new name for every reserved word
  Map String Name
sub <- [(String, Name)] -> Map String Name
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(String, Name)] -> Map String Name)
-> NameM [(String, Name)] -> NameM (Map String Name)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [NameM (String, Name)] -> NameM [(String, Name)]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence
    [ do Name
n <- String -> NameM Name
forall a. Named a => a -> NameM Name
newName (String
"smt_" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
k)
         (String, Name) -> NameM (String, Name)
forall (m :: * -> *) a. Monad m => a -> m a
return (String
k, Name
n)
    | String
k <- [String]
keywords ]
  a -> NameM a
forall (m :: * -> *) a. Monad m => a -> m a
return ((Name -> Name) -> a -> a
forall a. Symbolic a => (Name -> Name) -> a -> a
mapName (\Name
x -> Name -> String -> Map String Name -> Name
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault Name
x (Name -> String
forall a. Show a => a -> String
show Name
x) Map String Name
sub) a
x)

renameTPTP :: Symbolic a => a -> a
renameTPTP :: a -> a
renameTPTP = (Name -> Name) -> a -> a
forall a. Symbolic a => (Name -> Name) -> a -> a
mapName Name -> Name
f
  where
    f :: Name -> Name
f Name
x = Name -> Maybe Name -> Name
forall a. a -> Maybe a -> a
fromMaybe Name
x ((String -> Name) -> Maybe String -> Maybe Name
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap String -> Name
forall a. Named a => a -> Name
name (String -> [(String, String)] -> Maybe String
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup (Name -> String
forall a. Show a => a -> String
show Name
x) [(String, String)]
renamings))

showProblem :: Problem Form -> String
showProblem :: Problem Form -> String
showProblem = Doc -> String
forall a. Show a => a -> String
show (Doc -> String) -> (Problem Form -> Doc) -> Problem Form -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Problem Form -> Doc
pPrintProblem
    
pPrintProblem :: Problem Form -> Doc
pPrintProblem :: Problem Form -> Doc
pPrintProblem Problem Form
prob0 =
  [Doc] -> Doc
vcat (Problem Form -> [Doc]
pPrintDecls Problem Form
prob [Doc] -> [Doc] -> [Doc]
forall a. [a] -> [a] -> [a]
++ (Input Form -> Doc) -> Problem Form -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map Input Form -> Doc
pPrintInput Problem Form
prob [Doc] -> [Doc] -> [Doc]
forall a. [a] -> [a] -> [a]
++ [[Doc] -> Doc
sexp [Doc
"check-sat"]])
  where
    prob :: Problem Form
prob = Problem Form -> Problem Form
forall a. Symbolic a => a -> a
renameTPTP (Problem Form -> Problem Form
forall a. Symbolic a => a -> a
prettyNames (Problem Form
-> (Problem Form -> NameM (Problem Form)) -> Problem Form
forall a b. Symbolic a => a -> (a -> NameM b) -> b
run (Problem Form -> Problem Form
forall a. Symbolic a => a -> a
prettyNames Problem Form
prob0) Problem Form -> NameM (Problem Form)
forall a. Symbolic a => a -> NameM a
renameAvoidingKeywords))

pPrintDecls :: Problem Form -> [Doc]
pPrintDecls :: Problem Form -> [Doc]
pPrintDecls Problem Form
prob =
  (Type -> Doc) -> [Type] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map Type -> Doc
typeDecl ((Type -> Bool) -> [Type] -> [Type]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> (Type -> Bool) -> Type -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> Bool
forall a. Named a => a -> Bool
builtIn) ([Type] -> [Type]
forall a. Ord a => [a] -> [a]
usort (Problem Form -> [Type]
forall a. Symbolic a => a -> [Type]
types Problem Form
prob))) [Doc] -> [Doc] -> [Doc]
forall a. [a] -> [a] -> [a]
++
  ((Name ::: FunType) -> Doc) -> [Name ::: FunType] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (Name ::: FunType) -> Doc
forall a. Pretty a => (a ::: FunType) -> Doc
funcDecl (((Name ::: FunType) -> Bool)
-> [Name ::: FunType] -> [Name ::: FunType]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool)
-> ((Name ::: FunType) -> Bool) -> (Name ::: FunType) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Name ::: FunType) -> Bool
forall a. Named a => a -> Bool
builtIn) ([Name ::: FunType] -> [Name ::: FunType]
forall a. Ord a => [a] -> [a]
usort (Problem Form -> [Name ::: FunType]
forall a. Symbolic a => a -> [Name ::: FunType]
functions Problem Form
prob)))
  where
    builtIn :: a -> Bool
builtIn a
x =
      (Name -> String
forall a. Show a => a -> String
show (a -> Name
forall a. Named a => a -> Name
name a
x) String -> String -> Bool
forall a. Eq a => a -> a -> Bool
/= String
"individual" Bool -> Bool -> Bool
&& Name -> String
forall a. Show a => a -> String
show (a -> Name
forall a. Named a => a -> Name
name a
x) String -> [String] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` ((String, String) -> String) -> [(String, String)] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (String, String) -> String
forall a b. (a, b) -> b
snd [(String, String)]
renamings) Bool -> Bool -> Bool
||
      case a -> Name
forall a. Named a => a -> Name
name a
x of
        Fixed Integer{} Maybe String
_ -> Bool
True
        Fixed Rational{} Maybe String
_ -> Bool
True
        Fixed Real{} Maybe String
_ -> Bool
True
        Name
_ -> Bool
False

    typeDecl :: Type -> Doc
typeDecl Type
O = Doc
empty
    typeDecl Type
ty =
      [Doc] -> Doc
sexp [Doc
"declare-sort", Type -> Doc
pPrintType Type
ty, String -> Doc
text String
"0"]

    funcDecl :: (a ::: FunType) -> Doc
funcDecl (a
f ::: FunType [Type]
args Type
res) =
      [Doc] -> Doc
sexp ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$
        [Doc
"declare-fun", a -> Doc
forall a. Pretty a => a -> Doc
pPrint a
f, [Doc] -> Doc
sexp ((Type -> Doc) -> [Type] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map Type -> Doc
pPrintType [Type]
args), Type -> Doc
pPrintType Type
res]

sexp :: [Doc] -> Doc
sexp :: [Doc] -> Doc
sexp = Doc -> Doc
parens (Doc -> Doc) -> ([Doc] -> Doc) -> [Doc] -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Doc] -> Doc
fsep

pPrintName :: Name -> Doc
pPrintName :: Name -> Doc
pPrintName (Fixed (Integer Integer
n) Maybe String
_) = Integer -> Doc
forall a. Pretty a => a -> Doc
pPrint Integer
n
pPrintName (Fixed (Rational Rational
n) Maybe String
_) =
  [Doc] -> Doc
sexp [Doc
"/", Integer -> Doc
forall a. Pretty a => a -> Doc
pPrint (Rational -> Integer
forall a. Ratio a -> a
numerator Rational
n), Integer -> Doc
forall a. Pretty a => a -> Doc
pPrint (Rational -> Integer
forall a. Ratio a -> a
denominator Rational
n)]
pPrintName (Fixed (Real Rational
n) Maybe String
_) =
  [Doc] -> Doc
sexp [Doc
"/", Integer -> Doc
forall a. Pretty a => a -> Doc
pPrint (Rational -> Integer
forall a. Ratio a -> a
numerator Rational
n), Integer -> Doc
forall a. Pretty a => a -> Doc
pPrint (Rational -> Integer
forall a. Ratio a -> a
denominator Rational
n)]
pPrintName Name
x = String -> Doc
text (String -> Doc) -> (Name -> String) -> Name -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String
escape (String -> String) -> (Name -> String) -> Name -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> String
forall a. Show a => a -> String
show (Name -> Doc) -> Name -> Doc
forall a b. (a -> b) -> a -> b
$ Name
x
  where
    escape :: String -> String
escape String
xs
      | (Char -> Bool) -> String -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Char -> Bool
isOk String
xs = String
xs
      | Bool
otherwise = String
"|" String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Char -> String) -> String -> String
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Char -> String
escapeSym String
xs String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"|"

    isOk :: Char -> Bool
isOk Char
c
      | Char -> Bool
isAlphaNum Char
c = Bool
True
      | Char
c Char -> String -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` (String
"~!@$%^&*_-+=<>.?/" :: String) = Bool
True
      | Bool
otherwise = Bool
False

    escapeSym :: Char -> String
escapeSym Char
'|' = String
"\\|"
    escapeSym Char
'\\' = String
"\\\\"
    escapeSym Char
c = [Char
c]

pPrintType :: Type -> Doc
pPrintType :: Type -> Doc
pPrintType Type
O = Doc
"Bool"
pPrintType Type
ty = Name -> Doc
pPrintName (Type -> Name
forall a. Named a => a -> Name
name Type
ty)

pPrintInput :: Input Form -> Doc
pPrintInput :: Input Form -> Doc
pPrintInput Input{kind :: forall a. Input a -> Kind
kind = Ax AxKind
_, what :: forall a. Input a -> a
what = Form
form} =
  [Doc] -> Doc
sexp [Doc
"assert", Form -> Doc
pPrintForm Form
form]
pPrintInput Input{kind :: forall a. Input a -> Kind
kind = Conj ConjKind
_, what :: forall a. Input a -> a
what = Form
form} =
  [Doc] -> Doc
sexp [Doc
"assert", [Doc] -> Doc
sexp [Doc
"not", Form -> Doc
pPrintForm Form
form]]

pPrintForm :: Form -> Doc
pPrintForm :: Form -> Doc
pPrintForm (Literal (Pos Atomic
l)) = Atomic -> Doc
pPrintAtomic Atomic
l
pPrintForm (Literal (Neg Atomic
l)) = [Doc] -> Doc
sexp [Doc
"not", Atomic -> Doc
pPrintAtomic Atomic
l]
pPrintForm (Not Form
f) = [Doc] -> Doc
sexp [Doc
"not", Form -> Doc
pPrintForm Form
f]
pPrintForm (And []) = String -> Doc
text String
"true"
pPrintForm (And [Form]
ts) = [Doc] -> Doc
sexp (Doc
"and"Doc -> [Doc] -> [Doc]
forall a. a -> [a] -> [a]
:(Form -> Doc) -> [Form] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map Form -> Doc
pPrintForm [Form]
ts)
pPrintForm (Or []) = String -> Doc
text String
"false"
pPrintForm (Or [Form]
ts) = [Doc] -> Doc
sexp (Doc
"or"Doc -> [Doc] -> [Doc]
forall a. a -> [a] -> [a]
:(Form -> Doc) -> [Form] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map Form -> Doc
pPrintForm [Form]
ts)
pPrintForm (Equiv Form
t Form
u) = [Doc] -> Doc
sexp [Doc
"=", Form -> Doc
pPrintForm Form
t, Form -> Doc
pPrintForm Form
u]
pPrintForm (Connective Connective
Implies Form
t Form
u) = [Doc] -> Doc
sexp [Doc
"=>", Form -> Doc
pPrintForm Form
t, Form -> Doc
pPrintForm Form
u]
pPrintForm (Connective Connective
Follows Form
t Form
u) = [Doc] -> Doc
sexp [Doc
"=>", Form -> Doc
pPrintForm Form
u, Form -> Doc
pPrintForm Form
t]
pPrintForm (Connective Connective
Xor Form
t Form
u) = [Doc] -> Doc
sexp [Doc
"xor", Form -> Doc
pPrintForm Form
t, Form -> Doc
pPrintForm Form
u]
pPrintForm (Connective Connective
Nor Form
t Form
u) = [Doc] -> Doc
sexp [Doc
"not", [Doc] -> Doc
sexp [Doc
"or", Form -> Doc
pPrintForm Form
t, Form -> Doc
pPrintForm Form
u]]
pPrintForm (Connective Connective
Nand Form
t Form
u) = [Doc] -> Doc
sexp [Doc
"not", [Doc] -> Doc
sexp [Doc
"and", Form -> Doc
pPrintForm Form
t, Form -> Doc
pPrintForm Form
u]]
pPrintForm (ForAll (Bind Set Variable
vs Form
f)) = Doc -> Set Variable -> Form -> Doc
pPrintQuant Doc
"forall" Set Variable
vs Form
f
pPrintForm (Exists (Bind Set Variable
vs Form
f)) = Doc -> Set Variable -> Form -> Doc
pPrintQuant Doc
"exists" Set Variable
vs Form
f

pPrintQuant :: Doc -> Set.Set Variable -> Form -> Doc
pPrintQuant :: Doc -> Set Variable -> Form -> Doc
pPrintQuant Doc
q Set Variable
vs Form
f
  | Set Variable -> Bool
forall a. Set a -> Bool
Set.null Set Variable
vs = Form -> Doc
pPrintForm Form
f
  | Bool
otherwise =
    [Doc] -> Doc
sexp [Doc
q,
          [Doc] -> Doc
sexp [[Doc] -> Doc
sexp [Name -> Doc
pPrintName Name
x, Type -> Doc
pPrintType Type
ty] | Name
x ::: Type
ty <- Set Variable -> [Variable]
forall a. Set a -> [a]
Set.toList Set Variable
vs],
          Form -> Doc
pPrintForm Form
f]

pPrintAtomic :: Atomic -> Doc
pPrintAtomic :: Atomic -> Doc
pPrintAtomic (Term
t :=: Term
u) = [Doc] -> Doc
sexp [Doc
"=", Term -> Doc
pPrintTerm Term
t, Term -> Doc
pPrintTerm Term
u]
pPrintAtomic (Tru Term
t) = Term -> Doc
pPrintTerm Term
t

pPrintTerm :: Term -> Doc
pPrintTerm :: Term -> Doc
pPrintTerm (Var (Name
x ::: Type
_)) = Name -> Doc
pPrintName Name
x
pPrintTerm ((Name
f ::: FunType
_) :@: []) = Name -> Doc
pPrintName Name
f
pPrintTerm ((Name
f ::: FunType
_) :@: [Term]
ts) = [Doc] -> Doc
sexp (Name -> Doc
pPrintName Name
fDoc -> [Doc] -> [Doc]
forall a. a -> [a] -> [a]
:(Term -> Doc) -> [Term] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map Term -> Doc
pPrintTerm [Term]
ts)