From: ajreynol 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 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; ipopScope(); } @@ -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)