summaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2009-12-09A 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-08final (?) fixes to parser/generated build directory modificationsMorgan Deters
2009-12-08parser build fixesMorgan Deters
2009-12-08check in automake/libtool/autoconf-generated files; add better file not ↵Morgan Deters
found handling
2009-12-08broken formulaMorgan Deters
2009-12-08work on propositional layer, expression builder support for large ↵Morgan Deters
expressions, output classes, and minisat
2009-12-07fixing a few broken build-related items, adding test casesMorgan Deters
2009-12-07big check-in of various fixes and adjustmentsMorgan Deters
2009-12-07antlr parser for the cvc4 language (boolean only)Dejan Jovanović
yet to be finalized, it should work as expected
2009-12-06Big 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-05more build system workMorgan Deters
2009-12-04more build system workMorgan Deters
2009-12-04More 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-04Forgot to commit changes to configure.acDejan Jovanović
2009-12-04Adding 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-03Eclipse CVC4 settings (with code style)Dejan Jovanović
2009-12-03additional build system fixesMorgan Deters
2009-12-03first attempt at new build systemMorgan Deters
2009-12-03parsing/expr/command/result/various other fixesMorgan Deters
2009-12-01svignore for parser and utilDejan Jovanović
2009-11-28Added an EmptyCommand and a CommandSequence commands and changed the parser ↵Dejan Jovanović
a bit.
2009-11-26Commands and the eclipse C++ project settings.Dejan Jovanović
2009-11-26Enough 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-25additional work on parser hookup, configuration + buildMorgan Deters
2009-11-24Missed file: symbol_table.hChristopher L. Conway
2009-11-24Parser should be complete for BooleansChristopher L. Conway
2009-11-24oops, missed a fileMorgan Deters
2009-11-24various fixes and updates to use and support parserMorgan Deters
2009-11-24Stubbing commandsChristopher L. Conway
2009-11-24Stubbing commandsmakeChristopher L. Conway
2009-11-24Parser for boolean exprs (no commands)Christopher L. Conway
2009-11-24Partial parser for booleansChristopher L. Conway
2009-11-24configure option adjustments as per 11/24 meeting; various fixes and ↵Morgan Deters
improvements
2009-11-23fixups, file commentsMorgan Deters
2009-11-20fixes to build/test systemMorgan Deters
2009-11-20fix to expr #includes; better test-environment configurationMorgan Deters
2009-11-19testing framework, configure fixes, incorporations from meeting, continued workMorgan Deters
2009-11-18work on exprs, driver, utilMorgan Deters
2009-11-17ignored itemsMorgan Deters
2009-11-17from meetingMorgan Deters
2009-11-17from meetingMorgan Deters
2009-11-17from meetingMorgan Deters
2009-11-17fixes/redesign of source layout from meetingMorgan Deters
2009-11-17another passMorgan Deters
2009-11-17fixes and additionsMorgan Deters
2009-11-12minor fixesMorgan Deters
2009-11-12parser, minisat, other things..Morgan Deters
2009-11-09minor fixes, added contrib directoryMorgan Deters
2009-11-03additional headers and modifications; now passes syntax checkMorgan Deters
2009-11-03additional headersMorgan Deters
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback