Age | Commit message (Collapse) | Author | |
---|---|---|---|
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 | 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 | 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 | big check-in of various fixes and adjustments | Morgan Deters | |
2009-12-03 | parsing/expr/command/result/various other fixes | Morgan Deters | |
2009-11-25 | additional work on parser hookup, configuration + build | Morgan Deters | |
2009-11-24 | oops, missed a file | Morgan Deters | |
2009-11-24 | various fixes and updates to use and support parser | Morgan Deters | |
2009-11-24 | configure option adjustments as per 11/24 meeting; various fixes and ↵ | Morgan Deters | |
improvements | |||
2009-11-23 | fixups, file comments | Morgan Deters | |
2009-11-20 | fixes to build/test system | Morgan Deters | |
2009-11-19 | testing framework, configure fixes, incorporations from meeting, continued work | Morgan Deters | |
2009-11-17 | ignored items | Morgan Deters | |
2009-11-17 | from meeting | Morgan Deters | |