| 2016-09-01 |
Tim King | Removing the forward declaration of QuantInfo from... |
commit | commitdiff | tree |
| 2016-08-31 |
Tim King | Cleaning up the dead FORIT macros. |
commit | commitdiff | tree |
| 2016-08-31 |
Tim King | Removing the usage of typeof from theory_sets_private. |
commit | commitdiff | tree |
| 2016-08-31 |
Tim King | Beautifying theory_model.h. |
commit | commitdiff | tree |
| 2016-08-31 |
Tim King | Removing BOOST_FOREACH from theory/sets/scrutinize.h. |
commit | commitdiff | tree |
| 2016-08-31 |
Tim King | Removing typeof from sets normal form and beautifying... |
commit | commitdiff | tree |
| 2016-08-31 |
Tim King | Removing typeof from command_executor_portfolio.cpp. |
commit | commitdiff | tree |
| 2016-08-31 |
Tim King | Removing typeof from didyoumean.cpp. |
commit | commitdiff | tree |
| 2016-08-26 |
ajreynol | Basic support for EPR+CBQI. Minor cleanup. |
commit | commitdiff | tree |
| 2016-08-25 |
ajreynol | Minor cleanup preprocessing, add ppNotifyAssertions. |
commit | commitdiff | tree |
| 2016-08-25 |
ajreynol | Options for counterexample guided instantiation. |
commit | commitdiff | tree |
| 2016-08-20 |
Clark Barrett | Fixed two bugs |
commit | commitdiff | tree |
| 2016-08-19 |
Clark Barrett | Added fitsSignedLong and fitsUnsignedLong |
commit | commitdiff | tree |
| 2016-08-16 |
ajreynol | Initial infrastructure for ExtTheory, generalize extend... |
commit | commitdiff | tree |
| 2016-08-15 |
ajreynol | Expression sharing on demand in LFSC (replace definitio... |
commit | commitdiff | tree |
| 2016-08-15 |
ajreynol | Enable bounded set membership with --fmf-bound. Map... |
commit | commitdiff | tree |
| 2016-08-12 |
ajreynol | Add a few more regressions. |
commit | commitdiff | tree |
| 2016-08-12 |
ajreynol | Minor fixes to model construction to take singleton... |
commit | commitdiff | tree |
| 2016-08-12 |
guykatzz | Merge pull request #90 from 4tXJ7f/fewer_preproc_holes |
commit | commitdiff | tree |
| 2016-08-12 |
Andres Notzli | Add support for fewer preprocessing holes |
commit | commitdiff | tree |
| 2016-08-11 |
ajreynol | Minor change to strings, introduce proxy vars only... |
commit | commitdiff | tree |
| 2016-08-10 |
ajreynol | Improvements to strings: work on propagations for rever... |
commit | commitdiff | tree |
| 2016-08-09 |
guykatzz | Merge pull request #89 from 4tXJ7f/fix_proof_spaces |
commit | commitdiff | tree |
| 2016-08-09 |
ajreynol | Fixes for sep star rewrite. |
commit | commitdiff | tree |
| 2016-08-09 |
Andres Notzli | Fix missing/redundant spaces in proofs |
commit | commitdiff | tree |
| 2016-08-06 |
guykatzz | Merge pull request #88 from 4tXJ7f/fix_comments |
commit | commitdiff | tree |
| 2016-08-05 |
Andres Notzli | Minor: add/fix comments, remove redundant includes |
commit | commitdiff | tree |
| 2016-08-03 |
Guy | Fixed an issue where arrays proofs would sometimes... |
commit | commitdiff | tree |
| 2016-08-03 |
barrettcw | Merge pull request #87 from 4tXJ7f/fix_oob_access |
commit | commitdiff | tree |
| 2016-07-30 |
ajreynol | Prioritize inferences when processing normal forms... |
commit | commitdiff | tree |
| 2016-07-28 |
Guy | The "aggressive" optimizer for lemma L now returns... |
commit | commitdiff | tree |
| 2016-07-28 |
Guy | Merge branch 'master' of https://github.com/CVC4/CVC4 |
commit | commitdiff | tree |
| 2016-07-28 |
Guy | Bug fix involving negated lemmas |
commit | commitdiff | tree |
| 2016-07-28 |
ajreynol | Fix bug 749. |
commit | commitdiff | tree |
| 2016-07-28 |
Guy | Add the negative conjunction case |
commit | commitdiff | tree |
| 2016-07-28 |
Andres Notzli | Fix out-of-bounds access in ExprManager |
commit | commitdiff | tree |
| 2016-07-28 |
Guy | Proper instrumentation of the preprocessing phase |
commit | commitdiff | tree |
| 2016-07-28 |
Guy | proper handling of ITEs |
commit | commitdiff | tree |
| 2016-07-27 |
Guy | Proper handling of IFF lemmas in the unsat core. |
commit | commitdiff | tree |
| 2016-07-27 |
Guy | Added an option for a more aggressive weakest implicant... |
commit | commitdiff | tree |
| 2016-07-27 |
Guy | If we can't find a weaker implicant, fail gracefully... |
commit | commitdiff | tree |
| 2016-07-27 |
guykatzz | Merge pull request #86 from 4tXJ7f/fix_warnings |
commit | commitdiff | tree |
| 2016-07-27 |
Andres Notzli | Fix warnings in src/proof |
commit | commitdiff | tree |
| 2016-07-26 |
Guy | Merge branch 'master' of https://github.com/CVC4/CVC4 |
commit | commitdiff | tree |
| 2016-07-26 |
Guy | Bug fix: |
commit | commitdiff | tree |
| 2016-07-26 |
ajreynol | Add option to minimize sygus solutions based on using... |
commit | commitdiff | tree |
| 2016-07-26 |
Guy | Merge branch 'master' of https://github.com/CVC4/CVC4 |
commit | commitdiff | tree |
| 2016-07-26 |
Guy | Letification of BV constants |
commit | commitdiff | tree |
| 2016-07-26 |
ajreynol | Minor improvements to strings related to constant split... |
commit | commitdiff | tree |
| 2016-07-26 |
Guy | Added functionality to retrieve a lemma's "weakest... |
commit | commitdiff | tree |
| 2016-07-26 |
Guy | Bug fix |
commit | commitdiff | tree |
| 2016-07-26 |
Guy | Propagate the usage of proof let maps into constant... |
commit | commitdiff | tree |
| 2016-07-25 |
Guy | Bug fix |
commit | commitdiff | tree |
| 2016-07-25 |
Guy | Merge branch 'master' of https://github.com/CVC4/CVC4 |
commit | commitdiff | tree |
| 2016-07-25 |
Guy | cleanup |
commit | commitdiff | tree |
| 2016-07-25 |
Guy | Use letification for the aliasing declarations as well... |
commit | commitdiff | tree |
| 2016-07-25 |
Guy | Proper handling for lemmas that are conjuncts: |
commit | commitdiff | tree |
| 2016-07-22 |
ajreynol | Minor, error handling for polymorphism + sep logic. |
commit | commitdiff | tree |
| 2016-07-21 |
ajreynol | Fixes for strings, explanations for constant split... |
commit | commitdiff | tree |
| 2016-07-20 |
ajreynol | Infrastructure for storing and printing heap models... |
commit | commitdiff | tree |
| 2016-07-20 |
ajreynol | Print only instantiations that are in the unsat core... |
commit | commitdiff | tree |
| 2016-07-20 |
ajreynol | Infer conflicts in strings based on abstracting equalit... |
commit | commitdiff | tree |
| 2016-07-20 |
Guy | Bug fix |
commit | commitdiff | tree |
| 2016-07-20 |
Guy | Allow a caller to query whether an unsat core is availa... |
commit | commitdiff | tree |
| 2016-07-19 |
ajreynol | Add infrastructure for tracking instantiation lemmas... |
commit | commitdiff | tree |
| 2016-07-16 |
ajreynol | Refactor strings extf evaluation info. Ensure strings... |
commit | commitdiff | tree |
| 2016-07-15 |
Guy | Moved the assertion to a better spot |
commit | commitdiff | tree |
| 2016-07-15 |
Guy | The ProofManager now allows theory solvers to get their... |
commit | commitdiff | tree |
| 2016-07-15 |
ajreynol | Minor simplification to normal form explanations. |
commit | commitdiff | tree |
| 2016-07-08 |
ajreynol | Minor fix to last commit. |
commit | commitdiff | tree |
| 2016-07-08 |
ajreynol | Simplifications for strings normal forms, fix case... |
commit | commitdiff | tree |
| 2016-07-07 |
ajreynol | Ensure heap disjointness in sep refinements. |
commit | commitdiff | tree |
| 2016-07-07 |
ajreynol | Refactoring of strings preprocess module. When enabled... |
commit | commitdiff | tree |
| 2016-07-06 |
Guy | A few proof bugs fixed |
commit | commitdiff | tree |
| 2016-07-06 |
ajreynol | Minor cleanup in strings, mostly related to negated... |
commit | commitdiff | tree |
| 2016-07-06 |
ajreynol | Add comment field for model, resolves hack for printing... |
commit | commitdiff | tree |
| 2016-07-05 |
ajreynol | Refactor last call for theories, only create one model... |
commit | commitdiff | tree |
| 2016-07-05 |
ajreynol | Add option --trigger-active-sel. Recognize simple trigg... |
commit | commitdiff | tree |
| 2016-07-01 |
Guy | When proving a lemma, ignore literals that don't belong... |
commit | commitdiff | tree |
| 2016-07-01 |
Guy | Handle bitvector lemmas where a literal gets rewritten... |
commit | commitdiff | tree |
| 2016-06-30 |
Guy | Merge branch 'master' of https://github.com/CVC4/CVC4 |
commit | commitdiff | tree |
| 2016-06-30 |
Guy | Support for the letification of chained AND and OR... |
commit | commitdiff | tree |
| 2016-06-23 |
Clark Barrett | Add theory/sep/kinds to EXTRA_DIST to fix distcheck... |
commit | commitdiff | tree |
| 2016-06-23 |
Clark Barrett | Fixed some warnings, fixed bug in cdhashmap that was... |
commit | commitdiff | tree |
| 2016-06-20 |
Guy | Merge branch 'master' of https://github.com/CVC4/CVC4 |
commit | commitdiff | tree |
| 2016-06-20 |
Guy | Addressed a bug that occurs when proof production is... |
commit | commitdiff | tree |
| 2016-06-20 |
ajreynol | Minor change to sep/kinds |
commit | commitdiff | tree |
| 2016-06-20 |
Guy | Merge branch 'master' of https://github.com/CVC4/CVC4 |
commit | commitdiff | tree |
| 2016-06-20 |
Guy | Fixed a bug where the proofManager's init() call was... |
commit | commitdiff | tree |
| 2016-06-18 |
ajreynol | Fix unit test. |
commit | commitdiff | tree |
| 2016-06-17 |
ajreynol | Cleanup from last commit, treat sep.nil as variable... |
commit | commitdiff | tree |
| 2016-06-17 |
ajreynol | Support for separation logic. Enable cbqi by default... |
commit | commitdiff | tree |
| 2016-06-17 |
ajreynol | Add syguscomp2016 scripts. |
commit | commitdiff | tree |
| 2016-06-09 |
Clark Barrett | Dummy commit. |
commit | commitdiff | tree |
| 2016-06-08 |
Guy | Merge branch 'master' of https://github.com/CVC4/CVC4 |
commit | commitdiff | tree |
| 2016-06-08 |
Guy | LFSC letification is true by default |
commit | commitdiff | tree |
| 2016-06-08 |
Guy | Support for printing a global let map in LFSC proofs. |
commit | commitdiff | tree |
| 2016-06-06 |
guykatzz | Merge pull request #85 from CVC4/master_for_proof_merge |
commit | commitdiff | tree |
| 2016-06-04 |
ajreynol | Remove NodeListMap from datatypes and equality inferenc... |
commit | commitdiff | tree |
| 2016-06-03 |
Guy | Better infrastructure for proving constant disequality. |
commit | commitdiff | tree |
| next |
projects / cvc5.git / shortlog