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-09 |
Andrew Reynolds | Decouple sygus term database and term database. (... |
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-27 |
Andrew Reynolds | Refactor theory model (#1236) |
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-09-27 |
Andrew Reynolds | Minor fixes for partial quantifier elimination. (#1147) |
blob | commitdiff | raw | diff to current |
2017-08-24 |
Andrew Reynolds | Merge pull request #191 from timothy-king/cleanup-regexp |
blob | commitdiff | raw | diff to current |
2017-08-17 |
ajreynol | Add mbqi interleave option, change option fs-inst to... |
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-03-24 |
ajreynol | Refactor model building for quantifiers to be a single... |
blob | commitdiff | raw | diff to current |
2017-03-02 |
ajreynol | Eliminate Boolean term conversion. Generalizes removeIT... |
blob | commitdiff | raw | diff to current |
2017-02-16 |
ajreynol | Fixes for sets+rels check. Minor. |
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-12-02 |
Tim King | Merge pull request #95 from 4tXJ7f/fix_sierra_build |
blob | commitdiff | raw | diff to current |
2016-12-02 |
Clark Barrett | Merge pull request #113 from 4tXJ7f/remove_extract_rule |
blob | commitdiff | raw | diff to current |
2016-12-02 |
ajreynol | Refactor preprocessing of models in fmf. Fix options... |
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-15 |
ajreynol | Begin refactoring of cbqi, remove a few dead options... |
blob | commitdiff | raw | diff to current |
2016-09-15 |
ajreynol | Refactor setIncomplete in quantifiers. |
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-13 |
ajreynol | Minor changes to sep logic, epr, quantifier splitting. |
blob | commitdiff | raw | diff to current |
2016-09-12 |
ajreynol | Remove old implementation of cbqi |
blob | commitdiff | raw | diff to current |
2016-09-09 |
ajreynol | Support for separation logic + EPR. Refactor preprocess... |
blob | commitdiff | raw | diff to current |
2016-09-08 |
ajreynol | Refactor seplog preprocess. Handle case where sep data... |
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 | Cleanup quantifier elimination in smt engine. |
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-08-15 |
ajreynol | Enable bounded set membership with --fmf-bound. Map... |
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-20 |
ajreynol | Infrastructure for storing and printing heap models... |
blob | commitdiff | raw | diff to current |
2016-07-20 |
ajreynol | Print only instantiations that are in the unsat core... |
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-06-20 |
Guy | Merge branch 'master' of https://github.com/CVC4/CVC4 |
blob | commitdiff | raw | diff to current |
2016-06-17 |
ajreynol | Support for separation logic. Enable cbqi by default... |
blob | commitdiff | raw | diff to current |
2016-06-01 |
ajreynol | Initial infrastructure for bounded set quantification... |
blob | commitdiff | raw | diff to current |
2016-05-24 |
ajreynol | Improvements to symmetry breaking in sygus search.... |
blob | commitdiff | raw | diff to current |
2016-05-18 |
ajreynol | Refactor modes for sygus+single invocation. Add option... |
blob | commitdiff | raw | diff to current |
2016-05-16 |
ajreynol | Enable --sygus-direct-eval by default, limit to terms... |
blob | commitdiff | raw | diff to current |
2016-05-10 |
ajreynol | Fix for --inst-max-level |
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-11 |
ajreynol | Minor fixes for inst match generators. Updates to qip. |
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 | Minor cleanup from last commit (quant util, equality... |
blob | commitdiff | raw | diff to current |
2016-03-28 |
ajreynol | Implement equality inference module for arithmetic... |
blob | commitdiff | raw | diff to current |
2016-03-23 |
Tim King | Deleting the CDInstMatchTries in QuantifiersEngine... |
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-12 |
ajreynol | Add options related to interleaving quantifiers and... |
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 | Fixes and improvements for datatypes properties and... |
blob | commitdiff | raw | diff to current |
2016-02-19 |
ajreynol | Implement dynamic splitting for quantified formulas... |
blob | commitdiff | raw | diff to current |
2016-02-18 |
ajreynol | Correct subtyping for arrays, disable subtyping for... |
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-02-15 |
PaulMeng | Merge remote-tracking branch 'origin/master' |
blob | commitdiff | raw | diff to current |
2016-02-09 |
ajreynol | Eager introduction of eqc, lemma cache for ground fmf... |
blob | commitdiff | raw | diff to current |
2016-02-08 |
ajreynol | Updates related to finite model finding and (co)datatyp... |
blob | commitdiff | raw | diff to current |
next |