summaryrefslogtreecommitdiff
path: root/src/smt/smt_engine.h
AgeCommit message (Collapse)Author
2010-02-02Switched cnf conversion to go through CnfStream.Tim King
2010-01-30cnf conversion (variable-introducing), cleanups, fixes to minisat calling ↵Morgan Deters
for multiple-query cases
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-26cnf conversionMorgan Deters
2010-01-26fixes to build structure, util classes, lots of fixes to Node and ↵Morgan Deters
NodeBuilder. outstanding SEGVs fixed
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-11Extracted the public Expr and ExprManager interface to encapsulate the ↵Dejan Jovanović
optimized expressions and the internal expression manager.
2009-12-10killing expr into node...Dejan Jovanović
2009-12-08work on propositional layer, expression builder support for large ↵Morgan Deters
expressions, output classes, and minisat
2009-12-07big check-in of various fixes and adjustmentsMorgan Deters
2009-12-03parsing/expr/command/result/various other fixesMorgan Deters
2009-11-25additional work on parser hookup, configuration + buildMorgan Deters
2009-11-24various fixes and updates to use and support parserMorgan Deters
2009-11-24configure option adjustments as per 11/24 meeting; various fixes and ↵Morgan Deters
improvements
2009-11-23fixups, file commentsMorgan Deters
2009-11-19testing framework, configure fixes, incorporations from meeting, continued workMorgan Deters
2009-11-17from meetingMorgan Deters
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback