| 2016-04-09 |
Kshitij Bansal | cardinality operation for finite sets (based on my... |
commit | commitdiff | tree |
| 2016-04-09 |
ajreynol | Minor refactoring of entailment tests and quantifiers... |
commit | commitdiff | tree |
| 2016-04-07 |
ajreynol | Refactor trigger selection, revisions to --relational... |
commit | commitdiff | tree |
| 2016-04-04 |
ajreynol | New options for trigger selection, add option --strict... |
commit | commitdiff | tree |
| 2016-04-04 |
Tim King | Updating the copyright headers and scripts. |
commit | commitdiff | tree |
| 2016-04-04 |
Guy | s_ prefix for static members |
commit | commitdiff | tree |
| 2016-04-03 |
Guy | Removed the theory-specific merge reason types. Instead... |
commit | commitdiff | tree |
| 2016-04-01 |
ajreynol | Improvements to equality inference module: add missing... |
commit | commitdiff | tree |
| 2016-03-31 |
ajreynol | Improvements to trigger selection, min triggers by... |
commit | commitdiff | tree |
| 2016-03-30 |
ajreynol | Updates to E-matching to avoid entailed instantiations... |
commit | commitdiff | tree |
| 2016-03-30 |
Tim King | Updating the mailmap for git. |
commit | commitdiff | tree |
| 2016-03-28 |
ajreynol | Minor cleanup from last commit (quant util, equality... |
commit | commitdiff | tree |
| 2016-03-28 |
ajreynol | Implement equality inference module for arithmetic... |
commit | commitdiff | tree |
| 2016-03-24 |
Guy | Merge branch 'master' of https://github.com/CVC4/CVC4 |
commit | commitdiff | tree |
| 2016-03-24 |
Guy | Refactored the equality engine in order to remove theor... |
commit | commitdiff | tree |
| 2016-03-24 |
Tim King | Fixing a garbage collection issue in simplifyWithCare... |
commit | commitdiff | tree |
| 2016-03-24 |
Tim King | Deleting allocated NodeVecs in ITESimplifier. |
commit | commitdiff | tree |
| 2016-03-24 |
Tim King | Freeing CegConjecture::d_ceg_si. Also making d_ceg_si... |
commit | commitdiff | tree |
| 2016-03-24 |
Tim King | Fixing a memory leak in CDInstMatchTrie::d_data. |
commit | commitdiff | tree |
| 2016-03-24 |
Tim King | Fix for a memory leak in InstStrategyCegqi. |
commit | commitdiff | tree |
| 2016-03-24 |
Tim King | Fixing a memory leak in QuantInfo::d_var_mg. |
commit | commitdiff | tree |
| 2016-03-23 |
guykatzz | Merge pull request #82 from CVC4/master_for_merge |
commit | commitdiff | tree |
| 2016-03-23 |
Guy | squash-merge from proof branch |
commit | commitdiff | tree |
| 2016-03-23 |
Tim King | Fixing memory leaks in Trigger and TriggerTrie. |
commit | commitdiff | tree |
| 2016-03-23 |
Clark Barrett | Fixed help for tear-down-incremental option |
commit | commitdiff | tree |
| 2016-03-23 |
Tim King | Fixing two garbage collection issues in Region and... |
commit | commitdiff | tree |
| 2016-03-23 |
Tim King | Deleting the CDInstMatchTries in QuantifiersEngine... |
commit | commitdiff | tree |
| 2016-03-23 |
Tim King | Garbage collecting the EqcInfo s in TheoryDatatypes... |
commit | commitdiff | tree |
| 2016-03-23 |
Tim King | Garbage collecting the MinisatEmptyNotify for the Eager... |
commit | commitdiff | tree |
| 2016-03-22 |
ajreynol | Bug fix for define functions + incremental. Minor work... |
commit | commitdiff | tree |
| 2016-03-22 |
Tim King | Deleting the contents of d_modelGlobalsCommands before... |
commit | commitdiff | tree |
| 2016-03-22 |
Tim King | New version of the recursive options parsing strategy. |
commit | commitdiff | tree |
| 2016-03-18 |
ajreynol | Limit duplicate propagating instances to avoid exponent... |
commit | commitdiff | tree |
| 2016-03-16 |
ajreynol | Change internal representative selection for finite... |
commit | commitdiff | tree |
| 2016-03-12 |
ajreynol | Add options related to interleaving quantifiers and... |
commit | commitdiff | tree |
| 2016-03-10 |
ajreynol | Faster conditional rewriting for and/or beneath quantif... |
commit | commitdiff | tree |
| 2016-03-08 |
ajreynol | Extend synthesis solver to handle single invocation... |
commit | commitdiff | tree |
| 2016-03-07 |
ajreynol | Minor change to F-Length inference in strings. No inter... |
commit | commitdiff | tree |
| 2016-03-03 |
ajreynol | Add missing code to track dependencies recursively... |
commit | commitdiff | tree |
| 2016-03-02 |
ajreynol | Work towards complete instantiation for datatypes. |
commit | commitdiff | tree |
| 2016-03-01 |
ajreynol | Shorter explanations for strings based on tracking... |
commit | commitdiff | tree |
| 2016-02-29 |
ajreynol | Minor options to datatypes. |
commit | commitdiff | tree |
| 2016-02-26 |
ajreynol | Refactoring of inferences in strings. Add several options. |
commit | commitdiff | tree |
| 2016-02-25 |
ajreynol | Minor improvement to partial qe. Add options for repres... |
commit | commitdiff | tree |
| 2016-02-24 |
ajreynol | Add entailment checks between length terms to reduce... |
commit | commitdiff | tree |
| 2016-02-24 |
Tim King | Adding the missing clause_id.h file. |
commit | commitdiff | tree |
| 2016-02-24 |
Tim King | Unifying the definitions of ClauseId to a single source... |
commit | commitdiff | tree |
| 2016-02-23 |
ajreynol | Fix term database for non-equal, congruent terms in... |
commit | commitdiff | tree |
| 2016-02-19 |
ajreynol | Fixes and improvements for datatypes properties and... |
commit | commitdiff | tree |
| 2016-02-19 |
ajreynol | Implement dynamic splitting for quantified formulas... |
commit | commitdiff | tree |
| 2016-02-18 |
ajreynol | Correct subtyping for arrays, disable subtyping for... |
commit | commitdiff | tree |
| 2016-02-18 |
Kshitij Bansal | fix for windows builds |
commit | commitdiff | tree |
| 2016-02-17 |
ajreynol | Refactor quantifiers attributes. Make quantifier elimin... |
commit | commitdiff | tree |
| 2016-02-16 |
ajreynol | Public interface for quantifier elimination. Minor... |
commit | commitdiff | tree |
| 2016-02-16 |
ajreynol | More simplification to internal implementation of tuple... |
commit | commitdiff | tree |
| 2016-02-15 |
ajreynol | Minor change to last commit |
commit | commitdiff | tree |
| 2016-02-15 |
ajreynol | Eliminate most of the internal representation infrastru... |
commit | commitdiff | tree |
| 2016-02-11 |
ajreynol | More aggressive conditional rewriting for quantified... |
commit | commitdiff | tree |
| 2016-02-10 |
ajreynol | Fix model postprocessor for tuples, add regression. |
commit | commitdiff | tree |
| 2016-02-09 |
ajreynol | Fix regression, minor change to output. |
commit | commitdiff | tree |
| 2016-02-09 |
ajreynol | Eager introduction of eqc, lemma cache for ground fmf... |
commit | commitdiff | tree |
| 2016-02-08 |
ajreynol | Updates related to finite model finding and (co)datatyp... |
commit | commitdiff | tree |
| 2016-02-06 |
guykatzz | Changing the way the equality engine explains disequali... |
commit | commitdiff | tree |
| 2016-02-05 |
ajreynol | Add two optimizations for datatypes, currently disabled... |
commit | commitdiff | tree |
| 2016-02-04 |
Clark Barrett | Fixed two more memory leaks in array_info.cpp |
commit | commitdiff | tree |
| 2016-02-03 |
Clark Barrett | Added --omit-dont-cares option which doesn't print... |
commit | commitdiff | tree |
| 2016-02-02 |
Tim King | Moving dump.*, command.*, model.*, and ite_removal... |
commit | commitdiff | tree |
| 2016-02-01 |
Tim King | Removing the CVC4_PUBLIC attribute from the forward... |
commit | commitdiff | tree |
| 2016-02-01 |
Tim King | Removing the CVC4_NEEDS_REPLACEMENT_FUNCTIONS guard... |
commit | commitdiff | tree |
| 2016-02-01 |
Tim King | Generalizing lib/strtok_r.c so that it can always be... |
commit | commitdiff | tree |
| 2016-02-01 |
Tim King | Generalizing the implementation of lib/clock_gettime... |
commit | commitdiff | tree |
| 2016-02-01 |
Tim King | Fixing a potentially malformed template expansion when... |
commit | commitdiff | tree |
| 2016-02-01 |
Tim King | Fixing a memory leak in bv_subtheory_algebraic.cpp... |
commit | commitdiff | tree |
| 2016-02-01 |
Tim King | Adding an virtual destructor to OstreamUpdate. |
commit | commitdiff | tree |
| 2016-02-01 |
Tim King | Making the ManagedOstream::defaultSource() a const... |
commit | commitdiff | tree |
| 2016-02-01 |
Tim King | Adding a destructor to ProofOutputChannel. |
commit | commitdiff | tree |
| 2016-02-01 |
Tim King | Fixing white spaces in sat_proof.h. |
commit | commitdiff | tree |
| 2016-02-01 |
Tim King | Making the references to std more explicit in didyoumea... |
commit | commitdiff | tree |
| 2016-02-01 |
Tim King | Fixing a memory leak in array info. |
commit | commitdiff | tree |
| 2016-02-01 |
Tim King | Deleting the dead code in proof/sat_proof.cpp. |
commit | commitdiff | tree |
| 2016-02-01 |
ajreynol | Simplify fmc model construction, add regression. Improv... |
commit | commitdiff | tree |
| 2016-01-28 |
Tim King | Adding listeners to Options. |
commit | commitdiff | tree |
| 2016-01-27 |
Liana Hadarean | Merged bit-vector and uf proof branch. |
commit | commitdiff | tree |
| 2016-01-20 |
ajreynol | Fix bug in fmc mbqi where modelscomputed for mbqi could... |
commit | commitdiff | tree |
| 2016-01-19 |
ajreynol | Bug fixes for model construction with codatatypes,... |
commit | commitdiff | tree |
| 2016-01-18 |
ajreynol | Bug fix rewriter for fun defs. |
commit | commitdiff | tree |
| 2016-01-15 |
ajreynol | Type enumerators take optional argument indicating... |
commit | commitdiff | tree |
| 2016-01-14 |
ajreynol | Ensure model construction for parametric sorts involvin... |
commit | commitdiff | tree |
| 2016-01-13 |
ajreynol | Lemma cache datatypes. Do not send true lemma in quanti... |
commit | commitdiff | tree |
| 2016-01-09 |
Tim King | Adding a new Listener utility class. Changing the Resou... |
commit | commitdiff | tree |
| 2016-01-09 |
Tim King | Removing StatisticsRegistry's static functions current... |
commit | commitdiff | tree |
| 2016-01-08 |
Tim King | Disabling the RESTART command. |
commit | commitdiff | tree |
| 2016-01-06 |
Kshitij Bansal | fix windows builds |
commit | commitdiff | tree |
| 2016-01-06 |
Tim King | Fixing a SWIG ordering issue between bitvector and... |
commit | commitdiff | tree |
| 2016-01-06 |
Tim King | Improving the documentation of the CVC command CONTINUE. |
commit | commitdiff | tree |
| 2016-01-06 |
Tim King | Removing dead code. StackingMap only appeared in unit... |
commit | commitdiff | tree |
| 2016-01-06 |
Tim King | Moving sexpr.{cpp,h,i} from expr/ back into util/. |
commit | commitdiff | tree |
| 2016-01-06 |
Tim King | Add SmtGlobals Class |
commit | commitdiff | tree |
| 2016-01-05 |
Tim King | Adding a new class LastExceptionBuffer for the purpose... |
commit | commitdiff | tree |
| 2016-01-01 |
Clark Barrett | Added propagation rule for array ext lemmas to aid... |
commit | commitdiff | tree |
| next |
projects / cvc5.git / shortlog