| 2016-09-28 |
Kshitij Bansal | Fix the merge of kbansal/card branch (2039eab). |
commit | commitdiff | tree |
| 2016-09-27 |
Tim King | Removing an unused iterator. |
commit | commitdiff | tree |
| 2016-09-27 |
Tim King | Reverting part of the previous changes to unconstrained... |
commit | commitdiff | tree |
| 2016-09-26 |
Tim King | Simplifying control flow to avoid goto's in unconstrain... |
commit | commitdiff | tree |
| 2016-09-26 |
Tim King | Adding missing break statements. |
commit | commitdiff | tree |
| 2016-09-26 |
Tim King | Closing an open file descriptor in MemoryMapFile. |
commit | commitdiff | tree |
| 2016-09-26 |
Tim King | Freeing memory in error handling code for bounded_token... |
commit | commitdiff | tree |
| 2016-09-26 |
Tim King | Deleting the eager bitblasting solver if present in... |
commit | commitdiff | tree |
| 2016-09-26 |
Tim King | Adding a destructor to QuantAntiSkolem. |
commit | commitdiff | tree |
| 2016-09-26 |
Tim King | Adding a destructor to TermDb. |
commit | commitdiff | tree |
| 2016-09-26 |
Tim King | Adding a destructor to CegqiOutputSingleInv. |
commit | commitdiff | tree |
| 2016-09-26 |
Tim King | Deleting optional members of StrongSolverTheoryUF. |
commit | commitdiff | tree |
| 2016-09-26 |
Tim King | Disambiguating a vector insert warning coming from... |
commit | commitdiff | tree |
| 2016-09-26 |
Tim King | Deleting a temporary in theory sets enumerator. |
commit | commitdiff | tree |
| 2016-09-26 |
Tim King | Deleting the intermediate command singleton. |
commit | commitdiff | tree |
| 2016-09-26 |
Tim King | Disambiguating a type issue. Coverity scan reported... |
commit | commitdiff | tree |
| 2016-09-25 |
Tim King | Adding virtual destructors to several classes in expr.h . |
commit | commitdiff | tree |
| 2016-09-25 |
Tim King | Removing an unused iterator. |
commit | commitdiff | tree |
| 2016-09-25 |
Tim King | Fixing a potential use after free coming from a pop_bac... |
commit | commitdiff | tree |
| 2016-09-25 |
Tim King | Integrating a working coverity_scan travis rule back... |
commit | commitdiff | tree |
| 2016-09-21 |
ajreynol | Remove duplicate code from my last commit |
commit | commitdiff | tree |
| 2016-09-21 |
Tim King | Fixing an error in the previous travis commit. |
commit | commitdiff | tree |
| 2016-09-21 |
Tim King | Updating the travis file for coverity scan. |
commit | commitdiff | tree |
| 2016-09-20 |
ajreynol | Refactor, separate theory-specific counterexample-guide... |
commit | commitdiff | tree |
| 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 |
| next |
projects / cvc5.git / shortlog