From 663a6edef6b65d400e2d97dc9c8276da3d3cb0b1 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Fri, 19 Nov 2010 01:37:55 +0000 Subject: Merge from ufprop branch, including: * Theory::staticLearning() for statically adding new T-stuff before normal preprocessing. UF's staticLearning() does transitivity of equality/iff, solving the diamonds. * more aggressive T-propagation for UF * new KEEP_STATISTIC macro to hide Theories from having to register/deregister statistics (and also has the advantage of keeping the statistic type, field name, and the 'tag' used to output the statistic in the same place---instead of scattered in the theory definition and constructor initializer list. See documentation for KEEP_STATISTIC in src/util/stats.h for more of an explanation). * more statistics for UF * restart notifications from SAT (through TheoryEngine) via Theory::notifyRestart() * StackingMap and UnionFind unit tests * build fixes/adjustments * code cleanup; minor other improvements --- src/theory/uf/Makefile.am | 4 ++++ 1 file changed, 4 insertions(+) (limited to 'src/theory/uf/Makefile.am') diff --git a/src/theory/uf/Makefile.am b/src/theory/uf/Makefile.am index 85b41bdbe..04fe533ae 100644 --- a/src/theory/uf/Makefile.am +++ b/src/theory/uf/Makefile.am @@ -5,6 +5,10 @@ AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN) noinst_LTLIBRARIES = libuf.la +# force automake to link using g++ +nodist_EXTRA_libuf_la_SOURCES = \ + dummy.cpp + libuf_la_SOURCES = \ theory_uf.h \ theory_uf_type_rules.h -- cgit v1.2.3