Infer that terms are defined to send to SMT solver (#2292)

* Mock SMT env: add function for declaring arbitrary symbols

* Separate translatePattern from translatePredicateWith

* Export translatePattern, add warning

* Test pattern translator, add tests for expected behavior

* Fix nesting in expected result

* Make Translator a newtype; change test data

* Translator: use RWST instead of StateT

* Add TranslatorEnv as Reader of Translator; use it to send defined patts to SMT

* Comment out failing tests

* Switch env to True whenever we find Defined at top

* Clean-up

* Add documentation

* Update kore/src/Kore/Step/SMT/Translate.hs

Co-authored-by: Thomas Tuegel <[email protected]>

* Address review comment

* Add MonadSimplify instance

Co-authored-by: Thomas Tuegel <[email protected]>
Co-authored-by: Thomas Tuegel <[email protected]>

Author: ana-pantilie

kore/src/Kore/Step/SMT/Evaluator.hs

@@ -19,7 +19,6 @@ import Prelude.Kore
 
 import Control.Error
     ( MaybeT
-    , hoistMaybe
     , runMaybeT
     )
 import qualified Control.Lens as Lens
@@ -194,7 +193,7 @@ decidePredicate predicates =
     -- | Run the SMT query once.
     query :: MaybeT simplifier Result
     query =
-        SMT.withSolver $ evalTranslator $ do
+        SMT.withSolver . evalTranslator $ do
             tools <- Simplifier.askMetadataTools
             predicates' <- traverse (translatePredicate tools) predicates
             traverse_ SMT.assert predicates'
@@ -215,7 +214,7 @@ translatePredicate
         )
     => SmtMetadataTools Attribute.Symbol
     -> Predicate variable
-    -> Translator m variable SExpr
+    -> Translator variable m SExpr
 translatePredicate tools predicate =
     give tools $ translatePredicateWith translateTerm predicate
 
@@ -226,7 +225,7 @@ translateTerm
     => MonadLog m
     => SExpr  -- ^ type name
     -> TranslateItem variable  -- ^ uninterpreted pattern
-    -> Translator m variable SExpr
+    -> Translator variable m SExpr
 translateTerm smtType (QuantifiedVariable var) = do
     n <- Counter.increment
     let varName = "<" <> Text.pack (show n) <> ">"
@@ -277,24 +276,25 @@ lookupVariable
     :: InternalVariable variable
     => Monad m
     => TermLike.ElementVariable variable
-    -> Translator m variable SExpr
+    -> Translator variable m SExpr
 lookupVariable var =
     lookupQuantifiedVariable <|> lookupFreeVariable
   where
     lookupQuantifiedVariable = do
         TranslatorState { quantifiedVars } <- State.get
-        hoistMaybe $ SMT.Atom . smtName <$> Map.lookup var quantifiedVars
+        maybeToTranslator
+            $ SMT.Atom . smtName <$> Map.lookup var quantifiedVars
     lookupFreeVariable = do
         TranslatorState { freeVars} <- State.get
-        hoistMaybe $ Map.lookup var freeVars
+        maybeToTranslator $ Map.lookup var freeVars
 
 declareVariable
     :: InternalVariable variable
     => SMT.MonadSMT m
     => MonadLog m
     => SExpr  -- ^ type name
     -> TermLike.ElementVariable variable  -- ^ variable to be declared
-    -> Translator m variable SExpr
+    -> Translator variable m SExpr
 declareVariable t variable = do
     n <- Counter.increment
     let varName = "<" <> Text.pack (show n) <> ">"
@@ -308,7 +308,7 @@ logVariableAssignment
     => MonadLog m
     => Counter.Natural
     -> TermLike variable  -- ^ variable to be declared
-    -> Translator m variable ()
+    -> Translator variable m ()
 logVariableAssignment n pat =
     logDebug
     . Text.pack . show

kore/src/Kore/Step/SMT/Lemma.hs

@@ -100,7 +100,7 @@ translateUninterpreted
        )
     => SExpr  -- ^ type name
     -> TranslateItem variable -- ^ uninterpreted pattern
-    -> Translator m variable SExpr
+    -> Translator variable m SExpr
 translateUninterpreted _ (QuantifiedVariable _) =
     empty
 translateUninterpreted t (UninterpretedTerm pat)