Improve

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
       {

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 ...).
 

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)