| Age | Commit message (Expand) | Author |
|---|
| 2017-03-02 | Minor cleanup and reorganization related to last commit. | ajreynol |
| 2017-03-02 | Eliminate Boolean term conversion. Generalizes removeITE pass to remove Boole... | ajreynol |
| 2016-11-03 | Add priorities to getNextDecision. Properly handle case for finite types + un... | 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-29 | Address some coverity warnings, add another stat. | ajreynol |
| 2016-09-29 | Minor cleanup and additions to quantifiers statistics. | ajreynol |
| 2016-09-25 | Removing an unused iterator. | Tim King |
| 2016-09-15 | Refactor setIncomplete in quantifiers. | ajreynol |
| 2016-09-12 | Remove old implementation of cbqi | ajreynol |
| 2016-09-03 | Miniscope top level conjunctions for prenex normal form, allow one level mini... | ajreynol |
| 2016-09-03 | Option for prenex normal form | ajreynol |
| 2016-09-01 | Fix boolean term issue in invariants from sygus. Minor default options change... | ajreynol |
| 2016-09-01 | Cleanup quantifier elimination in smt engine. | ajreynol |
| 2016-09-01 | Updates to cbqi. New strategy --cbqi-nested-qe to do qe on nested quantifier... | ajreynol |
| 2016-08-26 | Basic support for EPR+CBQI. Minor cleanup. | ajreynol |
| 2016-08-25 | Options for counterexample guided instantiation. | 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-05-15 | Work on --sygus-direct-eval. Minor optimizations, updates to casc scripts. En... | ajreynol |
| 2016-04-20 | update from the master | PaulMeng |
| 2016-04-13 | Minor improvements for alpha equivalence and partial quantifier elimination i... | ajreynol |
| 2016-04-12 | Optimizations for QCF to check relevant domain of variable argument positions... | ajreynol |
| 2016-04-10 | More work on instantiation propagation. Enable external filtering of instanti... | ajreynol |
| 2016-04-03 | Updating the copyright headers and scripts. | Tim King |
| 2016-03-24 | Fix for a memory leak in InstStrategyCegqi. | Tim King |
| 2016-02-25 | Minor improvement to partial qe. Add options for representative selection in ... | ajreynol |
| 2016-02-18 | Implement dynamic splitting for quantified formulas. Minor refactoring of re... | ajreynol |
| 2016-02-17 | Refactor quantifiers attributes. Make quantifier elimination robust to prepro... | ajreynol |
| 2016-02-02 | Moving dump.*, command.*, model.*, and ite_removal.* from smt_util/ to smt/. ... | Tim King |
| 2015-12-22 | Bug fix for cbqi, do not use model values for terms involving non-enumerable ... | ajreynol |
| 2015-12-14 | Refactoring Options Handler & Library Cycle Breaking | Tim King |
| 2015-11-23 | Adding a missing delete to InstStrategyCegqi destructor. | Tim King |
| 2015-11-11 | Minor fixes to cbqi, purify-quant. Better error checking in addInstantiation. | ajreynol |
| 2015-11-10 | Fix infinite loop in datatype enumerator. Minor fixes and improvements to cbq... | ajreynol |
| 2015-11-04 | Better combination of UF with cbqi, refactor quantifiers intialization. | ajreynol |
| 2015-10-26 | Promote InstStrategyCbqi to quantifier module. Cleanup unused code. | ajreynol |
| 2015-10-22 | Enable counterexample-guided quantifier instantiation by default for quantifi... | ajreynol |
| 2015-09-29 | Fix for fmf+incremental. Restrict cbqi to literals from ce body. Add regress... | ajreynol |
| 2015-09-26 | Better organization of quantifiers modules, promote full saturation to module... | ajreynol |
| 2015-09-25 | Clear term caches for quantifiers + incremental, fixes bug 674. Refactoring ... | ajreynol |
| 2015-09-24 | Counterexample-guided instantiation for datatypes. Make sygus parsing more l... | ajreynol |
| 2015-08-27 | Do ITE term bookkeeping when solving Sygus inputs. Add missing script from S... | ajreynol |
| 2015-08-26 | Minor improvements to cbqi, fix bug in solving with vts symbols, round up for... | ajreynol |
| 2015-08-25 | Use zero in cbqi when not using infinities. | 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-08-19 | Make cbqi robust to term ITE removal. Separate vts infinities for int/real. | ajreynol |
| 2015-08-19 | Implementation of model-based projection in cbqi, cleanup, add regressions. | ajreynol |
| 2015-08-12 | Improvements to --macros-quant. Enable --clause-split by default. Bug fix for... | ajreynol |
