Adding functions/predicates to SMT grammar

4 files changed, 305 insertions, 9 deletions

diff --git a/src/parser/antlr_parser.cpp b/src/parser/antlr_parser.cpp
index 34bf4bc82..171da47e8 100644
--- a/src/parser/antlr_parser.cpp
+++ b/src/parser/antlr_parser.cpp
@@ -82,6 +82,19 @@ Expr AntlrParser::mkExpr(Kind kind, const std::vector<Expr>& children) {
   return result;
 }
 
+void AntlrParser::newFunction(std::string name, 
+                               const std::vector< std::string>& sorts) {
+  // FIXME: Need to actually create a function type
+  d_varSymbolTable.bindName(name, d_exprManager->mkVar());
+}
+
+void AntlrParser::newFunctions(const std::vector<std::string>& names, 
+                               const std::vector< std::string>& sorts) {
+  for(unsigned i = 0; i < names.size(); ++i) {
+    newFunction(names[i], sorts);
+  }
+}
+
 void AntlrParser::newPredicate(std::string name,
                                const std::vector<std::string>& sorts) {
   Debug("parser") << "newPredicate(" << name << ")" << std::endl;
@@ -99,6 +112,23 @@ void AntlrParser::newPredicates(const std::vector<std::string>& names,
   }
 }
 
+bool AntlrParser::isSort(std::string name) {
+  return d_sortTable.isBound(name);
+}
+
+void AntlrParser::newSort(std::string name) {
+  Assert( !isSort(name) ) ;
+  // Trivial binding
+  d_sortTable.bindName(name,name);
+  Assert( isSort(name) ) ;
+}
+
+void AntlrParser::newSorts(const std::vector<std::string>& names) {
+  for(unsigned i = 0; i < names.size(); ++i) {
+    newSort(names[i]);
+  }
+}
+
 void AntlrParser::setExpressionManager(ExprManager* em) {
   d_exprManager = em;
 }
@@ -132,5 +162,18 @@ bool AntlrParser::checkDeclaration(string varName, DeclarationCheck check) {
   }
 }
 
+bool AntlrParser::checkSort(std::string name, DeclarationCheck check) {
+  switch(check) {
+  case CHECK_DECLARED:
+    return isSort(name);
+  case CHECK_UNDECLARED:
+    return !isSort(name);
+  case CHECK_NONE:
+    return true;
+  default:
+    Unhandled("Unknown check type!");
+  }
+}
+
 }/* CVC4::parser namespace */
 }/* CVC4 namespace */
diff --git a/src/parser/antlr_parser.h b/src/parser/antlr_parser.h
index a3015eb22..0c6deb95a 100644
--- a/src/parser/antlr_parser.h
+++ b/src/parser/antlr_parser.h
@@ -120,6 +120,15 @@ protected:
   bool checkDeclaration(std::string varName, DeclarationCheck check);
 
   /**
+   * Return true if the the declaration policy we want to enforce is true
+   * on the given sort name.
+   * @param name the sort symbol to check
+   * @oaram check the kind of check to perform
+   * @return true if the check holds
+   */
+  bool checkSort(std::string name, DeclarationCheck check);
+
+  /**
    * Types of symbols.
    */
   enum SymbolType {
@@ -138,6 +147,12 @@ protected:
   bool isDeclared(std::string var_name, SymbolType type = SYM_VARIABLE);
 
   /**
+   * Checks if the sort has been declared.
+   * @param the sort name
+   */
+  bool isSort(std::string name);
+
+  /**
    * Returns the true expression.
    * @return the true expression
    */
@@ -185,8 +200,26 @@ protected:
   Expr mkExpr(Kind kind, const std::vector<Expr>& children);
 
   /**
-   * Creates a new predicate over the given sorts. The predicate
-   * has arity sorts.size().
+   * Creates a new function over the given sorts. The function
+   * has arity sorts.size() - 1 and range type sorts[sorts.size() - 1].
+   * @param name the name of the function
+   * @param sorts the sorts
+   */
+  void newFunction(std::string name, 
+                   const std::vector<std::string>& sorts);
+
+  /**
+   * Creates new functions over the given sorts. Each function has
+   * arity sorts.size() - 1 and range type sorts[sorts.size() - 1].
+   * @param name the name of the function
+   * @param sorts the sorts
+   */
+  void newFunctions(const std::vector<std::string>& names, 
+                    const std::vector<std::string>& sorts);
+
+  /**
+   * Creates a new predicate over the given sorts. The predicate has
+   * arity sorts.size().
    * @param name the name of the predicate
    * @param sorts the sorts
    */
@@ -201,6 +234,16 @@ protected:
       std::string>& sorts);
 
   /**
+   * Creates a new sort with the given name.
+   */
+  void newSort(std::string name);
+
+  /**
+   * Creates a new sorts with the given names.
+   */
+  void newSorts(const std::vector<std::string>& names);
+
+  /**
    * Returns the precedence rank of the kind.
    */
   static unsigned getPrecedence(Kind kind);
