summaryrefslogtreecommitdiff
path: root/test/regress/regress0/fmf
AgeCommit message (Collapse)Author
2020-01-30Ensure literals in FMF decision strategies are in the CNF stream (#3669)Andrew Reynolds
2019-09-18Decouple fmf-bound and finite-model-find (#3297)Andrew Reynolds
2019-09-06Remove SMT1 parser. (#3228)Mathias Preiner
This commit removes the SMT1 parser infrastructure and adds the SMT2 translations of the SMT1 regression tests. For now this commit removes regression test regress3/pp-regfile.smt since the SMT2 translation has a file size of 887M (vs. 172K for the SMT1 version). Fixes #2948 and fixes #1313.
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-11Remove alternate versions of mbqi (#2742)Andrew Reynolds
2018-09-22cmake: Added regression tests and target make regress.Aina Niemetz
2018-09-22cmake: Added initial build infrastructure.Aina Niemetz
2018-08-28Fix sort inference for quantified variables of interpreted types (#2393)Andrew Reynolds
2018-08-17 Fix spurious warning in sort inference (#2331)Andrew Reynolds
2018-08-15Make sort inference a preprocessing pass (#2309)Andrew Reynolds
2018-04-05 Python regression script (#1662)Andres Noetzli
Until now, we have been using a bash script for the running the regressions. That script had several issues, e.g. it was creating many temprorary files and it was calling itself recursively, making it difficult to maintain. This commit replaces the script with a Python script. The Python script uses the TAP protocol, which allows us to display the results of multiple tests per file (e.g. with --check-models and without) separately and with more details. It also outputs whenever it starts running a test, which allows finding "stuck" regression tests on Travis. As recommended in the automake documentation [0], the commit copies the TAP driver to enable TAP support for the test driver. Note: the commit also changes some of the regressions slightly because we were using "%" for the test directives in SMT files which does not correspond to the comment character ";". Using the comment character simplifies the handling and makes it easier for users to reproduce a failure (they can simply run CVC4 on the regression file). [0] https://www.gnu.org/software/automake/manual/html_node/Use-TAP-with-the-Automake-test-harness.html
2018-03-23Add a few quantifiers regressions to improve coverage (#1702)Andrew Reynolds
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-11-03Suppport SAT logic (#1310)Andrew Reynolds
* Support SAT logic. * Add lustre example. * Add to smt1 as well. * Fix. * Fix. * Fix for new option.
2017-09-28Improve finite model finding for recursive predicates (#1150)Andrew Reynolds
* Optimization for model finding for recursive functions involving branching positions. Update documentation, add regressions. * Simplifications, update comments.
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-31Answer unknown when uf-ss=no-minimal is combined with cardinality ↵Andrew Reynolds
constraints from user input, add regressions. (#1060)
2017-08-04Set default language to smt lib 2.6 (including as a base language for ↵ajreynol
sygus), update regressions.
2017-05-31Minor change to defaults, update smt comp script, minor changes to options ↵ajreynol
in regressions.
2017-05-05Do not eliminate extended arithmetic symbols when finite model finding is ↵ajreynol
on, add regression.
2017-04-28Do not eliminate non-standard arithmetic operators in recursive function ↵ajreynol
definitions, add regression.
2017-04-24Fixes and simplifications for fmf mbqi.ajreynol
2017-04-14Fix for fmf-fun when the option is set by user command.ajreynol
2017-04-05Caching for fun def process, add regression.ajreynol
2017-03-22Minor fix for bounded integers.ajreynol
2017-03-15Allow 0 argument recursive functions. Fixes bug 782.ajreynol
2017-03-02Eliminate Boolean term conversion. Generalizes removeITE pass to remove ↵ajreynol
Boolean terms, treats distinguished BOOLEAN_TERM_VARIABLE kind as theory literal. Fixes bugs 597, 604, 651, 652, 691, 694. Add regressions.
2017-02-07Generalize finite bound inference to unifiable variables in set membership ↵ajreynol
literals.
2017-01-11Fix for when variables are (partially) bound in multiple ways, add ↵ajreynol
regression. Improve printing for bound int module. Track when relations are enabled in sets, set incomplete if card+rels are both enabled since model construction is not guaranteed to succeed.
2017-01-04Marking regression test files as non-executable.Tim King
2016-12-07Fix boolean term conversion for INST_ATTRIBUTE, fixes bug 764.ajreynol
2016-12-07Refactoring, generalization of bounded inference module. Simplification of ↵ajreynol
rep set iterator. Disable quantifiers dynamic splitting for variables that are inferred bounded. Minor changes to fmc mbqi. Add regressions.
2016-12-02Refactor preprocessing of models in fmf. Fix options --fmf-empty-sorts and ↵ajreynol
--fmf-fun-rlv, fixes bug 723.
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-06-01Initial infrastructure for bounded set quantification (disabled). ↵ajreynol
Refactoring and fixes for --fmf-bound-int. Fix simple memory leaks in strings and bounded integers.
2016-05-23Fix related to parametric sorts whose interpretation is finite due to ↵ajreynol
uninterpreted sorts + FMF. Generalizes previous fix in term registration visitor.
2016-04-11Minor fixes for inst match generators. Updates to qip.googleajreynol
2016-04-10More work on instantiation propagation. Enable external filtering of ↵ajreynol
instantiations. All quantifiers strategies terminate when a conflict can be established.
2016-03-07Minor change to F-Length inference in strings. No internal tracking of ↵ajreynol
cardinality assertions in uf. Change fullModel false array collectModelInfo to assign constants.
2016-02-23Fix term database for non-equal, congruent terms in master equality engine. ↵ajreynol
Disable ITE terms in quant conflict find.
2016-02-19Fixes and improvements for datatypes properties and splitting.ajreynol
2016-02-18Implement dynamic splitting for quantified formulas. Minor refactoring of ↵ajreynol
reductions in quantifiers engine.
2016-02-09Fix regression, minor change to output.ajreynol
2016-02-08Updates related to finite model finding and (co)datatypes. Bug fix ↵ajreynol
enumerator and codatatype rewriter, further simplify fmc.
2016-02-01Simplify fmc model construction, add regression. Improve FMF debug assertions.ajreynol
2016-01-20Fix bug in fmc mbqi where modelscomputed for mbqi could involve non-constant ↵ajreynol
values. Add regression.
2016-01-19Bug fixes for model construction with codatatypes, add regressions.ajreynol
2016-01-18Bug fix rewriter for fun defs.ajreynol
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback