diff options
author | PaulMeng <baolmeng@gmail.com> | 2016-02-15 17:36:07 -0600 |
---|---|---|
committer | PaulMeng <baolmeng@gmail.com> | 2016-02-15 17:36:07 -0600 |
commit | 51fbe09f8b16ad0a49b2add0801b2963de08427e (patch) | |
tree | 4dbdd7df1a5b2181b7ac1f32725595b5be998d86 /src/parser | |
parent | 371c0799fa38452c2186efd268c73a42c282c96e (diff) |
extended smt parser for the finite relations
fixed typing rules for relational terms
added a benchmark example for the theory of finite relations
Diffstat (limited to 'src/parser')
-rw-r--r-- | src/parser/smt2/smt2.cpp | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index e3fbe36f2..530e9da8b 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -224,6 +224,10 @@ void Smt2::addTheory(Theory theory) { addOperator(kind::SETMINUS, "setminus"); addOperator(kind::SUBSET, "subset"); addOperator(kind::MEMBER, "member"); + addOperator(kind::TRANSPOSE, "transpose"); + addOperator(kind::TRANSCLOSURE, "transclosure"); + addOperator(kind::JOIN, "join"); + addOperator(kind::PRODUCT, "product"); addOperator(kind::SINGLETON, "singleton"); addOperator(kind::INSERT, "insert"); break; |