@@ -212,6 +255,9 @@ private:
 
   /** The symbol table lookup */
   SymbolTable<Expr> d_varSymbolTable;
+
+  /** The sort table */
+  SymbolTable<std::string> d_sortTable;
 };
 
 }/* CVC4::parser namespace */
diff --git a/src/parser/smt/smt_lexer.g b/src/parser/smt/smt_lexer.g
index e9abab61a..f1c01ea05 100644
--- a/src/parser/smt/smt_lexer.g
+++ b/src/parser/smt/smt_lexer.g
@@ -64,6 +64,20 @@ tokens {
   EXTRAFUNS_ATTR   = ":extrafuns";
   EXTRAPREDS_ATTR  = ":extrapreds";
   C_NOTES       = ":notes";
+  // arithmetic symbols
+  EQUAL         = "=";
+  LESS_THAN     = "<";
+  GREATER_THAN  = ">";
+  AMPERSAND     = "&";
+  AT            = "@";
+  POUND         = "#";
+  PLUS          = "+";
+  MINUS         = "-";
+  STAR          = "*";
+  DIV           = "/";
+  PERCENT       = "%";
+  PIPE          = "|";
+  TILDE         = "~";
 }
 
 /**
@@ -179,3 +193,18 @@ STRING_LITERAL options { paraphrase = "a string literal"; }
 COMMENT options { paraphrase = "comment"; }
   : ';' (~('\n' | '\r'))*                    { $setType(antlr::Token::SKIP); }
   ;
+
+/* Arithmetic symbol tokens */
+EQUAL :   "=";
+LESS_THAN : "<";
+GREATER_THAN : ">";
+AMPERSAND :  "&";
+AT :  "@";
+POUND :  "#";
+PLUS :  "+";
+MINUS :  "-";
+STAR :  "*";
+DIV :  "/";
+PERCENT :  "%";
+PIPE :  "|";
+TILDE : "~";
diff --git a/src/parser/smt/smt_parser.g b/src/parser/smt/smt_parser.g
index 3933a04f0..c0e53027d 100644
--- a/src/parser/smt/smt_parser.g
+++ b/src/parser/smt/smt_parser.g
@@ -98,10 +98,12 @@ benchAttribute returns [Command* smt_command = 0]
     { smt_command = new AssertCommand(formula);   }
   | FORMULA_ATTR formula = annotatedFormula
     { smt_command = new CheckSatCommand(formula); }
-  | STATUS_ATTR b_status = status
-    { smt_command = new SetBenchmarkStatusCommand(b_status); }
-  | EXTRAPREDS_ATTR LPAREN (predicateDeclaration)+ RPAREN
-  | NOTES_ATTR STRING_LITERAL
+  | STATUS_ATTR b_status = status                   
+    { smt_command = new SetBenchmarkStatusCommand(b_status); }        
+  | EXTRAFUNS_ATTR LPAREN (functionDeclaration)+ RPAREN  
+  | EXTRAPREDS_ATTR LPAREN (predicateDeclaration)+ RPAREN  
+  | EXTRASORTS_ATTR LPAREN (sortDeclaration)+ RPAREN  
+  | NOTES_ATTR STRING_LITERAL        
   | annotation
   ;
 
@@ -132,17 +134,102 @@ annotatedFormula returns [CVC4::Expr formula]
   Kind kind;
   vector<Expr> children;
 }
