summaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2017-01-04Reverting two files encoding with DOS linebreaks back into using unix ↵Tim King
linebreaks.
2017-01-04Merge pull request #122 from 4tXJ7f/fix_lfsc_strAndrew Reynolds
[LFSC] Minor fixes/improvements
2017-01-04Merge pull request #120 from 4tXJ7f/fix_f_pp_holesguykatzz
Fix dependency tracing for fewerPreprocessingHoles
2017-01-04Merge pull request #121 from 4tXJ7f/fix_lfsc_mem_leaksAndrew Reynolds
[LFSC] Fix memory leaks when creating CExprs
2016-12-29Changing 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-29Eliminating a signed vs. unsigned comparison.Tim King
2016-12-29Changing getTearDownIncremental() to return the type of ↵Tim King
options::tearDownIncremental.
2016-12-29Adding a destructor to InstantiationNotify.Tim King
2016-12-29Adding a destructor to RepBoundExt.Tim King
2016-12-29Reordering sep and sets in Makefile.theories.Tim King
2016-12-28[LFSC] Minor fixes/improvementsAndres 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_leaksAndres 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-16Fix dependency tracing for fewerPreprocessingHolesAndres 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-14Merge pull request #119 from 4tXJ7f/smt_v2_5Clark Barrett
Switch from SMT-LIB v2.0 to v2.5 for smt2 files
2016-12-14Switch from SMT-LIB v2.0 to v2.5 for smt2 filesAndres 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-14Made tear-down-incremental more like it used to be: when tear-down valueClark Barrett
is 1, it does not automatically enable incremental mode.
2016-12-13Merge pull request #118 from 4tXJ7f/fix_empAndrew Reynolds
Fix split-find-unsat-w-emp test
2016-12-12Merge pull request #117 from 4tXJ7f/fix_orderClark Barrett
Fix initialization order
2016-12-12Fix split-find-unsat-w-emp testAndres Notzli
Commit 2f2e9fcf1fbb27f8e799aeac2372c0a9113f01aa did not update the split-find-unsat-w-emp test, this commit fixes that.
2016-12-11Merge branch 'master' into fix_orderClark Barrett
2016-12-11Merge pull request #116 from 4tXJ7f/fix_multClark Barrett
Fix (inactive) `MultSlice` rewrite
2016-12-09Fixing a use after free bug in Polynomial::denominatorLCM.Tim King
2016-12-08Fix initialization orderAndres Notzli
This commit addresses the following warning: ``` warning: field 'd_negOne' will be initialized after field 'd_pivots' [-Wreorder] ```
2016-12-08Fix (inactive) `MultSlice` rewriteAndres 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-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-12-07Fix boolean term conversion for INST_ATTRIBUTE, fixes bug 764.ajreynol
2016-12-07Merge branch 'master' of https://github.com/CVC4/CVC4guykatzz
2016-12-07Turned off nonClausalSimplify when using fewerPreprocessingHoles.guykatzz
It was turned off for unsatCores, and fewerPreprocessingHoles using the same infrastructure.
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-07Fix nf exp tracking for non-linear string equalities, fixes bug 768.ajreynol
2016-12-06Improve bounds for global heap in sep, refactor preprocessing. Minor ↵ajreynol
improvement to sets.
2016-12-05Added "dump=raw-benchmark" option for dumping all user commands exactly as ↵Clark Barrett
received.
2016-12-03Fix unit test for datatypes, add interface functions to datatypes.ajreynol
2016-12-02Fix for bug 734Clark Barrett
2016-12-02Cleaning up Statistics::copyFrom to avoid casts.Tim King
2016-12-02Initializing the d_pivots variable.Tim King
2016-12-02Merge pull request #95 from 4tXJ7f/fix_sierra_buildTim King
Revert "Removing the CVC4_NEEDS_REPLACEMENT_FUNCTIONS guard to have a…
2016-12-02Merge pull request #113 from 4tXJ7f/remove_extract_ruleClark Barrett
Remove wrong `ExtractMultLeadingBit` rule
2016-12-02Bug fixes and refactoring of parametric datatypes, add some regressions.ajreynol
2016-12-02Refactor preprocessing of models in fmf. Fix options --fmf-empty-sorts and ↵ajreynol
--fmf-fun-rlv, fixes bug 723.
2016-12-01Fix build on macOS SierraAndres Notzli
Before this fix, the build died with `ar: no archive members specified when linking the empty libreplacements.la.` because macOS Sierra does not require the replacements anymore. With this fix, `ffs.c` and `strtok_r.c` are always getting compiled (even when they are empty) to prevent the error. Also removed the unused `CVC4_NEEDS_REPLACEMENT_FUNCTIONS` from `configure.ac` and added an `#ifndef HAVE_FFS` to `ffs.c` for consistency with `strtok_r.c`.
2016-12-01Fix quantifiers dynamic splitting module for incremental mode, fixes bug 765 ↵ajreynol
and 763.
2016-12-01Improvement and bug fix for str.indexof reduction, add regression. Other ↵ajreynol
minor changes.
2016-11-30Remove wrong `ExtractMultLeadingBit` ruleAndres 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-30Merge pull request #115 from 4tXJ7f/bug766Clark Barrett
Fix parsing of BVROTR by CVC parser
2016-11-30Merge pull request #114 from 4tXJ7f/add_unit_testClark Barrett
Add unit test for `MultDistrib` rule
2016-11-30Fix parsing of BVROTR by CVC parserAndres Notzli
This commit fixes Bugzilla bug 766 as proposed by jacobly.alt@gmail.com.
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback