summaryrefslogtreecommitdiff
path: root/src/theory/theory_model.cpp
AgeCommit message (Expand)Author
2018-09-11Support model cores via option --produce-model-cores. (#2407)Andrew Reynolds
2018-08-20More unused code elimination (#2339)Andrew Reynolds
2018-06-25Updated copyright headers.Aina Niemetz
2018-05-23Add notions of evaluated kinds in TheoryModel (#1947)Andrew Reynolds
2018-05-10Refactored BVAckermann preprocessing pass. (#1889)Aina Niemetz
2018-05-08Infrastructure for approximations in model output (#1884)Andrew Reynolds
2018-01-15Removing more miscellaneous throw specifiers. (#1509)Tim King
2017-12-08Make collect model info return a Bool (#1421)Andrew Reynolds
2017-11-30Fixes for issue 1404 (#1409)Andrew Reynolds
2017-11-01(Move-only) Refactor and document theory model part 2 (#1305)Andrew Reynolds
2017-10-27Refactor theory model (#1236)Andrew Reynolds
2017-10-05Ho model (#1120)Andrew Reynolds
2017-08-31Answer unknown when uf-ss=no-minimal is combined with cardinality constraints...Andrew Reynolds
2017-08-30Fix model construction for parametric types (#1059)Andrew Reynolds
2017-07-20Moving from the gnu extensions for hash maps to the c++11 hash mapsTim King
2017-07-07Update copyright headers.Mathias Preiner
2017-04-05Add non-linear regressions, disable nlAlgSubs, do not do rep checking for NON...ajreynol
2017-04-04Simplify Theory::collectModelInfo interface to not take deprecated fullModel ...ajreynol
2017-03-24Refactor model building for quantifiers to be a single pass, simplification. ...ajreynol
2016-12-02Bug fixes and refactoring of parametric datatypes, add some regressions.ajreynol
2016-12-02Refactor preprocessing of models in fmf. Fix options --fmf-empty-sorts and --...ajreynol
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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback