summaryrefslogtreecommitdiff
path: root/test/regress/regress0/sets
AgeCommit message (Collapse)Author
2014-07-10membership cvc token changed to `IS_IN' to avoid conflict with IN used for letKshitij Bansal
2014-07-09sets cvc parserKshitij Bansal
2014-07-09sets cvc printerKshitij Bansal
2014-06-30Use FS as the set-logic string for theory of setsKshitij Bansal
2014-06-29sets: "insert" operatorKshitij Bansal
new™! support for (insert (X (Set X)) (Set X) :right-associative) from the finte sets theory prosoal. e.g., (insert 1 2 3 4 (singleton 5))
2014-06-25rename subseteq to subset in smtlib, all kinds and smt operator names are ↵Kshitij Bansal
now consistent
2014-06-22Renaming of SMT2 operator names, kinds for set theoryKshitij 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-06-11disable another test, after recent merges taking too longKshitij Bansal
2014-06-11sets: comment out an assertion too strongKshitij Bansal
2014-06-11user/sat context issue in setsKshitij Bansal
2014-06-11fix in sets rewriterKshitij Bansal
2014-06-06sets: fix equality propagationKshitij Bansal
2014-05-25Improve quantifier instantiation: always use original terms when matching ↵Andrew Reynolds
(was missing for simple triggers). Minor updates to scripts.
2014-05-16sets: fix a bug in model building, another in handling set of setsKshitij Bansal
2014-04-09add testsKshitij Bansal
2014-04-09inputs to trigger bugKshitij Bansal
2014-03-28add construles, type_rules rm redundant, kinds cleanupKshitij Bansal
2014-03-20Merge pull request #22 from kbansal/sets-modelKshitij Bansal
Sets model
2014-03-20cleanupKshitij Bansal
2014-03-20fix for sets/mar2014/..317minimized..Kshitij Bansal
Observed behavior: --check-model failed for set-term (union (z3f69 z3v151) (setenum z3v143)) with different set of elements in the model for representative and the node itself. Issue: The trouble with data structure being mainted to ensure that things for which lemmas have been generated are not generated again. This data structure (d_pendingEverInserted) needs to be user context dependent. The bug was in the sequence of steps from requesting that a lemma be generated to when it actually was. Sequence was: addToPending (and also adds to pending ever inserted) -> isComplete (might remove things from pending if requirment met in other ways) -> getLemma (actually generated the lemma, if requirement not already met) Resolution: adding terms to d_pendingEverInserted was moved from addToPending() to getLemma().
2014-03-20Fix for registration issues of term appearing in a shared lemmaKshitij Bansal
(brought to attention by lianah -- fix currently just adapted using arrays -- this is to remind me to raise why do we even have this isPreregistered bussiness)
2014-03-20fix a sharing issues with setsKshitij Bansal
2014-03-20enable check-models for sets/ regressionsKshitij Bansal
2014-03-20testlemma regressionsKshitij Bansal
2014-03-12Some standardization of regression Makefiles that got out of sync. Fixes ↵Morgan Deters
cases of nonterminating rewrite-rules regressions.
2014-02-21add 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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback