some fixes and organizational adjustments to assert code, parsers/lexers, and build process

4 files changed, 64 insertions, 4 deletions

diff --git a/src/prop/Makefile.am b/src/prop/Makefile.am
index 4071197ad..715e79d16 100644
--- a/src/prop/Makefile.am
+++ b/src/prop/Makefile.am
@@ -5,6 +5,8 @@ AM_CPPFLAGS = -D__BUILDING_CVC4LIB
 noinst_LTLIBRARIES = libprop.la
 
 libprop_la_SOURCES = \
-	prop_engine.cpp
+	prop_engine.cpp \
+	prop_engine.h \
+	sat.h
 
 SUBDIRS = minisat
diff --git a/src/prop/Makefile.in b/src/prop/Makefile.in
index 1bfd4d706..5fb636c23 100644
--- a/src/prop/Makefile.in
+++ b/src/prop/Makefile.in
@@ -67,6 +67,15 @@ CXXLD = $(CXX)
 CXXLINK = $(LIBTOOL) --tag=CXX $(AM_LIBTOOLFLAGS) $(LIBTOOLFLAGS) \
 	--mode=link $(CXXLD) $(AM_CXXFLAGS) $(CXXFLAGS) $(AM_LDFLAGS) \
 	$(LDFLAGS) -o $@
+COMPILE = $(CC) $(DEFS) $(DEFAULT_INCLUDES) $(INCLUDES) $(AM_CPPFLAGS) \
+	$(CPPFLAGS) $(AM_CFLAGS) $(CFLAGS)
+LTCOMPILE = $(LIBTOOL) --tag=CC $(AM_LIBTOOLFLAGS) $(LIBTOOLFLAGS) \
+	--mode=compile $(CC) $(DEFS) $(DEFAULT_INCLUDES) $(INCLUDES) \
+	$(AM_CPPFLAGS) $(CPPFLAGS) $(AM_CFLAGS) $(CFLAGS)
+CCLD = $(CC)
+LINK = $(LIBTOOL) --tag=CC $(AM_LIBTOOLFLAGS) $(LIBTOOLFLAGS) \
+	--mode=link $(CCLD) $(AM_CFLAGS) $(CFLAGS) $(AM_LDFLAGS) \
+	$(LDFLAGS) -o $@
 SOURCES = $(libprop_la_SOURCES)
 DIST_SOURCES = $(libprop_la_SOURCES)
 RECURSIVE_TARGETS = all-recursive check-recursive dvi-recursive \
@@ -249,7 +258,9 @@ AM_CXXFLAGS = -Wall -fvisibility=hidden
 AM_CPPFLAGS = -D__BUILDING_CVC4LIB
 noinst_LTLIBRARIES = libprop.la
 libprop_la_SOURCES = \
-	prop_engine.cpp
+	prop_engine.cpp \
+	prop_engine.h \
+	sat.h
 
 SUBDIRS = minisat
 all: all-recursive
diff --git a/src/prop/minisat/Makefile.am b/src/prop/minisat/Makefile.am
index f2716ff56..cef9a4c1e 100644
--- a/src/prop/minisat/Makefile.am
+++ b/src/prop/minisat/Makefile.am
@@ -5,4 +5,23 @@ AM_CPPFLAGS = -D__BUILDING_CVC4LIB
 noinst_LTLIBRARIES = libminisat.la
 libminisat_la_SOURCES = \
 	core/Solver.C \
-	simp/SimpSolver.C
+	core/Solver.h \
+	core/SolverTypes.h \
+	simp/SimpSolver.C \
+	simp/SimpSolver.h
+
+EXTRA_DIST = \
+	core/Main.C \
+	core/Makefile \
+	simp/Main.C \
+	simp/Makefile \
+	README \
+	LICENSE \
+	mtl/Heap.h \
+	mtl/Map.h \
+	mtl/Queue.h \
+	mtl/Alg.h \
+	mtl/Sort.h \
+	mtl/BasicHeap.h \
+	mtl/BoxedVec.h \
+	mtl/template.mk
diff --git a/src/prop/minisat/Makefile.in b/src/prop/minisat/Makefile.in
index fe890e46a..646389c80 100644
--- a/src/prop/minisat/Makefile.in
+++ b/src/prop/minisat/Makefile.in
@@ -67,6 +67,15 @@ CXXLD = $(CXX)
 CXXLINK = $(LIBTOOL) --tag=CXX $(AM_LIBTOOLFLAGS) $(LIBTOOLFLAGS) \
 	--mode=link $(CXXLD) $(AM_CXXFLAGS) $(CXXFLAGS) $(AM_LDFLAGS) \
 	$(LDFLAGS) -o $@
+COMPILE = $(CC) $(DEFS) $(DEFAULT_INCLUDES) $(INCLUDES) $(AM_CPPFLAGS) \
+	$(CPPFLAGS) $(AM_CFLAGS) $(CFLAGS)
+LTCOMPILE = $(LIBTOOL) --tag=CC $(AM_LIBTOOLFLAGS) $(LIBTOOLFLAGS) \
+	--mode=compile $(CC) $(DEFS) $(DEFAULT_INCLUDES) $(INCLUDES) \
+	$(AM_CPPFLAGS) $(CPPFLAGS) $(AM_CFLAGS) $(CFLAGS)
+CCLD = $(CC)
+LINK = $(LIBTOOL) --tag=CC $(AM_LIBTOOLFLAGS) $(LIBTOOLFLAGS) \
+	--mode=link $(CCLD) $(AM_CFLAGS) $(CFLAGS) $(AM_LDFLAGS) \
+	$(LDFLAGS) -o $@
 SOURCES = $(libminisat_la_SOURCES)
 DIST_SOURCES = $(libminisat_la_SOURCES)
 ETAGS = etags
@@ -212,7 +221,26 @@ AM_CPPFLAGS = -D__BUILDING_CVC4LIB
 noinst_LTLIBRARIES = libminisat.la
 libminisat_la_SOURCES = \
 	core/Solver.C \
-	simp/SimpSolver.C
+	core/Solver.h \
+	core/SolverTypes.h \
+	simp/SimpSolver.C \
+	simp/SimpSolver.h
+
+EXTRA_DIST = \
+	core/Main.C \
+	core/Makefile \
+	simp/Main.C \
+	simp/Makefile \
+	README \
+	LICENSE \
+	mtl/Heap.h \
+	mtl/Map.h \
+	mtl/Queue.h \
+	mtl/Alg.h \
+	mtl/Sort.h \
+	mtl/BasicHeap.h \
+	mtl/BoxedVec.h \
+	mtl/template.mk
 
 all: all-am