Allow forward declarations of programs

src/cmd_parser.cpp

@@ -598,7 +598,7 @@ bool CmdParser::parseNextCommand()
       }
     }
     break;
-    // (program (<sort>*) <sort> (<sorted_var>*) <term_pair>+)
+    // (program <symbol> (<sorted_var>*) (<sort>*) <sort> (<term_pair>+)?)
     case Token::PROGRAM:
     {
       std::string name = d_eparser.parseSymbol();
@@ -612,53 +612,89 @@ bool CmdParser::parseNextCommand()
       {
         progType = d_state.mkFunctionType(argTypes, retType, false);
       }
-      // the type of the program variable is a function
-      Expr pvar = d_state.mkSymbol(Kind::PROGRAM_CONST, name, progType);
-      // bind the program
-      d_eparser.bind(name, pvar);
-      // parse the body
-      std::vector<Expr> pchildren = d_eparser.parseExprPairList();
-      if (pchildren.empty())
+      // it may have been forward declared
+      Expr pprev = d_state.getVar(name);
+      Expr pvar;
+      if (!pprev.isNull())
       {
-        d_lex.parseError("Expected non-empty list of cases");
-      }
-      // ensure program cases are
-      // (A) applications of the program
-      // (B) have arguments that are not evaluatable
-      for (Expr& p : pchildren)
-      {
-        Expr pc = p[0];
-        if (pc.getKind() != Kind::APPLY || pc[0] != pvar)
+        if (pprev.getKind()!=Kind::PROGRAM_CONST)
+        {
+          std::stringstream ss;
+          ss << "Already declared symbol " << name << " as a non-program";
+          d_lex.parseError(ss.str());
+        }
+        // should not already have a definition
+        Expr prevProg = d_state.getProgram(pprev.getValue());
+        if (!prevProg.isNull())
         {
-          d_lex.parseError("Expected application of program as case");
+          d_lex.parseError("Cannot define program more than once");
         }
-        if (pc.getNumChildren() != argTypes.size() + 1)
+        // it should be a program with the same type
+        d_eparser.typeCheck(pprev, progType);
+        pvar = pprev;
+      }
+      else
+      {
+        // the type of the program variable is a function
+        pvar = d_state.mkSymbol(Kind::PROGRAM_CONST, name, progType);
+        // bind the program, temporarily
+        d_eparser.bind(name, pvar);
+      }
+      Expr program;
+      tok = d_lex.peekToken();
+      // if RPAREN follows, it is a forward declaration, we do not define the program
+      if (tok!=Token::RPAREN)
+      {
+        // parse the body
+        std::vector<Expr> pchildren = d_eparser.parseExprPairList();
+        if (pchildren.empty())
         {
-          d_lex.parseError("Wrong arity for pattern");
+          d_lex.parseError("Expected non-empty list of cases");
         }
-        // ensure some type checking??
-        //d_eparser.typeCheck(pc);
-        // ensure the right hand side is bound by the left hand side
-        std::vector<Expr> bvs = Expr::getVariables(pc);
-        Expr rhs = p[1];
-        d_eparser.ensureBound(rhs, bvs);
-        // TODO: allow variable or default case?
-        for (size_t i = 0, nchildren = pc.getNumChildren(); i < nchildren; i++)
+        // ensure program cases are
+        // (A) applications of the program
+        // (B) have arguments that are not evaluatable
+        for (Expr& p : pchildren)
         {
-          Expr ecc = pc[i];
-          if (ecc.isEvaluatable())
+          Expr pc = p[0];
+          if (pc.getKind() != Kind::APPLY || pc[0] != pvar)
+          {
+            d_lex.parseError("Expected application of program as case");
+          }
+          if (pc.getNumChildren() != argTypes.size() + 1)
+          {
+            d_lex.parseError("Wrong arity for pattern");
+          }
+          // ensure some type checking??
+          //d_eparser.typeCheck(pc);
+          // ensure the right hand side is bound by the left hand side
+          std::vector<Expr> bvs = Expr::getVariables(pc);
+          Expr rhs = p[1];
+          d_eparser.ensureBound(rhs, bvs);
+          // TODO: allow variable or default case?
+          for (size_t i = 0, nchildren = pc.getNumChildren(); i < nchildren; i++)
           {
-            std::stringstream ss;
-            ss << "Cannot match on evaluatable subterm " << pc[i];
-            d_lex.parseError(ss.str());
+            Expr ecc = pc[i];
+            if (ecc.isEvaluatable())
+            {
+              std::stringstream ss;
+              ss << "Cannot match on evaluatable subterm " << pc[i];
+              d_lex.parseError(ss.str());
+            }
           }
         }
+        program = d_state.mkExpr(Kind::PROGRAM, pchildren);
       }
       d_state.popScope();
-      Expr program = d_state.mkExpr(Kind::PROGRAM, pchildren);
-      d_state.defineProgram(pvar, program);
-      // rebind the program
-      d_eparser.bind(name, pvar);
+      if (!program.isNull())
+      {
+        d_state.defineProgram(pvar, program);
+      }
+      if (pprev.isNull())
+      {
+        // rebind the program, if new
+        d_eparser.bind(name, pvar);
+      }
     }
     break;
     // (reset)

tests/CMakeLists.txt

@@ -109,6 +109,7 @@ set(alfc_test_file_list
     nground-nil-v3.smt3
     ff-nil.smt3
     or-variant.smt3
+    mutual-rec.smt3
 )
 
 macro(alfc_test file)

tests/mutual-rec.smt3

@@ -0,0 +1,45 @@
+
+
+(declare-sort Int 0)
+(declare-consts <numeral> Int)
+
+; forward declaration
+(program is-odd () (Int) Bool)
+
+(program is-even ((n Int))
+  (Int) Bool
+  (
+  ((is-even 0) true)
+  ((is-even 1) false)
+  ((is-even n) (is-odd (alf.add n -1)))
+  )
+)
+
+(program is-odd ((n Int))
+  (Int) Bool
+  (
+  ((is-odd 0) false)
+  ((is-odd 1) true)
+  ((is-odd n) (is-even (alf.add n -1)))
+  )
+)
+
+(declare-fun not (Bool) Bool)
+(declare-fun pred_is_even (Int) Bool)
+
+(declare-rule find_is_even ((n Int))
+   :args (n)
+   :requires (((is-even n) true))
+   :conclusion (pred_is_even n)
+)
+
+(declare-rule find_is_odd ((n Int))
+   :args (n)
+   :requires (((is-odd n) true))
+   :conclusion (not (pred_is_even n))
+)
+
+
+(step a1 (pred_is_even 4) :rule find_is_even :premises () :args (4))
+(step a2 (not (pred_is_even 3)) :rule find_is_odd :premises () :args (3))
+