Age | Commit message (Collapse) | Author | |
---|---|---|---|
2014-10-19 | Finish sets type enumerator implementation. | Kshitij Bansal | |
2014-10-10 | Merge remote-tracking branch 'origin/1.4.x' | Kshitij Bansal | |
2014-10-10 | Fix issue with shared but non-preregistered term setup. Thanks Alvise ↵ | Kshitij Bansal | |
Rabitti for the report. | |||
2014-10-07 | Fix portoflio issues (debugging code was being called even when tag was off) | Kshitij Bansal | |
2014-10-07 | update default Sets options | Kshitij Bansal | |
2014-10-07 | whitespace fixes | Kshitij Bansal | |
2014-10-07 | add couple of stats | Kshitij Bansal | |
2014-10-07 | sets stronger equality propagator | Kshitij Bansal | |
2014-10-06 | Merge branch '1.4.x' | Morgan Deters | |
2014-10-06 | fix for bug586 | Kshitij Bansal | |
2014-10-02 | fix getModelValue(<non-preregistered term>) | Kshitij Bansal | |
2014-09-03 | check() optimization | Kshitij Bansal | |
Details of testing here: http://church.cims.nyu.edu/wiki/User:Kshitij/theorycheckoptimization | |||
2014-08-24 | remove some debugging code | Kshitij Bansal | |
(it can be brought back from version control, if needed) | |||
2014-08-24 | improvements to sets sharing | Kshitij Bansal | |
* Add TheorySets::getEqualityStatus(TNode, TNode) * Add TheorySets::getModelValue(TNode) | |||
2014-07-03 | change lemma generation behavior | Kshitij Bansal | |
don't store lemmas in a pending queue, instead generate them right away doing with pending queue is tricky, needs rethinking to do it properly | |||
2014-07-01 | Update copyrights. | Morgan Deters | |
2014-06-29 | sets: "insert" operator | Kshitij 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-25 | fix sets eager lemmas | Kshitij Bansal | |
2014-06-25 | mv default care graph function inside the theory implementation | Kshitij Bansal | |
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-06-21 | Sets kinds documentation | Morgan Deters | |
2014-06-11 | sets: comment out an assertion too strong | Kshitij Bansal | |
2014-06-11 | user/sat context issue in sets | Kshitij Bansal | |
2014-06-11 | fix in sets rewriter | Kshitij Bansal | |
2014-06-06 | sets: fix equality propagation | Kshitij Bansal | |
2014-06-03 | Support E-matching/QCF for Set operators. | ajreynol | |
2014-05-26 | Fix bug 567 | Kshitij Bansal | |
This bug got introduced in 96eccb0d6134ccf4ead0134299b2e3750a890083. The backing Node didn't always exist because of the changes. | |||
2014-05-16 | sets: fix a bug in model building, another in handling set of sets | Kshitij Bansal | |
2014-04-28 | nodemanager robust skolem numbering | Kshitij Bansal | |
2014-04-24 | optimization | Kshitij Bansal | |
2014-04-17 | use internal skolem numbering | Kshitij Bansal | |
2014-04-09 | fix | Kshitij Bansal | |
2014-04-09 | prep for fix | Kshitij Bansal | |
2014-04-09 | try foreach on CD datastructure | Kshitij Bansal | |
2014-04-09 | more | Kshitij Bansal | |
2014-04-09 | some debugging changes | Kshitij Bansal | |
2014-03-28 | add construles, type_rules rm redundant, kinds cleanup | Kshitij Bansal | |
2014-03-20 | cleanup | Kshitij Bansal | |
2014-03-20 | fix 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-20 | Fix for registration issues of term appearing in a shared lemma | Kshitij 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-20 | rewriter fix, weaken an assertion | Kshitij Bansal | |
2014-03-20 | constant normal form and rewrite | Kshitij Bansal | |
2014-03-20 | fix a sharing issues with sets | Kshitij Bansal | |
2014-03-20 | work on set model | Kshitij Bansal | |
2014-02-28 | theory/sets: cleanup | Kshitij Bansal | |
2014-02-28 | rename kind::IN to kind::MEMBER (fixes some windows build conflicts) | Kshitij Bansal | |
2014-02-21 | disable test cvc3_main, attempt to fix dist_check | 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 |