summaryrefslogtreecommitdiff
path: root/src/theory/model.cpp
AgeCommit message (Expand)Author
2013-11-27General pre-release cleanup commitMorgan Deters
2013-11-19Add fair strategy for finite model finding multiple sorts --uf-ss-fair.Andrew Reynolds
2013-10-24Fix for bug515Clark Barrett
2013-07-19Minor fix for --no-condense-function-valuesMorgan Deters
2013-07-17Fix bug 516; include some bug testcases.Morgan Deters
2013-07-16Minor bugfixes to model-buildingMorgan Deters
2013-07-09Fix for bug 519; don't involve ITESimplifier in model generation.Morgan Deters
2013-06-05Fix bug in --fmf-fmc for producing models of functions not appearing in quant...Andrew Reynolds
2013-06-04Add --no-condense-function-values option for explicit function models (useful...Morgan Deters
2013-04-02Regenerated copyrights: canonicalized names, no emailsMorgan Deters
2013-04-01update copyrightsMorgan Deters
2013-04-01Fixes for two bugs:Morgan Deters
2013-04-01Fix bug 491 and related issues with checkModel() and quantifiers. Enabling p...Morgan Deters
2013-03-22Support for Boolean term conversion in datatypes.Morgan Deters
2013-02-04Model no longer adds subterms of quantifiers to equality engine, this fixed b...Andrew Reynolds
2013-01-25fix --check-model --finite-model-find when used together (related to bug 486)Morgan Deters
2013-01-23partially address bug 486: allow some model inspection of quantifiersMorgan Deters
2012-12-03Fix for fuzzer-found model bugClark Barrett
2012-11-29Fixing function models with Boolean terms. Also, LAMBDA's should not be const.Clark Barrett
2012-11-28Fix for getValue. Now it can handle lambda applicationsClark Barrett
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-21Added debugging output to --check-models. I've found this output quite useful...Tim King
2012-11-16fix a compiler warning in modelsMorgan Deters
2012-11-15More fixes to model generation, with previously failing testcasesClark Barrett
2012-11-14Fix for bug 407. mkAnonymousFunction() in the parser no longer uses ':'. CVC ...Tim King
2012-11-14bug fixes to models, array rewriter with previously failing testcasesClark Barrett
2012-11-13More bugfixes for modelsClark Barrett
2012-11-13Relaxing too-strict assertionClark Barrett
2012-11-10Fixed missing \ in uflra/Makefile.maClark Barrett
2012-11-09TheoryEngineModelBuilder::buildModel() is only called once with fullModel=tru...Morgan Deters
2012-11-09Fix for another model assertion failureClark Barrett
2012-11-08Fixed two small bugs in model generationClark Barrett
2012-10-29Disable some array optimizations when models are onClark Barrett
2012-10-26Fixed a failing datatype regression with check-modelsClark 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-23more updates to inst gen: fixed partial instantiations, recognize duplicate d...Andrew Reynolds
2012-10-12Added assertions and tracing code for collectModelInfo phaseClark Barrett
2012-10-12Latest changes to model codeClark Barrett
2012-10-11Standardizing copyright notice. Touches **ALL** sources, guys, sorry.. it'sMorgan Deters
2012-10-09fixed datatypes rewriter to detect clashes between non-datatype subfields. c...Andrew Reynolds
2012-10-09More fixes to model codeClark Barrett
2012-10-09* Add assertion in TheoryModel code to ensure we don't get inconsistentMorgan Deters
2012-10-08* Models' SubstitutionMaps are now attached to the user contextMorgan Deters
2012-10-08Fixed problem in assertEqualityEngine: predicates that are not false are noClark Barrett
2012-10-06* Clean up some options documentationMorgan Deters
2012-10-05Bug-related:Morgan Deters
2012-10-04Implemented array type enumerator, more fixes for modelsClark Barrett
2012-10-03minor fix for mbqi in finite model findingAndrew Reynolds
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback