summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/term_database.cpp
AgeCommit message (Expand)Author
2020-09-03Minor cleanup of quantifiers engine (#4994)Andrew Reynolds
2020-08-11Remove instantiation model true option (#4861)Andrew Reynolds
2020-06-16Update copyright headers.Aina Niemetz
2020-02-26Initial work towards -Wshadow (#3817)Andrew Reynolds
2020-02-19Delay enumerative instantiation if theory engine does not need check (#3774)Andrew Reynolds
2019-12-17Generate code for options with modes. (#3561)Mathias Preiner
2019-10-30Unify CVC4_CHECK/CVC4_DCHECK/AlwaysAssert/Assert. (#3366)Mathias Preiner
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-18Fail fast strategy for propagating instances (#2939)Andrew Reynolds
2019-04-17More use of isClosure (#2959)Andrew Reynolds
2019-03-26Update copyright headers.Aina Niemetz
2018-11-27Make (T)NodeTrie a general utility (#2489)Andrew Reynolds
2018-06-25Updated copyright headers.Aina Niemetz
2018-04-09Fix higher-order term indexing. (#1754)Andrew Reynolds
2018-04-04Fix for corner case of higher-order matching (#1708)Andrew Reynolds
2018-02-14Quantifiers subdirectories (#1608)Andrew Reynolds
2017-11-24(Refactor) Instantiate utility (#1387)Andrew Reynolds
2017-11-09 Decouple sygus term database and term database. (#1317)Andrew Reynolds
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-05-15Make conflict-based instantiation abort if a ground conflict is found in the ...ajreynol
2017-04-21Handle subtypes in sets. Bug fixes for tuples with subtypes.ajreynol
2017-03-29Add quantifiers options related to model and master equality engine.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-07More fixes for printing/parsing sets, fix kind name.ajreynol
2017-03-06Support for set compliment and universe set. Simplify approach for sep.nil no...ajreynol
2017-03-02Eliminate Boolean term conversion. Generalizes removeITE pass to remove Boole...ajreynol
2016-12-02Bug fixes and refactoring of parametric datatypes, add some regressions.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-29Address some coverity warnings, add another stat.ajreynol
2016-09-25Adding a destructor to TermDb.Tim King
2016-09-16Use matching heuristics for EPR instantiation.ajreynol
2016-09-15Begin refactoring of cbqi, remove a few dead options. Pre-skolemize by defaul...ajreynol
2016-09-15Make sep pto a trigger kind, track in equality engines and term database.ajreynol
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-08-26Basic support for EPR+CBQI. Minor cleanup.ajreynol
2016-07-05Merge branch 'master' of https://github.com/CVC4/CVC4.gitPaulMeng
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback