{-# 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"
, String
"par"
, String
"case"
, String
"match"
, String
"assert"
, String
"assert-not"
, String
"Bool", String
"Int", String
"Array", String
"List", String
"insert"
, String
"isZero"
, String
"map"
, String
"select"
, String
"subset", String
"union", String
"intersect"
, 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
">=")]
renameAvoidingKeywords :: Symbolic a => a -> NameM a
renameAvoidingKeywords :: forall a. Symbolic a => a -> NameM a
renameAvoidingKeywords a
x = do
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)
forall (m :: * -> *) a. Monad m => [m a] -> m [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 a. a -> NameM a
forall (m :: * -> *) a. Monad m => a -> m a
return (String
k, Name
n)
| String
k <- [String]
keywords ]
a -> NameM a
forall a. 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 :: forall a. Symbolic a => 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 a b. (a -> b) -> Maybe a -> Maybe b
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 a. Eq a => a -> [a] -> 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 a. Eq a => a -> [a] -> 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)