cvc5.git - CVC4 is an efficient open-source automatic theorem prover for satisfiability modulo theories (SMT) problems.

Age	Commit message (Collapse)	Author
2010-04-06	* Add some protected ContextObj accessors for ContextObj-derived classes:	Morgan Deters
	+ Context* getContext() -- gets the context + ContextMemoryManager* getCMM() -- gets the CMM + int getLevel() -- the scope level of the ContextObj's most recent update + bool isCurrent() -- true iff the most recent update is the current top level In particular, the ContextObj::getCMM() call cleans up by TheoryUF's ECData::addPredecessor() function substantially (re: code review bug #64). * Fix serious bugs in context operations that corrupted the ContextObj linked lists. Closes bug #85. * Identified a bug in the way objects of the "Link" class are allocated; see bug #96. * Re-enable context white-box tests that ensure proper links in linked lists. Closes bug #86. * Re-enable CDMap<>::emptyTrash(). Closes bug #87. * Add a tracing option (-t foo or --trace foo) to the driver to enable Trace("foo") output stream. -d foo implies -t foo. * Minor clean-up of some TheoryUF code; addition of some documentation (re: code review bug #64). * Address some things that caused Doxygen discomfort. * Address an issue raised in NodeManager's code review (bug #65). * Remove an inaccurate comment in Attribute code (re: code review bug #61).
2010-04-05	Minor refactorings, in response to code review (Bug #73)	Christopher L. Conway

2010-04-04	Recommit revision 365 (undoing revision 375, which reverted revision 365).	Morgan Deters
	Fix the case in NodeBuilderBlack that triggered bug #82. (Fixes bug #82.) This also fixes regression failures from this morning (2010 Apr 4), in the optimized builds, for which a fix was included in 365 and reverted in 375. They looked like this: In ExprBlack::testGetConst: /usr/local/share/cvc4/src/cvc4-2010-04-04/builds/x86_64-unknown-linux-gnu/production/../../../test/unit/expr/expr_black.h:377: Error: Expected (a->getConst<Kind>()) to throw (IllegalArgumentException) but it didn't throw /usr/local/share/cvc4/src/cvc4-2010-04-04/builds/x86_64-unknown-linux-gnu/production/../../../test/unit/expr/expr_black.h:378: Error: Expected (b->getConst<Kind>()) to throw (IllegalArgumentException) but it didn't throw [etc..]
2010-04-03	Reverting r365	Christopher L. Conway

2010-04-01	Changing min/maxArity to use metakind info.	Christopher L. Conway

2010-04-01	* Minor code formatting stuff in src/expr/type.{h,cpp}. Concluded	Morgan Deters
	Type code review and closed bug #25. * Do assertions on Expr creation (public library interface) even when assertions are off. Also a similar check for proper kind (in public interface) when Expr::getConst<>() is called. This fixes a unit test that was failing in production builds (an exception wasn't thrown but should have been). * kind::XOR must have exactly 2 arguments, not 2-or-more.
2010-04-01	PARSER STUFF:	Morgan Deters
	* Other minor changes to the new parser to match coding guidelines, add documentation, .... * Add CFLAGS stuff to configure.ac parser Makefile.ams. This ensures that profiling, coverage, optimization, debugging, and warning level options will apply to the new parser as well (which is in C, not C++). This fixes the deprecated warning we were seeing this evening. * Now, if you have ANTLR_HOME set in your environment, you don't need to specify --with-antlr-dir to ./configure or have libantlr3c installed in standard places. --with-antlr-dir still overrides $ANTLR_HOME, and if the installation in $ANTLR_HOME is missing or doesn't work, the standard places are still tried. * Extend "silent make" to new parser stuff. * Added src/parser/bounded_token_buffer.{h,cpp} to the list of exclusions in contrib/update-copyright.pl and mention them as excluded from CVC4 copyright in COPYING. They are antlr3-derived works, covered under a BSD license. OTHER STUFF: * expr_manager.h, expr.h, expr_manager.cpp, and expr.cpp are now auto-generated by a "mkexpr" script. This provides the correct instantiations of mkConst() for public use, e.g., by the parser. * Fix doxygen documentation in expr, expr_manager.. closes bug #35 * Node::isAtomic() implemented in a better way, based on theory kinds files. Fixes bug #40. To support this, a "nonatomic_operator" command has been added. All other "parameterized" or "operator" kinds are atomic. * Added expr_black test * Remove kind::TRUE and kind::FALSE and make a new CONST_BOOLEAN kind that takes a "bool" payload; for example, to make "true" you now do nodeManager->mkConst(true). * Make new "cvc4_public.h" and "cvc4parser_public.h" headers. Private headers should include "cvc4_private.h" (resp. "cvc4parser_private.h"), which existed previously. Public headers should include the others. No one should include the autoheader #include (which has been renamed "cvc4autoconfig.h") directly, and public CVC4 headers can't access its #defines. This is to avoid us having the same distribution problem as libantlr3c. * Preliminary fixes based on Tim's code review of attributes (bug #61). This includes splitting hairy template internals into attribute_internals.h, for which another code review ticket will be opened. Bug is still outstanding, but pending further refactoring/documentation. * Some HashFcns renamed to HashStrategy to match refactoring done elsewhere (done by Chris?) earlier this week. * Simplified creation of make rules for generated files (expr.cpp, expr.h, expr_manager.cpp, expr_manager.h, theoryof_table.h, kind.h, metakind.h). * CVC4::Configuration interface and implementation split (so private stuff doesn't leak into public headers). * Some documentation/code formatting fixes. * Add required versions of autotools to autogen.sh. * src/expr/mkmetakind: fix a nonportable thing in invocation of "expr" that was causing warnings on Red Hat. * src/context/cdmap.h: add workaround to what appears to be a g++ 4.1 parsing bug.