projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 9462ccd) | patch
* fix for Mac OS (includes some ThreadLocal stuff copied in from portfolio
authorMorgan Deters <mdeters@gmail.com>
Fri, 13 May 2011 20:42:57 +0000 (20:42 +0000)
committerMorgan Deters <mdeters@gmail.com>
Fri, 13 May 2011 20:42:57 +0000 (20:42 +0000)
commit69c9ec0e1e42f3f2f2f79d3e98398c5cd1559c66
tree4761dc1485594a7d26630b3eea7f305dde0e2766tree
parent9462ccde8b06aae3b13e271465ab74b2e312a095commit | diff
* fix for Mac OS (includes some ThreadLocal stuff copied in from portfolio
  branch)
* add Theory::isSharedTermFact() -- it currently always returns false,
  pending theory combination work
* Add "unknown" cardinalities to Cardinality class
* Fix run_regression script to handle CRLF line terminators on Macs
  (where sed is non-GNU)
* Convert CRLF line terminators in datatypes regressions to LF
17 files changed:
src/main/Makefile.am diff | blob | history
src/theory/theory.h diff | blob | history
src/util/cardinality.cpp diff | blob | history
src/util/cardinality.h diff | blob | history
src/util/tls.h.in diff | blob | history
test/regress/regress0/datatypes/typed_v10l30054.cvc diff | blob | history
test/regress/regress0/datatypes/typed_v1l80005.cvc diff | blob | history
test/regress/regress0/datatypes/typed_v2l30079.cvc diff | blob | history
test/regress/regress0/datatypes/typed_v3l20092.cvc diff | blob | history
test/regress/regress0/datatypes/typed_v5l30069.cvc diff | blob | history
test/regress/regress0/datatypes/v10l40099.cvc diff | blob | history
test/regress/regress0/datatypes/v1l20009.cvc diff | blob | history
test/regress/regress0/datatypes/v2l40025.cvc diff | blob | history
test/regress/regress0/datatypes/v3l60006.cvc diff | blob | history
test/regress/regress0/datatypes/v5l30058.cvc diff | blob | history
test/regress/run_regression diff | blob | history
test/unit/expr/type_cardinality_public.h diff | blob | history