diff options
| author | Morgan Deters <mdeters@cs.nyu.edu> | 2013-05-17 11:18:12 -0400 |
|---|---|---|
| committer | Morgan Deters <mdeters@cs.nyu.edu> | 2013-05-20 16:55:59 -0400 |
| commit | 3913e813456fc6cabb1208044fd36c92c0056385 (patch) | |
| tree | 0809c76ecd8302ea030c5e152370e4a4a8ec200c | |
| parent | 611c12a19eaf359dd26da9d0a2b2e2215066180d (diff) | |
As per SMT-LIB standard: make - and xor take n>2 args and be left-assoc; => takes n>2 args and is right-assoc.
Thanks to David Cok for pointing out this issue.
| -rw-r--r-- | src/parser/smt2/Smt2.g | 16 |
1 files changed, 15 insertions, 1 deletions
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index dbe1135b3..7c0c1aad3 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -711,13 +711,27 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2] } else if( CVC4::kind::isAssociative(kind) && args.size() > EXPR_MANAGER->maxArity(kind) ) { /* Special treatment for associative operators with lots of children */ - expr = EXPR_MANAGER->mkAssociative(kind,args); + expr = EXPR_MANAGER->mkAssociative(kind, args); } else if( kind == CVC4::kind::MINUS && args.size() == 1 ) { expr = MK_EXPR(CVC4::kind::UMINUS, args[0]); + } else if( ( kind == CVC4::kind::XOR || kind == CVC4::kind::MINUS ) && + args.size() > 2 ) { + /* left-associative, but CVC4 internally only supports 2 args */ + expr = args[0]; + for(size_t i = 1; i < args.size(); ++i) { + expr = MK_EXPR(kind, expr, args[i]); + } + } else if( kind == CVC4::kind::IMPLIES && args.size() > 2 ) { + /* right-associative, but CVC4 internally only supports 2 args */ + expr = args[args.size() - 1]; + for(size_t i = args.size() - 1; i > 0;) { + expr = MK_EXPR(kind, args[--i], expr); + } } else if( ( kind == CVC4::kind::IFF || kind == CVC4::kind::EQUAL || kind == CVC4::kind::LT || kind == CVC4::kind::GT || kind == CVC4::kind::LEQ || kind == CVC4::kind::GEQ ) && args.size() > 2 ) { + /* "chainable", but CVC4 internally only supports 2 args */ expr = MK_EXPR(CVC4::kind::CHAIN, MK_CONST(kind), args); } else { PARSER_STATE->checkOperator(kind, args.size()); |