summaryrefslogtreecommitdiff
path: root/src
AgeCommit message (Collapse)Author
2010-02-01Fixing the CVC grammar for parsing Boolean expressions. All the ↵Dejan Jovanović
associativity stufff is now in the grammar. All the parser tests pass now.
2010-02-01fix node manager code (bugzilla #15, comment #2) in case where there's a ↵Morgan Deters
hash collision for distinct objects
2010-01-30cnf conversion (variable-introducing), cleanups, fixes to minisat calling ↵Morgan Deters
for multiple-query cases
2010-01-29fixing the last context build problem, it compiles nowDejan Jovanović
2010-01-29one more bugClark Barrett
2010-01-29Fixed compile errorsClark Barrett
2010-01-29Adding Makefile.in to svn:ignoreChristopher L. Conway
2010-01-29Fixing boolean operator precedencesChristopher L. Conway
2010-01-29Update of context moduleClark Barrett
2010-01-29fixed CNF conversion, and more modular; CNF conversion command line option; ↵Morgan Deters
various cleanups; renamed numChildren() to getNumChildren() and added it to NodeBuilder interface; fancier, non-exponential CNF conversion with variable introduction is still buggy (?)
2010-01-28Removing Makefile.in'sChristopher L. Conway
2010-01-26cnf conversionMorgan Deters
2010-01-26fixes to build structure, util classes, lots of fixes to Node and ↵Morgan Deters
NodeBuilder. outstanding SEGVs fixed
2010-01-25minor fixes to scoped-context node managerMorgan Deters
2010-01-25scoped node managersMorgan Deters
2010-01-19minor changes to TheoryMorgan Deters
2009-12-18More fixes fot the parser tests.Dejan Jovanović
2009-12-18Changing some deatils on the parser. Now we know we are done if command is ↵Dejan Jovanović
null, or expression is null.
2009-12-18More fixesDejan Jovanović
2009-12-18numerous fixes to nodes; more comingMorgan Deters
2009-12-18more build system fix-upsMorgan Deters
2009-12-18Lots of parser changes to make Chris happy. Yet more to come later. Dejan Jovanović
2009-12-17more build system fix-upsMorgan Deters
2009-12-17update-copyright.pl now retrieves and incorporates author information from ↵Morgan Deters
repository history; re-ran update-copyright.pl; cleaned up some things with make
2009-12-17Adding more parser testsChristopher L. Conway
2009-12-17coding standard fix on SmtEngine; fix recursive makeMorgan Deters
2009-12-17CvcParserBlack and supporting Makefile changesChristopher L. Conway
2009-12-17+ test infrastructure fixesMorgan Deters
+ regenerate configure script + add CVC4::Message output class + add some IllegalArgument() assertion things + rename NodeManager::mkExpr() to mkNode()
2009-12-17addressed some concerns raised by Clark in bug #6 (code review of driver code)Morgan Deters
2009-12-17Minor changes from code reviewClark Barrett
2009-12-17build system cleanup; test system separation into white-box, black-box, and ↵Morgan Deters
public tests
2009-12-17support nonstandard, unconfigured builds (e.g., "./configure debug" followed ↵Morgan Deters
by "make production ASSERTIONS=1")
2009-12-16+ refactoring fixes for expr package based on code review (see bug #4)Morgan Deters
+ minor autogen/configure fixes for old versions of autotools
2009-12-16Small refactoring changes for the expr package.Tim King
2009-12-16Spelling correction in commentsChristopher L. Conway
2009-12-16Fixes to the build system:Morgan Deters
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
2009-12-15Minor changes to parser files from code review.Christopher L. Conway
2009-12-15Added context_mm (haven't tested compilation yet...)Clark Barrett
2009-12-15minor: fixing typosMorgan Deters
2009-12-11Extracted the public Expr and ExprManager interface to encapsulate the ↵Dejan Jovanović
optimized expressions and the internal expression manager.
2009-12-11build fixes, configuration simplificationsMorgan Deters
2009-12-10killing expr into node...Dejan Jovanović
2009-12-10cleanups, assert work, add a stubbed uf theory, fix driverMorgan Deters
2009-12-09some fixes and organizational adjustments to assert code, parsers/lexers, ↵Morgan Deters
and build process
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-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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback