Age | Commit message (Collapse) | Author | |
---|---|---|---|
2017-03-03 | Another minor fix for sets related to sharing + finite element types. | ajreynol | |
2017-03-02 | Fixes related to sets. | ajreynol | |
2017-03-02 | Minor cleanup and reorganization related to last commit. | ajreynol | |
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-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 |