Christopher L. Conway [Tue, 30 Mar 2010 20:51:08 +0000 (20:51 +0000)]
Removing unnecessary .gitignores
Christopher L. Conway [Tue, 30 Mar 2010 20:22:33 +0000 (20:22 +0000)]
Merging from branches/antlr3 (r246:354)
Morgan Deters [Tue, 30 Mar 2010 08:28:22 +0000 (08:28 +0000)]
again, re-enabling integer/rational tests (though they still fail to compile on 32-bit)
Morgan Deters [Tue, 30 Mar 2010 08:22:06 +0000 (08:22 +0000)]
I think this finishes off the CDMap<>/Attribute leaks
Morgan Deters [Tue, 30 Mar 2010 04:59:53 +0000 (04:59 +0000)]
fixing mistaken commit to unit test Makefile.am which removed tests
Morgan Deters [Tue, 30 Mar 2010 04:59:16 +0000 (04:59 +0000)]
Highlights of this commit are:
* add NodeManagerWhite unit test
* change kind::APPLY to kind::APPLY_UF
* better APPLY handling: operators are no longer considered children
* more efficient pool lookup; the NodeValue doesn't have to be as fully constructed for the lookup to proceed
* extend DSL for kind declarations
+ new "theory" command declares a theory and its header. theory_def.h no longer required.
+ arity enforced on operators
+ constant mapping, hashing, equality
* CONSTANT metakinds supported (via Node::getConst<T>(), for example, Node::getConst<CVC4::Rational>() gets a Rational out of a Node (assuming it is of CONST_RATIONAL kind)
* added CONST_RATIONAL and CONST_INTEGER kinds
* builtin operators (AND, OR, PLUS, etc..) returned by Node::getOperator() are now CONSTANT metakind and are created by NodeManager
* Pretty-printing of Nodes now has a depth limit settable by a stream manipulator (e.g. "cout << Node::setdepth(5) << m << endl;" prints DAG rooted at m to a depth of 5)
* getters added to Node, TNode, NodeValue, etc., for operators and metakinds
* build-time generators for kind.h, metakind.h, and theoryof_table.h headers now have a simpler design and flag errors better, and the templates (kind_template.h etc.) are easier to understand.
* DISTINCT is now a kind, and the SMT parser now passes through DISTINCT nodes instead of blowing them up into ANDs. Until theory rewriting is online, though, DISTINCTs are directly blown up into conjunctions in TheoryEngine::rewrite().
* add gmpxx detection and inclusion
* better Asserts throughout, some documentation, cleanup
Tim King [Sun, 28 Mar 2010 21:39:39 +0000 (21:39 +0000)]
Improved the documentation and testing for Rational.
Christopher L. Conway [Sun, 28 Mar 2010 19:56:59 +0000 (19:56 +0000)]
Rm'ing test file (sorry for spam)
Christopher L. Conway [Sun, 28 Mar 2010 19:51:48 +0000 (19:51 +0000)]
Adding test file
Tim King [Fri, 26 Mar 2010 22:37:12 +0000 (22:37 +0000)]
Added GMP backed Rational and Integer classes, and white box tests for them. You may have to reconfigure after this update.
Christopher L. Conway [Thu, 25 Mar 2010 20:25:04 +0000 (20:25 +0000)]
Merging let/flet rules in SMT parser
Christopher L. Conway [Thu, 25 Mar 2010 20:20:29 +0000 (20:20 +0000)]
Adding comments to NodeManager
Minor name changes for cleanup and hash function templates
Morgan Deters [Thu, 25 Mar 2010 05:03:55 +0000 (05:03 +0000)]
new domain-specific language for kinds files: permits characterization of different "kinds of kinds" (special, operator, parameterized, and constant), and permits doxygen comments on them
Clark Barrett [Tue, 23 Mar 2010 21:30:27 +0000 (21:30 +0000)]
Documented that ContextObj::destroy() only restores back to context level 0.
If there is more cleanup to do, it has to be done by the destructor.
Tim King [Tue, 23 Mar 2010 19:41:49 +0000 (19:41 +0000)]
Fixed some memory cleanup and destruction issues with ContextObj, ECData, CDList, and CDMap. Added the d_underTheShotgun field to NodeManager to keep track of which NodeValue is currently being deleted. If a Node or TNode has this node value, it can always be deleted. This avoids the need for introducing SoftNodes. Currently passes Debug and Production make check
Morgan Deters [Tue, 16 Mar 2010 20:24:37 +0000 (20:24 +0000)]
* test/unit/Makefile.am, test/unit/expr/attribute_white.h,
test/unit/expr/node_white.h: add whitebox attribute test (pulled out
attribute stuff from node_white)
* test/unit/parser/parser_black.h: fix memory leaks uncovered by
valgrind
* src/theory/interrupted.h: actually make this "lightweight" (not
derived from CVC4::Exception), as promised in my last commit
* src/theory/uf/theory_uf.h, test/unit/expr/attribute_black.h: match
the new-style cleanup function definition
* src/expr/attribute.cpp, src/expr/attribute.h: support for attribute
deletion, custom cleanup functions, clearer cleanup function
definition.
* src/expr/node_manager.h, src/expr/node_manager.cpp: reclaim
remaining zombies in dtor, rename NodeValueSet ==> "NodeValuePool",
and enable freeing of NodeValues
* src/expr/type.h, src/expr/type.cpp: reference-counting for types,
customized cleanup function for types, also code cleanup
* (various): changed "const Type*" to "Type*" (to enable
reference-counting etc. Types are still immutable.)
* src/util/output.h: add ::isOn()-- which queries whether a
Debug/Trace flag is currently on or not.
* src/smt/smt_engine.cpp, src/parser/antlr_parser.cpp,
src/expr/type.cpp, src/expr/expr_manager.cpp, various others:
minor code cleanup
Morgan Deters [Mon, 15 Mar 2010 21:10:29 +0000 (21:10 +0000)]
This checkin resolves bug #57.
* CVC4::theory::Interrupted no longer derives CVC4::Exception.
* Interrupted is only thrown if "safe" parameter is TRUE !
* UF returns one conflict (instead of waiting for Interrupted to be thrown).
* Minor build system work (quieter builds if V=0, better handling of build
profiles in configure)
Morgan Deters [Sun, 14 Mar 2010 01:55:36 +0000 (01:55 +0000)]
* test/unit/context/context_black.h: added a test for Clark's fix to bug #45.
* test/unit/context/cdlist_black.h: comment fix
Clark Barrett [Sat, 13 Mar 2010 01:57:01 +0000 (01:57 +0000)]
Fix for bug 45
Morgan Deters [Fri, 12 Mar 2010 23:52:14 +0000 (23:52 +0000)]
* src/context/cdmap.h: rename orderedIterator to iterator, do away
with old iterator (closes bug #47).
* src/context/cdset.h: implemented.
* src/expr/node_builder.h: fixed all the strict-aliasing warnings.
* Remove Node::hash() and Expr::hash() (they had been aliases for
getId()). There's now a NodeValue::internalHash(), for internal
expr package purposes only, that doesn't depend on the ID. That's
the only hashing of Nodes or Exprs.
* Automake-quiet generation of kind.h, theoryof_table.h, and CVC and
SMT parsers.
* various minor code cleanups.
Dejan Jovanović [Fri, 12 Mar 2010 23:41:12 +0000 (23:41 +0000)]
Fixing unnecessary construction of NOT nodes when generating conflict clauses and:
* adding the smallest test case (eq_diamond23.smt) that memouts in 50s
* adding the initial attributes black box test
Morgan Deters [Fri, 12 Mar 2010 19:41:04 +0000 (19:41 +0000)]
* Added shutdown() functions to SmtEngine, TheoryEngine, PropEngine,
DecisionEngine, and Theory. These are triggered from the SmtEngine
dtor before the other engines are deleted. This is important
because of potential issues with outstanding TNodes in Theory
implementations (which fail if the destruction is done in the wrong
order, in certain cases).
* Favor "FactQueueResetter" instead of clearAssertionQueues() for
resetting facts queue in Theory implementations.
* Better theory-rewriting code.
* Minor cleanups.
Morgan Deters [Thu, 11 Mar 2010 21:53:38 +0000 (21:53 +0000)]
naive rewriting to fix minisat invariant; rewrite x == x ==> TRUE
Dejan Jovanović [Thu, 11 Mar 2010 20:53:41 +0000 (20:53 +0000)]
Changing const TNode& to TNode in the CNF conversion + a new small benchmark that fail on "x != x"
Tim King [Thu, 11 Mar 2010 18:23:31 +0000 (18:23 +0000)]
Added some hand generated UF tests. Unfortunartely all of them work. Also fixed some cleanup stuff.
Dejan Jovanović [Thu, 11 Mar 2010 06:15:32 +0000 (06:15 +0000)]
Boolean variables were marked as theory literals by mistake. Fixed, should give us back the SAT performance we had before the theory stuff.
Dejan Jovanović [Thu, 11 Mar 2010 01:30:37 +0000 (01:30 +0000)]
Fix for the main bug that was bugging me -- Bug 49. The assertions queue in the theories didn't get cleared on SatSolver backtracking so there were unasserted literals being returned as part of some conflicts. Sat solver now explicitely calls in the theory engine after it backtracks in order to clear the queues (clearAssertionQueues).
Also, changed the let.smt as it used to exibit "single literal conflict" problem. The sat solve can not except conflicts similar to (x != x), these should be rewritten to false during pre-processing.
Adding 3 more small problems from the library that we can solve now to the regressions.
Morgan Deters [Wed, 10 Mar 2010 17:23:21 +0000 (17:23 +0000)]
fix production-build unit testing errors (they assumed that assertions were on)
Christopher L. Conway [Wed, 10 Mar 2010 03:58:23 +0000 (03:58 +0000)]
Lexical scoping for let-bound variables (Bug #53)
Christopher L. Conway [Wed, 10 Mar 2010 02:34:04 +0000 (02:34 +0000)]
Adding preliminary let/flet support to SMT parser (Bug #51)
Christopher L. Conway [Tue, 9 Mar 2010 23:43:35 +0000 (23:43 +0000)]
Adding support for "distinct" builtin in SMT parser
Christopher L. Conway [Tue, 9 Mar 2010 23:10:13 +0000 (23:10 +0000)]
Adding support for sort U in QF_UF.
Dejan Jovanović [Tue, 9 Mar 2010 21:56:35 +0000 (21:56 +0000)]
Adding the smallest of test cases from the smtlib.
Dejan Jovanović [Tue, 9 Mar 2010 18:06:25 +0000 (18:06 +0000)]
removing makefile.in
Tim King [Tue, 9 Mar 2010 14:38:51 +0000 (14:38 +0000)]
Fixed non-debug build problems
Dejan Jovanović [Tue, 9 Mar 2010 05:25:31 +0000 (05:25 +0000)]
one more simple test for uf
Dejan Jovanović [Tue, 9 Mar 2010 05:19:22 +0000 (05:19 +0000)]
Morgan Deters [Mon, 8 Mar 2010 23:49:47 +0000 (23:49 +0000)]
This fixes regressions at levels >= 1 which were failing
* implement zombification and garbage collection of NodeValues
(but GC not turned on yet)
* implement removal of key nodes from all attribute tables
* audit NodeBuilder and fix memory leaks and improper reference-count
management. This is in many places a re-write. Clearly documented
invariants on NodeBuilder state. (Closes Bug 38)
* created a "BackedNodeBuilder" that can be used to construct
NodeBuilders with a stack-based backing store for a size that's not
a compile-time constant.
* NodeValues no longer depend on Node for toStream()'ing
* make unit test-building "silent" with --enable-silent-rules
* (Makefile.am, Makefile.builds.in) fix top-level build system so that
"make regressN" works with unbuilt/out-of-date source trees in the
expected way.
* (various) code cleanup, documentation, formatting
Dejan Jovanović [Mon, 8 Mar 2010 23:03:48 +0000 (23:03 +0000)]
adding simple-uf to the regressions, and the code that apparently solves it
Dejan Jovanović [Mon, 8 Mar 2010 22:35:56 +0000 (22:35 +0000)]
Fixing Debug("prop") => Debug("node") typo
Tim King [Mon, 8 Mar 2010 21:29:50 +0000 (21:29 +0000)]
Improved output for theory uf
Dejan Jovanović [Mon, 8 Mar 2010 21:08:40 +0000 (21:08 +0000)]
some more sat stuff for tim: assertions now go to theory_uf
Dejan Jovanović [Mon, 8 Mar 2010 16:40:29 +0000 (16:40 +0000)]
Adding quiet output of make by default. There are two additional options to configure
--enable-silent-rules less verbose build output (undo: `make V=1')
--disable-silent-rules verbose build output (undo: `make V=0')
If you need the verbose output, you can either reconfigure with --disable-silent-rules, or do a make V=0.
Morgan Deters [Fri, 5 Mar 2010 08:26:37 +0000 (08:26 +0000)]
* public/private code untangled (smt/smt_engine.h no longer #includes
expr/node.h). This removes the warnings we had during compilation,
and heads off a number of potential linking errors due to improper
inlining of private (library-only) stuff in client (out-of-library)
code.
* "configure" now takes some options as part of a "bare-option" build
type (e.g., "./configure debug-coverage" or "./configure production-muzzle").
* split cdo.h, cdlist.h, cdmap.h, and cdset.h from context.h
* split cdlist_black unit test from context_black
* implement CDMap<>.
* give ExprManagers ownership of the context (and have SmtEngine share
that one)
* fix main driver to properly report file-not-found
* fix MemoryMappedInputBuffer class to report reasons for
"errno"-returned system errors
* src/expr/attribute.h: context-dependent attribute kinds now
supported
* test/unit/expr/node_white.h: context-dependent attribute tests
* src/prop/cnf_conversion.h and associated parts of src/util/options.h
and src/main/getopt.cpp: obsolete command-line option, removed.
* src/util/Assert.h: assertions are now somewhat more useful (in debug
builds, anyway) during stack unwinding.
* test/unit/theory/theory_black.h: test context-dependent behavior of
registerTerm() attribute for theories
* src/expr/node_builder.h: formatting, fixes for arithmetic
convenience node builders, check memory allocations
* test/unit/expr/node_builder_black.h: add tessts for addition,
subtraction, unary minus, and multiplication convenience node
builders
* src/expr/attribute.h: more comments
* (various) code formatting, comment cleanup, added throws specifier
to some destructors
* contrib/code-checker: prototype perl script to test (some) code policy
* contrib/indent-settings: command line for GNU indent to indent using
CVC4 style (sort of; this is a work in progress)
* COPYING: legal stuff
* DESIGN_QUESTIONS: obsolete, removed
Tim King [Thu, 4 Mar 2010 20:10:46 +0000 (20:10 +0000)]
Committing a bug fix from Dejan. This resolves an issue with restoring ECData.
Dejan Jovanović [Thu, 4 Mar 2010 18:45:15 +0000 (18:45 +0000)]
Adding phase-caching to minisat.
(A Lightweight Component Caching Scheme for Satisfiability Solvers <http://www.springerlink.com/content/y802q03263x84159/>)
Dejan Jovanović [Wed, 3 Mar 2010 23:39:43 +0000 (23:39 +0000)]
Some SAT stuff, not doing anything special yet, just to keep it in sync.
Morgan Deters [Tue, 2 Mar 2010 20:33:26 +0000 (20:33 +0000)]
* NodeBuilder work: specifically, convenience builders. "a && b && c || d && e"
(etc.) now work for Nodes a, b, c, d, e. Also refcounting fixes for
NodeBuilder in certain cases
* (various places) don't overload __gnu_cxx::hash<>, instead provide
an explicit hash function to hash_maps and hash_sets.
* add a new kind of assert, DtorAssert(), which doesn't throw
exceptions (right now it operates like a usual C assert()). For use
in destructors.
* don't import NodeValue into CVC4 namespace (leave under CVC4::expr::).
* fix some Make rule dependencies
* reformat node.h as per code formatting policy
* added Theory and NodeBuilder unit tests
Tim King [Mon, 1 Mar 2010 21:28:52 +0000 (21:28 +0000)]
Added theory black box test.
Tim King [Mon, 1 Mar 2010 20:19:48 +0000 (20:19 +0000)]
Node builder tests that targetted properly detecting and handling expections have been changed to be debug mode. (The Assert(..) calls these checks rely on get compiled out of production mode.) Production and debug mode should now both pass make check on everything.
Tim King [Mon, 1 Mar 2010 20:14:53 +0000 (20:14 +0000)]
Added some documentation to theory_uf.
Dejan Jovanović [Sun, 28 Feb 2010 00:57:25 +0000 (00:57 +0000)]
* context.h - Changed cdlist::push_back to use a new copy constructor instead of the assignment operator. This is important as Nodes, for example, check that d_nv != NULL in the assignemnt operator.
* node.h - Simplified the constructors, apparently it's ok to write ~ref_count in the template declaration. All the constructed nodes are now the ref-counted ones, i.e. eqNode() will return a ref-counted node.
Tim King [Sun, 28 Feb 2010 00:43:32 +0000 (00:43 +0000)]
TheoryUFWhite is passing. I fixed 2 errors. Unfortunately, I also changed a TNode to a Node at one point in the code. TNode failed for a completely unknown reason. I'm try to isolate the problem is a bit, but I am commiting this for now so other things can move forward.
Morgan Deters [Sat, 27 Feb 2010 23:46:38 +0000 (23:46 +0000)]
fix compile error in black parser unit test after today's change to parser code
Morgan Deters [Sat, 27 Feb 2010 23:43:24 +0000 (23:43 +0000)]
A bag of unrelated fixes to bring trunk more in-line with recent
policy discussion (no dead code, no unimplemented unit tests...), and
other fixes:
* src/expr/node_builder.h: uncomment AndNodeBuilder, OrNodeBuilder,
PlusNodeBuilder, and MultNodeBuilder. (These had been dead code for
awhile.)
* src/expr/node_value.cpp: toString() is much more reasonable now,
printing S-exprs and using variable names (instead of printing raw
pointer values). Next, we'll want to define a pretty-printing
theory interface and perhaps hook this up to that.
* test/unit/expr/node_black.h: implement testIterator(),
testToString(), and testToStream().
* test/unit/expr/node_builder_black.h: implement testIterator() and
testAppend(), and add some code to avoid the warnings on clear() for
unused NodeBuilders.
* src/expr/node_builder.h: redefine "iterator" to be over Nodes rather
than over NodeValues. Doesn't make sense to expose the underlying
NodeValues. This shouldn't affect anyone, no one was using
NodeBuilder iterators.
* fix some comments in source code
Christopher L. Conway [Sat, 27 Feb 2010 18:34:44 +0000 (18:34 +0000)]
Adding --mmap option to use memory-mapped file input, which provides a marginal improvement (<5%) on big benchmarks.
Morgan Deters [Fri, 26 Feb 2010 21:44:42 +0000 (21:44 +0000)]
* test/unit/context/context_black.h: Test CDList<>. In particular,
test behavior of grow(), which was previously very broken, fixed by
Tim earlier this afternoon.
* add the notion of a "private header". Private header files (those
not intended for distribution) should now #include "cvc4_private.h"
(or "cvc4parser_private.h" for the parser code). When not actually
building libcvc4 (resp. libcvc4parser), or associated unit tests, a
warning is emitted by the preprocessor. This should make it easier
to notice (and disentangle early) any unwanted public/private
mixing. Currently the warning identifies a couple places where we
need to fix things.
* added directory infrastructure for arrays and BV theories.
* the Theory inheritance hierarchy makes some assumptions about the
way inheritance is done. These are checked at runtime when
CVC4_ASSERTIONS is on. See src/theory/theory.h's TheoryImpl<>
definition for details.
* src/theory/booleans/theory_bool.h, src/theory/booleans/theory_def.h,
src/theory/arith/theory_arith.h, src/theory/arith/theory_def.h,
src/theory/uf/theory_uf.h, src/theory/uf/theory_def.h,
src/parser/antlr_parser.h: minor code formatting fixes as per
policy.
* src/theory/uf/theory_uf.cpp: fix for non-debug builds.
* src/util/options.h, src/util/model.h, src/util/result.h,
src/expr/type.h: make CVC4_PUBLIC.
* src/util/decision_engine.h: no longer CVC4_PUBLIC.
* src/expr/expr_manager.cpp: ExprManager::booleanType() and
ExprManager::kindType() weren't returning a value ?! Fixed.
* src/expr/expr_manager.h, src/expr/node_manager.h: ExprManager no
longer depends on NodeManager (public/private interface mixing).
ExprManagerScope is an internal implementation detail, and is moved
to node_manager.h.
* src/expr/node.h: mark gdb debug routines as "used" so that GCC
always emits code for them (even though its static analysis shows
they're unused).
Tim King [Fri, 26 Feb 2010 18:58:17 +0000 (18:58 +0000)]
TheoryUFWhite tests are added. There are also accompanying bug fixes. These currently do not pass. (See bug 39.) I modified node.h/cpp to get gdb debug printing working again
Tim King [Fri, 26 Feb 2010 18:40:08 +0000 (18:40 +0000)]
Fixed a bug in CDList reallocation. (Also corrected a couple whitespace problems.)
Dejan Jovanović [Fri, 26 Feb 2010 02:25:52 +0000 (02:25 +0000)]
Changing the hashing in attributes to what Nodes do, i.e. hash on the id of the node-value. This keeps coming up so we should rename the .hash() method in the node-value to something else. Morgan, feel free to change, but I had to go in as we were stuck on infinite parsing again.
Christopher L. Conway [Thu, 25 Feb 2010 22:32:03 +0000 (22:32 +0000)]
Adding Node::getOperator()
Removing references to ExprManager from Type, moving Type creation into NodeManager
Tim King [Thu, 25 Feb 2010 21:55:17 +0000 (21:55 +0000)]
Updated uf to reflect APPLY structure after conversation with Chris. Also corrected conflict generation to reflect this morning's discussion.
Morgan Deters [Thu, 25 Feb 2010 18:26:22 +0000 (18:26 +0000)]
* src/expr/node_builder.h: fixed some overly-aggressive refcount decrementing.
There remain memory leaks (and some over-decrementing of refcounts) that
I've identified; another commit forthcoming.
* src/expr/attribute.h: keys are now NodeValue* instead of TNode
* src/theory/output_channel.h: change OutputChannel::conflict() to the
negation of what we had before: it now takes an AND of TRUE literals
as a conflict clause rather than an OR of FALSE ones.
* src/expr/node.cpp: (non-template) CVC4::expr::debugPrint() routine
for use inside gdb
* src/expr/node.h: remove Node::debugPrint() member (now a function
instead of a member function, since Node is now a template it wasn't
being properly instantiated(?) and couldn't be called from gdb)
* src/expr/Makefile.am: add node.cpp
* src/expr/node_manager.h: code formatting
Morgan Deters [Thu, 25 Feb 2010 07:48:03 +0000 (07:48 +0000)]
* 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).
Tim King [Thu, 25 Feb 2010 01:05:40 +0000 (01:05 +0000)]
Created basic node builder and kind tests. Also fixed a couple of node builder problems.
Tim King [Wed, 24 Feb 2010 23:52:38 +0000 (23:52 +0000)]
Cleaned up and documented ecdata and theory_uf.
Tim King [Wed, 24 Feb 2010 21:08:15 +0000 (21:08 +0000)]
Committing small changes to attribute, and theory to avoid future merge problems for Moragn. Also cleaned up theory uf and ecdata, and updated both to reflect attribute. Should be close now.
Christopher L. Conway [Tue, 23 Feb 2010 17:15:44 +0000 (17:15 +0000)]
Minor optimizations to parser (use const string& for ids, keep only one binding in symtab)
Dejan Jovanović [Tue, 23 Feb 2010 00:24:21 +0000 (00:24 +0000)]
cosmetic changes, comments, and renaming of Expr related stuff to Node (leftovers from before switching to Node)
Dejan Jovanović [Mon, 22 Feb 2010 23:15:48 +0000 (23:15 +0000)]
finally works
Dejan Jovanović [Mon, 22 Feb 2010 23:01:16 +0000 (23:01 +0000)]
Merging from branch branches/Liana r241
Christopher L. Conway [Mon, 22 Feb 2010 21:28:25 +0000 (21:28 +0000)]
Switching to types-as-attributes in parser
Morgan Deters [Mon, 22 Feb 2010 20:51:01 +0000 (20:51 +0000)]
* src/expr/attribute.h: fixed an issue with "const pointer"-valued
attributes.
* src/expr/attribute.h, src/expr/node_manager.h, src/expr/node.h:
hasAttribute() and getAttribute() are now const member functions.
Morgan Deters [Mon, 22 Feb 2010 20:33:00 +0000 (20:33 +0000)]
* configure.ac: Remove doc/ from search path for Makefile.ams
* configure.ac, test/unit/Makefile.am: Resolved an issue where even
when not testing, one unit test was built.
* Re-ran contrib/update-copyright.pl on all source files to ensure
consistent and correct header comments.
* contrib/get-authors: Change definition of "minor contributor"
to >= 10% of lines (rather than strictly greater than 10% of lines)
Morgan Deters [Mon, 22 Feb 2010 19:24:43 +0000 (19:24 +0000)]
Re-committing revision 232 properly:
* Add virtual destructors to CnfStream, Theory, OutputChannel, and
ExplainOutputChannel. Safer and stops a compiler warning.
* node attributes: fix compiler warnings on 64-bit.
* Node: add asserts to make sure the current NodeManager is non-NULL
when it's needed. This can happen when public-facing functions
don't properly set the node manager, and it can look like a bug in
another part of the library. Also some code format cleanup.
* configure.ac, config/cvc4.m4: added --enable-static-binary (see
discussion on bug 33), fixed bad configure lines (bug 19), added
documentation for some things.
* config.h.in: removed; it's auto-generated.
Morgan Deters [Mon, 22 Feb 2010 19:22:56 +0000 (19:22 +0000)]
undoing improperly-committed revision 232; will re-commit to get "svn blame" correct, etc..
Cesare Tinelli [Mon, 22 Feb 2010 18:59:37 +0000 (18:59 +0000)]
* Add virtual destructors to CnfStream, Theory, OutputChannel, and
ExplainOutputChannel. Safer and stops a compiler warning.
* node attributes: fix compiler warnings on 64-bit.
* Node: add asserts to make sure the current NodeManager is non-NULL
when it's needed. This can happen when public-facing functions
don't properly set the node manager, and it can look like a bug in
another part of the library. Also some code format cleanup.
* configure.ac, config/cvc4.m4: added --enable-static-binary (see
discussion on bug 32), fixed bad configure lines (bug 19), added
documentation for some things.
* config.h.in: removed; it's auto-generated.
Dejan Jovanović [Mon, 22 Feb 2010 16:57:11 +0000 (16:57 +0000)]
Small changes to the smt-engine, removed the assertions list.
Morgan Deters [Mon, 22 Feb 2010 07:40:23 +0000 (07:40 +0000)]
resolve bug 32; public-facing interface functions in expr package must set current NodeManager
Morgan Deters [Mon, 22 Feb 2010 06:54:19 +0000 (06:54 +0000)]
fix bug 33 (statically link the "cvc4" binary); also main driver cleanup
Morgan Deters [Mon, 22 Feb 2010 01:10:58 +0000 (01:10 +0000)]
fix bug 22 (remove tracing from non-trace builds; remove all output
from muzzled builds)
add public-facing CVC4::Configuration class that gives CVC4's (static)
configuration (whether debugging is enabled, assertions, version
information, etc...)
add some whitebox tests for assertions, output classes, and new
CVC4::Configuration class
main driver now gets about() information from CVC4::Configuration.
configure.ac now more flexible at specifying major/minor/release
versions of CVC4
add --show-config option that dumps CVC4's static configuration
commented option processing strings in src/main/getopt.cpp
fixed some compilation problems for muzzled builds.
fixed some test code for non-assertion builds (where no assertions are expected)
Morgan Deters [Fri, 19 Feb 2010 23:10:02 +0000 (23:10 +0000)]
specialized implementation for boolean node attributes ("flags"): they now share memory words properly; also, implementations of some output functionality
Morgan Deters [Fri, 19 Feb 2010 20:29:58 +0000 (20:29 +0000)]
* Attribute infrastructure -- static design. Documentation is coming.
See test/unit/expr/node_white.h for use examples, including how to
define new attribute kinds.
Also:
* fixes to test infrastructure
* minor changes to code formatting throughout
* attribute tests in test/unit/expr/node_white.h
* fixes to NodeManagerScope ordering
* use NodeValue::getKind() to properly deal with UNDEFINED_KIND
(removing compiler warning)
* ExprManager: add proper NodeManagerScope to public-facing member
functions
* store variable names and types in attributes
* SoftNode is a placeholder, not a real implementation
Christopher L. Conway [Fri, 19 Feb 2010 17:36:23 +0000 (17:36 +0000)]
Changing minArity of AND/OR to 1 in SMT parser
Christopher L. Conway [Thu, 18 Feb 2010 23:24:26 +0000 (23:24 +0000)]
Adding --no-checking option to disable semantic checks in parser
Christopher L. Conway [Thu, 18 Feb 2010 21:29:17 +0000 (21:29 +0000)]
Rm'ing doc from SUBDIRS
Christopher L. Conway [Thu, 18 Feb 2010 19:53:59 +0000 (19:53 +0000)]
Adding doxygen configuration parameters and doxygen-doc Makefile target
Tim King [Wed, 17 Feb 2010 21:29:57 +0000 (21:29 +0000)]
Initial draft of TheoryUF. Should compile without problems. A decent amount of functionality is stubbed out. Still needs a bit of cleanup.
Morgan Deters [Wed, 17 Feb 2010 19:07:49 +0000 (19:07 +0000)]
fix bug 27: --with-cxxtest-dir=(relative-path) now works
Christopher L. Conway [Tue, 16 Feb 2010 19:35:34 +0000 (19:35 +0000)]
Moving parser error checking into AntlrParser
Christopher L. Conway [Tue, 16 Feb 2010 19:13:35 +0000 (19:13 +0000)]
Adding --parse-only option
Dejan Jovanović [Tue, 16 Feb 2010 18:24:00 +0000 (18:24 +0000)]
removing assertion and warning that shouldn't be there. adding initialization of kind to undefined to a default constructor.
Christopher L. Conway [Tue, 16 Feb 2010 18:08:02 +0000 (18:08 +0000)]
Removing spurious commit of configure
Christopher L. Conway [Tue, 16 Feb 2010 18:07:41 +0000 (18:07 +0000)]
Converting semantic predicates in parser to AlwaysAssertions
Dejan Jovanović [Sat, 13 Feb 2010 21:30:18 +0000 (21:30 +0000)]
simplification minisat
Dejan Jovanović [Sat, 13 Feb 2010 00:55:40 +0000 (00:55 +0000)]
Improvements to CNF conversion when already in CNF
Dejan Jovanović [Fri, 12 Feb 2010 20:30:24 +0000 (20:30 +0000)]
build fix
Dejan Jovanović [Fri, 12 Feb 2010 20:26:56 +0000 (20:26 +0000)]
Fix to compile out Debug(...) << ... statements in optimized mode. Someone please look to see if it makes sense.
Dejan Jovanović [Fri, 12 Feb 2010 01:07:22 +0000 (01:07 +0000)]
Changes to hashing that solve the xinetd boolean benchmark in 14s (from ~25min). Switched to standard hash_set, hash_map, new hash for the vector of node values (from boost), changed the hash for nodes to be over id's, all the hash values are now size_t. The parser is down from 11s to 10s on the benchmark, so most of the solve time is parsing and we need to figure this out.
Dejan Jovanović [Thu, 11 Feb 2010 21:19:48 +0000 (21:19 +0000)]
svn ignore