diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2017-03-16 14:19:58 -0500 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2017-03-16 14:19:58 -0500 |
| commit | e4fde716f0b8266412cb6dc6326642c718839b71 (patch) | |
| tree | 092819d4bf1c0d26f845a3393a6462937280a02c /src/parser | |
| parent | 00785f2b65eb9dfdfbfcd8b58b0cc57255919c31 (diff) | |
More fixes, features to examples.
Diffstat (limited to 'src/parser')
| -rw-r--r-- | src/parser/smt2/Smt2.g | 14 |
1 files changed, 7 insertions, 7 deletions
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 ); } } } |