diff options
| author | Christopher L. Conway <christopherleeconway@gmail.com> | 2010-03-09 23:43:35 +0000 |
|---|---|---|
| committer | Christopher L. Conway <christopherleeconway@gmail.com> | 2010-03-09 23:43:35 +0000 |
| commit | 8d85fb035b92f0fa0d852257dc00c9a85b1a350e (patch) | |
| tree | 4a63a19eaddb805a770dda158b8906e75000946d /src/parser/smt/smt_parser.g | |
| parent | 4ab7098ce928d69183d604e6b49b283f2f1283a6 (diff) | |
Adding support for "distinct" builtin in SMT parser
Diffstat (limited to 'src/parser/smt/smt_parser.g')
| -rw-r--r-- | src/parser/smt/smt_parser.g | 30 |
1 files changed, 21 insertions, 9 deletions
diff --git a/src/parser/smt/smt_parser.g b/src/parser/smt/smt_parser.g index 301859a37..7759cf965 100644 --- a/src/parser/smt/smt_parser.g +++ b/src/parser/smt/smt_parser.g @@ -126,6 +126,27 @@ annotatedFormula returns [CVC4::Expr formula] { checkArity(kind, args.size()); formula = mkExpr(kind,args); } + | /* a "distinct" expr */ + LPAREN DISTINCT annotatedFormulas[args] RPAREN + { std::vector<Expr> diseqs; + for(unsigned i = 0; i < args.size(); ++i) { + for(unsigned j = i+1; j < args.size(); ++j) { + diseqs.push_back(mkExpr(CVC4::kind::NOT, + mkExpr(CVC4::kind::EQUAL,args[i],args[j]))); + } + } + formula = mkExpr(CVC4::kind::AND, diseqs); } + + | /* An ite expression */ + LPAREN (ITE | IF_THEN_ELSE) + { Expr test, trueExpr, falseExpr; } + test = annotatedFormula + trueExpr = annotatedFormula + falseExpr = annotatedFormula + RPAREN + { formula = mkExpr(CVC4::kind::ITE, test, trueExpr, falseExpr); } + + | /* A non-built-in function application */ // Semantic predicate not necessary if parenthesized subexpressions @@ -139,15 +160,6 @@ annotatedFormula returns [CVC4::Expr formula] // TODO: check arity { formula = mkExpr(CVC4::kind::APPLY,args); } - | /* An ite expression */ - LPAREN (ITE | IF_THEN_ELSE) - { Expr test, trueExpr, falseExpr; } - test = annotatedFormula - trueExpr = annotatedFormula - falseExpr = annotatedFormula - RPAREN - { formula = mkExpr(CVC4::kind::ITE, test, trueExpr, falseExpr); } - | /* a variable */ { std::string name; } name = identifier[CHECK_DECLARED] |