From 7a98abea1d8ba6234574bdc1d162dbf9e6353404 Mon Sep 17 00:00:00 2001
From: Rob Dockins <rdockins@galois.com>
Date: Thu, 1 Jul 2021 15:18:07 -0700
Subject: [PATCH] Add a new experimental `term_theories` operation.

Evaluates a term into a proof obligation via What4 and examines
what logical theories would be required to attempt a proof
of the property.  The names of the required theories are computed
and returned to the user.
---
 src/SAWScript/Builtins.hs     |  8 ++++++++
 src/SAWScript/Interpreter.hs  | 16 ++++++++++++++++
 src/SAWScript/Prover/What4.hs | 36 +++++++++++++++++++++++++++++++++--
 3 files changed, 58 insertions(+), 2 deletions(-)

diff --git a/src/SAWScript/Builtins.hs b/src/SAWScript/Builtins.hs
index d80b209c93..e9417d39bd 100644
--- a/src/SAWScript/Builtins.hs
+++ b/src/SAWScript/Builtins.hs
@@ -1290,6 +1290,14 @@ eval_list t = do
   ts <- io $ traverse (scAt sc n' a' (ttTerm t)) idxs
   return (map (TypedTerm (TypedTermSchema (C.tMono a))) ts)
 
+term_theories :: [String] -> TypedTerm -> TopLevel [String]
+term_theories unints t = do
+  sc <- getSharedContext
+  unintSet <- resolveNames unints
+  hashConsing <- gets SV.rwWhat4HashConsing
+  prop <- io (predicateToProp sc Universal (ttTerm t))
+  Prover.what4Theories unintSet hashConsing prop
+
 default_typed_term :: TypedTerm -> TopLevel TypedTerm
 default_typed_term tt = do
   sc <- getSharedContext
diff --git a/src/SAWScript/Interpreter.hs b/src/SAWScript/Interpreter.hs
index e75ae5e5cd..fc2b49e190 100644
--- a/src/SAWScript/Interpreter.hs
+++ b/src/SAWScript/Interpreter.hs
@@ -929,6 +929,22 @@ primitives = Map.fromList
     , "variables."
     ]
 
+  , prim "term_theories" "[String] -> Term -> [String]"
+    (funVal2 term_theories)
+    Experimental
+    [ "Given a term of type \'Bool\', compute the SMT theories required"
+    , "to reason about this term. The functions (if any) given in the"
+    , "first argument will be treated as uninterpreted."
+    , ""
+    , "If the returned list is empty, the given term represents a problem"
+    , "that can be solved purely by boolean SAT reasoning."
+    , ""
+    , "Note: the given term will be simplified using the What4 backend"
+    , "before evaluating what theories are required.  For simple problems,"
+    , "this may simplify away some aspects of the problem altogether and may result"
+    , "in requiring fewer theories than one might expect."
+    ]
+
   , prim "default_term" "Term -> Term"
     (funVal1 default_typed_term)
     Experimental
diff --git a/src/SAWScript/Prover/What4.hs b/src/SAWScript/Prover/What4.hs
index 7c0c334ef9..6e62ab659c 100644
--- a/src/SAWScript/Prover/What4.hs
+++ b/src/SAWScript/Prover/What4.hs
@@ -6,10 +6,11 @@
 
 module SAWScript.Prover.What4 where
 
-import System.IO
 
+import           Control.Lens ((^.))
 import           Data.Set (Set)
 import qualified Data.Map as Map
+import           System.IO
 
 import Verifier.SAW.SharedTerm
 import Verifier.SAW.FiniteValue
@@ -19,12 +20,14 @@ import           SAWScript.Proof(Prop, propToSATQuery, propSize, CEX)
 import           SAWScript.Prover.SolverStats
 import           SAWScript.Value (TopLevel, io, getSharedContext)
 
-import Data.Parameterized.Nonce
+import           Data.Parameterized.Nonce
 
 import           What4.Config
 import           What4.Solver
 import           What4.Interface
 import           What4.Expr.GroundEval
+import           What4.Expr.VarIdentification
+import           What4.ProblemFeatures
 import qualified Verifier.SAW.Simulator.What4 as W
 import           Verifier.SAW.Simulator.What4.FirstOrder
 import qualified What4.Expr.Builder as B
@@ -47,6 +50,35 @@ setupWhat4_sym hashConsing =
      _ <- setOpt cacheTermsSetting hashConsing
      return sym
 
+what4Theories ::
+  Set VarIndex ->
+  Bool ->
+  Prop ->
+  TopLevel [String]
+what4Theories unintSet hashConsing goal =
+  getSharedContext >>= \sc -> io $
+  do sym <- setupWhat4_sym hashConsing
+     satq <- propToSATQuery sc unintSet goal
+     (_varMap, lit) <- W.w4Solve sym sc satq
+     let pf = (predicateVarInfo lit)^.problemFeatures
+     return (evalTheories pf)
+
+evalTheories :: ProblemFeatures -> [String]
+evalTheories pf = [ nm | (nm,f) <- xs, hasProblemFeature pf f ]
+ where
+  xs = [ ("LinearArithmetic", useLinearArithmetic)
+       , ("NonlinearArithmetic", useNonlinearArithmetic)
+       , ("TranscendentalFunctions", useComputableReals)
+       , ("Integers", useIntegerArithmetic)
+       , ("Bitvectors", useBitvectors)
+       , ("ExistsForall", useExistForall)
+       , ("FirstOrderQuantifiers", useQuantifiers)
+       , ("Arrays", useSymbolicArrays)
+       , ("Structs", useStructs)
+       , ("Strings", useStrings)
+       , ("FloatingPoint", useFloatingPoint)
+       ]
+
 proveWhat4_sym ::
   SolverAdapter St ->
   Set VarIndex ->