summary |
shortlog | log |
commit |
commitdiff |
tree
first ⋅ prev ⋅ next
Morgan Deters [Tue, 8 Dec 2009 19:00:53 +0000 (19:00 +0000)]
broken formula
Morgan Deters [Tue, 8 Dec 2009 10:10:20 +0000 (10:10 +0000)]
work on propositional layer, expression builder support for large expressions, output classes, and minisat
Morgan Deters [Mon, 7 Dec 2009 23:23:33 +0000 (23:23 +0000)]
fixing a few broken build-related items, adding test cases
Morgan Deters [Mon, 7 Dec 2009 23:14:15 +0000 (23:14 +0000)]
big check-in of various fixes and adjustments
Dejan Jovanović [Mon, 7 Dec 2009 05:51:09 +0000 (05:51 +0000)]
antlr parser for the cvc4 language (boolean only)
yet to be finalized, it should work as expected
Dejan Jovanović [Sun, 6 Dec 2009 02:21:46 +0000 (02:21 +0000)]
Big chunk of changes:
* 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.
Morgan Deters [Sat, 5 Dec 2009 00:40:57 +0000 (00:40 +0000)]
more build system work
Morgan Deters [Fri, 4 Dec 2009 21:03:50 +0000 (21:03 +0000)]
more build system work
Dejan Jovanović [Fri, 4 Dec 2009 04:22:02 +0000 (04:22 +0000)]
More changes to configure.ac to include the smt grammar directory. The parser refuses to be built in the new separate directory structure though.
Dejan Jovanović [Fri, 4 Dec 2009 04:18:26 +0000 (04:18 +0000)]
Forgot to commit changes to configure.ac
Dejan Jovanović [Fri, 4 Dec 2009 04:06:54 +0000 (04:06 +0000)]
Adding support for ANTLR checking in autogen.sh (config/antlr.m4). Commiting antlr SMT grammar that should compile, but is not yet integrated. Tests of compilation and antlr crashes appreciated.
Dejan Jovanović [Thu, 3 Dec 2009 21:13:55 +0000 (21:13 +0000)]
Eclipse CVC4 settings (with code style)
Morgan Deters [Thu, 3 Dec 2009 20:19:40 +0000 (20:19 +0000)]
additional build system fixes
Morgan Deters [Thu, 3 Dec 2009 19:43:54 +0000 (19:43 +0000)]
first attempt at new build system
Morgan Deters [Thu, 3 Dec 2009 14:59:30 +0000 (14:59 +0000)]
parsing/expr/command/result/various other fixes
Dejan Jovanović [Tue, 1 Dec 2009 17:58:17 +0000 (17:58 +0000)]
svignore for parser and util
Dejan Jovanović [Sat, 28 Nov 2009 02:59:11 +0000 (02:59 +0000)]
Added an EmptyCommand and a CommandSequence commands and changed the parser a bit.
Dejan Jovanović [Thu, 26 Nov 2009 03:24:04 +0000 (03:24 +0000)]
Commands and the eclipse C++ project settings.
Dejan Jovanović [Thu, 26 Nov 2009 03:22:53 +0000 (03:22 +0000)]
Enough parsing for tonight. Added:
* 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...
Morgan Deters [Wed, 25 Nov 2009 00:42:52 +0000 (00:42 +0000)]
additional work on parser hookup, configuration + build
Christopher L. Conway [Tue, 24 Nov 2009 23:08:04 +0000 (23:08 +0000)]
Missed file: symbol_table.h
Christopher L. Conway [Tue, 24 Nov 2009 23:05:52 +0000 (23:05 +0000)]
Parser should be complete for Booleans
Morgan Deters [Tue, 24 Nov 2009 23:04:45 +0000 (23:04 +0000)]
oops, missed a file
Morgan Deters [Tue, 24 Nov 2009 22:51:35 +0000 (22:51 +0000)]
various fixes and updates to use and support parser
Christopher L. Conway [Tue, 24 Nov 2009 21:55:37 +0000 (21:55 +0000)]
Stubbing commands
Christopher L. Conway [Tue, 24 Nov 2009 21:54:09 +0000 (21:54 +0000)]
Stubbing commandsmake
Christopher L. Conway [Tue, 24 Nov 2009 21:30:50 +0000 (21:30 +0000)]
Parser for boolean exprs (no commands)
Christopher L. Conway [Tue, 24 Nov 2009 21:28:03 +0000 (21:28 +0000)]
Partial parser for booleans
Morgan Deters [Tue, 24 Nov 2009 21:03:35 +0000 (21:03 +0000)]
configure option adjustments as per 11/24 meeting; various fixes and improvements
Morgan Deters [Mon, 23 Nov 2009 16:42:12 +0000 (16:42 +0000)]
fixups, file comments
Morgan Deters [Fri, 20 Nov 2009 23:47:56 +0000 (23:47 +0000)]
fixes to build/test system
Morgan Deters [Fri, 20 Nov 2009 20:10:43 +0000 (20:10 +0000)]
fix to expr #includes; better test-environment configuration
Morgan Deters [Thu, 19 Nov 2009 22:07:01 +0000 (22:07 +0000)]
testing framework, configure fixes, incorporations from meeting, continued work
Morgan Deters [Wed, 18 Nov 2009 22:02:11 +0000 (22:02 +0000)]
work on exprs, driver, util
Morgan Deters [Tue, 17 Nov 2009 17:27:56 +0000 (17:27 +0000)]
ignored items
Morgan Deters [Tue, 17 Nov 2009 17:11:35 +0000 (17:11 +0000)]
from meeting
Morgan Deters [Tue, 17 Nov 2009 17:09:13 +0000 (17:09 +0000)]
from meeting
Morgan Deters [Tue, 17 Nov 2009 17:06:57 +0000 (17:06 +0000)]
from meeting
Morgan Deters [Tue, 17 Nov 2009 16:40:19 +0000 (16:40 +0000)]
fixes/redesign of source layout from meeting
Morgan Deters [Tue, 17 Nov 2009 08:39:27 +0000 (08:39 +0000)]
another pass
Morgan Deters [Tue, 17 Nov 2009 07:19:39 +0000 (07:19 +0000)]
fixes and additions
Morgan Deters [Thu, 12 Nov 2009 20:39:30 +0000 (20:39 +0000)]
minor fixes
Morgan Deters [Thu, 12 Nov 2009 20:38:10 +0000 (20:38 +0000)]
parser, minisat, other things..
Morgan Deters [Mon, 9 Nov 2009 21:47:30 +0000 (21:47 +0000)]
minor fixes, added contrib directory
Morgan Deters [Tue, 3 Nov 2009 03:37:08 +0000 (03:37 +0000)]
additional headers and modifications; now passes syntax check
Morgan Deters [Tue, 3 Nov 2009 03:07:58 +0000 (03:07 +0000)]
additional headers
Morgan Deters [Tue, 3 Nov 2009 00:31:47 +0000 (00:31 +0000)]
commit of project structure including autotools support
Morgan Deters [Sat, 26 Sep 2009 20:35:51 +0000 (20:35 +0000)]
Initial setup of the cvc4 repository