summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/term_database.h
AgeCommit message (Expand)Author
2020-06-16Update copyright headers.Aina Niemetz
2019-09-13Move higher-order matching predicate (#3280)Andrew Reynolds
2019-08-14Fix issue related to higher-order purification in term database (#3157)Andrew Reynolds
2019-06-01 Require that FMF model basis terms are variables (#3031)Andrew Reynolds
2019-05-09Fixes for relational triggers (#2967)Andrew Reynolds
2019-04-24Do not use __ prefix for header guards. (#2974)Mathias Preiner
2019-04-18Fail fast strategy for propagating instances (#2939)Andrew Reynolds
2019-03-26Update copyright headers.Aina Niemetz
2018-11-27Make (T)NodeTrie a general utility (#2489)Andrew Reynolds
2018-07-17Minor cleanup and fixes for conflict-based instantiation (#2123)Andrew Reynolds
2018-06-25Updated copyright headers.Aina Niemetz
2018-04-09Fix higher-order term indexing. (#1754)Andrew Reynolds
2018-03-05Enable -Wsuggest-override by default. (#1643)Mathias Preiner
2017-11-01(Refactor) Split term util (#1303)Andrew Reynolds
2017-10-28Document term db (#1220)Andrew Reynolds
2017-10-09Split term database (#1206)Andrew Reynolds
2017-10-04Ho quant util (#1119)Andrew Reynolds
2017-09-29Simplify representation of inversion Skolems for bv cegqi (#1164)Andrew Reynolds
2017-07-20Moving from the gnu extensions for hash maps to the c++11 hash mapsTim King
2017-07-10Separate sygus term utilities to new file, minor cleanup from last commit.ajreynol
2017-07-10Merge datatype shared selectors/sygus comp 2017 branch. Modify the datatypes ...ajreynol
2017-07-07Update copyright headers.Mathias Preiner
2017-04-21Handle subtypes in sets. Bug fixes for tuples with subtypes.ajreynol
2017-03-28More work on sygus. Add regress4 to Makefile.ajreynol
2017-03-24Refactor model building for quantifiers to be a single pass, simplification. ...ajreynol
2017-03-02Eliminate Boolean term conversion. Generalizes removeITE pass to remove Boole...ajreynol
2016-10-13Revert "Merge branch 'origin' of https://github.com/CVC4/CVC4.git"Tim King
2016-10-11Merge branch 'origin' of https://github.com/CVC4/CVC4.gitPaul Meng
2016-09-25Adding a destructor to TermDb.Tim King
2016-09-03Option for prenex normal formajreynol
2016-09-01Updates to cbqi. New strategy --cbqi-nested-qe to do qe on nested quantifier...ajreynol
2016-07-05Merge branch 'master' of https://github.com/CVC4/CVC4.gitPaulMeng
2016-06-01Initial infrastructure for bounded set quantification (disabled). Refactoring...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-15Work on --sygus-direct-eval. Minor optimizations, updates to casc scripts. En...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-28More work on inst propagate. Optimization for qcf to check instances eagerly...ajreynol
2016-04-20update from the masterPaulMeng
2016-04-12Optimizations for QCF to check relevant domain of variable argument positions...ajreynol
2016-04-09Minor refactoring of entailment tests and quantifiers util. Initial draft of ...ajreynol
2016-04-07Refactor trigger selection, revisions to --relational-trigger. Properly proce...ajreynol
2016-04-04New options for trigger selection, add option --strict-triggers. Do not infer...ajreynol
2016-04-03Updating the copyright headers and scripts.Tim King
2016-03-31Improvements to trigger selection, min triggers by default. Optimizations for...ajreynol
2016-03-28Implement equality inference module for arithmetic terms. Optimization for e...ajreynol
2016-03-16Change internal representative selection for finite domains that do not invol...ajreynol
2016-03-10Faster conditional rewriting for and/or beneath quantifiers. Improvements to ...ajreynol
2016-02-25Minor improvement to partial qe. Add options for representative selection in ...ajreynol
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback