| 2016-09-20 |
ajreynol | More refactoring of cbqi. Add a few regressions. Add... |
commit | commitdiff | tree |
| 2016-09-19 |
Tim King | Merge pull request #92 from timothy-king/travis-cpp11 |
commit | commitdiff | tree |
| 2016-09-18 |
Tim King | Adding a gnu++11 rule to travis. |
commit | commitdiff | tree |
| 2016-09-18 |
ajreynol | Minor fix for strings |
commit | commitdiff | tree |
| 2016-09-17 |
guykatzz | In a ROW guard proof, if the transitivity proof does... |
commit | commitdiff | tree |
| 2016-09-17 |
guykatzz | Merge branch 'master' of https://github.com/CVC4/CVC4 |
commit | commitdiff | tree |
| 2016-09-17 |
ajreynol | Use matching heuristics for EPR instantiation. |
commit | commitdiff | tree |
| 2016-09-16 |
Guy | Handling a corner case where a ROW's guard is a constan... |
commit | commitdiff | tree |
| 2016-09-16 |
Guy | Let arith_proof print its own terms |
commit | commitdiff | tree |
| 2016-09-16 |
ajreynol | More refactoring of cbqi, start developing new interface. |
commit | commitdiff | tree |
| 2016-09-15 |
ajreynol | Further refactor cbqi. |
commit | commitdiff | tree |
| 2016-09-15 |
ajreynol | Begin refactoring of cbqi, remove a few dead options... |
commit | commitdiff | tree |
| 2016-09-15 |
ajreynol | Make sep pto a trigger kind, track in equality engines... |
commit | commitdiff | tree |
| 2016-09-15 |
ajreynol | Refactor setIncomplete in quantifiers. |
commit | commitdiff | tree |
| 2016-09-14 |
ajreynol | Support for unique variable generation in node manager. |
commit | commitdiff | tree |
| 2016-09-14 |
ajreynol | Lemma cache in theory sep. Minor optimization for sets... |
commit | commitdiff | tree |
| 2016-09-13 |
ajreynol | Minor changes to sep logic, epr, quantifier splitting. |
commit | commitdiff | tree |
| 2016-09-12 |
ajreynol | Refactor prenex modes. |
commit | commitdiff | tree |
| 2016-09-12 |
ajreynol | Remove old implementation of cbqi |
commit | commitdiff | tree |
| 2016-09-12 |
ajreynol | Prefer non-cardinality constants in term models for... |
commit | commitdiff | tree |
| 2016-09-12 |
ajreynol | Ensure sep.nil is unique per type at NodeManager level... |
commit | commitdiff | tree |
| 2016-09-09 |
ajreynol | Fix bug in unconstrained simplifier related to sep... |
commit | commitdiff | tree |
| 2016-09-09 |
ajreynol | Support for separation logic + EPR. Refactor preprocess... |
commit | commitdiff | tree |
| 2016-09-08 |
ajreynol | Refactor seplog preprocess. Handle case where sep data... |
commit | commitdiff | tree |
| 2016-09-03 |
ajreynol | Miniscope top level conjunctions for prenex normal... |
commit | commitdiff | tree |
| 2016-09-03 |
ajreynol | Option for prenex normal form |
commit | commitdiff | tree |
| 2016-09-02 |
Tim King | Merge pull request #91 from timothy-king/no-throw |
commit | commitdiff | tree |
| 2016-09-01 |
ajreynol | Fix boolean term issue in invariants from sygus. Minor... |
commit | commitdiff | tree |
| 2016-09-01 |
ajreynol | Cleanup quantifier elimination in smt engine. |
commit | commitdiff | tree |
| 2016-09-01 |
ajreynol | Updates to cbqi. New strategy --cbqi-nested-qe to... |
commit | commitdiff | tree |
| 2016-09-01 |
Tim King | Relaxing the throw specifiers for the destructors for... |
commit | commitdiff | tree |
| 2016-09-01 |
Tim King | Removing the forward declaration of QuantInfo from... |
commit | commitdiff | tree |
| 2016-08-31 |
Tim King | Cleaning up the dead FORIT macros. |
commit | commitdiff | tree |
| 2016-08-31 |
Tim King | Removing the usage of typeof from theory_sets_private. |
commit | commitdiff | tree |
| 2016-08-31 |
Tim King | Beautifying theory_model.h. |
commit | commitdiff | tree |
| 2016-08-31 |
Tim King | Removing BOOST_FOREACH from theory/sets/scrutinize.h. |
commit | commitdiff | tree |
| 2016-08-31 |
Tim King | Removing typeof from sets normal form and beautifying... |
commit | commitdiff | tree |
| 2016-08-31 |
Tim King | Removing typeof from command_executor_portfolio.cpp. |
commit | commitdiff | tree |
| 2016-08-31 |
Tim King | Removing typeof from didyoumean.cpp. |
commit | commitdiff | tree |
| 2016-08-26 |
ajreynol | Basic support for EPR+CBQI. Minor cleanup. |
commit | commitdiff | tree |
| 2016-08-25 |
ajreynol | Minor cleanup preprocessing, add ppNotifyAssertions. |
commit | commitdiff | tree |
| 2016-08-25 |
ajreynol | Options for counterexample guided instantiation. |
commit | commitdiff | tree |
| 2016-08-20 |
Clark Barrett | Fixed two bugs |
commit | commitdiff | tree |
| 2016-08-19 |
Clark Barrett | Added fitsSignedLong and fitsUnsignedLong |
commit | commitdiff | tree |
| 2016-08-16 |
ajreynol | Initial infrastructure for ExtTheory, generalize extend... |
commit | commitdiff | tree |
| 2016-08-15 |
ajreynol | Expression sharing on demand in LFSC (replace definitio... |
commit | commitdiff | tree |
| 2016-08-15 |
ajreynol | Enable bounded set membership with --fmf-bound. Map... |
commit | commitdiff | tree |
| 2016-08-12 |
ajreynol | Add a few more regressions. |
commit | commitdiff | tree |
| 2016-08-12 |
ajreynol | Minor fixes to model construction to take singleton... |
commit | commitdiff | tree |
| 2016-08-12 |
guykatzz | Merge pull request #90 from 4tXJ7f/fewer_preproc_holes |
commit | commitdiff | tree |
| 2016-08-12 |
Andres Notzli | Add support for fewer preprocessing holes |
commit | commitdiff | tree |
| 2016-08-11 |
ajreynol | Minor change to strings, introduce proxy vars only... |
commit | commitdiff | tree |
| 2016-08-10 |
ajreynol | Improvements to strings: work on propagations for rever... |
commit | commitdiff | tree |
| 2016-08-09 |
guykatzz | Merge pull request #89 from 4tXJ7f/fix_proof_spaces |
commit | commitdiff | tree |
| 2016-08-09 |
ajreynol | Fixes for sep star rewrite. |
commit | commitdiff | tree |
| 2016-08-09 |
Andres Notzli | Fix missing/redundant spaces in proofs |
commit | commitdiff | tree |
| 2016-08-06 |
guykatzz | Merge pull request #88 from 4tXJ7f/fix_comments |
commit | commitdiff | tree |
| 2016-08-05 |
Andres Notzli | Minor: add/fix comments, remove redundant includes |
commit | commitdiff | tree |
| 2016-08-03 |
Guy | Fixed an issue where arrays proofs would sometimes... |
commit | commitdiff | tree |
| 2016-08-03 |
barrettcw | Merge pull request #87 from 4tXJ7f/fix_oob_access |
commit | commitdiff | tree |
| 2016-07-30 |
ajreynol | Prioritize inferences when processing normal forms... |
commit | commitdiff | tree |
| 2016-07-28 |
Guy | The "aggressive" optimizer for lemma L now returns... |
commit | commitdiff | tree |
| 2016-07-28 |
Guy | Merge branch 'master' of https://github.com/CVC4/CVC4 |
commit | commitdiff | tree |
| 2016-07-28 |
Guy | Bug fix involving negated lemmas |
commit | commitdiff | tree |
| 2016-07-28 |
ajreynol | Fix bug 749. |
commit | commitdiff | tree |
| 2016-07-28 |
Guy | Add the negative conjunction case |
commit | commitdiff | tree |
| 2016-07-28 |
Andres Notzli | Fix out-of-bounds access in ExprManager |
commit | commitdiff | tree |
| 2016-07-28 |
Guy | Proper instrumentation of the preprocessing phase |
commit | commitdiff | tree |
| 2016-07-28 |
Guy | proper handling of ITEs |
commit | commitdiff | tree |
| 2016-07-27 |
Guy | Proper handling of IFF lemmas in the unsat core. |
commit | commitdiff | tree |
| 2016-07-27 |
Guy | Added an option for a more aggressive weakest implicant... |
commit | commitdiff | tree |
| 2016-07-27 |
Guy | If we can't find a weaker implicant, fail gracefully... |
commit | commitdiff | tree |
| 2016-07-27 |
guykatzz | Merge pull request #86 from 4tXJ7f/fix_warnings |
commit | commitdiff | tree |
| 2016-07-27 |
Andres Notzli | Fix warnings in src/proof |
commit | commitdiff | tree |
| 2016-07-26 |
Guy | Merge branch 'master' of https://github.com/CVC4/CVC4 |
commit | commitdiff | tree |
| 2016-07-26 |
Guy | Bug fix: |
commit | commitdiff | tree |
| 2016-07-26 |
ajreynol | Add option to minimize sygus solutions based on using... |
commit | commitdiff | tree |
| 2016-07-26 |
Guy | Merge branch 'master' of https://github.com/CVC4/CVC4 |
commit | commitdiff | tree |
| 2016-07-26 |
Guy | Letification of BV constants |
commit | commitdiff | tree |
| 2016-07-26 |
ajreynol | Minor improvements to strings related to constant split... |
commit | commitdiff | tree |
| 2016-07-26 |
Guy | Added functionality to retrieve a lemma's "weakest... |
commit | commitdiff | tree |
| 2016-07-26 |
Guy | Bug fix |
commit | commitdiff | tree |
| 2016-07-26 |
Guy | Propagate the usage of proof let maps into constant... |
commit | commitdiff | tree |
| 2016-07-25 |
Guy | Bug fix |
commit | commitdiff | tree |
| 2016-07-25 |
Guy | Merge branch 'master' of https://github.com/CVC4/CVC4 |
commit | commitdiff | tree |
| 2016-07-25 |
Guy | cleanup |
commit | commitdiff | tree |
| 2016-07-25 |
Guy | Use letification for the aliasing declarations as well... |
commit | commitdiff | tree |
| 2016-07-25 |
Guy | Proper handling for lemmas that are conjuncts: |
commit | commitdiff | tree |
| 2016-07-22 |
ajreynol | Minor, error handling for polymorphism + sep logic. |
commit | commitdiff | tree |
| 2016-07-21 |
ajreynol | Fixes for strings, explanations for constant split... |
commit | commitdiff | tree |
| 2016-07-20 |
ajreynol | Infrastructure for storing and printing heap models... |
commit | commitdiff | tree |
| 2016-07-20 |
ajreynol | Print only instantiations that are in the unsat core... |
commit | commitdiff | tree |
| 2016-07-20 |
ajreynol | Infer conflicts in strings based on abstracting equalit... |
commit | commitdiff | tree |
| 2016-07-20 |
Guy | Bug fix |
commit | commitdiff | tree |
| 2016-07-20 |
Guy | Allow a caller to query whether an unsat core is availa... |
commit | commitdiff | tree |
| 2016-07-19 |
ajreynol | Add infrastructure for tracking instantiation lemmas... |
commit | commitdiff | tree |
| 2016-07-16 |
ajreynol | Refactor strings extf evaluation info. Ensure strings... |
commit | commitdiff | tree |
| 2016-07-15 |
Guy | Moved the assertion to a better spot |
commit | commitdiff | tree |
| 2016-07-15 |
Guy | The ProofManager now allows theory solvers to get their... |
commit | commitdiff | tree |
| 2016-07-15 |
ajreynol | Minor simplification to normal form explanations. |
commit | commitdiff | tree |
| next |
projects / cvc5.git / shortlog