Unsatisfiable side condition involving \forall: add translatePredicateForall (#2181)

* translateQuantifier

* translatePredicateForall

* Add test

* Remove smt-transcript

* Use $KORE_EXEC in the test

* rename symbol

* remove smt-transcript

* Check K definition and spec instead

* Actually add files

* Change spec

* Add parentheses

* Remove p

* translatePredicateWith: Move sort translation into translateQuantifier

Co-authored-by: Thomas Tuegel <thomas.tuegel@runtimeverification.com>

Author: andreiburdusa

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

@@ -139,7 +139,9 @@ translatePredicateWith translateTerm predicate =
                 translatePredicateExists exists'
                 <|> translateUninterpreted SMT.tBool pat
             FloorF _ -> translateUninterpreted SMT.tBool pat
-            ForallF _ -> translateUninterpreted SMT.tBool pat
+            ForallF forall' ->
+                translatePredicateForall forall'
+                <|> translateUninterpreted SMT.tBool pat
             InF _ -> translateUninterpreted SMT.tBool pat
 
             -- Invalid: no translation, should not occur in predicates
@@ -258,34 +260,38 @@ translatePredicateWith translateTerm predicate =
     translatePredicateExists
         :: Exists Sort variable p -> Translator m variable SExpr
     translatePredicateExists Exists { existsVariable, existsChild } =
-        existsBuiltinSort <|> existsConstructorSort
-      where
-        existsBuiltinSort = case getHook of
-            Just builtinSort
-              | builtinSort == Builtin.Bool.sort
-              -> translateExists SMT.tBool existsVariable existsChild
-              | builtinSort == Builtin.Int.sort
-              -> translateExists SMT.tInt existsVariable existsChild
-            _ -> empty
-        existsConstructorSort = do
-            smtSort <- hoistMaybe $ translateSort varSort
-            translateExists smtSort existsVariable existsChild
-        varSort = variableSort existsVariable
-        tools :: SmtMetadataTools Attribute.Symbol
-        tools = given
-        Attribute.Sort { hook = Hook { getHook } } =
-            sortAttributes tools varSort
-
-    translateExists
-        :: SExpr -> ElementVariable variable -> p -> Translator m variable SExpr
-    translateExists varSort var predTerm
-      = do
+        translateQuantifier SMT.existsQ existsVariable existsChild
+
+    translatePredicateForall
+        :: Forall Sort variable p -> Translator m variable SExpr
+    translatePredicateForall Forall { forallVariable, forallChild } =
+        translateQuantifier SMT.forallQ forallVariable forallChild
+
+    translateQuantifier
+        :: ([SExpr] -> SExpr -> SExpr)
+        -> ElementVariable variable
+        -> p
+        -> Translator m variable SExpr
+    translateQuantifier quantifier var predTerm = do
+        smtSort <- translateVariableSort
         oldVar <- State.gets (Map.lookup var . quantifiedVars)
-        smtVar <- translateTerm varSort (QuantifiedVariable var)
+        smtVar <- translateTerm smtSort (QuantifiedVariable var)
         smtPred <- translatePredicatePattern predTerm
         field @"quantifiedVars" Lens.%=
             maybe (Map.delete var) (Map.insert var) oldVar
-        return $ SMT.existsQ [SMT.List [smtVar, varSort]] smtPred
+        return $ quantifier [SMT.List [smtVar, smtSort]] smtPred
+      where
+        Variable { variableSort } = var
+        translateVariableSort =
+            case getHook of
+              Just builtinSort
+                | builtinSort == Builtin.Bool.sort -> pure SMT.tBool
+                | builtinSort == Builtin.Int.sort  -> pure SMT.tInt
+              _ -> translateSort variableSort & hoistMaybe
+        tools :: SmtMetadataTools Attribute.Symbol
+        tools = given
+        Attribute.Sort { hook = Hook { getHook } } =
+            sortAttributes tools variableSort
 
     translatePattern :: Sort -> p -> Translator m variable SExpr
     translatePattern sort pat =

test/issue-2138/Makefile

@@ -0,0 +1 @@
+include $(CURDIR)/../include.mk

test/issue-2138/issue-2138-spec.k

@@ -0,0 +1,12 @@
+module VERIFICATION
+  import TEST
+endmodule
+
+module ISSUE-2138-SPEC
+  import VERIFICATION
+
+  rule
+    <k> #assert i ( 1 , 0 ) ==Int 0 => . </k>
+      requires true #And ( #Forall X. { i ( X, 0 ) #Equals 0 } )
+
+endmodule

test/issue-2138/issue-2138-spec.k.out.golden

@@ -0,0 +1 @@
+#Top

test/issue-2138/test.k

@@ -0,0 +1,19 @@
+module TEST
+    imports BOOL
+    imports INT
+
+    syntax Exp ::= Int | Bool
+                 | pair(Int, Int) [klabel(pair), symbol]
+
+    syntax KItem ::= "#assume" Exp [klabel(assume), symbol]
+    rule #assume true => .K
+    rule #assume false => #Bottom
+
+    syntax KItem ::= "#assert" Exp  [klabel(assert), symbol]
+                   | "#fail"
+    rule #assert true => .K
+    rule #assert false => #fail
+
+// Uninterpreted functions
+    syntax Int ::= i(Int, Int)   [function, functional, no-evaluators, smtlib(fi), klabel(i)]
+endmodule