extended smt parser for the finite relations

fixed typing rules for relational terms
added a benchmark example for the theory of finite relations

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;