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-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 | Minor fix in relations. | ajreynol | |
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 | 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 | 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-04 | Fix for tff type declarations inTPTP parser, fixes bug 748. Other minor ↵ | ajreynol | |
changes. | |||
2017-01-04 | Merge pull request #120 from 4tXJ7f/fix_f_pp_holes | guykatzz | |
Fix dependency tracing for fewerPreprocessingHoles | |||
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-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 | 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-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 | |
2016-12-08 | Fix initialization order | Andres Notzli | |
This commit addresses the following warning: ``` warning: field 'd_negOne' will be initialized after field 'd_pivots' [-Wreorder] ``` | |||
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-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 | Merge branch 'master' of https://github.com/CVC4/CVC4 | guykatzz | |
2016-12-07 | Turned off nonClausalSimplify when using fewerPreprocessingHoles. | guykatzz | |
It was turned off for unsatCores, and fewerPreprocessingHoles using the same infrastructure. | |||
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-06 | Improve bounds for global heap in sep, refactor preprocessing. Minor ↵ | ajreynol | |
improvement to sets. | |||
2016-12-05 | Added "dump=raw-benchmark" option for dumping all user commands exactly as ↵ | Clark Barrett | |
received. | |||
2016-12-03 | Fix unit test for datatypes, add interface functions to datatypes. | ajreynol | |
2016-12-02 | Fix for bug 734 | Clark Barrett | |
2016-12-02 | Cleaning up Statistics::copyFrom to avoid casts. | Tim King | |
2016-12-02 | Initializing the d_pivots variable. | Tim King | |
2016-12-02 | Merge pull request #95 from 4tXJ7f/fix_sierra_build | Tim King | |
Revert "Removing the CVC4_NEEDS_REPLACEMENT_FUNCTIONS guard to have a… | |||
2016-12-02 | Merge pull request #113 from 4tXJ7f/remove_extract_rule | Clark Barrett | |
Remove wrong `ExtractMultLeadingBit` rule |