summaryrefslogtreecommitdiff
path: root/src/theory/theory_model.cpp
AgeCommit message (Expand)Author
2016-08-12Minor fixes to model construction to take singleton equivalence classes into ...ajreynol
2016-07-20Infrastructure for storing and printing heap models for separation logic. Ens...ajreynol
2016-07-06Add comment field for model, resolves hack for printing sep logic models.ajreynol
2016-06-17Cleanup from last commit, treat sep.nil as variable kind.ajreynol
2016-06-17Support for separation logic. Enable cbqi by default for pure BV.ajreynol
2016-05-23Fix related to parametric sorts whose interpretation is finite due to uninter...ajreynol
2016-04-03Updating the copyright headers and scripts.Tim King
2016-03-01Shorter explanations for strings based on tracking which parts of normal form...ajreynol
2016-02-15Eliminate most of the internal representation infrastructure for tuples and r...ajreynol
2016-02-08Updates related to finite model finding and (co)datatypes. Bug fix enumerator...ajreynol
2016-02-03Added --omit-dont-cares option which doesn't print model values forClark Barrett
2016-01-19Bug fixes for model construction with codatatypes, add regressions.ajreynol
2016-01-18Bug fix rewriter for fun defs.ajreynol
2016-01-15Type enumerators take optional argument indicating fixed cardinalities of uni...ajreynol
2016-01-15Ensure model construction for parametric sorts involving uninterpreted sorts ...ajreynol
2015-12-24Miscellaneous fixesTim King
2015-12-14Refactoring Options Handler & Library Cycle BreakingTim King
2015-11-26Front-end support for get-value of sort cardinality, minor fixes for sygus so...ajreynol
2015-10-08Minor improvements to strings. Refactor rewriter. Enable fairness for multipl...ajreynol
2015-10-07Minor improvements, add endpoint eq inference to strings.ajreynol
2015-09-16Add option --fmf-fun-rlv, remove deprecated option --axiom-inst.ajreynol
2015-09-15Fix bug related to quantifiers + incremental, thanks John Backes for the bug ...ajreynol
2015-09-10Models for codatatypes. Fixes bug 662.ajreynol
2015-09-04Fix bugs 605 and 667.ajreynol
2015-06-27Refactor various corner cases of fmf, quantifiers modules. Enable cbqi2 by de...ajreynol
2015-04-26Bug fixes and improvements for mbqi with theory symbols, TheoryModel fullMode...ajreynol
2015-04-21Changes needed to compile at Google, plus some bug fixes from Google.Clark Barrett
2015-02-05Minor clean upTianyi Liang
2015-02-05Improved string performance, thanks to Peter's benchmarks.Tianyi Liang
2014-12-26Adding an option to the equality engine constructor to treat all constants asDejan Jovanovic
2014-12-22bug fix for constant regular expression model buildingTianyi Liang
2014-11-08Fix bug with incremental+datatypes. Minor cleanup. Disable regression bug48...ajreynol
2014-11-07Fixed bug in model builder with subtypesClark Barrett
2014-11-07Properly distinguish which EQC to assign values in datatypes, use assertRepre...ajreynol
2014-11-05Fix model bug in --mbqi=fmc. Minor cleanup in datatypes.ajreynol
2014-11-01Added cache to getModelValueClark Barrett
2014-07-01Update copyrights.Morgan Deters
2014-06-19added model generation to eager bit-blasting and turned abc off by defaultlianah
2014-05-16sets: fix a bug in model building, another in handling set of setsKshitij Bansal
2014-05-11More preparation for CASC proofs. Minor fix for sort inference (rewrite new ...Andrew Reynolds
2014-04-29Mostly resolves bug #561 memory leaks, and more.Morgan Deters
2014-04-10Expand definitions in theory datatypes, now has the expected semantics for in...Andrew Reynolds
2014-03-20cleanupKshitij Bansal
2014-03-20fix for sets/mar2014/..317minimized..Kshitij Bansal
2014-03-20fix a sharing issues with setsKshitij Bansal
2013-12-05Update copyrights, add missing file-level documentation; fix perms.Morgan Deters
2013-11-27General pre-release cleanup commitMorgan Deters
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback