summaryrefslogtreecommitdiff
path: root/src/theory/model.cpp
AgeCommit message (Expand)Author
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
2012-10-03New model code, mostly workinClark Barrett
2012-09-26updates to model generation : do not modify equality engine during getValue, ...Andrew Reynolds
2012-09-19General subscriber infrastructure for NodeManager, as discussed in theMorgan Deters
2012-09-17minor fix for models, added simple cliques option for uf strong solverAndrew Reynolds
2012-09-16store values returned by get-value in TheoryModel::d_reps if necessary, fixes...Andrew Reynolds
2012-09-13ensure that get-value and get-model are consistent, rewrite function value bo...Andrew Reynolds
2012-09-12Adding model assertions after SAT responses.Morgan Deters
2012-09-11added getCardinality to modelAndrew Reynolds
2012-09-11Partially reverting the changes made in 4308. There is now both an Expr and N...Tim King
2012-09-10modified getValue to return Expr instead of NodeAndrew Reynolds
2012-08-31merge from fmf-devel branch. more updates to models: now with collectModelIn...Andrew Reynolds
2012-08-24* disallow internal uses of mkVar() (you have to mkSkolem())Morgan Deters
2012-08-14Switched TheoryModel assertEqualityEngine to use const Equality Engine pointers.Tim King
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback