From 0b21354cec17130d369be7e5244d8cf4cc5d6fcb Mon Sep 17 00:00:00 2001
From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Fri, 1 Mar 2024 08:15:20 -0600
Subject: [PATCH] Improve

---
 src/cmd_parser.cpp         | 17 +++++++++++++++--
 src/state.cpp              |  3 ++-
 tests/conclusion-spec.smt3 |  5 ++++-
 3 files changed, 21 insertions(+), 4 deletions(-)

diff --git a/src/cmd_parser.cpp b/src/cmd_parser.cpp
index c9e70882..1cf76759 100644
--- a/src/cmd_parser.cpp
+++ b/src/cmd_parser.cpp
@@ -323,15 +323,28 @@ bool CmdParser::parseNextCommand()
         // parse requirements, optionally
         if (keyword=="requires")
         {
+          // we support alf.conclusion in requirements
+          d_state.pushScope();
+          d_state.bind("alf.conclusion", d_state.mkConclusion());
+          // parse the expression pair list
           reqs = d_eparser.parseExprPairList();
           keyword = d_eparser.parseKeyword();
+          d_state.popScope();
         }
         // parse conclusion
-        if (keyword!="conclusion")
+        if (keyword=="conclusion")
+        {
+          conc = d_eparser.parseExpr();
+        }
+        else if (keyword=="conclusion-given")
+        {
+          // :conclusion-given is equivalent to :conclusion alf.conclusion
+          conc = d_state.mkConclusion();
+        }
+        else
         {
           d_lex.parseError("Expected conclusion in declare-rule");
         }
-        conc = d_eparser.parseExpr();
       }
       else
       {
diff --git a/src/state.cpp b/src/state.cpp
index d4d81ec5..0ef4a381 100644
--- a/src/state.cpp
+++ b/src/state.cpp
@@ -87,7 +87,8 @@ State::State(Options& opts, Stats& stats)
   d_self = Expr(mkSymbolInternal(Kind::PARAM, "alf.self", mkAbstractType()));
   bind("alf.self", d_self);
   d_conclusion = Expr(mkSymbolInternal(Kind::PARAM, "alf.conclusion", mkBoolType()));
-  bind("alf.conclusion", d_conclusion);
+  // alf.conclusion is not globally bound, since it can only appear
+  // in :requires.
 
   // note we don't allow parsing (Proof ...), (Quote ...), or (quote ...).
 
diff --git a/tests/conclusion-spec.smt3 b/tests/conclusion-spec.smt3
index 3d341720..2c0fcb36 100644
--- a/tests/conclusion-spec.smt3
+++ b/tests/conclusion-spec.smt3
@@ -11,7 +11,10 @@
 
 (declare-rule split ()
   :requires (((is_split alf.conclusion) true))
-  :conclusion alf.conclusion
+  :conclusion-given
 )
 
 (step @p0 (or true (not true)) :rule split)
+
+; fails
+;(step @p1 (or false (not true)) :rule split)