summaryrefslogtreecommitdiff
path: root/test
AgeCommit message (Expand)Author
2016-04-12Optimizations for QCF to check relevant domain of variable argument positions...ajreynol
2016-04-11Minor fixes for inst match generators. Updates to qip.googleajreynol
2016-04-10More work on instantiation propagation. Enable external filtering of instanti...ajreynol
2016-04-09cardinality operation for finite sets (based on my thesis / ijcar16 paper)Kshitij Bansal
2016-04-07Refactor trigger selection, revisions to --relational-trigger. Properly proce...ajreynol
2016-04-03Updating the copyright headers and scripts.Tim King
2016-03-22Bug fix for define functions + incremental. Minor work on relational triggers.ajreynol
2016-03-21New version of the recursive options parsing strategy.Tim King
2016-03-18Limit duplicate propagating instances to avoid exponential behavior in QuantC...ajreynol
2016-03-12Add options related to interleaving quantifiers and theory combination, chang...ajreynol
2016-03-08Extend synthesis solver to handle single invocation with additional universal...ajreynol
2016-03-07Minor change to F-Length inference in strings. No internal tracking of cardin...ajreynol
2016-03-02Work towards complete instantiation for datatypes.ajreynol
2016-03-01Shorter explanations for strings based on tracking which parts of normal form...ajreynol
2016-02-26Refactoring of inferences in strings. Add several options.ajreynol
2016-02-23Fix term database for non-equal, congruent terms in master equality engine. D...ajreynol
2016-02-19Fixes and improvements for datatypes properties and splitting.ajreynol
2016-02-18Implement dynamic splitting for quantified formulas. Minor refactoring of re...ajreynol
2016-02-18Correct subtyping for arrays, disable subtyping for predicate subtypes. Bug ...ajreynol
2016-02-15Eliminate most of the internal representation infrastructure for tuples and r...ajreynol
2016-02-11More aggressive conditional rewriting for quantified formulas. Bug fix set in...ajreynol
2016-02-10Fix model postprocessor for tuples, add regression.ajreynol
2016-02-09Fix regression, minor change to output.ajreynol
2016-02-08Updates related to finite model finding and (co)datatypes. Bug fix enumerator...ajreynol
2016-02-02Moving dump.*, command.*, model.*, and ite_removal.* from smt_util/ to smt/. ...Tim King
2016-02-01Simplify fmc model construction, add regression. Improve FMF debug assertions.ajreynol
2016-01-28Adding listeners to Options.Tim King
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-15Ensure model construction for parametric sorts involving uninterpreted sorts ...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-06Improving the documentation of the CVC command CONTINUE.Tim King
2016-01-05Removing dead code. StackingMap only appeared in unit tests.Tim King
2016-01-05Moving sexpr.{cpp,h,i} from expr/ back into util/.Tim King
2016-01-05Add SmtGlobals ClassTim King
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-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-14Refactoring Options Handler & Library Cycle BreakingTim King
2015-11-25Infrastructure for partially single invocation properties. Bug fix for uncons...ajreynol
2015-11-23Adding a missing delete to smt2_compliance.Tim King
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-06Changing file permissions to add or remove executable tag as appropriate.Tim King
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback