summaryrefslogtreecommitdiff
path: root/test/regress/regress0/sets
AgeCommit message (Collapse)Author
2021-07-29Integrate central equality engine approach into theory engine, add option ↵Andrew Reynolds
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`.
2021-06-02Remove redundant logic ALL_SUPPORTED. (#6664)Aina Niemetz
2020-12-09Remove obsolete regressions (#5633)Andrew Reynolds
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
2020-10-05Remove subtyping for sets (#5205)mudathirmahgoub
Removed subtyping for sets in type_node.h Fixes #4502, fixes #4631.
2020-10-04Remove subtyping for sets theory (#5179)mudathirmahgoub
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
2020-03-31Rename checkValid/query to checkEntailed. (#4191)Aina Niemetz
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.
2019-12-13Add support for set comprehension (#3312)Andrew Reynolds
2019-06-04Add check that result matches benchmark status (#3028)Andres Noetzli
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.
2018-12-14 Fix extended rewriter for binary associative operators. (#2751)Andrew Reynolds
This was causing assertion failures when using Sets + Sygus.
2018-09-22cmake: Added regression tests and target make regress.Aina Niemetz
2018-09-22cmake: Added initial build infrastructure.Aina Niemetz
2018-05-03Sets subtypes (#1095)Andrew Reynolds
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.
2018-03-21 Move regression tests to single Makefile.am (#1658)Andres Noetzli
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.
2018-02-15Refactor regressions (#1581)Andrew Reynolds
2017-09-14Remove unhandled subtypes (#1098)Andrew Reynolds
* 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)).
2017-09-10Ensure that expand definitions is called on all non-variable expressi… (#1070)Andrew Reynolds
* 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
2017-08-04Set default language to smt lib 2.6 (including as a base language for ↵ajreynol
sygus), update regressions.
2017-06-30Minor change to trigger selection, fixes related to subtypes (in macros, ↵ajreynol
cbqi, tptp parser), fix full saturation instantiation to not loop in rare case, update regressions, update casc scripts.
2017-04-23Changing spaces to tabs in Makefile.Tim King
2017-04-21Handle subtypes in sets. Bug fixes for tuples with subtypes.ajreynol
2017-04-19Fixes for handling set universe: restrict upwards rule for universe to ↵ajreynol
memberships into variable sets, do not variable eliminate sets during ppAssert.
2017-04-14Actively split for upwards closusure intersection. Minor clean up, add ↵ajreynol
regressions.
2017-03-20fixed cvc4 parser for set complementPaul Meng
2017-03-07More fixes for printing/parsing sets, fix kind name.ajreynol
2017-03-07Fix cvc parser for set compliment.ajreynol
2017-03-06Support for set compliment and universe set. Simplify approach for sep.nil ↵ajreynol
nodes.
2017-03-03Fix for collectModelInfo related to finite types + preregistration. ↵ajreynol
Generalize previous fix for sets, minor changes to Datatypes.
2017-03-03Another minor fix for sets related to sharing + finite element types.ajreynol
2017-03-02Fixes related to sets.ajreynol
2016-12-08Enable remaining cardinality benchmarksajreynol
2016-12-07Add missing regressionajreynol
2016-12-07Add sets regression, fixes bug 754. Minor fix to regexp in strings.ajreynol
2016-12-07Added cardinality to cvc language, fixes bug 753. Throw logic exception when ↵ajreynol
using cardinality on sets with finite element type.
2016-11-17Fix Makefiles in testAndres Notzli
With the recent changes to the regress tests, some of the Makefiles were not in sync anymore. This commit fixes that.
2016-10-21Move slow regress0 benchmarks to regress1, increment regress1 through regress3.ajreynol
2016-10-13Revert "Merge branch 'origin' of https://github.com/CVC4/CVC4.git"Tim King
This reverts commit 3395c5c13cd61d98aec0d9806e3b9bc3d707968a, reversing changes made to 5f415d4585134612bc24e9a823289fee35541a01.
2016-10-11Merge branch 'origin' of https://github.com/CVC4/CVC4.gitPaul Meng
Conflicts: src/options/quantifiers_options
2016-09-28Fix the merge of kbansal/card branch (2039eab).Kshitij Bansal
A bug was introduced in the cleanup process as preparation for the merge (theory_sets_private.cpp, lines 2502-2508 in this commit).
2016-09-13refactored the code, added more benchmarks and minor fixesPaul Meng
2016-09-12fixed capitalized "kind"Paul Meng
2016-08-30added more benchmarksPaul Meng
2016-08-24Merge remote-tracking branch 'origin/master'PaulMeng
2016-08-12Add a few more regressions.ajreynol
2016-08-12Minor fixes to model construction to take singleton equivalence classes into ↵ajreynol
account (fixes sets+dt model bug). Minor fix for mixed int/real quantifier instantiation.
2016-04-20update from the masterPaulMeng
2016-04-12added more benchmarksPaulMeng
2016-04-09cardinality operation for finite sets (based on my thesis / ijcar16 paper)Kshitij Bansal
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 * ...
2016-03-10fixed the transpose-occur rulePaulMeng
2016-03-08make skolems and tuple reduction terms as shared termsPaulMeng
- 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
2016-03-04refactored the codePaulMeng
- send out facts as lemmas - fixed the non-termination problem caused by sending facts as lemmas - unfolded symbolic tuples by adding equality lemmas
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback