diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2017-03-02 14:45:21 -0600 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2017-03-02 14:45:21 -0600 |
| commit | 1f4b954a2cc7667a56a3007fa75c125fba93ed23 (patch) | |
| tree | ea8734e89aa5fba170781c7148d3fd886c597d4e /src/parser/smt1 | |
| parent | 21b0cedd7dadd96e5d256885e3b65a926a7e4a81 (diff) | |
Eliminate Boolean term conversion. Generalizes removeITE pass to remove Boolean terms, treats distinguished BOOLEAN_TERM_VARIABLE kind as theory literal. Fixes bugs 597, 604, 651, 652, 691, 694. Add regressions.
Diffstat (limited to 'src/parser/smt1')
| -rw-r--r-- | src/parser/smt1/Smt1.g | 2 | ||||
| -rw-r--r-- | src/parser/smt1/smt1.cpp | 1 |
2 files changed, 1 insertions, 2 deletions
diff --git a/src/parser/smt1/Smt1.g b/src/parser/smt1/Smt1.g index 3e63fb3ab..28c54fc80 100644 --- a/src/parser/smt1/Smt1.g +++ b/src/parser/smt1/Smt1.g @@ -379,7 +379,7 @@ builtinOp[CVC4::Kind& kind] | AND_TOK { $kind = CVC4::kind::AND; } | OR_TOK { $kind = CVC4::kind::OR; } | XOR_TOK { $kind = CVC4::kind::XOR; } - | IFF_TOK { $kind = CVC4::kind::IFF; } + | IFF_TOK { $kind = CVC4::kind::EQUAL; } | EQUAL_TOK { $kind = CVC4::kind::EQUAL; } | DISTINCT_TOK { $kind = CVC4::kind::DISTINCT; } // Arithmetic diff --git a/src/parser/smt1/smt1.cpp b/src/parser/smt1/smt1.cpp index 015129f10..c8d1b774c 100644 --- a/src/parser/smt1/smt1.cpp +++ b/src/parser/smt1/smt1.cpp @@ -79,7 +79,6 @@ Smt1::Smt1(ExprManager* exprManager, Input* input, bool strictMode, bool parseOn // Boolean symbols are always defined addOperator(kind::AND); addOperator(kind::EQUAL); - addOperator(kind::IFF); addOperator(kind::IMPLIES); addOperator(kind::ITE); addOperator(kind::NOT); |