summaryrefslogtreecommitdiff
path: root/src/smt/quant_elim_solver.cpp
AgeCommit message (Expand)Author
2021-04-28Remove exception headers from options.h (#6456)Gereon Kremer
2021-04-12Refactor and update copyright headers. (#6316)Aina Niemetz
2021-04-07Replace calls to NodeManager::mkSkolem with SkolemManager::mkDummySkolem (#6291)Andrew Reynolds
2021-04-01Rename namespace CVC5 to cvc5. (#6258)Aina Niemetz
2021-03-31Rename namespace CVC4 to CVC5. (#6249)Aina Niemetz
2021-03-30Implement simple tracking of instantiation lemmas (#6077)Andrew Reynolds
2021-03-10(proof-new) Replace witness form by original form in the internal proof calcu...Andrew Reynolds
2021-03-09Update copyright headers to 2021. (#6081)Aina Niemetz
2021-01-27(proof-new) Improvements to quantifiers engine and instantiate interfaces (#5...Andrew Reynolds
2020-11-30More fixes for quantifier elimination (#5533)Andrew Reynolds
2020-11-20Support nested quantifier elimination for get-qe command (#5490)Andrew Reynolds
2020-11-19Enable new implementation of CEGQI based on nested quantifier elimination (#5...Andrew Reynolds
2020-09-22Update copyright header script to support CMake and Python files (#5067)Mathias Preiner
2020-08-20Split QuantElimSolver from SmtEngine (#4919)Andrew Reynolds
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback