summaryrefslogtreecommitdiff
path: root/src/theory/sets
AgeCommit message (Collapse)Author
2014-10-19Finish sets type enumerator implementation.Kshitij Bansal
2014-10-10Merge remote-tracking branch 'origin/1.4.x'Kshitij Bansal
2014-10-10Fix issue with shared but non-preregistered term setup. Thanks Alvise ↵Kshitij Bansal
Rabitti for the report.
2014-10-07Fix portoflio issues (debugging code was being called even when tag was off)Kshitij Bansal
2014-10-07update default Sets optionsKshitij Bansal
2014-10-07whitespace fixesKshitij Bansal
2014-10-07add couple of statsKshitij Bansal
2014-10-07sets stronger equality propagatorKshitij Bansal
2014-10-06Merge branch '1.4.x'Morgan Deters
2014-10-06fix for bug586Kshitij Bansal
2014-10-02fix getModelValue(<non-preregistered term>)Kshitij Bansal
2014-09-03check() optimizationKshitij Bansal
Details of testing here: http://church.cims.nyu.edu/wiki/User:Kshitij/theorycheckoptimization
2014-08-24remove some debugging codeKshitij Bansal
(it can be brought back from version control, if needed)
2014-08-24improvements to sets sharingKshitij Bansal
* Add TheorySets::getEqualityStatus(TNode, TNode) * Add TheorySets::getModelValue(TNode)
2014-07-03change lemma generation behaviorKshitij 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-01Update copyrights.Morgan Deters
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-25fix sets eager lemmasKshitij Bansal
2014-06-25mv default care graph function inside the theory implementationKshitij Bansal
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-21Sets kinds documentationMorgan Deters
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-06-03Support E-matching/QCF for Set operators.ajreynol
2014-05-26Fix bug 567Kshitij Bansal
This bug got introduced in 96eccb0d6134ccf4ead0134299b2e3750a890083. The backing Node didn't always exist because of the changes.
2014-05-16sets: fix a bug in model building, another in handling set of setsKshitij Bansal
2014-04-28nodemanager robust skolem numberingKshitij Bansal
2014-04-24optimizationKshitij Bansal
2014-04-17use internal skolem numberingKshitij Bansal
2014-04-09fixKshitij Bansal
2014-04-09prep for fixKshitij Bansal
2014-04-09try foreach on CD datastructureKshitij Bansal
2014-04-09moreKshitij Bansal
2014-04-09some debugging changesKshitij Bansal
2014-03-28add construles, type_rules rm redundant, kinds cleanupKshitij Bansal
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-20rewriter fix, weaken an assertionKshitij Bansal
2014-03-20constant normal form and rewriteKshitij Bansal
2014-03-20fix a sharing issues with setsKshitij Bansal
2014-03-20work on set modelKshitij Bansal
2014-02-28theory/sets: cleanupKshitij Bansal
2014-02-28rename kind::IN to kind::MEMBER (fixes some windows build conflicts)Kshitij Bansal
2014-02-21disable test cvc3_main, attempt to fix dist_checkKshitij Bansal
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