Age | Commit message (Collapse) | Author |
|
|
|
|
|
|
|
|
|
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))
|
|
now consistent
|
|
* 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".
|
|
|
|
|
|
|
|
|
|
|
|
(was missing for simple triggers). Minor updates to scripts.
|
|
|
|
|
|
|
|
|
|
Sets model
|
|
|
|
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().
|
|
(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)
|
|
|
|
|
|
|
|
cases of nonterminating rewrite-rules regressions.
|
|
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
|