Add ProblemFeature values for tracking the use of

uninterpreted and defined functions.

Use these to enhance the information collected in `VarIdentification`.

Fixes #139

what4/src/What4/Expr/VarIdentification.hs

@@ -361,10 +361,14 @@ recordExprVars _ (BoundVarExpr info) = do
 recordFnVars :: ExprSymFn t args ret -> VarRecorder s t ()
 recordFnVars f = do
   case symFnInfo f of
-    UninterpFnInfo{}  -> return ()
-    DefinedFnInfo _ d _ -> recordExprVars ExistsForall d
-    MatlabSolverFnInfo _ _ d -> recordExprVars ExistsForall d
-
+    UninterpFnInfo{}  ->
+      addFeatures useUninterpFunctions
+    DefinedFnInfo _ d _ ->
+      do addFeatures useDefinedFunctions
+         recordExprVars ExistsForall d
+    MatlabSolverFnInfo _ _ d ->
+      do addFeatures useDefinedFunctions
+         recordExprVars ExistsForall d
 
 -- | Recurse through the variables in the element, adding bound variables
 -- as both exist and forall vars.
@@ -386,7 +390,6 @@ recurseNonceAppVars scope ea0 = do
     ArrayTrueOnEntries f a -> do
       recordFnVars f
       recordExprVars scope a
-
     FnApp f a -> do
       recordFnVars f
       traverseFC_ (recordExprVars scope) a

what4/src/What4/ProblemFeatures.hs

@@ -22,6 +22,8 @@
 -- 10 : Uses floating-point
 -- 11 : Computes UNSAT cores
 -- 12 : Computes UNSAT assumptions
+-- 13 : Uses uninterpreted functions
+-- 14 : Uses defined functions
 ------------------------------------------------------------------------
 
 {-# LANGUAGE GeneralizedNewtypeDeriving #-}
@@ -41,6 +43,8 @@ module What4.ProblemFeatures
   , useFloatingPoint
   , useUnsatCores
   , useUnsatAssumptions
+  , useUninterpFunctions
+  , useDefinedFunctions
   , hasProblemFeature
   ) where
 
@@ -116,5 +120,18 @@ useUnsatCores = ProblemFeatures 0x800
 useUnsatAssumptions :: ProblemFeatures
 useUnsatAssumptions = ProblemFeatures 0x1000
 
+-- | Indicates if the solver is able and configured to use
+--   uninterpreted functions.
+useUninterpFunctions :: ProblemFeatures
+useUninterpFunctions = ProblemFeatures 0x2000
+
+-- | Indicates if the solver is able and configured to use
+--   defined functions.
+useDefinedFunctions :: ProblemFeatures
+useDefinedFunctions = ProblemFeatures 0x4000
+
+-- | Tests if one set of problem features subsumes another.
+--   In particular, @hasProblemFeature x y@ is true iff
+--   the set of features in @x@ is a superset of those in @y@.
 hasProblemFeature :: ProblemFeatures -> ProblemFeatures -> Bool
 hasProblemFeature x y = (x .&. y) == y