| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2017-02-16 | Minor fixes for relations, quantifiers dsplit. | ajreynol | |
| 2017-02-16 | Fixes for sets+rels check. Minor. | ajreynol | |
| 2017-02-15 | Minimization modes for fmf bound. | ajreynol | |
| 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-18 | Merge pull request #128 from 4tXJ7f/fix_lfsc_perf | Andrew Reynolds | |
| [LFSC] Fix performance issues, more determinism | |||
| 2017-01-18 | Minor fix in relations. | ajreynol | |
| 2017-01-16 | [LFSC] Fix performance issues, more determinism | Andres Notzli | |
| For certain proofs, the performance was drastically different on different OSes. The cause for this difference was a pointer comparison in the deduplication in `Expr::defeq()`. Depending on how the OS allocated the memory, an expression `a` would get replaced with an equivalent expression `b` or vice versa, which in turn affected performance of `Expr::free_in()` dramatically (sub-second vs. >5 min running times). This commit makes the process more deterministic by using a heuristic that favors symbolic expressions and greedily tries to make small refcounts smaller when replacing, and changes `Expr::free_in()` to not repeatedly explore the same subexpressions. | |||
| 2017-01-13 | Fix call to SExpr constructor for greater portability. | Clark Barrett | |
| 2017-01-13 | Merge pull request #130 from chadbrewbaker/master | Clark Barrett | |
| Fixing memory leak | |||
| 2017-01-13 | Do not rewrite explanations in strings. | ajreynol | |
| 2017-01-11 | Merge pull request #129 from timothy-king/regression-scrubber | Clark Barrett | |
| Adding regression test scrubbing. | |||
| 2017-01-11 | Merge pull request #131 from makaimann/fix_702 | Clark Barrett | |
| Proposed fix for bug 702 | |||
| 2017-01-11 | Proposed fix for bug 702. Checks to make sure the Expr's operator is not of ↵ | makaimann | |
| kind BUILTIN before passing to prefixPrintGetValue() | |||
| 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-11 | Merge pull request #127 from cristian-mattarei/issue_679 | Clark Barrett | |
| Bug 679 fix | |||
| 2017-01-10 | revert | Chad Brewbaker | |
| 2017-01-10 | Quashing memory leak | Chad Brewbaker | |
| 2017-01-10 | Adding regression test scrubbing. | Tim King | |
| 2017-01-08 | With reference to Bug 679, this commit integrates part of the patch ↵ | Cristian Mattarei | |
| proposed, and it fixes the correct float parsing of an std::istringstream. The compilation issue in Bug 679 does not apply anymore with gcc6.3.1 | |||
| 2017-01-06 | quashing debug memory leak | Chad Brewbaker | |
| 2017-01-06 | Minor fix for sets. | ajreynol | |
| 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 | Marking the proof signature files as non-executable. | Tim King | |
| 2017-01-04 | Setting the executable bit for the newer run scripts in contrib. | Tim King | |
| 2017-01-04 | Reverting two files encoding with DOS linebreaks back into using unix ↵ | Tim King | |
| linebreaks. | |||
| 2017-01-04 | Merge pull request #122 from 4tXJ7f/fix_lfsc_str | Andrew Reynolds | |
| [LFSC] Minor fixes/improvements | |||
| 2017-01-04 | Merge pull request #120 from 4tXJ7f/fix_f_pp_holes | guykatzz | |
| Fix dependency tracing for fewerPreprocessingHoles | |||
| 2017-01-04 | Merge pull request #121 from 4tXJ7f/fix_lfsc_mem_leaks | Andrew Reynolds | |
| [LFSC] Fix memory leaks when creating CExprs | |||
| 2016-12-29 | Changing a set of TNodes to a set of Nodes in the BV inequality solver. The ↵ | Tim King | |
| ref count of the TNodes in the set can become 0. Set operations containing garbage collected TNodes could then fail. | |||
| 2016-12-29 | Eliminating a signed vs. unsigned comparison. | Tim King | |
| 2016-12-29 | Changing getTearDownIncremental() to return the type of ↵ | Tim King | |
| options::tearDownIncremental. | |||
| 2016-12-29 | Adding a destructor to InstantiationNotify. | Tim King | |
| 2016-12-29 | Adding a destructor to RepBoundExt. | Tim King | |
| 2016-12-29 | Reordering sep and sets in Makefile.theories. | Tim King | |
| 2016-12-28 | [LFSC] Minor fixes/improvements | Andres Notzli | |
| - Avoid mixing new/delete with malloc/free - Remove reimplementation of strcmp - Add assertions | |||
| 2016-12-28 | [LFSC] Fix memory leaks when creating CExprsfix_lfsc_mem_leaks | Andres Notzli | |
| In certain cases, LFSC was creating CExprs with the single-argument constructor, which allocates an array of one child, only to immediately replace it with a new array (without deleting the old one). Additionally, this commit fixes the construction of TYPE/KIND/MPZ/MPQ expressions (the null pointer is appended automatically by the single argument constructor, an array with two null pointer entries should not be necessary). | |||
| 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-14 | Merge pull request #119 from 4tXJ7f/smt_v2_5 | Clark Barrett | |
| Switch from SMT-LIB v2.0 to v2.5 for smt2 files | |||
| 2016-12-14 | Switch from SMT-LIB v2.0 to v2.5 for smt2 files | Andres Notzli | |
| As mentioned in bug 741, CVC4 was parsing `.smt2` files using the SMT-LIB v2.0 standard by default. This commit switches to v2.5. | |||
| 2016-12-14 | Made tear-down-incremental more like it used to be: when tear-down value | Clark Barrett | |
| is 1, it does not automatically enable incremental mode. | |||
| 2016-12-13 | Merge pull request #118 from 4tXJ7f/fix_emp | Andrew Reynolds | |
| Fix split-find-unsat-w-emp test | |||
| 2016-12-12 | Merge pull request #117 from 4tXJ7f/fix_order | Clark Barrett | |
| Fix initialization order | |||
| 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-11 | Merge branch 'master' into fix_order | Clark Barrett | |
| 2016-12-11 | Merge pull request #116 from 4tXJ7f/fix_mult | Clark Barrett | |
| Fix (inactive) `MultSlice` rewrite | |||
| 2016-12-09 | Fixing a use after free bug in Polynomial::denominatorLCM. | Tim King | |
 |
index : cvc5.git | |
| CVC4 is an efficient open-source automatic theorem prover for satisfiability modulo theories (SMT) problems. | git repository hosting |
| summaryrefslogtreecommitdiff |
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback