| 2017-04-18 |
Clark Barrett | Fix for bug 639. |
commit | commitdiff | tree |
| 2017-04-14 |
ajreynol | Actively split for upwards closusure intersection.... |
commit | commitdiff | tree |
| 2017-04-14 |
ajreynol | Fix bug related to portfolio with nullary operators. |
commit | commitdiff | tree |
| 2017-04-14 |
ajreynol | Fix nullary operator printers, minor. |
commit | commitdiff | tree |
| 2017-04-14 |
ajreynol | Fix for fmf-fun when the option is set by user command. |
commit | commitdiff | tree |
| 2017-04-13 |
Clark Barrett | Fix for some compilers |
commit | commitdiff | tree |
| 2017-04-12 |
ajreynol | Add nullary operator metakind. |
commit | commitdiff | tree |
| 2017-04-11 |
ajreynol | Bug fix in conjecture generation for --quant-ind. |
commit | commitdiff | tree |
| 2017-04-07 |
ajreynol | Change option names for nl. |
commit | commitdiff | tree |
| 2017-04-06 |
Clark Barrett | Merge pull request #143 from FabianWolff/master |
commit | commitdiff | tree |
| 2017-04-05 |
ajreynol | Fix bug 698. |
commit | commitdiff | tree |
| 2017-04-05 |
ajreynol | Fixes for nlAlgSolveSubs. |
commit | commitdiff | tree |
| 2017-04-05 |
Andrew Reynolds | Merge pull request #145 from 4tXJ7f/fix_lfsc_args |
commit | commitdiff | tree |
| 2017-04-05 |
ajreynol | Caching for fun def process, add regression. |
commit | commitdiff | tree |
| 2017-04-05 |
Andres Notzli | [LFSC] Fix segfault |
commit | commitdiff | tree |
| 2017-04-05 |
ajreynol | Remove extraneous portion of an nl regression. |
commit | commitdiff | tree |
| 2017-04-05 |
ajreynol | Add non-linear regressions, disable nlAlgSubs, do not... |
commit | commitdiff | tree |
| 2017-04-04 |
Fabian Wolff | Fix several spelling errors |
commit | commitdiff | tree |
| 2017-04-04 |
ajreynol | Enable multi-trigger-linear by default, add option. |
commit | commitdiff | tree |
| 2017-04-04 |
ajreynol | Simplify Theory::collectModelInfo interface to not... |
commit | commitdiff | tree |
| 2017-04-04 |
ajreynol | Do not solve for 0-ary non-constant symbols (for which... |
commit | commitdiff | tree |
| 2017-04-04 |
Clark Barrett | Merge pull request #141 from 4tXJ7f/remove_def |
commit | commitdiff | tree |
| 2017-04-03 |
Andrew Reynolds | Merge pull request #142 from timothy-king/nlAlgMerge |
commit | commitdiff | tree |
| 2017-04-03 |
Tim King | Adding a model based axiom instantiation scheme for... |
commit | commitdiff | tree |
| 2017-03-31 |
Andres Notzli | Remove decl. of getStatisticsRegistry(SmtEngine*) |
commit | commitdiff | tree |
| 2017-03-31 |
ajreynol | Add option multi-trigger-linear, minor optimization... |
commit | commitdiff | tree |
| 2017-03-30 |
Clark Barrett | Merge pull request #139 from 4tXJ7f/remove_throw |
commit | commitdiff | tree |
| 2017-03-30 |
Andres Notzli | [Coverity] Remove throw qualifiers in src/smt |
commit | commitdiff | tree |
| 2017-03-30 |
ajreynol | Minor fixes for trigger selection max. |
commit | commitdiff | tree |
| 2017-03-29 |
ajreynol | Add quantifiers options related to model and master... |
commit | commitdiff | tree |
| 2017-03-29 |
PaulMeng | Merge pull request #138 from PaulMeng/master |
commit | commitdiff | tree |
| 2017-03-29 |
Paul Meng | Refactor the standard effort of relational solver |
commit | commitdiff | tree |
| 2017-03-29 |
ajreynol | Fix bug 787. |
commit | commitdiff | tree |
| 2017-03-29 |
Clark Barrett | Fix for bug 733 |
commit | commitdiff | tree |
| 2017-03-28 |
ajreynol | Minor refactoring sygus. |
commit | commitdiff | tree |
| 2017-03-28 |
ajreynol | More work on sygus. Add regress4 to Makefile. |
commit | commitdiff | tree |
| 2017-03-28 |
Tim King | Fixing a bug for checking whether a node was visited. |
commit | commitdiff | tree |
| 2017-03-28 |
Tim King | Minor cleanups to ExtTheory. |
commit | commitdiff | tree |
| 2017-03-28 |
Tim King | Removing the friend class modifier from ExtTheory to... |
commit | commitdiff | tree |
| 2017-03-27 |
Clark Barrett | Merge pull request #137 from 4tXJ7f/throw_quals |
commit | commitdiff | tree |
| 2017-03-27 |
Tim King | Making the ExtTheory object a private member of Theory. |
commit | commitdiff | tree |
| 2017-03-27 |
Tim King | Making ppNotifyAssertions take a const vector. |
commit | commitdiff | tree |
| 2017-03-27 |
Tim King | Moving the CareGraph into its own file. |
commit | commitdiff | tree |
| 2017-03-27 |
Tim King | Moving the theory::Assertion struct into its own file. |
commit | commitdiff | tree |
| 2017-03-27 |
Andres Notzli | Remove throw qualifiers in type enumerators |
commit | commitdiff | tree |
| 2017-03-27 |
Tim King | Alphabetizing libcvc4_la_SOURCES. |
commit | commitdiff | tree |
| 2017-03-24 |
ajreynol | Add some regressions. Minor. |
commit | commitdiff | tree |
| 2017-03-24 |
ajreynol | Refactor model building for quantifiers to be a single... |
commit | commitdiff | tree |
| 2017-03-23 |
Clark Barrett | Fixing warning message. |
commit | commitdiff | tree |
| 2017-03-23 |
guykatzz | support incremental unsat cores |
commit | commitdiff | tree |
| 2017-03-22 |
ajreynol | Fix more cases of rewritten explanations in strings... |
commit | commitdiff | tree |
| 2017-03-22 |
ajreynol | Minor fix for bounded integers. |
commit | commitdiff | tree |
| 2017-03-22 |
ajreynol | Work on new approach for sygus involving conditional... |
commit | commitdiff | tree |
| 2017-03-21 |
ajreynol | Improve computeCareGraph functions to check shared... |
commit | commitdiff | tree |
| 2017-03-20 |
Andrew Reynolds | Merge pull request #135 from PaulMeng/master |
commit | commitdiff | tree |
| 2017-03-20 |
Paul Meng | fixed cvc4 parser for set complement |
commit | commitdiff | tree |
| 2017-03-18 |
Clark Barrett | Fix for bug 707. |
commit | commitdiff | tree |
| 2017-03-18 |
Clark Barrett | Fix to help with bug 717 |
commit | commitdiff | tree |
| 2017-03-17 |
guykatzz | better support for proof production when encountering... |
commit | commitdiff | tree |
| 2017-03-16 |
Tim King | Fixes bug 781. Copy constructor for Expr needed to... |
commit | commitdiff | tree |
| 2017-03-16 |
ajreynol | More fixes, features to examples. |
commit | commitdiff | tree |
| 2017-03-16 |
ajreynol | Minor fixes, always expand applications of lambdas... |
commit | commitdiff | tree |
| 2017-03-16 |
ajreynol | Support for SMT LIB 2.6 syntax declare-datatype and... |
commit | commitdiff | tree |
| 2017-03-16 |
ajreynol | Parsing support for SMT LIB 2.6. Minor fixes for printi... |
commit | commitdiff | tree |
| 2017-03-15 |
ajreynol | Fix regress1 Makefile for rewriterules, fixes bug 783. |
commit | commitdiff | tree |
| 2017-03-15 |
Clark Barrett | Merge pull request #134 from 4tXJ7f/fix_host |
commit | commitdiff | tree |
| 2017-03-15 |
ajreynol | Allow 0 argument recursive functions. Fixes bug 782. |
commit | commitdiff | tree |
| 2017-03-15 |
Andres Notzli | Fix win-build script to use MinGW-w64 by default |
commit | commitdiff | tree |
| 2017-03-14 |
guykatzz | Merge pull request #133 from 4tXJ7f/fix_uninitialized |
commit | commitdiff | tree |
| 2017-03-14 |
Andres Notzli | fix uninitialized variable |
commit | commitdiff | tree |
| 2017-03-14 |
Clark Barrett | Merge pull request #132 from 4tXJ7f/fix_mingw64 |
commit | commitdiff | tree |
| 2017-03-10 |
ajreynol | Minor fix for cbqi-all. |
commit | commitdiff | tree |
| 2017-03-09 |
guykatzz | bug fix |
commit | commitdiff | tree |
| 2017-03-09 |
guykatzz | better proof support for bools and formulas |
commit | commitdiff | tree |
| 2017-03-08 |
Andres Notzli | Fix MinGW-w64 build |
commit | commitdiff | tree |
| 2017-03-07 |
ajreynol | More fixes for printing/parsing sets, fix kind name. |
commit | commitdiff | tree |
| 2017-03-07 |
ajreynol | Fix cvc parser for set compliment. |
commit | commitdiff | tree |
| 2017-03-06 |
ajreynol | Do not eagerly construct explanations in relation solver. |
commit | commitdiff | tree |
| 2017-03-06 |
ajreynol | Support for set compliment and universe set. Simplify... |
commit | commitdiff | tree |
| 2017-03-06 |
Clark Barrett | Adding support for bool-to-bv |
commit | commitdiff | tree |
| 2017-03-03 |
ajreynol | Fix for collectModelInfo related to finite types +... |
commit | commitdiff | tree |
| 2017-03-03 |
ajreynol | Another minor fix for sets related to sharing + finite... |
commit | commitdiff | tree |
| 2017-03-02 |
ajreynol | Fixes related to sets. |
commit | commitdiff | tree |
| 2017-03-02 |
ajreynol | Minor cleanup and reorganization related to last commit. |
commit | commitdiff | tree |
| 2017-03-02 |
ajreynol | Eliminate Boolean term conversion. Generalizes removeIT... |
commit | commitdiff | tree |
| 2017-02-16 |
ajreynol | Minor fixes for relations, quantifiers dsplit. |
commit | commitdiff | tree |
| 2017-02-16 |
ajreynol | Fixes for sets+rels check. Minor. |
commit | commitdiff | tree |
| 2017-02-15 |
ajreynol | Minimization modes for fmf bound. |
commit | commitdiff | tree |
| 2017-02-07 |
ajreynol | Generalize finite bound inference to unifiable variable... |
commit | commitdiff | tree |
| 2017-01-30 |
ajreynol | Fix regexp cache issue in strings, add regression. |
commit | commitdiff | tree |
| 2017-01-18 |
Andres Noetzli | Fix non-idempotent rewrite in Array rewriter |
commit | commitdiff | tree |
| 2017-01-18 |
Andrew Reynolds | Merge pull request #128 from 4tXJ7f/fix_lfsc_perf |
commit | commitdiff | tree |
| 2017-01-18 |
ajreynol | Minor fix in relations. |
commit | commitdiff | tree |
| 2017-01-16 |
Andres Notzli | [LFSC] Fix performance issues, more determinism |
commit | commitdiff | tree |
| 2017-01-14 |
Clark Barrett | Fix call to SExpr constructor for greater portability. |
commit | commitdiff | tree |
| 2017-01-14 |
Clark Barrett | Merge pull request #130 from chadbrewbaker/master |
commit | commitdiff | tree |
| 2017-01-13 |
ajreynol | Do not rewrite explanations in strings. |
commit | commitdiff | tree |
| 2017-01-11 |
Clark Barrett | Merge pull request #129 from timothy-king/regression... |
commit | commitdiff | tree |
| 2017-01-11 |
Clark Barrett | Merge pull request #131 from makaimann/fix_702 |
commit | commitdiff | tree |
| 2017-01-11 |
makaimann | Proposed fix for bug 702. Checks to make sure the Expr... |
commit | commitdiff | tree |
| next |
projects / cvc5.git / shortlog