From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Thu, 16 Mar 2017 19:19:58 +0000 (-0500)
Subject: More fixes, features to examples.
X-Git-Tag: cvc5-1.0.0~5885
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=e4fde716f0b8266412cb6dc6326642c718839b71;p=cvc5.git

More fixes, features to examples.
---

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index c52f2ad51..15495265e 100644
--- 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 a44219954..f6148994e 100644
--- 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 e2f4a779b..430b22c59 100644
--- 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)