summaryrefslogtreecommitdiff
path: root/src/theory
AgeCommit message (Expand)Author
2016-01-26Merged bit-vector and uf proof branch.Liana Hadarean
2016-01-20Fix bug in fmc mbqi where modelscomputed for mbqi could involve non-constant ...ajreynol
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
2016-01-13Lemma cache datatypes. Do not send true lemma in quantifiers. Minor fix for d...ajreynol
2016-01-08Adding a new Listener utility class. Changing the ResourceManager to use List...Tim King
2016-01-08Removing StatisticsRegistry's static functions current() and registerStat().Tim King
2016-01-05Add SmtGlobals ClassTim King
2016-01-01Added propagation rule for array ext lemmas to aid proofsClark Barrett
2015-12-30Shuffling around public vs. private headersTim King
2015-12-26Merged my changes from experimental branch (new array decision procedure,Clark Barrett
2015-12-24Miscellaneous fixesTim King
2015-12-23Enabled array propagation during lemma propagation - this should catch someClark Barrett
2015-12-22Bug fix uf-ss-totality.ajreynol
2015-12-22Always split on constructor types for datatypes involving uninterpreted sorts...ajreynol
2015-12-22Bug fix for cbqi, do not use model values for terms involving non-enumerable ...ajreynol
2015-12-18Modifying emptyset.h and sexpr. Adding SetLanguage.Tim King
2015-12-17Minorajreynol
2015-12-16Work on purification for quantifiers, minor updates.ajreynol
2015-12-15Breaking the include cycle between Record and Expr.Tim King
2015-12-15Add option uf-ss-fair-monotone. Minor cleanup and improvement of sort inference.ajreynol
2015-12-14Refactoring Options Handler & Library Cycle BreakingTim King
2015-12-10Add option fmf-empty-sorts.ajreynol
2015-12-02Minor fixes for cegqi-si-partial.ajreynol
2015-12-01More work on --cegqi-si-partial, incomplete.ajreynol
2015-11-28Initial work on --cegqi-si-partial, refactoring.ajreynol
2015-11-26Update to new implementation of single invocation partition by default.ajreynol
2015-11-26Front-end support for get-value of sort cardinality, minor fixes for sygus so...ajreynol
2015-11-25Infrastructure for partially single invocation properties. Bug fix for uncons...ajreynol
2015-11-23Adding a missing delete to InstStrategyCegqi destructor.Tim King
2015-11-18Option for midpoints in cbqi.ajreynol
2015-11-17Improve relevant domain computation for arithmetic, full saturation strategy....ajreynol
2015-11-12Minor fixes and improvements to purify quant, relational triggers.ajreynol
2015-11-11Minor fixes to cbqi, purify-quant. Better error checking in addInstantiation.ajreynol
2015-11-10Fix infinite loop in datatype enumerator. Minor fixes and improvements to cbq...ajreynol
2015-11-09Replacing an inefficient use of std::find(...) to use std::set's find() instead.Tim King
2015-11-06Changing file permissions to add or remove executable tag as appropriate.Tim King
2015-11-05Merging the google branch back into master.Tim King
2015-11-05Fixes some initialization and desctruction problems in quantifiers. Also rest...Tim King
2015-11-04Better combination of UF with cbqi, refactor quantifiers intialization.ajreynol
2015-11-03Fixing typo.Tim King
2015-10-31Improvements to handling of mixed Int/Real quantifiers.ajreynol
2015-10-26This commit fixes a bug related to a public header depending on a compiler fl...Tim King
2015-10-26This commit removes using absolute paths in the generation of the .subdirs fi...Tim King
2015-10-26Promote InstStrategyCbqi to quantifier module. Cleanup unused code.ajreynol
2015-10-26Extend counterexample-guided instantiation to extended theory of Int/Real, mi...ajreynol
2015-10-24Fixes related to string contains.ajreynol
2015-10-23This removes a bug for reading data that has been popped from the back of a v...Tim King
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback