Age | Commit message (Collapse) | Author | |
---|---|---|---|
2017-03-27 | Remove throw qualifiers in type enumerators | Andres Notzli | |
This addresses Coverity issues: - 1172154 - 1172156 - 1172157 - 1172158 - 1172159 - 1379612 - 1379612 - 1421430 - 1172166 - 1172144 - 1362709 - 1362696 - 1172145 - 1172147 - 1172148 - 1379610 - 1362772 - 1362676 - 1362704 - 1362749 - 1362876 - 1362843 - 1362837 - 1362881 - 1172223 - 1172155 | |||
2017-03-24 | Add some regressions. Minor. | ajreynol | |
2017-03-24 | Refactor model building for quantifiers to be a single pass, simplification. ↵ | ajreynol | |
Modify datatypes collect model info to include dt equivalence classes. Further work on sygus. Other minor fixes. | |||
2017-03-22 | Fix more cases of rewritten explanations in strings for bug 784. Minor. | ajreynol | |
2017-03-22 | Minor fix for bounded integers. | ajreynol | |
2017-03-22 | Work on new approach for sygus involving conditional solutions. Refactoring ↵ | ajreynol | |
of sygus solver. Bug fix for sygus solution reconstruction. | |||
2017-03-21 | Improve computeCareGraph functions to check shared term equality status once ↵ | ajreynol | |
per equivalence class pair. | |||
2017-03-18 | Fix for bug 707. | Clark Barrett | |
2017-03-18 | Fix to help with bug 717 | Clark Barrett | |
2017-03-10 | Minor fix for cbqi-all. | ajreynol | |
2017-03-07 | More fixes for printing/parsing sets, fix kind name. | ajreynol | |
2017-03-06 | Do not eagerly construct explanations in relation solver. | ajreynol | |
2017-03-06 | Support for set compliment and universe set. Simplify approach for sep.nil ↵ | ajreynol | |
nodes. | |||
2017-03-06 | Adding support for bool-to-bv | Clark Barrett | |
Squashed commit of the following: commit 5197a663eb262afbeb7740f53b5bd27479dccea0 Author: Clark Barrett <barrett@cs.stanford.edu> Date: Mon Mar 6 00:16:16 2017 -0800 Remove IFF case commit 2119b25a30ed42eca54f632e7232c9f76ae5755a Author: guykatzz <katz911@gmail.com> Date: Mon Feb 20 12:37:06 2017 -0800 proof support for bvcomp commit d8c0c0d2c9c92ce06a5033ec0f3f85ea7bda1a22 Author: Clark Barrett <barrett@cs.stanford.edu> Date: Fri Feb 17 21:09:04 2017 -0800 Added missing cases to operator<< for bv rewrite rules. commit 0ed797c31d0e66cadc35b2397716c841d1aff270 Author: Clark Barrett <barrett@cs.stanford.edu> Date: Fri Feb 17 11:43:51 2017 -0800 Added rewrite rules for new bitvector kinds. commit 3b23dffb317de5559f8a95118fef633f711c114a Author: Clark Barrett <barrett@cs.stanford.edu> Date: Mon Feb 13 14:41:49 2017 -0800 First draft of bool-to-bv pass. | |||
2017-03-03 | Fix for collectModelInfo related to finite types + preregistration. ↵ | ajreynol | |
Generalize previous fix for sets, minor changes to Datatypes. | |||
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 | Minor fix in relations. | ajreynol | |
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 | Adding regression test scrubbing. | Tim King | |
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 | Adding a destructor to InstantiationNotify. | Tim King | |
2016-12-29 | Adding a destructor to RepBoundExt. | 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-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 | 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-02 | Fix for bug 734 | Clark Barrett | |
2016-12-02 | Initializing the d_pivots variable. | Tim King | |
2016-12-02 | Merge pull request #113 from 4tXJ7f/remove_extract_rule | Clark Barrett | |
Remove wrong `ExtractMultLeadingBit` rule |