summaryrefslogtreecommitdiff
path: root/test
AgeCommit message (Expand)Author
2016-06-01Initial infrastructure for bounded set quantification (disabled). Refactoring...ajreynol
2016-05-28Fix buildClark Barrett
2016-05-28Disabling failing unit test for nowClark Barrett
2016-05-26Use term indexing in TheoryUF::computeCareGraph. Do not reject model value in...ajreynol
2016-05-25Fixed unit testLiana Hadarean
2016-05-23Fix related to parametric sorts whose interpretation is finite due to uninter...ajreynol
2016-05-21Minor fix for strings.ajreynol
2016-05-20Minor fix to strings, cleanup in datatypes.ajreynol
2016-05-18Refactor modes for sygus+single invocation. Add option --inst-rlv-cond. Mino...ajreynol
2016-05-16Enable --sygus-direct-eval by default, limit to terms that do not induce Bool...ajreynol
2016-05-10Fix for --inst-max-levelajreynol
2016-05-06Minor clean up, fixes related to sygus.ajreynol
2016-05-05Compute term indices lazily in TermDb. Optimization for qcf to recognize irre...ajreynol
2016-05-02Clean up issues related to compiled scc in LFSC. Refactor --partial-trigger, ...ajreynol
2016-04-20update from the masterPaulMeng
2016-04-13Update native language support for strings.ajreynol
2016-04-12Bug fixes related to parametric datatypes + theory combination + quantifiers....ajreynol
2016-04-12Optimizations for QCF to check relevant domain of variable argument positions...ajreynol
2016-04-12added more benchmarksPaulMeng
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-10fixed the transpose-occur rulePaulMeng
2016-03-08make skolems and tuple reduction terms as shared termsPaulMeng
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-04refactored the codePaulMeng
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-29Added more benchmarksPaulMeng
2016-02-28implemented a basic solving procedure for finite relations (only forPaulMeng
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-17added rules for join and transpose operatorsPaulMeng
2016-02-15Merge remote-tracking branch 'origin/master'PaulMeng
2016-02-15extended smt parser for the finite relationsPaulMeng
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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback