diff options
| author | Kshitij Bansal <kshitij@cs.nyu.edu> | 2014-06-30 13:28:09 -0400 |
|---|---|---|
| committer | Kshitij Bansal <kshitij@cs.nyu.edu> | 2014-06-30 13:28:09 -0400 |
| commit | b06d25a020240fa455798308418ad802f9f40ea3 (patch) | |
| tree | 8203c68da0861a823674b942595ae8cfbfeac256 /src/parser | |
| parent | 7c009ac38ef5ccda070d8d7fb3955273574e94eb (diff) | |
| parent | fa53ae111cd314f455456a884f1247bb9b8e2c7b (diff) | |
Merge pull request #47 from kbansal/sets
Sets theory operators in SMTLIB2 and kinds to use from API have changed. They now are:
SMTLIB: emptyset, singleton*, insert*, union, intersection, setminus, member*, subset*
API: EMPTYSET, SINGLETON*, INSERT*, UNION, INTERSECTION, SETMINUS, MEMBER, SUBSET
(those marked with [*] have changed or been added, others are as earlier)
In the set-logic string use FS to enable sets.
A not-so-well-tested perl command for translating old benchmarks:
perl -pi -e 's/\(set-logic (.+)_SETS\)/\(set-logic \1FS\)/; s/\(in\b/\(member/g; s/\(setenum\b/\(singleton/g; s/\(subseteq\b/\(subset/g; '
Diffstat (limited to 'src/parser')
| -rw-r--r-- | src/parser/smt2/Smt2.g | 2 | ||||
| -rw-r--r-- | src/parser/smt2/smt2.cpp | 7 |
2 files changed, 5 insertions, 4 deletions
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 8590229a2..457c9c82f 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -1115,7 +1115,7 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2] { std::vector< Expr > nvec; expr = MK_EXPR( CVC4::kind::REGEXP_SIGMA, nvec ); } | EMPTYSET_TOK - { expr = MK_CONST( ::CVC4::EmptySet()); } + { expr = MK_CONST( ::CVC4::EmptySet(Type())); } // NOTE: Theory constants go here ; diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index 5baa0b16f..0c4b1258f 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -149,9 +149,10 @@ void Smt2::addTheory(Theory theory) { addOperator(kind::UNION, "union"); addOperator(kind::INTERSECTION, "intersection"); addOperator(kind::SETMINUS, "setminus"); - addOperator(kind::SUBSET, "subseteq"); - addOperator(kind::MEMBER, "in"); - addOperator(kind::SET_SINGLETON, "setenum"); + addOperator(kind::SUBSET, "subset"); + addOperator(kind::MEMBER, "member"); + addOperator(kind::SINGLETON, "singleton"); + addOperator(kind::INSERT, "insert"); break; case THEORY_DATATYPES: |