From 42c58baf0a2a96c1f3bd797d64834d02adfb9a59 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Sun, 4 Apr 2010 19:55:47 +0000 Subject: * Node::isAtomic() now looks at an "atomic" attribute of arguments instead of assuming it's atomic based on kind. Atomicity is determined at node building time. Fixes bug #81. If this is determined to make node building too slow, we can allocate another attribute "AtomicHasBeenComputed" to lazily compute atomicity. * TheoryImpl<> has gone away. Theory implementations now derive from Theory directly and share a single RegisteredAttr attribute for term registration (which shouldn't overlap: every term is "owned" by exactly one Theory). Fixes bug #79. * Additional atomicity tests in ExprBlack unit test. * More appropriate whitebox testing for attribute ID assignment (AttributeWhite unit test). * Better (and more correct) assertion checking in NodeBuilderBlack. * run-regression script now checks exit status against what's provided in "% EXIT: " gesture in .cvc input files, and stderr against "% EXPECT-ERROR: ". These can be used to support intended failures. Fixes bug #84. Also add "% EXIT: " gestures to all .cvc regressions in repository. * Solved some "control reaches end of non-void function" warnings in src/parser/bounded_token_buffer.cpp by replacing "AlwaysAssert(false)" with "Unreachable()" (which is known statically to never return normally). * Regression tests now use the cvc4 binary under builds/$(CURRENT_BUILD)/src/main instead of the one in bin/ which may not be properly installed yet at that point of the build. (Partially fixes bug #46.) * -fvisibility=hidden is now included by configure.ac instead of each Makefile.am, which will make it easier to support platforms (e.g. cygwin) that do things a different way. * TheoryUF code formatting. (re: my code review bug #64) * CDMap<> is leaking memory again, pending a fix for bug #85 in the context subsystem. (To avoid serious errors, can't free context objects.) * add ContextWhite unit test for bug #85 (though it's currently "defanged," awaiting the bugfix) * Minor documentation, other cleanup. --- src/theory/uf/Makefile.am | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) (limited to 'src/theory/uf/Makefile.am') diff --git a/src/theory/uf/Makefile.am b/src/theory/uf/Makefile.am index 156733c5b..e0aa3a1df 100644 --- a/src/theory/uf/Makefile.am +++ b/src/theory/uf/Makefile.am @@ -1,12 +1,11 @@ AM_CPPFLAGS = \ -D__BUILDING_CVC4LIB \ -I@srcdir@/../../include -I@srcdir@/../.. -AM_CXXFLAGS = -Wall -fvisibility=hidden +AM_CXXFLAGS = -Wall $(FLAG_VISIBILITY_HIDDEN) noinst_LTLIBRARIES = libuf.la libuf_la_SOURCES = \ - theory_def.h \ ecdata.h \ ecdata.cpp \ theory_uf.h \ -- cgit v1.2.3