summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/term_database.cpp
AgeCommit message (Expand)Author
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
2016-06-17Cleanup from last commit, treat sep.nil as variable kind.ajreynol
2016-06-17Support for separation logic. Enable cbqi by default for pure BV.ajreynol
2016-06-03Simple memory fixes, minor cleanup in quantifiers.ajreynol
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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback