summaryrefslogtreecommitdiff
path: root/src/smt/smt_engine.h
AgeCommit message (Expand)Author
2013-04-02Regenerated copyrights: canonicalized names, no emailsMorgan Deters
2013-04-01update copyrightsMorgan Deters
2013-03-22Support for Boolean term conversion in datatypes.Morgan Deters
2013-02-20Some exception specification fixes in SmtEngine/Command infrastructureMorgan Deters
2013-01-25Fix errors and reduce warnings on clang (merge from mdeters/clang)Morgan Deters
2012-12-01Adding SmtEngine::setLogic(const char* logic) so that smt.setLogic("QF_LRA");...Tim King
2012-11-27Functions and predicates over Boolean now work with --check-models and output...Morgan Deters
2012-11-27Tuples and records merge. Resolves bug 270.Morgan Deters
2012-11-26don't include internal variables in model outputMorgan Deters
2012-11-17* Fix for bug 445 agreed to in meeting 11/13/2012: always dump in ALL_SUPPORT...Morgan Deters
2012-11-12Fix for bug 444, dealing with the placing of set-logic in dumping modes.Morgan Deters
2012-11-09Bug-fix for a crash involving improperly-thrown exceptions; also, add LogicEx...Morgan Deters
2012-10-11Standardizing copyright notice. Touches **ALL** sources, guys, sorry.. it'sMorgan Deters
2012-10-10Abstract values for SMT-LIB.Morgan Deters
2012-10-09* make Model class private (as discussed at meeting today)Morgan Deters
2012-10-05Bug-related:Morgan Deters
2012-10-05BoolExpr removed and replaced with ExprDejan Jovanović
2012-10-04Implemented array type enumerator, more fixes for modelsClark Barrett
2012-10-02* re-enable some Z3 extended commands:Morgan Deters
2012-10-01"Fix" (disable) portfolio when using quantifiersKshitij Bansal
2012-09-28Public interface review items:Morgan Deters
2012-09-24some api changesDejan Jovanović
2012-09-22Separate public-facing and internal-facing interfaces to Statistics.Morgan Deters
2012-09-19General subscriber infrastructure for NodeManager, as discussed in theMorgan Deters
2012-09-15minor interface improvements, compliance fixesMorgan Deters
2012-09-12Adding model assertions after SAT responses.Morgan Deters
2012-09-06Remove SmtEngine::getStackLevel(), which exposed implementation details and w...Morgan Deters
2012-08-31merge from fmf-devel branch. more updates to models: now with collectModelIn...Andrew Reynolds
2012-08-28Improved compatibility layer, now supports quantifiers. Also incorporatesMorgan Deters
2012-08-08Public interface review items:Morgan Deters
2012-08-06Support setting :regular-output-channel and :diagnostic-output-channel.Morgan Deters
2012-08-01add isFinished() to type enumerators (so we don't rely on exception-throwing ...Morgan Deters
2012-08-01a couple fixes to SmtEngine::setOption(). thanks Andy for the report!Morgan Deters
2012-08-01fix for the SmtEngine::beforeSearch() option predicateMorgan Deters
2012-07-31Options merge. This commit:Morgan Deters
2012-07-17SMT-LIBv2 compliance updates:Morgan Deters
2012-07-16Support for having two SmtEngines with the same ExprManager.Morgan Deters
2012-07-12merged fmf-devel branch, includes support for SMT2 command get-value and (ext...Andrew Reynolds
2012-06-14This commit:Kshitij Bansal
2012-06-12Moved some things around in the preprocessor. Now theory preprocessing getsClark Barrett
2012-06-12cleanup of exit mechanism when decisionEngine is on\n\n fixes some bugs we we...Kshitij Bansal
2012-06-12Adding constant propagation code - needs more testing - off by defaultClark Barrett
2012-06-07LogicInfo locking implemented, and some initialization-order issues in SmtEng...Morgan Deters
2012-06-04Added preprocessing pass that propagates unconstrained values - solves all ofClark Barrett
2012-05-11Added some ITE rewrites,Clark Barrett
2012-04-28New LogicInfo functionality.Morgan Deters
2012-04-23Merge from decision branch -- partially working justification heuristicKshitij Bansal
2012-04-17A dummy decision engine. Expected performance impact: none.Kshitij Bansal
2012-03-02CDMap -> CDHashMapDejan Jovanović
2012-03-01Partial merge from kind-backend branch, including Minisat and CNF work toMorgan Deters
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback