| 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-03 |
Guy | Better infrastructure for proving constant disequality. |
commit | commitdiff | tree |
| 2016-06-03 |
Guy | A better mechanism for handling BV terms with aliases... |
commit | commitdiff | tree |
| 2016-06-02 |
Guy | Fixed a magical bug that only appears when compiling... |
commit | commitdiff | tree |
| 2016-06-02 |
Guy | Fix |
commit | commitdiff | tree |
| 2016-06-02 |
Guy | Merge from proof branch |
commit | commitdiff | tree |
| 2016-06-02 |
Guy | Revert "Merging proof branch" |
commit | commitdiff | tree |
| 2016-06-02 |
Guy | Merging proof branch |
commit | commitdiff | tree |
| 2016-06-01 |
ajreynol | Fix to ignore a case of triggers with no free variables. |
commit | commitdiff | tree |
| 2016-06-01 |
ajreynol | Initial infrastructure for bounded set quantification... |
commit | commitdiff | tree |
| 2016-05-31 |
Clark Barrett | Added Guy to authors list. |
commit | commitdiff | tree |
| 2016-05-28 |
Clark Barrett | Fix build |
commit | commitdiff | tree |
| 2016-05-28 |
Clark Barrett | Updated incremental run script |
commit | commitdiff | tree |
| 2016-05-28 |
Clark Barrett | Disabling failing unit test for now |
commit | commitdiff | tree |
| 2016-05-28 |
Clark Barrett | Removing check that is no longer valid. |
commit | commitdiff | tree |
| 2016-05-27 |
Clark Barrett | Merged QF_UFBV support from experimental branch |
commit | commitdiff | tree |
| 2016-05-27 |
Clark Barrett | Enabled bit-blasting option for QF_UFBV |
commit | commitdiff | tree |
| 2016-05-27 |
Clark Barrett | Updated incremental script |
commit | commitdiff | tree |
| 2016-05-27 |
Clark Barrett | Fixed bug in run script |
commit | commitdiff | tree |
| 2016-05-26 |
Kshitij Bansal | Added cryptominisat flag to QF_NIA |
commit | commitdiff | tree |
| 2016-05-26 |
Clark Barrett | Merge branch 'master' of https://github.com/CVC4/CVC4 |
commit | commitdiff | tree |
| 2016-05-26 |
Clark Barrett | Small change in run script |
commit | commitdiff | tree |
| 2016-05-26 |
lianah | Changed aig_bitblaster to work with cryptominisat |
commit | commitdiff | tree |
| 2016-05-26 |
lianah | Disabled m4ri in cryptominisat cmake command |
commit | commitdiff | tree |
| 2016-05-26 |
Kshitij Bansal | Fix for aig_bitblaster.cpp |
commit | commitdiff | tree |
| 2016-05-26 |
ajreynol | Use term indexing in TheoryUF::computeCareGraph. Do... |
commit | commitdiff | tree |
| 2016-05-26 |
Clark Barrett | Updated script, fixed bug in QF_NIA conversion. |
commit | commitdiff | tree |
| 2016-05-25 |
Liana Hadarean | Fixed unit test |
commit | commitdiff | tree |
| 2016-05-25 |
Liana Hadarean | Fixed build issue due to dummy Cryptominisat constructor. |
commit | commitdiff | tree |
| 2016-05-25 |
Liana Hadarean | Forgot to add second patch file. |
commit | commitdiff | tree |
| 2016-05-25 |
Liana Hadarean | Merged cryptominisat from experimental branch. |
commit | commitdiff | tree |
| 2016-05-24 |
ajreynol | Improvements to symmetry breaking in sygus search.... |
commit | commitdiff | tree |
| 2016-05-23 |
ajreynol | Fix related to parametric sorts whose interpretation... |
commit | commitdiff | tree |
| 2016-05-21 |
ajreynol | Minor fix for strings. |
commit | commitdiff | tree |
| 2016-05-20 |
ajreynol | Minor fix to strings, cleanup in datatypes. |
commit | commitdiff | tree |
| 2016-05-20 |
ajreynol | Improvements to theory combination + strings: do not... |
commit | commitdiff | tree |
| 2016-05-20 |
Clark Barrett | Updated AUTHORS file |
commit | commitdiff | tree |
| 2016-05-18 |
ajreynol | Refactor modes for sygus+single invocation. Add option... |
commit | commitdiff | tree |
| 2016-05-17 |
ajreynol | Minor fix cbqi for constant monomials. |
commit | commitdiff | tree |
| 2016-05-16 |
Clark Barrett | Fix memory leak in interactive_shell.cpp |
commit | commitdiff | tree |
| 2016-05-16 |
ajreynol | Enable --sygus-direct-eval by default, limit to terms... |
commit | commitdiff | tree |
| 2016-05-15 |
ajreynol | Work on --sygus-direct-eval. Minor optimizations, updat... |
commit | commitdiff | tree |
| 2016-05-12 |
ajreynol | Add casc scripts. Improvements to qcf related to nested... |
commit | commitdiff | tree |
| 2016-05-10 |
ajreynol | Fix for --inst-max-level |
commit | commitdiff | tree |
| 2016-05-10 |
ajreynol | Add smt comp 2016 scripts. Fix for --relevant-triggers... |
commit | commitdiff | tree |
| 2016-05-09 |
Clark Barrett | Re-enabling ite simplification in incremental mode... |
commit | commitdiff | tree |
| 2016-05-06 |
ajreynol | Minor clean up, fixes related to sygus. |
commit | commitdiff | tree |
| 2016-05-05 |
ajreynol | Compute term indices lazily in TermDb. Optimization... |
commit | commitdiff | tree |
| 2016-05-05 |
Tim King | Removing a null pointer reference that was found by... |
commit | commitdiff | tree |
| 2016-05-05 |
Clark Barrett | Update to COPYING |
commit | commitdiff | tree |
| 2016-05-02 |
ajreynol | Clean up issues related to compiled scc in LFSC. Refact... |
commit | commitdiff | tree |
| 2016-04-30 |
Liana Hadarean | Reviewed Tim's Asan changes and improved SatProof comments. |
commit | commitdiff | tree |
| 2016-04-28 |
Clark Barrett | Workaround for a problem in clang |
commit | commitdiff | tree |
| 2016-04-28 |
ajreynol | More work on inst propagate. Optimization for qcf... |
commit | commitdiff | tree |
| 2016-04-27 |
Tim King | Adding an example lsan supression file. |
commit | commitdiff | tree |
| 2016-04-26 |
Tim King | Fixing memory leaks for garbage collection of ResChains... |
commit | commitdiff | tree |
| 2016-04-26 |
Tim King | Fixing a memory leak of the ProofManager. |
commit | commitdiff | tree |
| 2016-04-19 |
Clark Barrett | Fixed typo |
commit | commitdiff | tree |
| 2016-04-18 |
Clark Barrett | More fixes for python interface |
commit | commitdiff | tree |
| 2016-04-15 |
Guy | Rolling back the rewrite code |
commit | commitdiff | tree |
| 2016-04-15 |
Clark Barrett | Fix for bug 717 |
commit | commitdiff | tree |
| 2016-04-15 |
Clark Barrett | Fixes for python bindings |
commit | commitdiff | tree |
| 2016-04-14 |
Guy | Merge branch 'master' of https://github.com/CVC4/CVC4 |
commit | commitdiff | tree |
| 2016-04-14 |
Guy | Remove some no-longer-required rewrites of array lemmas |
commit | commitdiff | tree |
| 2016-04-14 |
ajreynol | Add option --snorm-infer-eq to infer equalities based... |
commit | commitdiff | tree |
| 2016-04-14 |
ajreynol | Add missing function for regexp to expr manager. |
commit | commitdiff | tree |
| 2016-04-13 |
ajreynol | Update native language support for strings. |
commit | commitdiff | tree |
| 2016-04-13 |
ajreynol | Minor improvements for alpha equivalence and partial... |
commit | commitdiff | tree |
| 2016-04-13 |
ajreynol | Handle parametric datatypes with --quant-ind. Minor... |
commit | commitdiff | tree |
| 2016-04-12 |
ajreynol | Bug fixes related to parametric datatypes + theory... |
commit | commitdiff | tree |
| 2016-04-12 |
ajreynol | Optimizations for QCF to check relevant domain of varia... |
commit | commitdiff | tree |
| 2016-04-11 |
ajreynol | Minor fixes for inst match generators. Updates to qip. |
commit | commitdiff | tree |
| 2016-04-10 |
ajreynol | More work on instantiation propagation. Enable external... |
commit | commitdiff | tree |
| 2016-04-09 |
Guy | Merge branch 'master' of https://github.com/CVC4/CVC4 |
commit | commitdiff | tree |
| 2016-04-09 |
Guy | Made ProofArray's printing functions non-static, and... |
commit | commitdiff | tree |
| 2016-04-09 |
Kshitij Bansal | cardinality operation for finite sets (based on my... |
commit | commitdiff | tree |
| 2016-04-09 |
ajreynol | Minor refactoring of entailment tests and quantifiers... |
commit | commitdiff | tree |
| 2016-04-07 |
ajreynol | Refactor trigger selection, revisions to --relational... |
commit | commitdiff | tree |
| 2016-04-04 |
ajreynol | New options for trigger selection, add option --strict... |
commit | commitdiff | tree |
| 2016-04-04 |
Tim King | Updating the copyright headers and scripts. |
commit | commitdiff | tree |
| 2016-04-04 |
Guy | s_ prefix for static members |
commit | commitdiff | tree |
| 2016-04-03 |
Guy | Removed the theory-specific merge reason types. Instead... |
commit | commitdiff | tree |
| 2016-04-01 |
ajreynol | Improvements to equality inference module: add missing... |
commit | commitdiff | tree |
| 2016-03-31 |
ajreynol | Improvements to trigger selection, min triggers by... |
commit | commitdiff | tree |
| 2016-03-30 |
ajreynol | Updates to E-matching to avoid entailed instantiations... |
commit | commitdiff | tree |
| 2016-03-30 |
Tim King | Updating the mailmap for git. |
commit | commitdiff | tree |
| 2016-03-28 |
ajreynol | Minor cleanup from last commit (quant util, equality... |
commit | commitdiff | tree |
| 2016-03-28 |
ajreynol | Implement equality inference module for arithmetic... |
commit | commitdiff | tree |
| 2016-03-24 |
Guy | Merge branch 'master' of https://github.com/CVC4/CVC4 |
commit | commitdiff | tree |
| 2016-03-24 |
Guy | Refactored the equality engine in order to remove theor... |
commit | commitdiff | tree |
| 2016-03-24 |
Tim King | Fixing a garbage collection issue in simplifyWithCare... |
commit | commitdiff | tree |
| 2016-03-24 |
Tim King | Deleting allocated NodeVecs in ITESimplifier. |
commit | commitdiff | tree |
| 2016-03-24 |
Tim King | Freeing CegConjecture::d_ceg_si. Also making d_ceg_si... |
commit | commitdiff | tree |
| 2016-03-24 |
Tim King | Fixing a memory leak in CDInstMatchTrie::d_data. |
commit | commitdiff | tree |
| 2016-03-24 |
Tim King | Fix for a memory leak in InstStrategyCegqi. |
commit | commitdiff | tree |
| 2016-03-24 |
Tim King | Fixing a memory leak in QuantInfo::d_var_mg. |
commit | commitdiff | tree |
| 2016-03-23 |
guykatzz | Merge pull request #82 from CVC4/master_for_merge |
commit | commitdiff | tree |
| 2016-03-23 |
Guy | squash-merge from proof branch |
commit | commitdiff | tree |
| 2016-03-23 |
Tim King | Fixing memory leaks in Trigger and TriggerTrie. |
commit | commitdiff | tree |
| next |
projects / cvc5.git / shortlog