Age | Commit message (Collapse) | Author | |
---|---|---|---|
2009-12-11 | build fixes, configuration simplifications | Morgan Deters | |
2009-12-10 | killing expr into node... | Dejan Jovanović | |
2009-12-10 | cleanups, assert work, add a stubbed uf theory, fix driver | Morgan Deters | |
2009-12-09 | some fixes and organizational adjustments to assert code, parsers/lexers, ↵ | Morgan Deters | |
and build process | |||
2009-12-09 | A mess of changes in the expression manager, simple example still failing ↵ | Dejan Jovanović | |
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. | |||
2009-12-08 | final (?) fixes to parser/generated build directory modifications | Morgan Deters | |
2009-12-08 | parser build fixes | Morgan Deters | |
2009-12-08 | check in automake/libtool/autoconf-generated files; add better file not ↵ | Morgan Deters | |
found handling | |||
2009-12-08 | broken formula | Morgan Deters | |
2009-12-08 | work on propositional layer, expression builder support for large ↵ | Morgan Deters | |
expressions, output classes, and minisat | |||
2009-12-07 | fixing a few broken build-related items, adding test cases | Morgan Deters | |
2009-12-07 | big check-in of various fixes and adjustments | Morgan Deters | |
2009-12-07 | antlr parser for the cvc4 language (boolean only) | Dejan Jovanović | |
yet to be finalized, it should work as expected | |||
2009-12-06 | Big chunk of changes: | Dejan Jovanović | |
* 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. | |||
2009-12-05 | more build system work | Morgan Deters | |
2009-12-04 | more build system work | Morgan Deters | |
2009-12-04 | More changes to configure.ac to include the smt grammar directory. The ↵ | Dejan Jovanović | |
parser refuses to be built in the new separate directory structure though. | |||
2009-12-04 | Forgot to commit changes to configure.ac | Dejan Jovanović | |
2009-12-04 | Adding support for ANTLR checking in autogen.sh (config/antlr.m4). Commiting ↵ | Dejan Jovanović | |
antlr SMT grammar that should compile, but is not yet integrated. Tests of compilation and antlr crashes appreciated. | |||
2009-12-03 | Eclipse CVC4 settings (with code style) | Dejan Jovanović | |
2009-12-03 | additional build system fixes | Morgan Deters | |
2009-12-03 | first attempt at new build system | Morgan Deters | |
2009-12-03 | parsing/expr/command/result/various other fixes | Morgan Deters | |
2009-12-01 | svignore for parser and util | Dejan Jovanović | |
2009-11-28 | Added an EmptyCommand and a CommandSequence commands and changed the parser ↵ | Dejan Jovanović | |
a bit. | |||
2009-11-26 | Commands and the eclipse C++ project settings. | Dejan Jovanović | |
2009-11-26 | Enough parsing for tonight. Added: | Dejan Jovanović | |
* Everything goes through the ParserState instead of coding in lex/yacc files * Bare Boolean SMT lexer/parser * Basic commands To be completed: ParserState method implementations, parser.h/parser.cpp, make it compile and run... | |||
2009-11-25 | additional work on parser hookup, configuration + build | Morgan Deters | |
2009-11-24 | Missed file: symbol_table.h | Christopher L. Conway | |
2009-11-24 | Parser should be complete for Booleans | Christopher L. Conway | |
2009-11-24 | oops, missed a file | Morgan Deters | |
2009-11-24 | various fixes and updates to use and support parser | Morgan Deters | |
2009-11-24 | Stubbing commands | Christopher L. Conway | |
2009-11-24 | Stubbing commandsmake | Christopher L. Conway | |
2009-11-24 | Parser for boolean exprs (no commands) | Christopher L. Conway | |
2009-11-24 | Partial parser for booleans | Christopher L. Conway | |
2009-11-24 | configure option adjustments as per 11/24 meeting; various fixes and ↵ | Morgan Deters | |
improvements | |||
2009-11-23 | fixups, file comments | Morgan Deters | |
2009-11-20 | fixes to build/test system | Morgan Deters | |
2009-11-20 | fix to expr #includes; better test-environment configuration | Morgan Deters | |
2009-11-19 | testing framework, configure fixes, incorporations from meeting, continued work | Morgan Deters | |
2009-11-18 | work on exprs, driver, util | Morgan Deters | |
2009-11-17 | ignored items | Morgan Deters | |
2009-11-17 | from meeting | Morgan Deters | |
2009-11-17 | from meeting | Morgan Deters | |
2009-11-17 | from meeting | Morgan Deters | |
2009-11-17 | fixes/redesign of source layout from meeting | Morgan Deters | |
2009-11-17 | another pass | Morgan Deters | |
2009-11-17 | fixes and additions | Morgan Deters | |
2009-11-12 | minor fixes | Morgan Deters | |