Merge pull request #47 from cvc5/rmDefineFun

define-fun is syntax sugar for declare-fun + assert and thus should only be accepted in reference files.

Moreover define is already used as a macro. This PR adds an additional attribute :type T to recover the old functionality that define-fun provided (as means of invoking type checking).

src/attr.cpp

@@ -17,6 +17,7 @@ std::ostream& operator<<(std::ostream& o, Attr a)
     case Attr::NONE: o << "NONE"; break;
     case Attr::VAR: o << "VAR"; break;
     case Attr::IMPLICIT: o << "IMPLICIT"; break;
+    case Attr::TYPE: o << "TYPE"; break;
     case Attr::LIST: o << "LIST"; break;
     case Attr::REQUIRES: o << "REQUIRES"; break;
     case Attr::PREMISE_LIST: o << "PREMISE_LIST"; break;

src/attr.h

@@ -23,6 +23,7 @@ enum class Attr
   VAR,
   IMPLICIT,
   REQUIRES,
+  TYPE,
 
   //------------------ below here is mutually exclusive?
   LIST,

src/cmd_parser.cpp

@@ -36,7 +36,6 @@ CmdParser::CmdParser(Lexer& lex,
   d_table["declare-fun"] = Token::DECLARE_FUN;
   d_table["declare-sort"] = Token::DECLARE_SORT;
   d_table["define-const"] = Token::DEFINE_CONST;
-  d_table["define-fun"] = Token::DEFINE_FUN;
   d_table["define-sort"] = Token::DEFINE_SORT;
   d_table["echo"] = Token::ECHO;
   d_table["exit"] = Token::EXIT;
@@ -56,6 +55,7 @@ CmdParser::CmdParser(Lexer& lex,
   {
     // only used in smt2 queries
     d_table["assert"] = Token::ASSERT;
+    d_table["define-fun"] = Token::DEFINE_FUN;
     d_table["check-sat"] = Token::CHECK_SAT;
     d_table["check-sat-assuming"] = Token::CHECK_SAT_ASSUMING;
     d_table["set-logic"] = Token::SET_LOGIC;
@@ -476,7 +476,7 @@ bool CmdParser::parseNextCommand()
     break;
     // (define-fun <symbol> (<sorted_var>*) <sort> <term>)
     // (define-type <symbol> (<sorted_var>*) <term>)
-    // (define <symbol> (<sorted_var>*) <term>)
+    // (define <symbol> (<sorted_var>*) <term> <attr>*)
     case Token::DEFINE_FUN:
     case Token::DEFINE_TYPE:
     case Token::DEFINE:
@@ -519,14 +519,60 @@ bool CmdParser::parseNextCommand()
         d_eparser.typeCheck(expr, ret);
       }
       d_state.popScope();
-      // make a lambda if given arguments
-      if (vars.size() > 0)
+      if (tok == Token::DEFINE_FUN)
       {
-        Expr vl = d_state.mkExpr(Kind::TUPLE, vars);
-        expr = d_state.mkExpr(Kind::LAMBDA, {vl, expr});
+        // This is for reference checking only. Note that = and lambda are
+        // not builtin symbols, thus we must assume they are defined by the user.
+        // We assume that a symbol named "=" has been defined.
+        Expr eq = d_state.getVar("=");
+        if (eq.isNull())
+        {
+          d_lex.parseError("Expected symbol '=' to be defined when parsing define-fun.");
+        }
+        Expr rhs = expr;
+        Expr t = ret;
+        if (!vars.empty())
+        {
+          // We assume that a symbol named "lambda" has been defined as a binder.
+          Expr lambda = d_state.getVar("lambda");
+          if (lambda.isNull())
+          {
+            d_lex.parseError("Expected symbol 'lambda' to be defined when parsing define-fun.");
+          }
+          Expr bvl = d_state.mkBinderList(lambda.getValue(), vars);
+          rhs = d_state.mkExpr(Kind::APPLY, {lambda, bvl, rhs});
+          std::vector<Expr> types;
+          for (Expr& e : vars)
+          {
+            types.push_back(d_eparser.typeCheck(e));
+          }
+          t = d_state.mkFunctionType(types, t, false);
+        }
+        Expr sym = d_state.mkSymbol(Kind::CONST, name, t);
+        Trace("define") << "Define: " << name << " -> " << sym << std::endl;
+        d_eparser.bind(name, sym);
+        Expr a = d_state.mkExpr(Kind::APPLY, {eq, sym, rhs});
+        Trace("define") << "Define-fun reference assert " << a << std::endl;
+        d_state.addReferenceAssert(a);
+      }
+      else
+      {
+        // defines as a macro
+        // make a lambda if given arguments
+        if (vars.size() > 0)
+        {
+          Expr vl = d_state.mkExpr(Kind::TUPLE, vars);
+          expr = d_state.mkExpr(Kind::LAMBDA, {vl, expr});
+        }
+        d_eparser.bind(name, expr);
+        Trace("define") << "Define: " << name << " -> " << expr << std::endl;
+        // define additionally takes attributes
+        if (tok == Token::DEFINE)
+        {
+          AttrMap attrs;
+          d_eparser.parseAttributeList(expr, attrs);
+        }
       }
-      d_eparser.bind(name, expr);
-      Trace("define") << "Define: " << name << " -> " << expr << std::endl;
     }
     break;
     // (define-sort <symbol> (<symbol>*) <sort>)

src/expr_parser.cpp

@@ -78,6 +78,7 @@ ExprParser::ExprParser(Lexer& lex, State& state, bool isReference)
 {
   d_strToAttr[":var"] = Attr::VAR;
   d_strToAttr[":implicit"] = Attr::IMPLICIT;
+  d_strToAttr[":type"] = Attr::TYPE;
   d_strToAttr[":list"] = Attr::LIST;
   d_strToAttr[":requires"] = Attr::REQUIRES;
   d_strToAttr[":left-assoc"] = Attr::LEFT_ASSOC;
@@ -1016,7 +1017,7 @@ std::string ExprParser::parseStr(bool unescape)
   return s;
 }
 
-void ExprParser::parseAttributeList(const Expr& e, AttrMap& attrs, bool& pushedScope)
+void ExprParser::parseAttributeList(Expr& e, AttrMap& attrs, bool& pushedScope)
 {
   std::map<std::string, Attr>::iterator its;
   // while the next token is KEYWORD, exit if RPAREN
@@ -1092,6 +1093,17 @@ void ExprParser::parseAttributeList(const Expr& e, AttrMap& attrs, bool& pushedS
         parseLiteralKind();
       }
         break;
+      case Attr::TYPE:
+      {
+        val = parseExpr();
+        // run type checking
+        if (e.isNull())
+        {
+          d_lex.parseError("Cannot use :type in this context");
+        }
+        typeCheck(e, val);
+      }
+        break;
       default:
         d_lex.parseError("Unhandled attribute");
         break;
@@ -1101,7 +1113,7 @@ void ExprParser::parseAttributeList(const Expr& e, AttrMap& attrs, bool& pushedS
   d_lex.reinsertToken(Token::RPAREN);
 }
 
-void ExprParser::parseAttributeList(const Expr& e, AttrMap& attrs)
+void ExprParser::parseAttributeList(Expr& e, AttrMap& attrs)
 {
   bool pushedScope = false;
   parseAttributeList(e, attrs, pushedScope);

src/expr_parser.h

@@ -107,9 +107,9 @@ class ExprParser
    * is true when e.g. the attribute :var is read. The caller of this method
    * is responsible for popping the scope.
    */
-  void parseAttributeList(const Expr& e, AttrMap& attrs, bool& pushedScope);
+  void parseAttributeList(Expr& e, AttrMap& attrs, bool& pushedScope);
   /** Same as above, but ensures we pop the scope */
-  void parseAttributeList(const Expr& e, AttrMap& attrs);
+  void parseAttributeList(Expr& e, AttrMap& attrs);
 
   /**
    * Parse literal kind.

tests/Strings-theory.smt3

@@ -4,7 +4,7 @@
 (declare-sort RegLan 0)
 (declare-type Seq (Type))
 (declare-sort Char 0)
-(define-fun String () Type (Seq Char))
+(define String () (Seq Char))
 
 (declare-consts <string> String)
 

tests/beta-reduce-define-fun.smt3

@@ -5,7 +5,7 @@
 
 
 (declare-sort U 0)
-(define-fun f_true ((x U)) Bool true)
+(define f_true ((x U)) true)
 
 
 (declare-rule trust ((f Bool))

tests/bv-concat.smt3

@@ -20,5 +20,5 @@
 
 (declare-fun x () (BitVec 2))
 (declare-fun y () (BitVec 3))
-(define-fun z () (BitVec 5) (bvconcat x y))
+(define z () (bvconcat x y) :type (BitVec 5))
 

tests/bv-dep-type.smt3

@@ -13,4 +13,4 @@
 
 (declare-fun x () (BitVec m))
 (declare-fun y () (BitVec m))
-(define-fun z () (BitVec m) (bvadd m x y))
+(define z () (bvadd m x y) :type (BitVec m))

tests/define-fun-dep-type.smt3

@@ -2,5 +2,5 @@
 (declare-const = (-> (! Type :var A :implicit) A A Bool))
 
 ; note that U is bound before x is parsed
-(define-fun eq ((U Type) (x U)) Bool (= x x))
+(define eq ((U Type) (x U)) (= x x))
 

tests/define-fun.alfc.smt3

@@ -6,12 +6,12 @@
 
 (define alf.1.x () (alf.var "alf.1.x" Int))
 (define x () (alf.var "x" Int))
-(define-fun f () (-> Int Bool) (lambda x false))
-(define-fun g () (-> Int Bool) (lambda alf.1.x true))
-(define-fun @t1 () (-> Int Bool) (lambda x false))
-(define-fun @t2 () (-> Int Bool) (lambda alf.1.x true))
-(define-fun @t3 () Bool (f 0))
-(define-fun @t4 () Bool (_ @t1 0))
+(define f () (lambda x false))
+(define g () (lambda alf.1.x true))
+(define @t1 () (lambda x false))
+(define @t2 () (lambda alf.1.x true))
+(define @t3 () (f 0))
+(define @t4 () (_ @t1 0))
 (step @p1 (= @t1 @t1) :rule refl :args (@t1))
 (step @p2 (= @t2 @t2) :rule refl :args (@t2))
 (assume @p3 @t3)

tests/define-sort-iarray.smt3

@@ -5,4 +5,4 @@
 (define-sort IntArray (T) (Array Int T))
 (declare-const a (Array Int Bool))
 (declare-const b (IntArray Bool))
-(define-fun P () Bool (= a b))
+(define P () (= a b) :type Bool)

tests/or-variant.smt3

@@ -5,8 +5,8 @@
 (declare-const a Bool)
 (declare-const b Bool)
 
-(define-fun P ((x Bool)) Bool x)
-(define-fun Q ((x Bool :list)) Bool (or x))
+(define P ((x Bool)) x)
+(define Q ((x Bool :list)) (or x))
 
 (declare-const = (-> (! Type :var A :implicit) A A Bool))
 (declare-rule refl ((T Type) (t T))

tests/par-dt.smt3

@@ -1,5 +1,5 @@
 (declare-sort Int 0)
 (declare-datatypes ((List 1)) ((par (T) ((nil) (cons (head T) (tail (List T)))))))
 (define y () (alf.var "y" (List Int)))
-(define-fun @t1 () (List Int) (tail y))
-(define-fun @t2 () Int (head y))
+(define @t1 () (tail y) :type (List Int))
+(define @t2 () (head y) :type Int)

tests/pf-haniel.smt3

@@ -10,12 +10,12 @@
 (declare-fun d () U)
 (declare-fun a () U)
 (declare-fun b () U)
-(define-fun @t1 () Bool (= a b))
-(define-fun @t2 () Bool (= c d))
-(define-fun @t3 () Bool (and p1 true))
-(define-fun @t4 () Bool (and p2 p3))
-(define-fun @t5 () Bool (= (f a c) (f b d)))
-(define-fun @t6 () Bool (and @t1 @t2))
+(define @t1 () (= a b))
+(define @t2 () (= c d))
+(define @t3 () (and p1 true))
+(define @t4 () (and p2 p3))
+(define @t5 () (= (f a c) (f b d)))
+(define @t6 () (and @t1 @t2))
 (assume @p1 @t1)
 (assume @p2 @t2)
 (assume @p3 @t3)

tests/pf-quant.smt3

@@ -13,7 +13,7 @@
 (step a_inst (=> (forall x1 (= x1 x1)) (= a a)) :rule forall-inst :premises (forall_x_eq_x) :args (a))
 
 
-(define-fun F_x () Bool (exists x1 (= x1 x1)))
+(define F_x () (exists x1 (= x1 x1)))
 
 (assume ex_x F_x)
 

tests/quant-sk-small.alfc.smt3

@@ -6,12 +6,12 @@
 (define x () (alf.var "x" Int))
 (define y () (alf.var "y" Int))
 (declare-fun P (Int Int) Bool)
-(define-fun @t1 () Bool (forall (@list x y) (P x y)))
-(define-fun @t2 () Bool (P alf.1.x 5))
-(define-fun @t3 () Bool (exists (@list alf.1.x @list.nil) (not @t2)))
-(define-fun @t4 () Bool (not (forall (@list alf.1.x @list.nil) @t2)))
-(define-fun @t5 () Int (skolem (@k.QUANTIFIERS_SKOLEMIZE @t3 alf.1.x)))
-(define-fun @t6 () Bool (P @t5 5))
+(define @t1 () (forall (@list x y) (P x y)))
+(define @t2 () (P alf.1.x 5))
+(define @t3 () (exists (@list alf.1.x @list.nil) (not @t2)))
+(define @t4 () (not (forall (@list alf.1.x @list.nil) @t2)))
+(define @t5 () (skolem (@k.QUANTIFIERS_SKOLEMIZE @t3 alf.1.x)))
+(define @t6 () (P @t5 5))
 (assume @p1 @t1)
 (assume @p2 @t3)
 ; WARNING: add trust step for THEORY_REWRITE

tests/simple.smt3

@@ -1,3 +1,3 @@
 (declare-sort Int 0)
 (declare-fun x () Int)
-(define-fun y () Int x)
+(define y () x :type Int)