| Age | Commit message (Collapse) | Author |
|---|
|
Until now, regression tests were split across tens of different
Makefile.am, which required a lot of code duplication and does not
really seem to be in the spirit of automake. If we want to change the
LOG_COMPILER/LOG_DRIVER for example, we have to change every single
Makefile.am, which is cumbersome (I was able to get something
semi-working by exporting those variables but it didn't seem very
clean). Additionally, it made the output of the regression tests fairly
verbose and split the output across multiple log files. Finally
it also limited parallelism when running the regression tests (this fix lowers
the time it takes to run regression level 1 from 3m to 1m45s on my
machine with 16 threads).
This commit moves all the regression tests into
test/regress/Makefile.tests and changes test/regress/Makefile.am to deal
with this new structure. Finally, it changes how the test summary in
test/Makefile.am is produced: instead of relying on the log files for
the subdirectories, it greps for the test results in the log files of
the individual tests. Not the most elegant solution but we should
probably anyway delegate that task to a Python script at some point.
|
|
|
|
* Ensure that expand definitions is called on all non-variable expressions. In particular, it is necessary that the sets theory is notified when a set universe term occurs in the input to ensure options are set correctly. The commit moves this check from within check() to expandDefinitions(), and also adds the check for join image which relies on universe set. This fixes a bug reported by Arjun. Add and update regressions.
* Add comments concerning expandDefinitions
* Expand comment, move to .h
|
|
|
|
|
|
memberships into variable sets, do not variable eliminate sets during ppAssert.
|
|
regressions.
|
|
|
|
|
|
|
|
nodes.
|
|
Generalize previous fix for sets, minor changes to Datatypes.
|
|
|
|
|
|
|
|
|
|
using cardinality on sets with finite element type.
|
|
With the recent changes to the regress tests, some of the Makefiles were
not in sync anymore. This commit fixes that.
|
|
|
|
This reverts commit 3395c5c13cd61d98aec0d9806e3b9bc3d707968a, reversing
changes made to 5f415d4585134612bc24e9a823289fee35541a01.
|
|
Conflicts:
src/options/quantifiers_options
|
|
A bug was introduced in the cleanup process as preparation for the merge
(theory_sets_private.cpp, lines 2502-2508 in this commit).
|
|
|
|
|
|
account (fixes sets+dt model bug). Minor fix for mixed int/real quantifier instantiation.
|
|
added more benchmarks
|
|
fixed typing rules for relational terms
added a benchmark example for the theory of finite relations
|
|
|
|
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))
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
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().
|
|
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
|
