summaryrefslogtreecommitdiff
path: root/src/theory/theory_engine.cpp
AgeCommit message (Expand)Author
2014-01-22Delay QuantifiersEngine and UF strong solver initialization until after final...Morgan Deters
2014-01-18strings with new ideasTianyi Liang
2014-01-10Add new method --quant-cf for finding conflicts eagerly for quantified formul...Andrew Reynolds
2013-12-23Proof-checking code; fixups of segfaults and missing functionality in proof g...Morgan Deters
2013-12-05Update copyrights, add missing file-level documentation; fix perms.Morgan Deters
2013-11-27General pre-release cleanup commitMorgan Deters
2013-11-25Substantial Changes:Tim King
2013-10-07fixed some bugsLiana Hadarean
2013-09-27Some fixes to recent strings commits.Morgan Deters
2013-09-27adds model generation for strings, and a hacked way in arith engine for modelsTianyi Liang
2013-09-13Documentation fixes, some code typo fixes, file perms, other minor things.Morgan Deters
2013-09-05Fix bugs/issues with missed-t-prop dump outputMorgan Deters
2013-06-27Better check-models output for some kinds of problems; add anassertion that t...Morgan Deters
2013-05-21Fix bug 512: an assertion failure only appearing with clang on Mac OS, due to...Morgan Deters
2013-05-20disable Logic-checking with finite model finding for now, since FMF uses Rati...Morgan Deters
2013-05-20Fix erroneous results when the logic was incorrectly specified (by throwing L...Morgan Deters
2013-05-07fix for bug500Dejan Jovanović
2013-05-02* splitLemma to request atomsDejan Jovanović
2013-04-30innd examples are solved fast, but destruction assertion faillianah
2013-04-30fixed compile errorLiana Hadarean
2013-04-30uncompiling new bv to bool liftinglianah
2013-04-30finished implementing bv to bool lifting and added --bv-to-bool optionlianah
2013-04-02Regenerated copyrights: canonicalized names, no emailsMorgan Deters
2013-04-01update copyrightsMorgan Deters
2013-03-27Updates to model-based array solverClark Barrett
2013-03-26addingDejan Jovanović
2013-02-16Some cleanup and copyright updatingMorgan Deters
2013-02-12Fix a preprocessing performance issue.Morgan Deters
2013-02-03new miplib pass, works for 1 or 2 varsMorgan Deters
2013-01-28made QuantifiersEngine::d_inst_match_trie and QuantifiersEngine::d_lemmas_pro...Andrew Reynolds
2013-01-25fix --check-model --finite-model-find when used together (related to bug 486)Morgan Deters
2013-01-22fix for theory preprocessing cache on clang, perhaps others.Morgan Deters
2012-12-01drastic simplification of quantifiers code regarding equality queries, instan...Andrew Reynolds
2012-11-30quantifiers now uses master equality engine, preparation work to cleanup codeAndrew Reynolds
2012-11-29Fixing function models with Boolean terms. Also, LAMBDA's should not be const.Clark Barrett
2012-11-27First chunk of boolean-terms support.Morgan Deters
2012-11-26fixup for incremental solvingDejan Jovanović
2012-11-26Adding support for a master equality engine. Each theory gets the master equa...Dejan Jovanović
2012-11-17* Fix for bug 445 agreed to in meeting 11/13/2012: always dump in ALL_SUPPORT...Morgan Deters
2012-11-15d_incomplete is context-dependent; we shouldn't be saving its value and resto...Morgan Deters
2012-11-15Fixed another AUFBV model bug. BV equality subtheory needed to do somethingClark Barrett
2012-11-13refactoring of quantifiers rewriter based on code review from yesterday, refa...Andrew Reynolds
2012-11-09TheoryEngineModelBuilder::buildModel() is only called once with fullModel=tru...Morgan Deters
2012-11-09Bug-fix for a crash involving improperly-thrown exceptions; also, add LogicEx...Morgan Deters
2012-10-29Disable some array optimizations when models are onClark Barrett
2012-10-26More bug fixes and more checks for modelsClark Barrett
2012-10-23More debugging info, small changes to model builderClark Barrett
2012-10-11Standardizing copyright notice. Touches **ALL** sources, guys, sorry.. it'sMorgan Deters
2012-10-08* Models' SubstitutionMaps are now attached to the user contextMorgan Deters
2012-10-06* Fix some regressions' expected outputs.Morgan Deters
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback