| Age | Commit message (Collapse) | Author |
|---|
|
|
|
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
|
|
|
|
optimized expressions and the internal expression manager.
|
|
|
|
|
|
|
|
due to some problems in the prop_engine
* default null expr and expr value and reorganisation/rewrite of some methods
* fixed some bugs
* expressions should always be passed as const Expr& to methods, otherwise copy constructors are called
Problematic code:
* Expr class has a bunch of methods that return Exprs, such as a.andExpr(b). None of these know what is their expression manager. We should
(a) Not allow this, all expression construction should go through the ExprBuilder or directly thorugh the expression manager
(b) Allow this, as it is now, but the have the default expression manager be setup in every entry into the smt solver + these construction methods shouldn't be available to the user (oterwise a mess ensues)
* We have to decide how to construct ExprBuilders:
(a) constructing ExprBuilders with em = ExprBuilder(e).andExpr(b) is problematic as at construction we can't know the expression manager, and the kind of em will be UNDEFINED, so when adding b we can't assume its not UNDEFINED
(b) constructing it with ExprBuilder(em) << AND << a << b or ExprBuilder(em, AND) << a << b seems like a nicer approach
I am still confused about these expression builders so we should talk about this.
|
|
found handling
|
|
expressions, output classes, and minisat
|
|
|
|
* 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.
|
|
|
|
|
|
improvements
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
