SyGuS (#226)

* What4.Interface improvements.

* Add SyGuS to SMT writer and SMTLib2.

* Parse SMTLib2/SyGuS response.

* Add CVC5 SyGuS support.

* Add Z3 CHC support.

* Add test.

* Address comments.

* Fix test.

* Add comment.

* Remove stray comments.

what4/src/What4/Expr/App.hs

@@ -1722,6 +1722,8 @@ testExprSymFnEq f g = testEquality (symFnId f) (symFnId g)
 instance IsSymFn (ExprSymFn t) where
   fnArgTypes = symFnArgTypes
   fnReturnType = symFnReturnType
+  fnTestEquality = testExprSymFnEq
+  fnCompare f g = compareF (symFnId f) (symFnId g)
 
 
 -------------------------------------------------------------------------------

what4/src/What4/Expr/Builder.hs

@@ -134,6 +134,8 @@ module What4.Expr.Builder
   , SymFnInfo(..)
   , symFnArgTypes
   , symFnReturnType
+  , SomeExprSymFn(..)
+  , ExprSymFnWrapper(..)
 
     -- * SymbolVarBimap
   , SymbolVarBimap
@@ -247,19 +249,19 @@ import           What4.Utils.StringLiteral
 toDouble :: Rational -> Double
 toDouble = fromRational
 
-cachedEval :: (HashableF k, TestEquality k)
+cachedEval :: (HashableF k, TestEquality k, MonadIO m)
            => PH.HashTable RealWorld k a
            -> k tp
-           -> IO (a tp)
-           -> IO (a tp)
+           -> m (a tp)
+           -> m (a tp)
 cachedEval tbl k action = do
-  mr <- stToIO $ PH.lookup tbl k
+  mr <- liftIO $ stToIO $ PH.lookup tbl k
   case mr of
     Just r -> return r
     Nothing -> do
       r <- action
       seq r $ do
-      stToIO $ PH.insert tbl k r
+      liftIO $ stToIO $ PH.insert tbl k r
       return r
 
 ------------------------------------------------------------------------
@@ -319,7 +321,19 @@ instance HashableF (MatlabFnWrapper t) where
 data ExprSymFnWrapper t c
    = forall a r . (c ~ (a ::> r)) => ExprSymFnWrapper (ExprSymFn t a r)
 
-data SomeSymFn sym = forall args ret . SomeSymFn (SymFn sym args ret)
+data SomeExprSymFn t = forall args ret . SomeExprSymFn (ExprSymFn t args ret)
+
+instance Eq (SomeExprSymFn t) where
+  (SomeExprSymFn fn1) == (SomeExprSymFn fn2) =
+    isJust $ fnTestEquality fn1 fn2
+
+instance Ord (SomeExprSymFn t) where
+  compare (SomeExprSymFn fn1) (SomeExprSymFn fn2) =
+    toOrdering $ fnCompare fn1 fn2
+
+instance Show (SomeExprSymFn t) where
+  show (SomeExprSymFn f) = show f
+
 
 ------------------------------------------------------------------------
 -- ExprBuilder
@@ -751,12 +765,12 @@ betaReduce sym f args =
 --
 -- It is used when an action may modify a value, and we only want to run a
 -- second action if the value changed.
-runIfChanged :: Eq e
+runIfChanged :: (Eq e, Monad m)
              => e
-             -> (e -> IO e) -- ^ First action to run
+             -> (e -> m e) -- ^ First action to run
              -> r           -- ^ Result if no change.
-             -> (e -> IO r) -- ^ Second action to run
-             -> IO r
+             -> (e -> m r) -- ^ Second action to run
+             -> m r
 runIfChanged x f unChanged onChange = do
   y <- f x
   if x == y then
@@ -807,11 +821,14 @@ evalSimpleFn :: EvalHashTables t
              -> ExprBuilder t st fs
              -> ExprSymFn t idx ret
              -> IO (Bool,ExprSymFn t idx ret)
-evalSimpleFn tbl sym f =
+evalSimpleFn tbl sym f = do
+  let n = symFnId f
   case symFnInfo f of
-    UninterpFnInfo{} -> return (False, f)
+    UninterpFnInfo{} -> do
+      CachedSymFn changed f' <- cachedEval (fnTable tbl) n $
+        return $! CachedSymFn False f
+      return (changed, f')
     DefinedFnInfo vars e evalFn -> do
-      let n = symFnId f
       let nm = symFnName f
       CachedSymFn changed f' <-
         cachedEval (fnTable tbl) n $ do
@@ -4028,6 +4045,30 @@ instance IsSymExprBuilder (ExprBuilder t st fs) where
        evalMatlabSolverFn f sym args
      _ -> sbNonceExpr sym $! FnApp fn args
 
+  substituteBoundVars sym subst e = do
+    tbls <- stToIO $ do
+      expr_tbl <- PH.newSized $ PM.size subst
+      fn_tbl <- PH.new
+      PM.traverseWithKey_ (PH.insert expr_tbl . BoundVarExpr) subst
+      return $ EvalHashTables
+        { exprTable = expr_tbl
+        , fnTable  = fn_tbl
+        }
+    evalBoundVars' tbls sym e
+
+  substituteSymFns sym subst e = do
+    tbls <- stToIO $ do
+      expr_tbl <- PH.new
+      fn_tbl <- PH.newSized $ PM.size subst
+      PM.traverseWithKey_
+        (\(SymFnWrapper f) (SymFnWrapper g) -> PH.insert fn_tbl (symFnId f) (CachedSymFn True g))
+        subst
+      return $ EvalHashTables
+        { exprTable = expr_tbl
+        , fnTable  = fn_tbl
+        }
+    evalBoundVars' tbls sym e
+
 
 instance IsInterpretedFloatExprBuilder (ExprBuilder t st fs) => IsInterpretedFloatSymExprBuilder (ExprBuilder t st fs)
 

what4/src/What4/Interface.hs

@@ -38,6 +38,12 @@ provide several type family definitions and class instances for @sym@:
 
   [@instance 'HashableF' ('SymExpr' sym)@]
 
+  [@instance 'OrdF' ('BoundVar' sym)@]
+
+  [@instance 'TestEquality' ('BoundVar' sym)@]
+
+  [@instance 'HashableF' ('BoundVar' sym)@]
+
 The canonical implementation of these interface classes is found in "What4.Expr.Builder".
 -}
 {-# LANGUAGE CPP #-}
@@ -72,6 +78,8 @@ module What4.Interface
     -- ** Expression recognizers
   , IsExpr(..)
   , IsSymFn(..)
+  , SomeSymFn(..)
+  , SymFnWrapper(..)
   , UnfoldPolicy(..)
   , shouldUnfold
 
@@ -202,6 +210,7 @@ import           Data.Parameterized.Classes
 import qualified Data.Parameterized.Context as Ctx
 import           Data.Parameterized.Ctx
 import           Data.Parameterized.Utils.Endian (Endian(..))
+import           Data.Parameterized.Map (MapF)
 import           Data.Parameterized.NatRepr
 import           Data.Parameterized.TraversableFC
 import qualified Data.Parameterized.Vector as Vector
@@ -587,7 +596,7 @@ instance (HashableF (SymExpr sym), TestEquality (SymExpr sym)) => Hashable (SymN
 -- of an undefined function is _not_ guaranteed to be equivalant to a free
 -- constant, and no guarantees are made about what properties such values
 -- will satisfy.
-class ( IsExpr (SymExpr sym), HashableF (SymExpr sym)
+class ( IsExpr (SymExpr sym), HashableF (SymExpr sym), HashableF (BoundVar sym)
       , TestEquality (SymAnnotation sym), OrdF (SymAnnotation sym)
       , HashableF (SymAnnotation sym)
       ) => IsExprBuilder sym where
@@ -2718,14 +2727,42 @@ iteList ite sym ((mp,mx):xs) def =
 -- 'IsSymExprBuilder'.
 type family SymFn sym :: Ctx BaseType -> BaseType -> Type
 
+data SomeSymFn sym = forall args ret . SomeSymFn (SymFn sym args ret)
+
+-- | Wrapper for `SymFn` that concatenates the arguments and the return types.
+--
+-- This is useful for implementing `TestEquality` and `OrdF` instances for
+-- `SymFn`, and for using `SymFn` as a key or a value in a `MapF`.
+data SymFnWrapper sym ctx where
+  SymFnWrapper :: forall sym args ret . SymFn sym args ret -> SymFnWrapper sym (args ::> ret)
+
+instance IsSymFn (SymFn sym) => TestEquality (SymFnWrapper sym) where
+  testEquality (SymFnWrapper fn1) (SymFnWrapper fn2) = fnTestEquality fn1 fn2
+
+instance IsSymFn (SymFn sym) => OrdF (SymFnWrapper sym) where
+  compareF (SymFnWrapper fn1) (SymFnWrapper fn2) = fnCompare fn1 fn2
+
 -- | A class for extracting type representatives from symbolic functions
-class IsSymFn fn where
+class IsSymFn (fn :: Ctx BaseType -> BaseType -> Type) where
   -- | Get the argument types of a function.
   fnArgTypes :: fn args ret -> Ctx.Assignment BaseTypeRepr args
 
   -- | Get the return type of a function.
   fnReturnType :: fn args ret -> BaseTypeRepr ret
 
+  -- | Test whether two functions are equal.
+  --
+  -- The implementation may be incomplete, that is, if it returns `Just` then
+  -- the functions are equal, while if it returns `Nothing` then the functions
+  -- may or may not be equal. The result of `freshTotalUninterpFn` or
+  -- `definedFn` tests equal with itself.
+  fnTestEquality :: fn args1 ret1 -> fn args2 ret2 -> Maybe ((args1 ::> ret1) :~: (args2 ::> ret2))
+
+  -- | Compare two functions for ordering.
+  --
+  -- The underlying equality test is provided by `fnTestEquality`.
+  fnCompare :: fn args1 ret1 -> fn args2 ret2 -> OrderingF (args1 ::> ret1) (args2 ::> ret2)
+
 
 -- | Describes when we unfold the body of defined functions.
 data UnfoldPolicy
@@ -2769,6 +2806,7 @@ instance Show InvalidRange where
 class ( IsExprBuilder sym
       , IsSymFn (SymFn sym)
       , OrdF (SymExpr sym)
+      , OrdF (BoundVar sym)
       ) => IsSymExprBuilder sym where
 
   ----------------------------------------------------------------------
@@ -2914,6 +2952,22 @@ class ( IsExprBuilder sym
                 -- ^ Arguments to function
              -> IO (SymExpr sym ret)
 
+  -- | Apply a variable substitution (variable to symbolic expression mapping)
+  -- to a symbolic expression.
+  substituteBoundVars ::
+    sym ->
+    MapF (BoundVar sym) (SymExpr sym) ->
+    SymExpr sym tp ->
+    IO (SymExpr sym tp)
+
+  -- | Apply a function substitution (function to function mapping) to a
+  -- symbolic expression.
+  substituteSymFns ::
+    sym ->
+    MapF (SymFnWrapper sym) (SymFnWrapper sym) ->
+    SymExpr sym tp ->
+    IO (SymExpr sym tp)
+
 -- | This returns true if the value corresponds to a concrete value.
 baseIsConcrete :: forall e bt
                 . IsExpr e