| 2017-11-25 |
Andrew Reynolds | (Refactor) Instantiate utility (#1387) |
blob | commitdiff | raw |
| 2017-11-15 |
Andrew Reynolds | Make QEffort an enum (#1366) |
blob | commitdiff | raw | diff to current |
| 2017-11-02 |
Andrew Reynolds | (Move-only) Split quant util (#1306) |
blob | commitdiff | raw | diff to current |
| 2017-11-01 |
Andrew Reynolds | (Refactor) Split term util (#1303) |
blob | commitdiff | raw | diff to current |
| 2017-10-28 |
Andrew Reynolds | (Move only) Move enumerative instantiation strategy... |
blob | commitdiff | raw | diff to current |
| 2017-10-28 |
Andrew Reynolds | Document term db (#1220) |
blob | commitdiff | raw | diff to current |
| 2017-10-10 |
Andres Noetzli | Fix memory leak in quantifiers engine (#1219) |
blob | commitdiff | raw | diff to current |
| 2017-10-10 |
Andrew Reynolds | Split term database (#1206) |
blob | commitdiff | raw | diff to current |
| 2017-09-29 |
Andrew Reynolds | Simplify representation of inversion Skolems for bv... |
blob | commitdiff | raw | diff to current |
| 2017-07-21 |
Tim King | Merge branch 'master' into cleanup-regexp |
blob | commitdiff | raw | diff to current |
| 2017-07-21 |
Tim King | Moving from the gnu extensions for hash maps to the... |
blob | commitdiff | raw | diff to current |
| 2017-07-07 |
Mathias Preiner | Update copyright headers. |
blob | commitdiff | raw | diff to current |
| 2017-06-01 |
ajreynol | Minor optimizations related to cbqi. |
blob | commitdiff | raw | diff to current |
| 2017-05-17 |
Clark Barrett | Merge pull request #155 from makaimann/conditional_coverage |
blob | commitdiff | raw | diff to current |
| 2017-05-16 |
Andrew Reynolds | Merge pull request #156 from 4tXJ7f/fix_safe_print |
blob | commitdiff | raw | diff to current |
| 2017-05-15 |
Andrew Reynolds | Merge pull request #159 from 4tXJ7f/fix_set_types |
blob | commitdiff | raw | diff to current |
| 2017-05-15 |
Andrew Reynolds | Merge pull request #158 from 4tXJ7f/fix_sets_rewriter |
blob | commitdiff | raw | diff to current |
| 2017-05-15 |
Andrew Reynolds | Merge pull request #157 from 4tXJ7f/fix_iterator |
blob | commitdiff | raw | diff to current |
| 2017-05-15 |
ajreynol | Make conflict-based instantiation abort if a ground... |
blob | commitdiff | raw | diff to current |
| 2017-03-29 |
ajreynol | Add quantifiers options related to model and master... |
blob | commitdiff | raw | diff to current |
| 2017-03-27 |
Clark Barrett | Merge pull request #137 from 4tXJ7f/throw_quals |
blob | commitdiff | raw | diff to current |
| 2017-03-27 |
Tim King | Making ppNotifyAssertions take a const vector. |
blob | commitdiff | raw | diff to current |
| 2017-01-04 |
Andrew Reynolds | Merge pull request #122 from 4tXJ7f/fix_lfsc_str |
blob | commitdiff | raw | diff to current |
| 2017-01-04 |
guykatzz | Merge pull request #120 from 4tXJ7f/fix_f_pp_holes |
blob | commitdiff | raw | diff to current |
| 2017-01-04 |
Andrew Reynolds | Merge pull request #121 from 4tXJ7f/fix_lfsc_mem_leaks |
blob | commitdiff | raw | diff to current |
| 2016-12-29 |
Tim King | Adding a destructor to InstantiationNotify. |
blob | commitdiff | raw | diff to current |
| 2016-12-07 |
guykatzz | Merge branch 'master' of https://github.com/CVC4/CVC4 |
blob | commitdiff | raw | diff to current |
| 2016-12-07 |
ajreynol | Refactoring, generalization of bounded inference module... |
blob | commitdiff | raw | diff to current |
| 2016-11-21 |
ajreynol | Refactoring related to track instantiation option. |
blob | commitdiff | raw | diff to current |
| 2016-11-03 |
ajreynol | Add priorities to getNextDecision. Properly handle... |
blob | commitdiff | raw | diff to current |
| 2016-10-28 |
ajreynol | Add get instantiations utilities to API. |
blob | commitdiff | raw | diff to current |
| 2016-10-11 |
Paul Meng | Merge branch 'origin' of https://github.com/CVC4/CVC4.git |
blob | commitdiff | raw | diff to current |
| 2016-10-01 |
Tim King | Merge pull request #93 from timothy-king/clang-format |
blob | commitdiff | raw | diff to current |
| 2016-09-29 |
ajreynol | Address some coverity warnings, add another stat. |
blob | commitdiff | raw | diff to current |
| 2016-09-29 |
ajreynol | Minor cleanup and additions to quantifiers statistics. |
blob | commitdiff | raw | diff to current |
| 2016-09-14 |
ajreynol | Lemma cache in theory sep. Minor optimization for sets... |
blob | commitdiff | raw | diff to current |
| 2016-09-02 |
Tim King | Merge pull request #91 from timothy-king/no-throw |
blob | commitdiff | raw | diff to current |
| 2016-09-01 |
ajreynol | Updates to cbqi. New strategy --cbqi-nested-qe to... |
blob | commitdiff | raw | diff to current |
| 2016-08-26 |
ajreynol | Basic support for EPR+CBQI. Minor cleanup. |
blob | commitdiff | raw | diff to current |
| 2016-08-25 |
ajreynol | Minor cleanup preprocessing, add ppNotifyAssertions. |
blob | commitdiff | raw | diff to current |
| 2016-08-24 |
PaulMeng | Merge remote-tracking branch 'origin/master' |
blob | commitdiff | raw | diff to current |
| 2016-07-26 |
Guy | Merge branch 'master' of https://github.com/CVC4/CVC4 |
blob | commitdiff | raw | diff to current |
| 2016-07-26 |
ajreynol | Add option to minimize sygus solutions based on using... |
blob | commitdiff | raw | diff to current |
| 2016-07-19 |
ajreynol | Add infrastructure for tracking instantiation lemmas... |
blob | commitdiff | raw | diff to current |
| 2016-07-05 |
PaulMeng | Merge branch 'master' of https://github.com/CVC4/CVC4.git |
blob | commitdiff | raw | diff to current |
| 2016-05-15 |
ajreynol | Work on --sygus-direct-eval. Minor optimizations, updat... |
blob | commitdiff | raw | diff to current |
| 2016-05-06 |
ajreynol | Minor clean up, fixes related to sygus. |
blob | commitdiff | raw | diff to current |
| 2016-05-05 |
ajreynol | Compute term indices lazily in TermDb. Optimization... |
blob | commitdiff | raw | diff to current |
| 2016-04-28 |
ajreynol | More work on inst propagate. Optimization for qcf... |
blob | commitdiff | raw | diff to current |
| 2016-04-20 |
PaulMeng | update from the master |
blob | commitdiff | raw | diff to current |
| 2016-04-13 |
ajreynol | Minor improvements for alpha equivalence and partial... |
blob | commitdiff | raw | diff to current |
| 2016-04-12 |
ajreynol | Optimizations for QCF to check relevant domain of varia... |
blob | commitdiff | raw | diff to current |
| 2016-04-10 |
ajreynol | More work on instantiation propagation. Enable external... |
blob | commitdiff | raw | diff to current |
| 2016-04-09 |
Guy | Merge branch 'master' of https://github.com/CVC4/CVC4 |
blob | commitdiff | raw | diff to current |
| 2016-04-09 |
ajreynol | Minor refactoring of entailment tests and quantifiers... |
blob | commitdiff | raw | diff to current |
| 2016-04-07 |
ajreynol | Refactor trigger selection, revisions to --relational... |
blob | commitdiff | raw | diff to current |
| 2016-04-04 |
ajreynol | New options for trigger selection, add option --strict... |
blob | commitdiff | raw | diff to current |
| 2016-04-04 |
Tim King | Updating the copyright headers and scripts. |
blob | commitdiff | raw | diff to current |
| 2016-04-01 |
ajreynol | Improvements to equality inference module: add missing... |
blob | commitdiff | raw | diff to current |
| 2016-03-28 |
ajreynol | Implement equality inference module for arithmetic... |
blob | commitdiff | raw | diff to current |
| 2016-03-22 |
ajreynol | Bug fix for define functions + incremental. Minor work... |
blob | commitdiff | raw | diff to current |
| 2016-03-16 |
ajreynol | Change internal representative selection for finite... |
blob | commitdiff | raw | diff to current |
| 2016-03-10 |
ajreynol | Faster conditional rewriting for and/or beneath quantif... |
blob | commitdiff | raw | diff to current |
| 2016-03-01 |
ajreynol | Shorter explanations for strings based on tracking... |
blob | commitdiff | raw | diff to current |
| 2016-02-25 |
ajreynol | Minor improvement to partial qe. Add options for repres... |
blob | commitdiff | raw | diff to current |
| 2016-02-19 |
ajreynol | Implement dynamic splitting for quantified formulas... |
blob | commitdiff | raw | diff to current |
| 2016-02-17 |
ajreynol | Refactor quantifiers attributes. Make quantifier elimin... |
blob | commitdiff | raw | diff to current |
| 2016-02-16 |
ajreynol | Public interface for quantifier elimination. Minor... |
blob | commitdiff | raw | diff to current |
| 2016-01-09 |
Tim King | Removing StatisticsRegistry's static functions current... |
blob | commitdiff | raw | diff to current |
| 2015-12-15 |
Tim King | Refactoring Options Handler & Library Cycle Breaking |
blob | commitdiff | raw | diff to current |
| 2015-11-05 |
Tim King | Merging the google branch back into master. |
blob | commitdiff | raw | diff to current |
| 2015-11-04 |
ajreynol | Better combination of UF with cbqi, refactor quantifier... |
blob | commitdiff | raw | diff to current |
| 2015-10-31 |
ajreynol | Improvements to handling of mixed Int/Real quantifiers. |
blob | commitdiff | raw | diff to current |
| 2015-10-26 |
ajreynol | Promote InstStrategyCbqi to quantifier module. Cleanup... |
blob | commitdiff | raw | diff to current |
| 2015-10-26 |
ajreynol | Extend counterexample-guided instantiation to extended... |
blob | commitdiff | raw | diff to current |
| 2015-09-28 |
ajreynol | Improve quantifiers engine wrt incremental presolve... |
blob | commitdiff | raw | diff to current |
| 2015-09-26 |
ajreynol | Better organization of quantifiers modules, promote... |
blob | commitdiff | raw | diff to current |
| 2015-09-25 |
ajreynol | Clear term caches for quantifiers + incremental, fixes... |
blob | commitdiff | raw | diff to current |
| 2015-09-18 |
ajreynol | Fix bug in quantifiers engine where model construction... |
blob | commitdiff | raw | diff to current |
| 2015-09-15 |
ajreynol | Fix bug related to quantifiers + incremental, thanks... |
blob | commitdiff | raw | diff to current |
| 2015-09-02 |
Kshitij Bansal | Merge remote-tracking branch 'origin/master' |
blob | commitdiff | raw | diff to current |
| 2015-08-26 |
ajreynol | Minor improvements to cbqi, fix bug in solving with... |
blob | commitdiff | raw | diff to current |
| 2015-08-12 |
ajreynol | Improvements to --macros-quant. Enable --clause-split... |
blob | commitdiff | raw | diff to current |
| 2015-07-30 |
ajreynol | Implement virtual term substitution for non-nested... |
blob | commitdiff | raw | diff to current |
| 2015-07-28 |
Tianyi Liang | Merge branch 'master' of https://github.com/CVC4/CVC4 |
blob | commitdiff | raw | diff to current |
| 2015-07-20 |
ajreynol | Squashed merge of SygusComp 2015 branch. |
blob | commitdiff | raw | diff to current |
| 2015-06-29 |
ajreynol | Module to infer alpha equivalence of quantified formula... |
blob | commitdiff | raw | diff to current |
| 2015-06-27 |
ajreynol | Refactor various corner cases of fmf, quantifiers modul... |
blob | commitdiff | raw | diff to current |
| 2015-06-22 |
ajreynol | Add --user-pat=interleave. Remove unused lte inst strategy. |
blob | commitdiff | raw | diff to current |
| 2015-05-15 |
ajreynol | Avoid ensureLiteral on unpreprocessed formulas in cbqi. |
blob | commitdiff | raw | diff to current |
| 2015-05-13 |
ajreynol | Refactor interface for incompleteness in quantifiers... |
blob | commitdiff | raw | diff to current |
| 2015-05-12 |
barrettcw | Merge pull request #74 from finnhaedicke/namespace_minisat |
blob | commitdiff | raw | diff to current |
| 2015-05-10 |
ajreynol | Minor improvements to infrastructure. Minor changes... |
blob | commitdiff | raw | diff to current |
| 2015-03-11 |
ajreynol | Minor fixes and improvements to cegqi-si for linear... |
blob | commitdiff | raw | diff to current |
| 2015-02-06 |
Tianyi Liang | Merge branch 'master' of github.com:tiliang/CVC4 |
blob | commitdiff | raw | diff to current |
| 2015-02-04 |
ajreynol | Refactor sygus_util to TermDb. Initial work on solutio... |
blob | commitdiff | raw | diff to current |
| 2015-01-29 |
ajreynol | Restrict LtePartialInst instantiations based on E-match... |
blob | commitdiff | raw | diff to current |
| 2015-01-26 |
ajreynol | Output solutions for synthesis conjectures with --dump... |
blob | commitdiff | raw | diff to current |
| 2015-01-24 |
ajreynol | Variable patterns only look at eligible terms. Minor... |
blob | commitdiff | raw | diff to current |
| 2015-01-23 |
ajreynol | Rework inst-closure. |
blob | commitdiff | raw | diff to current |
| next |
projects / cvc5.git / history