summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/term_database.cpp
AgeCommit message (Expand)Author
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
2016-05-12Add casc scripts. Improvements to qcf related to nested quantifiers and varia...ajreynol
2016-05-10Add smt comp 2016 scripts. Fix for --relevant-triggers. Add minor optimizatio...ajreynol
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-28More work on inst propagate. Optimization for qcf to check instances eagerly...ajreynol
2016-04-20update from the masterPaulMeng
2016-04-13Handle parametric datatypes with --quant-ind. Minor updates.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-09Minor refactoring of entailment tests and quantifiers util. Initial draft of ...ajreynol
2016-04-07Refactor trigger selection, revisions to --relational-trigger. Properly proce...ajreynol
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback