From 826f583ee14b922f39666dc827a5624fff753724 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Thu, 25 Feb 2010 07:48:03 +0000 Subject: * src/expr/node.h: add a copy constructor. Apparently GCC doesn't recognize an instantiation of the join conversion/copy ctor with ref_count = ref_count_1 as a copy constructor. Problems with reference counts ensue. * src/theory/theory.h, src/theory/theory.cpp: Theory base implementation work. Changed from continuation-style theory calls to having an data member for the output channel. registerTerm() and preRegisterTerm() work. * src/theory/output_channel.h, src/theory/theory.h, src/theory/theory.cpp, src/theory/uf/theory_uf.h, src/theory/uf/theory_uf.cpp: merged ExplainOutputChannel into OutputChannel. * test/unit/expr/node_black.h: remove testPlusNode(), testUMinusNode(), testMultNode(). * src/expr/attribute.h: new facilities ManagedAttribute<> and CDAttribute<>, and add new template parameters to Attribute<>. Make CDAttribute<>s work with context manager. * src/expr/attribute.h, src/expr/node_manager.h: VarNameAttr and TypeAttr are now "owned" (defined) by the NodeManager. The AttributeManager knows nothing of specific attributes, it just as all the code for dealing generically with attributes. * test/unit/expr/node_white.h: test new attribute facilities. * src/expr/soft_node.h: removed: We now have TNode, so SoftNode goes away. * src/theory/Makefile.am: fixed improper linking of theories * src/theory/theory_engine.h: some implementation work (mainly stubs for now, just to make sure TheoryUF can be instantiated properly, etc.) * src/expr/node_value.cpp, src/expr/node_value.h: move a number of function implementations to the header and make them inline * src/expr/node_manager.cpp, src/expr/node_manager.h: move a number of function implementations to the header and make them inline * src/theory/theoryof_table_prologue.h, src/theory/theoryof_table_epilogue.h, src/theory/mktheoryof, src/theory/Makefile.am: make the theoryOf() table from kinds and implement TheoryEngine::theoryOf(). * src/theory/arith/Makefile, src/theory/bool/Makefile: generated these stub Makefiles (with contrib/addsourcedir) as per policy * src/theory/arith, src/theory/bool [directory properties]: add .deps to svn:ignore. * contrib/configure-in-place: permit configuring "in-place" in the source directory. * contrib/get-authors, contrib/dimacs_to_smt.pl, contrib/update-copyright.pl, contrib/get-authors, contrib/addsourcedir, src/expr/mkkind: copyright notice * src/expr/node_manager.h, src/expr/node_builder.h, src/prop/prop_engine.h, src/prop/prop_engine.cpp, src/theory/theory_engine.h, src/smt/smt_engine.h, src/smt/smt_engine.cpp, src/theory/output_channel.h: turn "const Node&"-typed formal parameters into "TNode" * src/theory/bool, src/theory/booleans: "bool" directory renamed "booleans" to avoid keyword clash on containing namespace * src/theory/booleans/theory_def.h, src/theory/uf/theory_def.h, src/theory/arith/theory_def.h: "define" a theory simply (for automatic theoryOf() generator). * src/Makefile.am: build theory subdirectory before prop, smt, etc. so that src/theory/theoryof_table.h header gets generated before it's needed * src/expr/node_prologue.h, src/expr/node_middle.h: move "Kind" into a separate CVC4::kind namespace to avoid its contents from cluttering the CVC4 root namespace. Import the symbol "Kind" into the CVC4 namespace but not the enum values. * src/expr/node_manager.h, src/expr/node.h, src/expr/node_value.h, src/expr/node_value.cpp, src/expr/expr.cpp, src/theory/uf/theory_uf.cpp, src/prop/cnf_stream.cpp, src/parser/smt/smt_parser.g, src/parser/cvc/cvc_parser.g, src/parser/antlr_parser.cpp, test/unit/expr/node_white.h, test/unit/expr/node_black.h, test/unit/expr/kind_black.h, test/unit/expr/node_builder_black.h: update for having moved Kind into CVC4::kind. * src/parser/parser.cpp: added file-does-not-exist check (was failing silently). --- src/theory/booleans/Makefile | 4 ++++ src/theory/booleans/Makefile.am | 12 ++++++++++++ src/theory/booleans/kinds | 8 ++++++++ src/theory/booleans/theory_bool.h | 24 ++++++++++++++++++++++++ src/theory/booleans/theory_def.h | 9 +++++++++ 5 files changed, 57 insertions(+) create mode 100644 src/theory/booleans/Makefile create mode 100644 src/theory/booleans/Makefile.am create mode 100644 src/theory/booleans/kinds create mode 100644 src/theory/booleans/theory_bool.h create mode 100644 src/theory/booleans/theory_def.h (limited to 'src/theory/booleans') diff --git a/src/theory/booleans/Makefile b/src/theory/booleans/Makefile new file mode 100644 index 000000000..a74a72d83 --- /dev/null +++ b/src/theory/booleans/Makefile @@ -0,0 +1,4 @@ +topdir = ../../.. +srcdir = src/theory/bool + +include $(topdir)/Makefile.subdir diff --git a/src/theory/booleans/Makefile.am b/src/theory/booleans/Makefile.am new file mode 100644 index 000000000..cbdf13add --- /dev/null +++ b/src/theory/booleans/Makefile.am @@ -0,0 +1,12 @@ +AM_CPPFLAGS = \ + -D__BUILDING_CVC4LIB \ + -I@srcdir@/../../include -I@srcdir@/../.. +AM_CXXFLAGS = -Wall -fvisibility=hidden + +noinst_LTLIBRARIES = libbooleans.la + +libbooleans_la_SOURCES = \ + theory_def.h \ + theory_bool.h + +EXTRA_DIST = kinds diff --git a/src/theory/booleans/kinds b/src/theory/booleans/kinds new file mode 100644 index 000000000..7f1267383 --- /dev/null +++ b/src/theory/booleans/kinds @@ -0,0 +1,8 @@ +FALSE +TRUE +NOT +AND +IFF +IMPLIES +OR +XOR diff --git a/src/theory/booleans/theory_bool.h b/src/theory/booleans/theory_bool.h new file mode 100644 index 000000000..26e5a69fb --- /dev/null +++ b/src/theory/booleans/theory_bool.h @@ -0,0 +1,24 @@ +#include "theory/theory.h" +#include "context/context.h" + +namespace CVC4 { +namespace theory { +namespace booleans { + +class TheoryBool : public TheoryImpl { +public: + TheoryBool(context::Context* c, OutputChannel& out) : + TheoryImpl(c, out) { + } + + void preRegisterTerm(TNode n) { Unimplemented(); } + void registerTerm(TNode n) { Unimplemented(); } + void check(Effort e) { Unimplemented(); } + void propagate(Effort e) { Unimplemented(); } + void explain(TNode n, Effort e) { Unimplemented(); } +}; + +} +} +} + diff --git a/src/theory/booleans/theory_def.h b/src/theory/booleans/theory_def.h new file mode 100644 index 000000000..37aacb353 --- /dev/null +++ b/src/theory/booleans/theory_def.h @@ -0,0 +1,9 @@ +#include "theory/booleans/theory_bool.h" + +namespace CVC4 { + namespace theory { + namespace booleans { + typedef TheoryBool TheoryBOOLEANS; + } + } +} -- cgit v1.2.3