Add support for cvc5

src/Language/Fixpoint/Smt/Interface.hs

@@ -300,6 +300,10 @@ makeContext' cfg ctxLog
                       Process.defaultConfig
                              { Process.exe = "cvc4"
                              , Process.args = ["--incremental", "-L", "smtlib2"] }
+         Cvc5    -> makeProcess ctxLog $
+                      Process.defaultConfig
+                             { Process.exe = "cvc5"
+                             , Process.args = ["--incremental", "-L", "smtlib2"] }
        solver <- SMTLIB.Backends.initSolver SMTLIB.Backends.Queuing backend
        loud <- isLoud
        return Ctx { ctxSolver  = solver

src/Language/Fixpoint/Smt/Theories.hs

@@ -248,6 +248,10 @@ cvc4Preamble :: Config -> [Builder]
 cvc4Preamble z
   = "(set-logic ALL_SUPPORTED)" : commonPreamble z
 
+cvc5Preamble :: Config -> [Builder]
+cvc5Preamble z
+  = "(set-logic ALL)" : commonPreamble z
+
 commonPreamble :: Config -> [Builder]
 commonPreamble _ --TODO use uif flag u (see z3Preamble)
   = [ bSort string "Int"
@@ -351,6 +355,7 @@ sortAppInfo t = case bkFFunc t of
 preamble :: Config -> SMTSolver -> [Builder]
 preamble u Z3   = z3Preamble u
 preamble u Cvc4 = cvc4Preamble u
+preamble u Cvc5 = cvc5Preamble u
 preamble u _    = commonPreamble u
 
 --------------------------------------------------------------------------------

src/Language/Fixpoint/Types/Config.hs

@@ -144,7 +144,7 @@ instance Read RESTOrdering where
 
 ---------------------------------------------------------------------------------------
 
-data SMTSolver = Z3 | Z3mem | Cvc4 | Mathsat
+data SMTSolver = Z3 | Z3mem | Cvc4 | Cvc5 | Mathsat 
                  deriving (Eq, Data, Typeable, Generic)
 
 instance Default SMTSolver where
@@ -154,6 +154,7 @@ instance Show SMTSolver where
   show Z3      = "z3"
   show Z3mem   = "z3 API"
   show Cvc4    = "cvc4"
+  show Cvc5    = "cvc5"
   show Mathsat = "mathsat"
 
 instance S.Store SMTSolver