Age | Commit message (Collapse) | Author | |
---|---|---|---|
2010-02-01 | Fixing 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-01 | fix node manager code (bugzilla #15, comment #2) in case where there's a ↵ | Morgan Deters | |
hash collision for distinct objects | |||
2010-01-30 | cnf conversion (variable-introducing), cleanups, fixes to minisat calling ↵ | Morgan Deters | |
for multiple-query cases | |||
2010-01-29 | fixing the last context build problem, it compiles now | Dejan Jovanović | |
2010-01-29 | one more bug | Clark Barrett | |
2010-01-29 | Fixed compile errors | Clark Barrett | |
2010-01-29 | Adding Makefile.in to svn:ignore | Christopher L. Conway | |
2010-01-29 | Fixing boolean operator precedences | Christopher L. Conway | |
2010-01-29 | Update of context module | Clark Barrett | |
2010-01-29 | fixed 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-28 | Removing Makefile.in's | Christopher L. Conway | |
2010-01-26 | cnf conversion | Morgan Deters | |
2010-01-26 | fixes to build structure, util classes, lots of fixes to Node and ↵ | Morgan Deters | |
NodeBuilder. outstanding SEGVs fixed | |||
2010-01-25 | minor fixes to scoped-context node manager | Morgan Deters | |
2010-01-25 | scoped node managers | Morgan Deters | |
2010-01-19 | minor changes to Theory | Morgan Deters | |
2009-12-18 | More fixes fot the parser tests. | Dejan Jovanović | |
2009-12-18 | Changing some deatils on the parser. Now we know we are done if command is ↵ | Dejan Jovanović | |
null, or expression is null. | |||
2009-12-18 | More fixes | Dejan Jovanović | |
2009-12-18 | numerous fixes to nodes; more coming | Morgan Deters | |
2009-12-18 | more build system fix-ups | Morgan Deters | |
2009-12-18 | Lots of parser changes to make Chris happy. Yet more to come later. | Dejan Jovanović | |
2009-12-17 | more build system fix-ups | Morgan Deters | |
2009-12-17 | update-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-17 | Adding more parser tests | Christopher L. Conway | |
2009-12-17 | coding standard fix on SmtEngine; fix recursive make | Morgan Deters | |
2009-12-17 | CvcParserBlack and supporting Makefile changes | Christopher L. Conway | |
2009-12-17 | + test infrastructure fixes | Morgan Deters | |
+ regenerate configure script + add CVC4::Message output class + add some IllegalArgument() assertion things + rename NodeManager::mkExpr() to mkNode() | |||
2009-12-17 | addressed some concerns raised by Clark in bug #6 (code review of driver code) | Morgan Deters | |
2009-12-17 | Minor changes from code review | Clark Barrett | |
2009-12-17 | build system cleanup; test system separation into white-box, black-box, and ↵ | Morgan Deters | |
public tests | |||
2009-12-17 | support 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-16 | Small refactoring changes for the expr package. | Tim King | |
2009-12-16 | Spelling correction in comments | Christopher L. Conway | |
2009-12-16 | Fixes 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-15 | Minor changes to parser files from code review. | Christopher L. Conway | |
2009-12-15 | Added context_mm (haven't tested compilation yet...) | Clark Barrett | |
2009-12-15 | minor: fixing typos | Morgan Deters | |
2009-12-11 | Extracted the public Expr and ExprManager interface to encapsulate the ↵ | Dejan Jovanović | |
optimized expressions and the internal expression manager. | |||
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 | 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 | |