| 2012-11-12 |
Tim King | Improved error reporting for improperly using non-linea... |
commit | commitdiff | tree |
| 2012-11-12 |
Tim King | Delta is now generated in arithmetic to keep consistent... |
commit | commitdiff | tree |
| 2012-11-12 |
Liana Hadarean | changed BitVector::unsignedRem to match the behavior... |
commit | commitdiff | tree |
| 2012-11-12 |
Morgan Deters | Fix for bug 444, dealing with the placing of set-logic... |
commit | commitdiff | tree |
| 2012-11-12 |
Morgan Deters | * Fix language bindings: various issues |
commit | commitdiff | tree |
| 2012-11-12 |
Andrew Reynolds | minor bug fixes for quantifiers, added sort inference... |
commit | commitdiff | tree |
| 2012-11-11 |
Tim King | Fixes for the arithmetic normal form and rewriter to... |
commit | commitdiff | tree |
| 2012-11-10 |
Tim King | Beautifying integer_cln_imp.h |
commit | commitdiff | tree |
| 2012-11-10 |
Tim King | Fix to quantifier rewritting not being idempotent.... |
commit | commitdiff | tree |
| 2012-11-10 |
Tim King | Removing rewriter call in SmtEngine::addFormula(). |
commit | commitdiff | tree |
| 2012-11-10 |
Clark Barrett | Fixed missing \ in uflra/Makefile.ma |
commit | commitdiff | tree |
| 2012-11-10 |
Tim King | Fix for bug 439. Delta computation now includes disequa... |
commit | commitdiff | tree |
| 2012-11-10 |
Morgan Deters | Change run-regression script to *additionally* run... |
commit | commitdiff | tree |
| 2012-11-10 |
Morgan Deters | Updates to Clark's commit r4540: |
commit | commitdiff | tree |
| 2012-11-10 |
Morgan Deters | fix typo in language bindings |
commit | commitdiff | tree |
| 2012-11-10 |
Clark Barrett | Finally tracked down problems in regressions and fuzz... |
commit | commitdiff | tree |
| 2012-11-09 |
Morgan Deters | TheoryEngineModelBuilder::buildModel() is only called... |
commit | commitdiff | tree |
| 2012-11-09 |
Kshitij Bansal | export null nodes (fixes a bug in portfolio model stuff) |
commit | commitdiff | tree |
| 2012-11-09 |
Tim King | Test that breaks arithmetic model building due to diseq... |
commit | commitdiff | tree |
| 2012-11-09 |
Tim King | Arithmetic problem that fails --check-models due incomp... |
commit | commitdiff | tree |
| 2012-11-09 |
Morgan Deters | Bug-fix for a crash involving improperly-thrown excepti... |
commit | commitdiff | tree |
| 2012-11-09 |
Morgan Deters | In non-linear logics, rewrite DIVISION, INTS_DIVISION... |
commit | commitdiff | tree |
| 2012-11-09 |
Morgan Deters | another DISTCLEANFILES entry, for proper "make distclea... |
commit | commitdiff | tree |
| 2012-11-09 |
Clark Barrett | Fix for another model assertion failure |
commit | commitdiff | tree |
| 2012-11-08 |
Tim King | Turns on TheoryUF when non-linear arithmetic is turned... |
commit | commitdiff | tree |
| 2012-11-08 |
Morgan Deters | fix "make distcheck" |
commit | commitdiff | tree |
| 2012-11-08 |
Morgan Deters | Review of trunk r4525 (TypeNode::getBaseType()): |
commit | commitdiff | tree |
| 2012-11-08 |
Tim King | Improved support for division by zero. This adds the... |
commit | commitdiff | tree |
| 2012-11-08 |
Morgan Deters | exception fix |
commit | commitdiff | tree |
| 2012-11-08 |
Clark Barrett | Fixed two small bugs in model generation |
commit | commitdiff | tree |
| 2012-11-08 |
Clark Barrett | Added getBaseType - Morgan please check |
commit | commitdiff | tree |
| 2012-11-08 |
Andrew Reynolds | added support for parametric datatypes in smt2 parser... |
commit | commitdiff | tree |
| 2012-11-07 |
Morgan Deters | * Type ascription bug fixed (resolves bug 432), but... |
commit | commitdiff | tree |
| 2012-11-07 |
Tim King | Fix to a bug in integer mod lemmas. |
commit | commitdiff | tree |
| 2012-11-06 |
Morgan Deters | fix issue in compatibility layer that could segfault |
commit | commitdiff | tree |
| 2012-11-05 |
Tim King | Fix to the context dependent static learning code. |
commit | commitdiff | tree |
| 2012-11-05 |
Morgan Deters | fixes for replacement function library |
commit | commitdiff | tree |
| 2012-11-05 |
Morgan Deters | fixes for mac os |
commit | commitdiff | tree |
| 2012-11-05 |
Morgan Deters | fix for tarball building (fixes debian and distcheck... |
commit | commitdiff | tree |
| 2012-11-02 |
Andrew Reynolds | more minor updates to inst gen and representative selec... |
commit | commitdiff | tree |
| 2012-10-31 |
Andrew Reynolds | cleaning up some of the equality query stuff, implement... |
commit | commitdiff | tree |
| 2012-10-30 |
Dejan Jovanović | delta of a model-building failure case |
commit | commitdiff | tree |
| 2012-10-29 |
Andrew Reynolds | more updates and minor bug fixes for fmf/inst-gen quant... |
commit | commitdiff | tree |
| 2012-10-29 |
Clark Barrett | Tweak to options configuration for turning off minisat... |
commit | commitdiff | tree |
| 2012-10-29 |
Clark Barrett | Disable minisat elimination when models are on |
commit | commitdiff | tree |
| 2012-10-29 |
Clark Barrett | Disable some array optimizations when models are on |
commit | commitdiff | tree |
| 2012-10-29 |
Clark Barrett | auflia directory missing from regression summary -... |
commit | commitdiff | tree |
| 2012-10-26 |
Morgan Deters | Fix to subrange type enumerator, and its unit test... |
commit | commitdiff | tree |
| 2012-10-26 |
Andrew Reynolds | bug fix for parametric datatypes, previously datatypes... |
commit | commitdiff | tree |
| 2012-10-26 |
Tim King | Fix for bug 430. d_delta in PartialModel was never... |
commit | commitdiff | tree |
| 2012-10-26 |
Morgan Deters | build options sources into distribution tarballs (in... |
commit | commitdiff | tree |
| 2012-10-26 |
Morgan Deters | new boost.m4 makes boost-thread require boost-system... |
commit | commitdiff | tree |
| 2012-10-26 |
Morgan Deters | better parametric datatype arity checking; fixes bug 433 |
commit | commitdiff | tree |
| 2012-10-26 |
Clark Barrett | Fixed a failing datatype regression with check-models |
commit | commitdiff | tree |
| 2012-10-26 |
ACSYS | today's build system fix: sometimes examples weren... |
commit | commitdiff | tree |
| 2012-10-26 |
Andrew Reynolds | fixed bug in datatypes decision procedure enforcing... |
commit | commitdiff | tree |
| 2012-10-26 |
Clark Barrett | More bug fixes and more checks for models |
commit | commitdiff | tree |
| 2012-10-25 |
ACSYS | last build system fix for now: fix some typos affecting Mac |
commit | commitdiff | tree |
| 2012-10-25 |
Morgan Deters | extra quoting for special character |
commit | commitdiff | tree |
| 2012-10-25 |
ACSYS | more minor fixes to build system |
commit | commitdiff | tree |
| 2012-10-25 |
Morgan Deters | One of my changes to the build system yesterday broke... |
commit | commitdiff | tree |
| 2012-10-24 |
Andrew Reynolds | fixed assertion failures in efficient e-matching |
commit | commitdiff | tree |
| 2012-10-24 |
Morgan Deters | Includes many fixes to build system for Solaris (thanks... |
commit | commitdiff | tree |
| 2012-10-24 |
Tim King | Updated the ArithStaticLearner to be user context depen... |
commit | commitdiff | tree |
| 2012-10-24 |
Tim King | Fix for systems that do not have the MAP_FILE macro... |
commit | commitdiff | tree |
| 2012-10-24 |
Dejan Jovanović | fix for bug 429 |
commit | commitdiff | tree |
| 2012-10-24 |
Dejan Jovanović | two smaller random pure LRA push-pop cases that fail |
commit | commitdiff | tree |
| 2012-10-24 |
Andrew Reynolds | efficient e-matching now specific to rewrite rules |
commit | commitdiff | tree |
| 2012-10-23 |
Andrew Reynolds | more major cleanup of quantifiers code, separating... |
commit | commitdiff | tree |
| 2012-10-23 |
Andrew Reynolds | fixed problem with datatypes giving incorrect explanati... |
commit | commitdiff | tree |
| 2012-10-23 |
Clark Barrett | More debugging info, small changes to model builder |
commit | commitdiff | tree |
| 2012-10-23 |
Morgan Deters | some fixes for "make examples" and "make install-exampl... |
commit | commitdiff | tree |
| 2012-10-23 |
Clark Barrett | Added reads that were missing in collectModelInfo |
commit | commitdiff | tree |
| 2012-10-23 |
Liana Hadarean | fixed TheoryBV collectModel info to check for shared... |
commit | commitdiff | tree |
| 2012-10-23 |
Tim King | The contrib/get-antlr-3.4 script: |
commit | commitdiff | tree |
| 2012-10-23 |
Andrew Reynolds | more updates to inst gen: fixed partial instantiations... |
commit | commitdiff | tree |
| 2012-10-22 |
Morgan Deters | fix parser generation in distributed tarballs (should... |
commit | commitdiff | tree |
| 2012-10-22 |
Morgan Deters | one more incorrect #line fixed |
commit | commitdiff | tree |
| 2012-10-22 |
Morgan Deters | fix misleading comment in example |
commit | commitdiff | tree |
| 2012-10-22 |
Morgan Deters | fix installation of certain header files |
commit | commitdiff | tree |
| 2012-10-22 |
Morgan Deters | add bug 425 models regression; fix mac-build execute... |
commit | commitdiff | tree |
| 2012-10-19 |
Tim King | Fix for model building with shared terms for arithmetic. |
commit | commitdiff | tree |
| 2012-10-19 |
Kshitij Bansal | Fix problem with incremental with portfolio. Fixes... |
commit | commitdiff | tree |
| 2012-10-19 |
Liana Hadarean | BV theory model fix |
commit | commitdiff | tree |
| 2012-10-19 |
Kshitij Bansal | --fallback-sequential / --no-fallback-sequential option |
commit | commitdiff | tree |
| 2012-10-17 |
Andrew Reynolds | first working version of new inst-gen-style quantifier... |
commit | commitdiff | tree |
| 2012-10-16 |
Andrew Reynolds | more cleanup of quantifiers code |
commit | commitdiff | tree |
| 2012-10-16 |
Andrew Reynolds | first draft of new inst gen method (still with bugs... |
commit | commitdiff | tree |
| 2012-10-14 |
Morgan Deters | fix #line number warnings (sorry!) |
commit | commitdiff | tree |
| 2012-10-12 |
Clark Barrett | Added assertions and tracing code for collectModelInfo... |
commit | commitdiff | tree |
| 2012-10-12 |
Clark Barrett | Latest changes to model code |
commit | commitdiff | tree |
| 2012-10-11 |
Morgan Deters | Fix bug 421, again, and add a second, independent test... |
commit | commitdiff | tree |
| 2012-10-11 |
Morgan Deters | minor changes in wording for "cvc4 --version", and... |
commit | commitdiff | tree |
| 2012-10-11 |
Morgan Deters | Standardizing copyright notice. Touches **ALL** source... |
commit | commitdiff | tree |
| 2012-10-11 |
Morgan Deters | Fix wording on GPL in legal notices; also remove an... |
commit | commitdiff | tree |
| 2012-10-11 |
Morgan Deters | compliance note |
commit | commitdiff | tree |
| 2012-10-10 |
Morgan Deters | Abstract values for SMT-LIB. |
commit | commitdiff | tree |
| 2012-10-10 |
Andrew Reynolds | cleanup up some static data members in the quantifiers... |
commit | commitdiff | tree |
| 2012-10-10 |
Dejan Jovanović | fixing the cvc bv parser and typechecker |
commit | commitdiff | tree |
| 2012-10-09 |
Kshitij Bansal | typo |
commit | commitdiff | tree |
| next |
projects / cvc5.git / shortlog