2 files changed, 21 insertions, 0 deletions
diff --git a/src/parser/parser.h b/src/parser/parser.h
index 42badf4c5..642b81fb0 100644
--- a/src/parser/parser.h
+++ b/src/parser/parser.h
@@ -739,6 +739,14 @@ public:
    */
   inline size_t scopeLevel() const { return d_symtab->getLevel(); }
 
+  /**
+   * Pushes a scope. All subsequent symbol declarations made are only valid in
+   * this scope, i.e. they are deleted on the next call to popScope.
+   *
+   * The argument bindingLevel is true, the assertion level is set to the
+   * current scope level. This determines which scope assertions are declared
+   * at.
+   */
   inline void pushScope(bool bindingLevel = false) {
     d_symtab->pushScope();
     if(!bindingLevel) {
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 96ac7d48e..30239dc2f 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -1733,6 +1733,18 @@ termNonVariable[CVC4::Expr& expr, CVC4::Expr& expr2]
         expr = MK_EXPR(kind, args);
       }
     }
+  | LPAREN_TOK COMPREHENSION_TOK
+    { PARSER_STATE->pushScope(true); }
+    boundVarList[bvl]
+    {
+      args.push_back(bvl);
+    }
+    term[f, f2] { args.push_back(f); }
+    term[f, f2] { 
+      args.push_back(f); 
+      expr = MK_EXPR(CVC4::kind::COMPREHENSION, args);
+    }
+    RPAREN_TOK
   | LPAREN_TOK qualIdentifier[p]
     termList[args,expr] RPAREN_TOK
     { 
@@ -2683,6 +2695,7 @@ DECLARE_DATATYPES_TOK : { PARSER_STATE->v2_6() || PARSER_STATE->sygus() }?'decla
 DECLARE_CODATATYPES_2_5_TOK : { !( PARSER_STATE->v2_6() || PARSER_STATE->sygus() ) }?'declare-codatatypes';
 DECLARE_CODATATYPES_TOK : { PARSER_STATE->v2_6() || PARSER_STATE->sygus() }?'declare-codatatypes';
 PAR_TOK : { PARSER_STATE->v2_6() }?'par';
+COMPREHENSION_TOK : { PARSER_STATE->isTheoryEnabled(Smt2::THEORY_SETS) }?'comprehension';
 TESTER_TOK : { ( PARSER_STATE->v2_6() || PARSER_STATE->sygus() ) && PARSER_STATE->isTheoryEnabled(Smt2::THEORY_DATATYPES) }?'is';
 MATCH_TOK : { ( PARSER_STATE->v2_6() || PARSER_STATE->sygus() ) && PARSER_STATE->isTheoryEnabled(Smt2::THEORY_DATATYPES) }?'match';
 GET_MODEL_TOK : 'get-model';