Age | Commit message (Collapse) | Author | |
---|---|---|---|
2018-09-22 | cmake: Added regression tests and target make regress. | Aina Niemetz | |
2018-09-22 | cmake: Added initial build infrastructure. | Aina Niemetz | |
2018-02-15 | Refactor regressions (#1581) | Andrew Reynolds | |
2014-06-25 | rename subseteq to subset in smtlib, all kinds and smt operator names are ↵ | Kshitij Bansal | |
now consistent | |||
2014-06-22 | Renaming of SMT2 operator names, kinds for set theory | Kshitij Bansal | |
* SET_SINGLETON kind renamed to just SINGLETON * "setenum" smt2 opertor renamed to "singleton"[1] * "in" smt2 operator renamed to "member"[2] [1] It was anyhow accepting exactly one argument, so was bit misleading to call set enumerator. [2] The corresponding kind was called MEMBER, so this will also make them consistent. Only inconsistency now is for subset: kind is called SUBSET but operator is called "subseteq". | |||
2014-03-20 | enable check-models for sets/ regressions | Kshitij Bansal | |
2014-02-21 | add new theory (sets) | Kshitij Bansal | |
Specification (smt2) -- as per this commit, subject to change - Parameterized sort Set, e.g. (Set Int) - Empty set constant (typed), use with "as" to specify the type, e.g. (as emptyset (Set Int)) - Create a singleton set (setenum X (Set X)) : creates singleton set - Functions/operators (union (Set X) (Set X) (Set X)) (intersection (Set X) (Set X) (Set X)) (setminus (Set X) (Set X) (Set X)) - Predicates (in X (Set X) Bool) : membership (subseteq (Set X) (Set X) Bool) : set containment |