2016-11-03 |
ajreynol | Add priorities to getNextDecision. Properly handle... |
tree | commitdiff |
2016-11-02 |
ajreynol | Fix bug in separation logic for finite pto-data types... |
tree | commitdiff |
2016-11-02 |
ajreynol | Fix a few obvious memory leaks in sygus and quantifiers... |
tree | commitdiff |
2016-10-13 |
Tim King | Revert "Merge branch 'origin' of https://github.com... |
tree | commitdiff |
2016-10-11 |
Paul Meng | Merge branch 'origin' of https://github.com/CVC4/CVC4.git |
tree | commitdiff |
2016-10-01 |
Tim King | Merge pull request #93 from timothy-king/clang-format |
tree | commitdiff |
2016-09-29 |
ajreynol | Address some coverity warnings, add another stat. |
tree | commitdiff |
2016-09-29 |
ajreynol | Minor cleanup and additions to quantifiers statistics. |
tree | commitdiff |
2016-09-26 |
Tim King | Adding a destructor to QuantAntiSkolem. |
tree | commitdiff |
2016-09-26 |
Tim King | Adding a destructor to TermDb. |
tree | commitdiff |
2016-09-26 |
Tim King | Adding a destructor to CegqiOutputSingleInv. |
tree | commitdiff |
2016-09-26 |
Tim King | Disambiguating a vector insert warning coming from... |
tree | commitdiff |
2016-09-25 |
Tim King | Removing an unused iterator. |
tree | commitdiff |
2016-09-21 |
ajreynol | Remove duplicate code from my last commit |
tree | commitdiff |
2016-09-20 |
ajreynol | Refactor, separate theory-specific counterexample-guide... |
tree | commitdiff |
2016-09-20 |
ajreynol | More refactoring of cbqi. Add a few regressions. Add... |
tree | commitdiff |
2016-09-17 |
guykatzz | Merge branch 'master' of https://github.com/CVC4/CVC4 |
tree | commitdiff |
2016-09-17 |
ajreynol | Use matching heuristics for EPR instantiation. |
tree | commitdiff |
2016-09-16 |
ajreynol | More refactoring of cbqi, start developing new interface. |
tree | commitdiff |
2016-09-15 |
ajreynol | Further refactor cbqi. |
tree | commitdiff |
2016-09-15 |
ajreynol | Begin refactoring of cbqi, remove a few dead options... |
tree | commitdiff |
2016-09-15 |
ajreynol | Make sep pto a trigger kind, track in equality engines... |
tree | commitdiff |
2016-09-15 |
ajreynol | Refactor setIncomplete in quantifiers. |
tree | commitdiff |
2016-09-14 |
ajreynol | Lemma cache in theory sep. Minor optimization for sets... |
tree | commitdiff |
2016-09-13 |
ajreynol | Minor changes to sep logic, epr, quantifier splitting. |
tree | commitdiff |
2016-09-12 |
ajreynol | Refactor prenex modes. |
tree | commitdiff |
2016-09-12 |
ajreynol | Remove old implementation of cbqi |
tree | commitdiff |
2016-09-03 |
ajreynol | Miniscope top level conjunctions for prenex normal... |
tree | commitdiff |
2016-09-03 |
ajreynol | Option for prenex normal form |
tree | commitdiff |
2016-09-02 |
Tim King | Merge pull request #91 from timothy-king/no-throw |
tree | commitdiff |
2016-09-01 |
ajreynol | Fix boolean term issue in invariants from sygus. Minor... |
tree | commitdiff |
2016-09-01 |
ajreynol | Cleanup quantifier elimination in smt engine. |
tree | commitdiff |
2016-09-01 |
ajreynol | Updates to cbqi. New strategy --cbqi-nested-qe to... |
tree | commitdiff |
2016-09-01 |
Tim King | Removing the forward declaration of QuantInfo from... |
tree | commitdiff |
2016-08-26 |
ajreynol | Basic support for EPR+CBQI. Minor cleanup. |
tree | commitdiff |
2016-08-25 |
ajreynol | Minor cleanup preprocessing, add ppNotifyAssertions. |
tree | commitdiff |
2016-08-25 |
ajreynol | Options for counterexample guided instantiation. |
tree | commitdiff |
2016-08-24 |
PaulMeng | Merge remote-tracking branch 'origin/master' |
tree | commitdiff |
2016-08-15 |
ajreynol | Enable bounded set membership with --fmf-bound. Map... |
tree | commitdiff |
2016-08-12 |
ajreynol | Minor fixes to model construction to take singleton... |
tree | commitdiff |
2016-08-03 |
barrettcw | Merge pull request #87 from 4tXJ7f/fix_oob_access |
tree | commitdiff |
2016-07-28 |
Guy | Merge branch 'master' of https://github.com/CVC4/CVC4 |
tree | commitdiff |
2016-07-28 |
ajreynol | Fix bug 749. |
tree | commitdiff |
2016-07-26 |
Guy | Merge branch 'master' of https://github.com/CVC4/CVC4 |
tree | commitdiff |
2016-07-26 |
ajreynol | Add option to minimize sygus solutions based on using... |
tree | commitdiff |
2016-07-20 |
ajreynol | Infrastructure for storing and printing heap models... |
tree | commitdiff |
2016-07-20 |
ajreynol | Print only instantiations that are in the unsat core... |
tree | commitdiff |
2016-07-19 |
ajreynol | Add infrastructure for tracking instantiation lemmas... |
tree | commitdiff |
2016-07-05 |
ajreynol | Add option --trigger-active-sel. Recognize simple trigg... |
tree | commitdiff |
2016-07-05 |
PaulMeng | Merge branch 'master' of https://github.com/CVC4/CVC4.git |
tree | commitdiff |
2016-06-20 |
Guy | Merge branch 'master' of https://github.com/CVC4/CVC4 |
tree | commitdiff |
2016-06-17 |
ajreynol | Cleanup from last commit, treat sep.nil as variable... |
tree | commitdiff |
2016-06-17 |
ajreynol | Support for separation logic. Enable cbqi by default... |
tree | commitdiff |
2016-06-08 |
Guy | Merge branch 'master' of https://github.com/CVC4/CVC4 |
tree | commitdiff |
2016-06-06 |
guykatzz | Merge pull request #85 from CVC4/master_for_proof_merge |
tree | commitdiff |
2016-06-04 |
ajreynol | Remove NodeListMap from datatypes and equality inferenc... |
tree | commitdiff |
2016-06-03 |
ajreynol | Simple memory fixes, minor cleanup in quantifiers. |
tree | commitdiff |
2016-06-03 |
ajreynol | Reduce number of passes in quantifiers rewriter. |
tree | commitdiff |
2016-06-01 |
ajreynol | Fix to ignore a case of triggers with no free variables. |
tree | commitdiff |
2016-06-01 |
ajreynol | Initial infrastructure for bounded set quantification... |
tree | commitdiff |
2016-05-26 |
Clark Barrett | Merge branch 'master' of https://github.com/CVC4/CVC4 |
tree | commitdiff |
2016-05-26 |
ajreynol | Use term indexing in TheoryUF::computeCareGraph. Do... |
tree | commitdiff |
2016-05-24 |
ajreynol | Improvements to symmetry breaking in sygus search.... |
tree | commitdiff |
2016-05-23 |
ajreynol | Fix related to parametric sorts whose interpretation... |
tree | commitdiff |
2016-05-20 |
ajreynol | Improvements to theory combination + strings: do not... |
tree | commitdiff |
2016-05-18 |
ajreynol | Refactor modes for sygus+single invocation. Add option... |
tree | commitdiff |
2016-05-17 |
ajreynol | Minor fix cbqi for constant monomials. |
tree | commitdiff |
2016-05-16 |
ajreynol | Enable --sygus-direct-eval by default, limit to terms... |
tree | commitdiff |
2016-05-15 |
ajreynol | Work on --sygus-direct-eval. Minor optimizations, updat... |
tree | commitdiff |
2016-05-12 |
ajreynol | Add casc scripts. Improvements to qcf related to nested... |
tree | commitdiff |
2016-05-10 |
ajreynol | Add smt comp 2016 scripts. Fix for --relevant-triggers... |
tree | commitdiff |
2016-05-06 |
ajreynol | Minor clean up, fixes related to sygus. |
tree | commitdiff |
2016-05-05 |
ajreynol | Compute term indices lazily in TermDb. Optimization... |
tree | commitdiff |
2016-05-02 |
ajreynol | Clean up issues related to compiled scc in LFSC. Refact... |
tree | commitdiff |
2016-04-28 |
ajreynol | More work on inst propagate. Optimization for qcf... |
tree | commitdiff |
2016-04-20 |
PaulMeng | update from the master |
tree | commitdiff |
2016-04-13 |
ajreynol | Minor improvements for alpha equivalence and partial... |
tree | commitdiff |
2016-04-13 |
ajreynol | Handle parametric datatypes with --quant-ind. Minor... |
tree | commitdiff |
2016-04-12 |
ajreynol | Bug fixes related to parametric datatypes + theory... |
tree | commitdiff |
2016-04-12 |
ajreynol | Optimizations for QCF to check relevant domain of varia... |
tree | commitdiff |
2016-04-11 |
ajreynol | Minor fixes for inst match generators. Updates to qip. |
tree | commitdiff |
2016-04-10 |
ajreynol | More work on instantiation propagation. Enable external... |
tree | commitdiff |
2016-04-09 |
Guy | Merge branch 'master' of https://github.com/CVC4/CVC4 |
tree | commitdiff |
2016-04-09 |
ajreynol | Minor refactoring of entailment tests and quantifiers... |
tree | commitdiff |
2016-04-07 |
ajreynol | Refactor trigger selection, revisions to --relational... |
tree | commitdiff |
2016-04-04 |
ajreynol | New options for trigger selection, add option --strict... |
tree | commitdiff |
2016-04-04 |
Tim King | Updating the copyright headers and scripts. |
tree | commitdiff |
2016-04-01 |
ajreynol | Improvements to equality inference module: add missing... |
tree | commitdiff |
2016-03-31 |
ajreynol | Improvements to trigger selection, min triggers by... |
tree | commitdiff |
2016-03-30 |
ajreynol | Updates to E-matching to avoid entailed instantiations... |
tree | commitdiff |
2016-03-28 |
ajreynol | Minor cleanup from last commit (quant util, equality... |
tree | commitdiff |
2016-03-28 |
ajreynol | Implement equality inference module for arithmetic... |
tree | commitdiff |
2016-03-24 |
Tim King | Freeing CegConjecture::d_ceg_si. Also making d_ceg_si... |
tree | commitdiff |
2016-03-24 |
Tim King | Fixing a memory leak in CDInstMatchTrie::d_data. |
tree | commitdiff |
2016-03-24 |
Tim King | Fix for a memory leak in InstStrategyCegqi. |
tree | commitdiff |
2016-03-24 |
Tim King | Fixing a memory leak in QuantInfo::d_var_mg. |
tree | commitdiff |
2016-03-23 |
Tim King | Fixing memory leaks in Trigger and TriggerTrie. |
tree | commitdiff |
2016-03-22 |
ajreynol | Bug fix for define functions + incremental. Minor work... |
tree | commitdiff |
2016-03-18 |
ajreynol | Limit duplicate propagating instances to avoid exponent... |
tree | commitdiff |
2016-03-16 |
ajreynol | Change internal representative selection for finite... |
tree | commitdiff |
next |