Age | Commit message (Expand) | Author |
2017-03-02 | Eliminate Boolean term conversion. Generalizes removeITE pass to remove Boole... | ajreynol |
2016-12-06 | Improve bounds for global heap in sep, refactor preprocessing. Minor improvem... | ajreynol |
2016-10-13 | Revert "Merge branch 'origin' of https://github.com/CVC4/CVC4.git" | Tim King |
2016-10-11 | Merge branch 'origin' of https://github.com/CVC4/CVC4.git | Paul Meng |
2016-09-15 | Refactor setIncomplete in quantifiers. | ajreynol |
2016-09-14 | Lemma cache in theory sep. Minor optimization for sets. Minor improvements to... | ajreynol |
2016-09-13 | Minor changes to sep logic, epr, quantifier splitting. | ajreynol |
2016-08-26 | Basic support for EPR+CBQI. Minor cleanup. | ajreynol |
2016-07-05 | Merge branch 'master' of https://github.com/CVC4/CVC4.git | PaulMeng |
2016-06-17 | Support for separation logic. Enable cbqi by default for pure BV. | ajreynol |
2016-04-28 | More work on inst propagate. Optimization for qcf to check instances eagerly... | ajreynol |
2016-04-20 | update from the master | PaulMeng |
2016-04-09 | Minor refactoring of entailment tests and quantifiers util. Initial draft of ... | ajreynol |
2016-04-03 | Updating the copyright headers and scripts. | Tim King |
2016-04-01 | Improvements to equality inference module: add missing cases for solvable var... | ajreynol |
2016-03-30 | Updates to E-matching to avoid entailed instantiations earlier. Minor updates... | ajreynol |
2016-03-28 | Minor cleanup from last commit (quant util, equality infer). Do not set fmfBo... | ajreynol |
2016-03-28 | Implement equality inference module for arithmetic terms. Optimization for e... | ajreynol |
2016-02-11 | More aggressive conditional rewriting for quantified formulas. Bug fix set in... | ajreynol |
2015-11-25 | Infrastructure for partially single invocation properties. Bug fix for uncons... | ajreynol |
2015-11-10 | Fix infinite loop in datatype enumerator. Minor fixes and improvements to cbq... | ajreynol |
2015-10-31 | Improvements to handling of mixed Int/Real quantifiers. | ajreynol |
2015-10-26 | Promote InstStrategyCbqi to quantifier module. Cleanup unused code. | ajreynol |
2015-08-24 | Improvements to vts in cbqi, bug fix vts for non-atomic terms containing vts ... | ajreynol |
2015-08-21 | Fix disequality bounds in cbqi, record literals for ITE skolems in cbqi. Ena... | ajreynol |
2015-06-16 | Avoid completion for large finite types. Fix bug for --fmf-fun. | ajreynol |
2015-03-04 | More work on arithmetic single invocation synthesis conjectures. | ajreynol |
2015-02-26 | Robust strategy for single invocation LIA synthesis conjectures. Add regress... | ajreynol |
2015-02-06 | Handle missing cases for single inv solution reconstruction. Minor fixes. Re... | ajreynol |
2015-02-04 | Start work on simplifying single inv solutions. Minor. | ajreynol |
2015-02-02 | Single invocation module for counterexample guided quantifier instantiation -... | ajreynol |
2015-01-29 | Restrict LtePartialInst instantiations based on E-matching, promote to quanti... | ajreynol |
2015-01-24 | Variable patterns only look at eligible terms. Minor refactoring of quantifi... | ajreynol |
2015-01-22 | Add option --lte-partial-inst. Remove inst-closure. | ajreynol |
2014-11-16 | Add term db mode. Minor changes to quantifiers rewriter: split ITE's where e... | ajreynol |
2014-07-01 | Update copyrights. | Morgan Deters |
2014-01-10 | Add new method --quant-cf for finding conflicts eagerly for quantified formul... | Andrew Reynolds |
2013-05-22 | Significant work on bounded integer quantification to handle non-trivial boun... | Andrew Reynolds |
2013-05-11 | Preliminary version of finite model finding over bounded integer quantificati... | Andrew Reynolds |
2013-05-08 | Add new method for checking candidate models, --fmf-fmc. Add infrastructure ... | Andrew Reynolds |
2013-04-02 | Regenerated copyrights: canonicalized names, no emails | Morgan Deters |
2013-02-04 | fixed files with DOS newlines; fixed contrib/ scripts to use git | Morgan Deters |
2012-10-23 | more major cleanup of quantifiers code, separating rewrite-rules-specific cod... | Andrew Reynolds |
2012-10-16 | more cleanup of quantifiers code | Andrew Reynolds |