Age | Commit message (Collapse) | Author |
|
* 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)
|
|
* 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.
|
|
correct, etc..
|
|
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.
|
|
|
|
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)
|
|
|
|
|
|
configure script differently and we get useless commits of it; fix NodeBuilder memory leak in response to Kaustubh's expr code review (bug#15)
|
|
recursive Makefile to configure.ac
|
|
symbol table
|
|
|
|
|
|
Some parts split into other bugs: 19, 20, 21.
Addressed concerns of bug 11 (util package code review).
Slight parser source file modifications: file comments, #included
headers in generated parsers/lexers
Added CVC4::Result propagation back through
MiniSat->PropEngine->SmtEngine->main(). Silenced MiniSat when
verbosity is not requested.
|
|
NodeBuilder. outstanding SEGVs fixed
|
|
|
|
|
|
by "make production ASSERTIONS=1")
|
|
|
|
Makefile.am files - remove obsolete INCLUDES, incorporate into AM_CPPFLAGS
Makefile files in src/ - support "make" under src/ (current build profile)
configure.ac - updates to fix warnings
config/antlr.m4 - updates to fix warnings
autogen.sh - updates to generate warnings from autotools; also support Macs
src/include/cvc4_config.h - guard with #ifdef
total reimplementation of NodeBuilder
ExprValue => NodeValue
context_mm.{h,cpp} - fixed numerous compile errors
|
|
|
|
|
|
found handling
|
|
expressions, output classes, and minisat
|
|
|
|
yet to be finalized, it should work as expected
|
|
* Fixed bugs in option parsing
* Simplified the main.cpp significantly (more c++ like)
* Added the null kind, expr value, and expression, with the default constructor public
* Simplified commands, we need to discuss this in the meeting (what to do with command results?)
* Removed all the lex/yacc files
* Symbol table is now a templated class, as we will have tables for variables, predicates and functions
* The ANTLR parsing infrastructure/makefiles is all in. SMT lib Boolean benchmarks should parse + giving nice error such as
Parse Error: /home/dejan/eclipse-cxx/smtlib-parser/test/test4.smt:3:16: Undeclared variable p
Parse Error: /home/dejan/eclipse-cxx/smtlib-parser/test/test2.smt:2:11: unexpected token: sa
Didn't add any unit tests as the unit testing doesn't work with the updated build system -- it doesn't know how to create directories in the corresponding build directory.
TODO:
* add the PL grammar and unit test when the testing becomes available
* with this build setup my eclipse debugger doesn't work. Might have something to do with the visibility of symbols?
* i'm getting g++ depracated warnings regarding the hash_map from the symbol table, need to figure out how to use it in a standard manner. the new <unordered_map> header is for C++0x, and the <ext/hash_map> is getting deprecation warningns... weird.
|
|
|
|
|
|
parser refuses to be built in the new separate directory structure though.
|
|
|
|
|
|
|
|
|
|
improvements
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|