Age | Commit message (Collapse) | Author |
|
and regressions (#6943)
This commit makes TheoryEngine take into account whether theories are using the central equality engine.
With this commit, the central equality engine can now be optionally enabled via `--ee-mode=central`.
|
|
|
|
This removes benchmarks for the following reasons:
- regress1/arith/arith-int are removed since there are many similar regressions (10 from this set are already enabled)
- bitvector cvc benchmarks are removed since their *.smt2 benchmarks are enabled
- other benchmarks are removed due to features we do not plan to support
- one placeholder benchmark is removed
|
|
Removed subtyping for sets in type_node.h
Fixes #4502, fixes #4631.
|
|
This PR removes subtyping for sets theory due to issues like #4502, #4507 and #4631.
Changes:
Add SingletonOp for singletons to specify the type of the single element in the set.
Add mkSingleton to the solver to enable the user to pass the sort of the single element.
Update smt and cvc parsers to use mkSingleton when the kind is SINGLETON
|
|
This renames api::Solver::checkValidAssuming to checkEntailed and
removes api::Solver::checkValid. Internally, SmtEngine::query is renamed
to SmtEngine::checkEntailed, and these changes are further propagated to
the Result class.
|
|
|
|
This commit adds a check to make sure that the result of a `(check-sat)`
call matches the expected result set via `(set-info :status ...)`. In
doing so, it also fixes an issue where CVC4 would crash if asked for the
unsat core after setting the status to `unsat` but before calling
`(check-sat)` (see regression for concrete example). This happened
because CVC4 was storing the expected result and the computed result
both in the same variable (the expected result wasn't really being used
though). This commit keeps track of the expected result and the computed
result in separate variables to fix that issue.
|
|
This was causing assertion failures when using Sets + Sygus.
|
|
|
|
|
|
Make sets theory properly handle equalities between (Set T1) and (Set T2) whenever equalities between T1 and T2 are also handled. Generalizes previous approach for type correctness conditions. Add regression.
|
|
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.
|
|
|
|
* Remove unhandled subtypes, which consequently makes typing rules uniformly stricter based on weakening the subtype relation. Ensure coercions in the smt2 and cvc parser for Real decimal constants whose type is Integer. Ensure type annotations are computed during preRewrite to ensure rewriting (which does not preserve types) does not impact term construction for parametric datatypes. This fixes issue #1048 (we now give an type exception).
* Update unit test for parametric datatypes to reflect new subtyping relation.
* Remove deprecated test.
* Make array construction for lambdas work with new subtype relations to handle lambdas like (lambda ((x Int) (y Int)) (ite (= x 0) 0.5 0.0)).
|
|
* 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
|
|
sygus), update regressions.
|
|
cbqi, tptp parser), fix full saturation instantiation to not loop in rare case, update regressions, update casc scripts.
|
|
|
|
|
|
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.
|
|
|
|
|
|
Some further cleanup/fixes pending
This is squash of 39 commits (kbansal/card branch + cleanup):
* add card operator
* local reasoning
* towards graph building
* first implementation
* close cardinality terms
* model building
* more
* more
* more
* Add aggressive sets rewriting.
* Recursively aggressive rewrite sets.
* Fix
* incomplete card2 implementation
* ...
* Avoid using auto in sets.
* fix merge
* more
* ...
* more
* ...
* Fixed for loops
* Slight modification to computeRelevantTerms
* more
* ..
* more
* ...
* mv empty set lemma generation to later point
* more options/reordering
* debug related
* more trace
* ...
* fix merge_nodes, models
* rm warnigns
* fix compile errors
* warning
* bug fixes/cleanup
* mroe fixes
* cleanup
* ...
|
|
|
|
- added more benchmarks for pressure and theory combination tests
- fixed find terms method in trie data structure
- use a separate membership map to store positive membership terms
|
|
- send out facts as lemmas
- fixed the non-termination problem caused by sending facts as lemmas
- unfolded symbolic tuples by adding equality lemmas
|