More fixes, features to examples.

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index c52f2ad519f42f716ba97a835e03bbe57e6ec08d..15495265e05c77e87ef5f827b23f6c436cf701da 100644 (file)
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -2097,16 +2097,16 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2]
            }
            // build a lambda
            std::vector<Expr> largs;
-           largs.push_back( MK_EXPR( CVC4::Kind::BOUND_VAR_LIST, args ) );
+           largs.push_back( MK_EXPR( CVC4::kind::BOUND_VAR_LIST, args ) );
            largs.push_back( f3 );
            std::vector< Expr > aargs;
-           aargs.push_back( MK_EXPR( CVC4::Kind::LAMBDA, largs ) );
+           aargs.push_back( MK_EXPR( CVC4::kind::LAMBDA, largs ) );
            for( unsigned i=0; i<dtc.getNumArgs(); i++ ){
              //can apply total version since we will be guarded by ITE condition
-             aargs.push_back( MK_EXPR( CVC4::Kind::APPLY_SELECTOR_TOTAL, dtc[i].getSelector(), expr ) );
+             aargs.push_back( MK_EXPR( CVC4::kind::APPLY_SELECTOR_TOTAL, dtc[i].getSelector(), expr ) );
            }
-           patexprs.push_back( MK_EXPR( CVC4::Kind::APPLY, aargs ) );
-           patconds.push_back( MK_EXPR( CVC4::Kind::APPLY_TESTER, dtc.getTester(), expr ) );
+           patexprs.push_back( MK_EXPR( CVC4::kind::APPLY, aargs ) );
+           patconds.push_back( MK_EXPR( CVC4::kind::APPLY_TESTER, dtc.getTester(), expr ) );
          }
          RPAREN_TOK 
          { PARSER_STATE->popScope(); }
@@ -2120,7 +2120,7 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2]
          term[f3, f2] {
            const DatatypeConstructor& dtc = Datatype::datatypeOf(f)[Datatype::indexOf(f)];
            patexprs.push_back( f3 );
-           patconds.push_back( MK_EXPR( CVC4::Kind::APPLY_TESTER, dtc.getTester(), expr ) );
+           patconds.push_back( MK_EXPR( CVC4::kind::APPLY_TESTER, dtc.getTester(), expr ) );
          }
          RPAREN_TOK
     )+
@@ -2152,7 +2152,7 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2]
           expr = patexprs[index];
           first_time = false;
         }else{
-          expr = MK_EXPR( CVC4::Kind::ITE, patconds[index], patexprs[index], expr );
+          expr = MK_EXPR( CVC4::kind::ITE, patconds[index], patexprs[index], expr );
         }
       }
     }

diff --git a/test/regress/regress0/datatypes/dt-color-2.6.smt2 b/test/regress/regress0/datatypes/dt-color-2.6.smt2
index a44219954fc1c217668491faa14b73af715f6318..f6148994eab1ffbca1b8ed502d53cc7db332277d 100644 (file)
--- a/test/regress/regress0/datatypes/dt-color-2.6.smt2
+++ b/test/regress/regress0/datatypes/dt-color-2.6.smt2
@@ -10,6 +10,8 @@
 (declare-fun d () Color)
 
 (assert (or (distinct a b c d)
- (< (match a ((red 5) (green 3) (blue 2))) 0)))
+ (< (match a ((red 5) (green 3) (blue 2))) 0)
+ (< (match b ((red 2) (_ 1))) 0)
+ ))
 
 (check-sat)

diff --git a/test/regress/regress0/datatypes/dt-match-pat-param-2.6.smt2 b/test/regress/regress0/datatypes/dt-match-pat-param-2.6.smt2
index e2f4a779b9266b383d33966c704c39b862960881..430b22c59b92429f414e810567cf41fb3f162e86 100644 (file)
--- a/test/regress/regress0/datatypes/dt-match-pat-param-2.6.smt2
+++ b/test/regress/regress0/datatypes/dt-match-pat-param-2.6.smt2
@@ -11,4 +11,14 @@
 (declare-fun t () TreeList)
 (assert (<= 100 (match t ((empty (- 1)) ((insert x1 x2) (value x1))))))
 
+
+(declare-datatypes ( ( PTree 1) ( PTreeList 1) ) (
+(par ( X ) ( ( pnode ( pvalue X ) ( pchildren ( PTreeList X )) )))
+(par ( Y ) ( ( pempty ) ( pinsert ( phead ( PTree Y )) ( ptail ( PTreeList Y ))) ))
+))
+
+(declare-fun pt () (PTreeList Int))
+(assert (<= 200 (match pt ((pempty (- 1)) ((pinsert x1 x2) (pvalue x1))))))
+
+
 (check-sat)