+<<<<<<< .mine
+  :  formula = annotatedAtom 
+  |  LPAREN kind = boolConnective annotatedFormulas[children] RPAREN 
+    { formula = mkExpr(kind, children);  }    
+    /* TODO: let, flet, quantifiers */
+=======
   :  formula = annotatedAtom
   |  LPAREN kind = boolConnective annotatedFormulas[children] RPAREN { formula = mkExpr(kind, children);  }
+>>>>>>> .r150
   ;
 
 /**
+<<<<<<< .mine
+ * Matches a sequence of annotaed formulas and puts them into the formulas
+ * vector.
+ * @param formulas the vector to fill with formulas
+ */   
+annotatedFormulas[std::vector<Expr>& formulas]
+{
+  Expr f;
+}
+  : ( f = annotatedFormula { formulas.push_back(f); } )+
+  ;
+
+/**
+ * Matches an annotated proposition atom, which is either a propositional atom 
+ * or built of other atoms using a predicate symbol.  
+=======
  * Matches an annotated proposition atom, which is either a propositional atom
  * or built of other atoms using a predicate symbol.
+>>>>>>> .r150
  * @return expression representing the atom
  */
+<<<<<<< .mine
+annotatedAtom returns [CVC4::Expr atom] 
+{ 
+  Kind kind;
+  string predName;
+  Expr pred;
+  vector<Expr> children;
+}
+  : atom = propositionalAtom  
+=======
 annotatedAtom returns [CVC4::Expr atom]
   : atom = propositionalAtom
+>>>>>>> .r150
+  | LPAREN kind = arithPredicate annotatedTerms[children] RPAREN
+    { atom = mkExpr(kind,children); }
+  | LPAREN pred = predicateSymbol
+    { children.push_back(pred); }
+    annotatedTerms[children] RPAREN
+    { atom = mkExpr(CVC4::APPLY,children); }
+  ;
+
+/** 
+ * Matches an annotated term.
+ * @return the expression representing the term 
+ */
+annotatedTerm returns [CVC4::Expr term] 
+{ 
+  Kind kind;
+  Expr f, t1, t2;
+  vector<Expr> children;
+}
+  : term = baseTerm
+  | LPAREN f = functionSymbol
+    { children.push_back(f); }
+    annotatedTerms[children] RPAREN 
+    { term = mkExpr(CVC4::APPLY, children);  }
+  // | LPAREN kind = arithFunction annotatedTerms[children] RPAREN
+  //   { term = mkExpr(kind,children); }
+  | LPAREN ITE 
+    f = annotatedFormula 
+    t1 = annotatedTerm 
+    t2 = annotatedTerm RPAREN
+    { term = mkExpr(CVC4::ITE, f, t1, t2); }
+  ;
+
+/**
+ * Matches a sequence of annotaed formulas and puts them into the formulas
+ * vector.
+ * @param formulas the vector to fill with formulas
+ */   
+annotatedTerms[std::vector<Expr>& terms]
+{
+  Expr t;
+}
+  : ( t = annotatedFormula { terms.push_back(t); } )+
+  ;
+
+baseTerm returns [CVC4::Expr term]
+{
+  string name;
+}
+  : name = identifier[CHECK_DECLARED] { term = getVariable(name); }
+    /* TODO: constants */
   ;
 
 /**
@@ -159,6 +246,8 @@ boolConnective returns [CVC4::Kind kind]
   ;
 
 /**
+<<<<<<< .mine
+=======
  * Mathces a sequence of annotaed formulas and puts them into the formulas
  * vector.
  * @param formulas the vector to fill with formulas
@@ -171,6 +260,7 @@ annotatedFormulas[std::vector<Expr>& formulas]
   ;
 
 /**
+>>>>>>> .r150
  * Matches a propositional atom and returns the expression of the atom.
  * @return atom the expression of the atom
  */
@@ -178,20 +268,63 @@ propositionalAtom returns [CVC4::Expr atom]
 {
   std::string p;
 }
