Age | Commit message (Collapse) | Author | |
---|---|---|---|
2017-03-02 | Eliminate 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-07 | Generalize finite bound inference to unifiable variables in set membership ↵ | ajreynol | |
literals. | |||
2017-01-30 | Fix regexp cache issue in strings, add regression. | ajreynol | |
2017-01-18 | Fix non-idempotent rewrite in Array rewriter | Andres Noetzli | |
This commit fixes bug 637 ( http://church.cims.nyu.edu/bugzilla3/show_bug.cgi?id=637 ) as proposed in Bugzilla and adds the minified test case to the regression tests. | |||
2017-01-11 | Merge pull request #129 from timothy-king/regression-scrubber | Clark Barrett | |
Adding regression test scrubbing. | |||
2017-01-11 | Fix 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-10 | Adding regression test scrubbing. | Tim King | |
2017-01-05 | Disabling a regression test that assumes CVC4 is configured with proofs on. ↵ | Tim King | |
Modifying the travis rules so there are instances with proofs disabled. | |||
2017-01-04 | Fix for tff type declarations inTPTP parser, fixes bug 748. Other minor ↵ | ajreynol | |
changes. | |||
2017-01-04 | Marking regression test files as non-executable. | Tim King | |
2017-01-04 | Reverting two files encoding with DOS linebreaks back into using unix ↵ | Tim King | |
linebreaks. | |||
2016-12-16 | Fix dependency tracing for fewerPreprocessingHoles | Andres Notzli | |
Previously, dependency tracing in `ite_removal.cpp` was only done with the `unsatCores` option but `fewerPreprocessingHoles` requires dependencies, too. This lead to errors during proof construction when `fewerPreprocessingHoles` was active. This commit fixes the condition and includes a test case that previously failed. Additionally, it fixes a similar issue in the theory engine. NOTE: this commit might not fix all instances of this problem. `smt_engine.cpp` turns certain flags off with `unsatCores`. Compatibility between those flags and `fewerPreprocessingHoles` needs to be checked separately. | |||
2016-12-12 | Fix split-find-unsat-w-emp test | Andres Notzli | |
Commit 2f2e9fcf1fbb27f8e799aeac2372c0a9113f01aa did not update the split-find-unsat-w-emp test, this commit fixes that. | |||
2016-12-08 | Fix (inactive) `MultSlice` rewrite | Andres Notzli | |
The `MultSlice` rewrite was previously accepting multiplications of three and more variables even though it was designed for multiplications of two variables only. Fortunately, the rewrite was not actively used in the bitvector solver. This commit strengthens the condition in `applies()` and adds a unit test that checks that x * y * z and x * y do not get rewritten to the same term. | |||
2016-12-08 | Enable remaining cardinality benchmarks | ajreynol | |
2016-12-07 | Add missing regression | ajreynol | |
2016-12-07 | Add sets regression, fixes bug 754. Minor fix to regexp in strings. | ajreynol | |
2016-12-07 | Added cardinality to cvc language, fixes bug 753. Throw logic exception when ↵ | ajreynol | |
using cardinality on sets with finite element type. | |||
2016-12-07 | Fix boolean term conversion for INST_ATTRIBUTE, fixes bug 764. | ajreynol | |
2016-12-07 | Refactoring, 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-07 | Fix nf exp tracking for non-linear string equalities, fixes bug 768. | ajreynol | |
2016-12-02 | Fix for bug 734 | Clark Barrett | |
2016-12-02 | Merge pull request #113 from 4tXJ7f/remove_extract_rule | Clark Barrett | |
Remove wrong `ExtractMultLeadingBit` rule | |||
2016-12-02 | Bug fixes and refactoring of parametric datatypes, add some regressions. | ajreynol | |
2016-12-02 | Refactor preprocessing of models in fmf. Fix options --fmf-empty-sorts and ↵ | ajreynol | |
--fmf-fun-rlv, fixes bug 723. | |||
2016-12-01 | Fix quantifiers dynamic splitting module for incremental mode, fixes bug 765 ↵ | ajreynol | |
and 763. | |||
2016-12-01 | Improvement and bug fix for str.indexof reduction, add regression. Other ↵ | ajreynol | |
minor changes. | |||
2016-11-30 | Remove wrong `ExtractMultLeadingBit` rule | Andres Notzli | |
The rule `ExtractMultLeadingBit` estimated the number of leading zeros wrong: when there were ones in the leading constant parts of the factors, it was using the length of the non-zero part instead of the length of the zero part. This commit includes an example for which the previous version of the rule would cause a wrong answer. | |||
2016-11-30 | Merge pull request #115 from 4tXJ7f/bug766 | Clark Barrett | |
Fix parsing of BVROTR by CVC parser | |||
2016-11-30 | Fix parsing of BVROTR by CVC parser | Andres Notzli | |
This commit fixes Bugzilla bug 766 as proposed by jacobly.alt@gmail.com. | |||
2016-11-30 | Add unit test for `MultDistrib` rule | Andres Notzli | |
This unit test checks that the issue fixed by commit c0c424283c12cfce2874ea92188487d91acecdf3 has been resolved. | |||
2016-11-21 | Remove unused, libstdc++-exclusive include | Andres Notzli | |
The file `ext/stdio_filebuf.h` does not seem to be available in libc++, which made compilation of the unit tests for macOS unnecessarily complicated given that it is not used anyway. | |||
2016-11-18 | Fix for unit test after changing default "all supported" logic name. | Clark Barrett | |
2016-11-18 | Merge pull request #110 from 4tXJ7f/fix_makefiles | Clark Barrett | |
Fix Makefiles in test | |||
2016-11-18 | Modified a couple of regressoins to use ALL/QF_ALL instead of ↵ | Clark Barrett | |
ALL_SUPPORTED/QF_ALL_SUPPORTED | |||
2016-11-17 | Fix Makefiles in test | Andres Notzli | |
With the recent changes to the regress tests, some of the Makefiles were not in sync anymore. This commit fixes that. | |||
2016-11-13 | Switching a large allocation to be heap allocated. | Tim King | |
2016-11-13 | Deleting a parsed Command in the interactive_shell_black test. | Tim King | |
2016-11-12 | Merge pull request #106 from timothy-king/cvc-parser-exception-leaks | Clark Barrett | |
Adding garbage collection for the CVC Parser for Commands when except… | |||
2016-11-12 | Fixed a bug in cdhashmap in which doubly-linked list was not properly ↵ | Clark Barrett | |
cleaned up on a call to obliterate. Also, removed some experimental code and a unit test from cdmap_black that used it. This test created a CDList *in* context memory which seems like a very bad idea (and it was improperly implemented resulting in a memory leak). | |||
2016-11-11 | Adding garbage collection for the CVC Parser for Commands when exceptions ↵ | Tim King | |
are thrown. | |||
2016-11-11 | Merge pull request #105 from timothy-king/delete-maxed-out | Tim King | |
Adding garbage collection of nodes with maxed out reference counts. | |||
2016-11-11 | Deleting successfully parsed commands in the parser_black unit test. | Tim King | |
2016-11-11 | Add simple inferences for extended bitvector functions, add a few related ↵ | ajreynol | |
options. Use bv2nat, int2bv as triggers. Add regressions. | |||
2016-11-10 | Fixing a delete vs free mismatch in parser_builder_black.h. | Tim King | |
2016-11-10 | Adding garbage collection of nodes with maxed out reference counts. | Tim King | |
2016-11-08 | Add a few options to separation logic and sets. Minor changes to separation ↵ | ajreynol | |
logic, change syntax for empty heap constraint. | |||
2016-11-07 | Disabling out of memory tests unit tests when ASAN is enabled. ASAN failures ↵ | Tim King | |
are too hard for the unit testing framework. | |||
2016-11-07 | Changing ArrayStoreAll's constructor to delay allocation until it is done ↵ | Tim King | |
checking error conditions. This prevents a memory leak in exception throwing branches. | |||
2016-11-07 | Fixing a memory leak in the CnfStream unit tests. | Tim King | |