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/printer | |
| 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/printer')
| -rw-r--r-- | src/printer/smt2/smt2_printer.cpp | 9 |
1 files changed, 5 insertions, 4 deletions
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 15101b0e4..270e0dba0 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -418,7 +418,7 @@ void Smt2Printer::toStream(std::ostream& out, TNode n, case kind::SUBSET: case kind::MEMBER: case kind::SET_TYPE: - case kind::SET_SINGLETON: out << smtKindString(k) << " "; break; + case kind::SINGLETON: out << smtKindString(k) << " "; break; // datatypes case kind::APPLY_TYPE_ASCRIPTION: { @@ -618,10 +618,11 @@ static string smtKindString(Kind k) throw() { case kind::UNION: return "union"; case kind::INTERSECTION: return "intersection"; case kind::SETMINUS: return "setminus"; - case kind::SUBSET: return "subseteq"; - case kind::MEMBER: return "in"; + case kind::SUBSET: return "subset"; + case kind::MEMBER: return "member"; case kind::SET_TYPE: return "Set"; - case kind::SET_SINGLETON: return "setenum"; + case kind::SINGLETON: return "singleton"; + case kind::INSERT: return "insert"; default: ; /* fall through */ } |