-   : p = predicateName[CHECK_DECLARED] { atom = getVariable(p); }
+   : atom = predicateSymbol
    | TRUE          { atom = getTrueExpr(); }
    | FALSE         { atom = getFalseExpr(); }
    ;
 
+arithPredicate returns [CVC4::Kind kind]
+  : EQUAL { kind = CVC4::EQUAL; }
+    /* TODO: lt, gt */
+  ;
+
 /**
+<<<<<<< .mine
+ * Matches a (possibly undeclared) predicate identifier (returning the string). 
+=======
  * Matches a predicate symbol.
+>>>>>>> .r150
  * @param check what kind of check to do with the symbol
  */
 predicateName[DeclarationCheck check = CHECK_NONE] returns [std::string p]
   :  p = identifier[check]
   ;
+<<<<<<< .mine
+
+/**
+ * Matches an previously declared predicate symbol (returning an Expr)
+ */
+predicateSymbol returns [CVC4::Expr pred]
+{ 
+  string name;
+}
+  : name = predicateName[CHECK_DECLARED]
+    { pred = getVariable(name); }
+  ;
+
+/**
+ * Matches a (possibly undeclared) function identifier (returning the string)
+ * @param check what kind of check to do with the symbol
+ */
+functionName[DeclarationCheck check = CHECK_NONE] returns [std::string name]
+  :  name = identifier[check]
+  ;
 
 /**
+ * Matches an previously declared function symbol (returning an Expr)
+ */
+functionSymbol returns [CVC4::Expr fun]
+{ 
+  string name;
+}
+  : name = functionName[CHECK_DECLARED]
+    { fun = getVariable(name); }
+  ;
+  
+=======
+
+>>>>>>> .r150
+/**
  * Matches an attribute name from the input (:attribute_name).
  */
 attribute
@@ -202,10 +335,32 @@ attribute
  * Matches the sort symbol, which can be an arbitrary identifier.
  * @param check the check to perform on the name
  */
+<<<<<<< .mine
+sortName[DeclarationCheck check = CHECK_NONE] returns [std::string name] 
+  : name = identifier[CHECK_NONE] 
+    /* We pass CHECK_NONE to identifier, because identifier checks
+       in the variable namespace, not the sorts namespace. */
+    { checkSort(name,check) }?
+=======
 sortName[DeclarationCheck check = CHECK_NONE] returns [std::string s]
   : s = identifier[check]
+>>>>>>> .r150
   ;
+<<<<<<< .mine
 
+functionDeclaration
+{
+  string name;
+  vector<string> sorts;
+}
+  : LPAREN name = functionName[CHECK_UNDECLARED]
+        sortNames[sorts, CHECK_DECLARED] RPAREN
+    { newFunction(name, sorts); } 
+  ;
+              
+=======
+
+>>>>>>> .r150
 /**
  * Matches the declaration of a predicate and declares it
  */
@@ -214,17 +369,40 @@ predicateDeclaration
   string p_name;
   vector<string> p_sorts;
 }
+<<<<<<< .mine
+  : LPAREN p_name = predicateName[CHECK_UNDECLARED] 
+        sortNames[p_sorts, CHECK_DECLARED] RPAREN
+    { newPredicate(p_name, p_sorts); } 
+=======
   :  LPAREN p_name = predicateName[CHECK_UNDECLARED] sortNames[p_sorts] RPAREN { newPredicate(p_name, p_sorts); }
+>>>>>>> .r150
+  ;
+<<<<<<< .mine
+
+sortDeclaration 
+{
+  string name;
+}
+  : name = sortName[CHECK_UNDECLARED]
+    { newSort(name); }
   ;
+  
+=======
 
+>>>>>>> .r150
 /**
  * Matches a sequence of sort symbols and fills them into the given vector.
  */
-sortNames[std::vector<std::string>& sorts]
+sortNames[std::vector<std::string>& sorts,DeclarationCheck check = CHECK_NONE]
 {
-  std::string sort;
+  std::string name;
 }
+<<<<<<< .mine
+  : ( name = sortName[check] 
+      { sorts.push_back(name); })* 
+=======
   : ( sort = sortName[CHECK_UNDECLARED] { sorts.push_back(sort); })*
+>>>>>>> .r150
   ;
 
 /**