| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2017-04-14 | Fix bug related to portfolio with nullary operators. | ajreynol | |
| 2017-04-14 | Fix nullary operator printers, minor. | ajreynol | |
| 2017-04-14 | Fix for fmf-fun when the option is set by user command. | ajreynol | |
| 2017-04-13 | Fix for some compilers | Clark Barrett | |
| 2017-04-12 | Add nullary operator metakind. | ajreynol | |
| 2017-04-11 | Bug fix in conjecture generation for --quant-ind. | ajreynol | |
| 2017-04-07 | Change option names for nl. | ajreynol | |
| 2017-04-05 | Merge pull request #143 from FabianWolff/master | Clark Barrett | |
| Fix several spelling errors | |||
| 2017-04-05 | Fix bug 698. | ajreynol | |
| 2017-04-05 | Fixes for nlAlgSolveSubs. | ajreynol | |
| 2017-04-05 | Merge pull request #145 from 4tXJ7f/fix_lfsc_args | Andrew Reynolds | |
| [LFSC] Fix segfault | |||
| 2017-04-05 | Caching for fun def process, add regression. | ajreynol | |
| 2017-04-05 | [LFSC] Fix segfault | Andres Notzli | |
| LFSC did not detect when the number of arguments provided to a side condition did not match the expected number of arguments, which could lead to out-of-bounds reads and writes. This commit adds a check and fixes one of the proof rules that provided the wrong number of arguments. | |||
| 2017-04-05 | Remove extraneous portion of an nl regression. | ajreynol | |
| 2017-04-05 | Add non-linear regressions, disable nlAlgSubs, do not do rep checking for ↵ | ajreynol | |
| NONLINEAR_MULT terms. Ensure shared terms have correct model values in non-linear solver. | |||
| 2017-04-05 | Fix several spelling errors | Fabian Wolff | |
| 2017-04-04 | Enable multi-trigger-linear by default, add option. | ajreynol | |
| 2017-04-04 | Simplify Theory::collectModelInfo interface to not take deprecated fullModel ↵ | ajreynol | |
| argument. | |||
| 2017-04-04 | Do not solve for 0-ary non-constant symbols (for which isVar returns true), ↵ | ajreynol | |
| add regressions. | |||
| 2017-04-03 | Merge pull request #141 from 4tXJ7f/remove_def | Clark Barrett | |
| Remove decl. of getStatisticsRegistry(SmtEngine*) | |||
| 2017-04-03 | Merge pull request #142 from timothy-king/nlAlgMerge | Andrew Reynolds | |
| Adding a model based axiom instantiation scheme for multiplication. M… | |||
| 2017-04-02 | Adding a model based axiom instantiation scheme for multiplication. Merge ↵ | Tim King | |
| commit for nlAlgMaster. | |||
| 2017-03-31 | Remove decl. of getStatisticsRegistry(SmtEngine*) | Andres Notzli | |
| Commit f4ef7af0a2295691f281ee1604dfeb4082fe229c removed the definition of getStatisticsRegistry(SmtEngine*) but not the declaration. | |||
| 2017-03-31 | Add option multi-trigger-linear, minor optimization to E-matching. | ajreynol | |
| 2017-03-30 | Merge pull request #139 from 4tXJ7f/remove_throw | Clark Barrett | |
| [Coverity] Remove throw qualifiers in src/smt | |||
| 2017-03-30 | [Coverity] Remove throw qualifiers in src/smtremove_throw | Andres Notzli | |
| Addresses coverity issues: 1172167 1172174 1172176 1172183 1172185 1172186 1172188 1172189 1172191 1172192 1172193 1172194 1172197 1172197 1172198 1172434 1172437 1172438 1172443 1172445 1172446 1172447 1172448 1362695 1362700 1362717 1362736 1362768 1362786 1362811 1379599 1421404 1421405 1421406 1421407 1421408 1421409 1421410 1421411 1421412 1421413 | |||
| 2017-03-30 | Minor fixes for trigger selection max. | ajreynol | |
| 2017-03-29 | Add quantifiers options related to model and master equality engine. | ajreynol | |
| 2017-03-29 | Merge pull request #138 from PaulMeng/master | PaulMeng | |
| Refactor the standard effort of relational solver | |||
| 2017-03-28 | Refactor the standard effort of relational solver | Paul Meng | |
| 2017-03-28 | Fix bug 787. | ajreynol | |
| 2017-03-28 | Fix for bug 733 | Clark Barrett | |
| 2017-03-28 | Minor refactoring sygus. | ajreynol | |
| 2017-03-28 | More work on sygus. Add regress4 to Makefile. | ajreynol | |
| 2017-03-27 | Fixing a bug for checking whether a node was visited. | Tim King | |
| 2017-03-27 | Minor cleanups to ExtTheory. | Tim King | |
| 2017-03-27 | Removing the friend class modifier from ExtTheory to Theory. | Tim King | |
| 2017-03-27 | Merge pull request #137 from 4tXJ7f/throw_quals | Clark Barrett | |
| Remove throw qualifiers in type enumerators | |||
| 2017-03-27 | Making the ExtTheory object a private member of Theory. | Tim King | |
| 2017-03-27 | Making ppNotifyAssertions take a const vector. | Tim King | |
| 2017-03-27 | Moving the CareGraph into its own file. | Tim King | |
| 2017-03-27 | Moving the theory::Assertion struct into its own file. | Tim King | |
| 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-26 | Alphabetizing libcvc4_la_SOURCES. | Tim King | |
| 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-23 | Fixing warning message. | Clark Barrett | |
| 2017-03-23 | support incremental unsat cores | guykatzz | |
| 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 | |
 |
index : cvc5.git | |
| CVC4 is an efficient open-source automatic theorem prover for satisfiability modulo theories (SMT) problems. | git repository hosting |
| summaryrefslogtreecommitdiff |
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback