cvc5.git
14 years agoantlr parser for the cvc4 language (boolean only)
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

14 years agoBig chunk of changes:
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.

14 years agomore build system work
Morgan Deters [Sat, 5 Dec 2009 00:40:57 +0000 (00:40 +0000)]
more build system work

14 years agomore build system work
Morgan Deters [Fri, 4 Dec 2009 21:03:50 +0000 (21:03 +0000)]
more build system work

14 years agoMore changes to configure.ac to include the smt grammar directory. The parser refuses...
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.

14 years agoForgot to commit changes to configure.ac
Dejan Jovanović [Fri, 4 Dec 2009 04:18:26 +0000 (04:18 +0000)]
Forgot to commit changes to configure.ac

14 years agoAdding support for ANTLR checking in autogen.sh (config/antlr.m4). Commiting antlr...
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.

14 years agoEclipse CVC4 settings (with code style)
Dejan Jovanović [Thu, 3 Dec 2009 21:13:55 +0000 (21:13 +0000)]
Eclipse CVC4 settings (with code style)

14 years agoadditional build system fixes
Morgan Deters [Thu, 3 Dec 2009 20:19:40 +0000 (20:19 +0000)]
additional build system fixes

14 years agofirst attempt at new build system
Morgan Deters [Thu, 3 Dec 2009 19:43:54 +0000 (19:43 +0000)]
first attempt at new build system

14 years agoparsing/expr/command/result/various other fixes
Morgan Deters [Thu, 3 Dec 2009 14:59:30 +0000 (14:59 +0000)]
parsing/expr/command/result/various other fixes

14 years agosvignore for parser and util
Dejan Jovanović [Tue, 1 Dec 2009 17:58:17 +0000 (17:58 +0000)]
svignore for parser and util

15 years agoAdded an EmptyCommand and a CommandSequence commands and changed the parser a bit.
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.

15 years agoCommands and the eclipse C++ project settings.
Dejan Jovanović [Thu, 26 Nov 2009 03:24:04 +0000 (03:24 +0000)]
Commands and the eclipse C++ project settings.

15 years agoEnough parsing for tonight. Added:
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...

15 years agoadditional work on parser hookup, configuration + build
Morgan Deters [Wed, 25 Nov 2009 00:42:52 +0000 (00:42 +0000)]
additional work on parser hookup, configuration + build

15 years agoMissed file: symbol_table.h
Christopher L. Conway [Tue, 24 Nov 2009 23:08:04 +0000 (23:08 +0000)]
Missed file: symbol_table.h

15 years agoParser should be complete for Booleans
Christopher L. Conway [Tue, 24 Nov 2009 23:05:52 +0000 (23:05 +0000)]
Parser should be complete for Booleans

15 years agooops, missed a file
Morgan Deters [Tue, 24 Nov 2009 23:04:45 +0000 (23:04 +0000)]
oops, missed a file

15 years agovarious fixes and updates to use and support parser
Morgan Deters [Tue, 24 Nov 2009 22:51:35 +0000 (22:51 +0000)]
various fixes and updates to use and support parser

15 years agoStubbing commands
Christopher L. Conway [Tue, 24 Nov 2009 21:55:37 +0000 (21:55 +0000)]
Stubbing commands

15 years agoStubbing commandsmake
Christopher L. Conway [Tue, 24 Nov 2009 21:54:09 +0000 (21:54 +0000)]
Stubbing commandsmake

15 years agoParser for boolean exprs (no commands)
Christopher L. Conway [Tue, 24 Nov 2009 21:30:50 +0000 (21:30 +0000)]
Parser for boolean exprs (no commands)

15 years agoPartial parser for booleans
Christopher L. Conway [Tue, 24 Nov 2009 21:28:03 +0000 (21:28 +0000)]
Partial parser for booleans

15 years agoconfigure option adjustments as per 11/24 meeting; various fixes and improvements
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

15 years agofixups, file comments
Morgan Deters [Mon, 23 Nov 2009 16:42:12 +0000 (16:42 +0000)]
fixups, file comments

15 years agofixes to build/test system
Morgan Deters [Fri, 20 Nov 2009 23:47:56 +0000 (23:47 +0000)]
fixes to build/test system

15 years agofix to expr #includes; better test-environment configuration
Morgan Deters [Fri, 20 Nov 2009 20:10:43 +0000 (20:10 +0000)]
fix to expr #includes; better test-environment configuration

15 years agotesting framework, configure fixes, incorporations from meeting, continued work
Morgan Deters [Thu, 19 Nov 2009 22:07:01 +0000 (22:07 +0000)]
testing framework, configure fixes, incorporations from meeting, continued work

15 years agowork on exprs, driver, util
Morgan Deters [Wed, 18 Nov 2009 22:02:11 +0000 (22:02 +0000)]
work on exprs, driver, util

15 years agoignored items
Morgan Deters [Tue, 17 Nov 2009 17:27:56 +0000 (17:27 +0000)]
ignored items

15 years agofrom meeting
Morgan Deters [Tue, 17 Nov 2009 17:11:35 +0000 (17:11 +0000)]
from meeting

15 years agofrom meeting
Morgan Deters [Tue, 17 Nov 2009 17:09:13 +0000 (17:09 +0000)]
from meeting

15 years agofrom meeting
Morgan Deters [Tue, 17 Nov 2009 17:06:57 +0000 (17:06 +0000)]
from meeting

15 years agofixes/redesign of source layout from meeting
Morgan Deters [Tue, 17 Nov 2009 16:40:19 +0000 (16:40 +0000)]
fixes/redesign of source layout from meeting

15 years agoanother pass
Morgan Deters [Tue, 17 Nov 2009 08:39:27 +0000 (08:39 +0000)]
another pass

15 years agofixes and additions
Morgan Deters [Tue, 17 Nov 2009 07:19:39 +0000 (07:19 +0000)]
fixes and additions

15 years agominor fixes
Morgan Deters [Thu, 12 Nov 2009 20:39:30 +0000 (20:39 +0000)]
minor fixes

15 years agoparser, minisat, other things..
Morgan Deters [Thu, 12 Nov 2009 20:38:10 +0000 (20:38 +0000)]
parser, minisat, other things..

15 years agominor fixes, added contrib directory
Morgan Deters [Mon, 9 Nov 2009 21:47:30 +0000 (21:47 +0000)]
minor fixes, added contrib directory

15 years agoadditional headers and modifications; now passes syntax check
Morgan Deters [Tue, 3 Nov 2009 03:37:08 +0000 (03:37 +0000)]
additional headers and modifications; now passes syntax check

15 years agoadditional headers
Morgan Deters [Tue, 3 Nov 2009 03:07:58 +0000 (03:07 +0000)]
additional headers

15 years agocommit of project structure including autotools support
Morgan Deters [Tue, 3 Nov 2009 00:31:47 +0000 (00:31 +0000)]
commit of project structure including autotools support

15 years agoInitial setup of the cvc4 repository
Morgan Deters [Sat, 26 Sep 2009 20:35:51 +0000 (20:35 +0000)]
Initial setup of the cvc4 repository