Age | Commit message (Collapse) | Author |
|
|
|
|
|
state.
|
|
|
|
comments to files without them
|
|
|
|
|
|
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
|
|
|
|
* 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)
|
|
|
|
|
|
cvc4-c++-editing-mode from contrib/editing-with-emacs
|
|
Build src/expr before src/util.
Moved CVC4::Command to the expr package.
Re-quieted the "result is sat/invalid" etc. from PropEngine (this is
now done at the main driver level).
Added file-level documentation to Antlr sources
When built for debug, spin on SEGV instead of aborting. Really useful
for debugging problems that crop up only on long runs. Added
'--segv-nospin' to override this spinning so that "make check,"
nightly regressions, etc. don't hang when built with debug.
Updated src/main/about.h for 2010.
|
|
regenerated configure script
|
|
|
|
|
|
associativity stufff is now in the grammar. All the parser tests pass now.
|
|
|
|
null, or expression is null.
|
|
|