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). --- contrib/get-authors | 1 + 1 file changed, 1 insertion(+) (limited to 'contrib/get-authors') diff --git a/contrib/get-authors b/contrib/get-authors index 40aaf6a6d..dbe878d6b 100755 --- a/contrib/get-authors +++ b/contrib/get-authors @@ -2,6 +2,7 @@ # # get-authors # Morgan Deters for CVC4 +# Copyright (c) 2009, 2010 The CVC4 Project # # usage: get-authors [ files... ] # -- cgit v1.2.3