| 2016-07-05 |
PaulMeng | fixes bugs in std effort for TC |
commit | commitdiff | tree |
| 2016-06-25 |
PaulMeng | debug statement |
commit | commitdiff | tree |
| 2016-06-25 |
PaulMeng | Merge remote-tracking branch 'origin/master' |
commit | commitdiff | tree |
| 2016-06-25 |
PaulMeng | test |
commit | commitdiff | tree |
| 2016-06-25 |
PaulMeng | reimplemented std effort for TC |
commit | commitdiff | tree |
| 2016-05-05 |
PaulMeng | change to use tuple element representatives to build... |
commit | commitdiff | tree |
| 2016-05-04 |
PaulMeng | implemented TC for standard effort |
commit | commitdiff | tree |
| 2016-04-20 |
PaulMeng | update from the master |
commit | commitdiff | tree |
| 2016-04-20 |
PaulMeng | add utils class for relational theory |
commit | commitdiff | tree |
| 2016-04-20 |
PaulMeng | Refactored code |
commit | commitdiff | tree |
| 2016-04-15 |
PaulMeng | change transitive closure operator name to TCLOUSRE |
commit | commitdiff | tree |
| 2016-04-15 |
PaulMeng | - Implement constant rewriter for relational operators... |
commit | commitdiff | tree |
| 2016-04-12 |
PaulMeng | added more benchmarks |
commit | commitdiff | tree |
| 2016-04-12 |
PaulMeng | fixed explanation for transitive closure inferences |
commit | commitdiff | tree |
| 2016-04-07 |
PaulMeng | implement standard effort support for product |
commit | commitdiff | tree |
| 2016-04-07 |
PaulMeng | - added standard effort for transpose |
commit | commitdiff | tree |
| 2016-03-23 |
PaulMeng | added typing rule for transitive closure |
commit | commitdiff | tree |
| 2016-03-22 |
PaulMeng | minor fix |
commit | commitdiff | tree |
| 2016-03-22 |
PaulMeng | minor fix |
commit | commitdiff | tree |
| 2016-03-11 |
PaulMeng | minor fix |
commit | commitdiff | tree |
| 2016-03-10 |
PaulMeng | minor fix |
commit | commitdiff | tree |
| 2016-03-10 |
PaulMeng | fixed the transpose-occur rule |
commit | commitdiff | tree |
| 2016-03-09 |
PaulMeng | make skolems and tuple reduction terms as shared terms |
commit | commitdiff | tree |
| 2016-03-07 |
PaulMeng | modified CVC4 native language parser to accept 1-tuple... |
commit | commitdiff | tree |
| 2016-03-04 |
PaulMeng | refactored the code |
commit | commitdiff | tree |
| 2016-03-01 |
PaulMeng | small fixes for eq rep names |
commit | commitdiff | tree |
| 2016-03-01 |
PaulMeng | small fix for naming |
commit | commitdiff | tree |
| 2016-03-01 |
PaulMeng | fixed product rules |
commit | commitdiff | tree |
| 2016-03-01 |
PaulMeng | adapted the solver to accept sets of built-in types... |
commit | commitdiff | tree |
| 2016-02-29 |
PaulMeng | Added more benchmarks |
commit | commitdiff | tree |
| 2016-02-28 |
PaulMeng | implemented a basic solving procedure for finite relati... |
commit | commitdiff | tree |
| 2016-02-17 |
PaulMeng | added rules for join and transpose operators |
commit | commitdiff | tree |
| 2016-02-15 |
PaulMeng | Merge remote-tracking branch 'origin/master' |
commit | commitdiff | tree |
| 2016-02-15 |
PaulMeng | extended smt parser for the finite relations |
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 |
PaulMeng | - extend cvc4 frontend parser to accept relational... |
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 |
| 2015-12-31 |
Clark Barrett | Modified tear-down-incremental option to take an intege... |
commit | commitdiff | tree |
| 2015-12-30 |
Tim King | Shuffling around public vs. private headers |
commit | commitdiff | tree |
| 2015-12-29 |
Tim King | Adding a missing header include for cvc4_assert.h in... |
commit | commitdiff | tree |
| 2015-12-27 |
Clark Barrett | Merged my changes from experimental branch (new array... |
commit | commitdiff | tree |
| 2015-12-24 |
Tim King | Changing the attribute on the forward declaration of... |
commit | commitdiff | tree |
| 2015-12-24 |
Tim King | Adding a missing return on the new ArrayStoreAll::opera... |
commit | commitdiff | tree |
| 2015-12-24 |
Tim King | Miscellaneous fixes |
commit | commitdiff | tree |
| 2015-12-23 |
Clark Barrett | Enabled array propagation during lemma propagation... |
commit | commitdiff | tree |
| 2015-12-23 |
Clark Barrett | Added extract.cpp example |
commit | commitdiff | tree |
| 2015-12-22 |
ajreynol | Bug fix uf-ss-totality. |
commit | commitdiff | tree |
| 2015-12-22 |
ajreynol | Always split on constructor types for datatypes involvi... |
commit | commitdiff | tree |
| 2015-12-22 |
ajreynol | Bug fix for cbqi, do not use model values for terms... |
commit | commitdiff | tree |
| 2015-12-19 |
Tim King | Modifying emptyset.h and sexpr. Adding SetLanguage. |
commit | commitdiff | tree |
| 2015-12-17 |
ajreynol | Minor |
commit | commitdiff | tree |
| 2015-12-16 |
Tim King | Removing the Record iterator from the swig interface... |
commit | commitdiff | tree |
| 2015-12-16 |
ajreynol | Work on purification for quantifiers, minor updates. |
commit | commitdiff | tree |
| 2015-12-15 |
Tim King | Breaking the include cycle between Record and Expr. |
commit | commitdiff | tree |
| 2015-12-15 |
Tim King | Adding destructors for CDO an CDOhash_map in the restor... |
commit | commitdiff | tree |
| 2015-12-15 |
Tim King | Removing the build cycle for predicate. |
commit | commitdiff | tree |
| 2015-12-15 |
Tim King | Moving SExpr(bool) out of the header into sexpr.cpp... |
commit | commitdiff | tree |
| next |
projects / cvc5.git / shortlog