summaryrefslogtreecommitdiff
path: root/test
AgeCommit message (Expand)Author
2016-07-05Merge branch 'master' of https://github.com/CVC4/CVC4.gitPaulMeng
2016-06-23Fixed some warnings, fixed bug in cdhashmap that was crashing cdmap_black,Clark Barrett
2016-06-18Fix unit test.ajreynol
2016-06-17Support for separation logic. Enable cbqi by default for pure BV.ajreynol
2016-06-01Merge from proof branchGuy
2016-06-01Revert "Merging proof branch"Guy
2016-06-01Merging proof branchGuy
2016-06-01Fix to ignore a case of triggers with no free variables.ajreynol
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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback