Age | Commit message (Collapse) | Author | |
---|---|---|---|
2021-04-12 | Refactor and update copyright headers. (#6316) | Aina Niemetz | |
2021-04-01 | Rename namespace CVC5 to cvc5. (#6258) | Aina Niemetz | |
2021-03-31 | Rename namespace CVC4 to CVC5. (#6249) | Aina Niemetz | |
2021-03-31 | Eliminate dependencies on quantifiers engine in internal quantifiers code ↵ | Andrew Reynolds | |
(#6240) This completes eliminating dependencies on quantifiers engine from internal quantifiers code. It eliminates quantifiers_engine.h as an include from src/theory/quantifiers/ apart from theory_quantifiers.cpp where it is owned. Followup PRs will further eliminate circular dependencies that arose will refactoring quantifiers engine. | |||
2021-03-29 | Eliminate the use of quantifiers engine in sygus solver (#6232) | Andrew Reynolds | |
2021-03-09 | Update copyright headers to 2021. (#6081) | Aina Niemetz | |
2021-02-22 | Eliminate raw use of output channel and valuation in quantifiers (#5933) | Andrew Reynolds | |
This makes all lemmas in quantifiers sent through the inference manager. It begins adding InferenceId values for some of these calls. All uses of Valuation are replaced by calls to QuantifiersState. | |||
2020-09-22 | Update copyright header script to support CMake and Python files (#5067) | Mathias Preiner | |
This PR updates the update-copyright.pl script to also update/add copyright headers to CMake specific files. It further fixes a small typo in the header. | |||
2020-06-16 | Update copyright headers. | Aina Niemetz | |
2019-08-05 | Remove forward declarations in quantifiers engine (#3156) | Andrew Reynolds | |
2019-03-26 | Update copyright headers. | Aina Niemetz | |
2018-09-18 | Move and rename sygus solver classes (#2488) | Andrew Reynolds | |
2018-06-25 | Updated copyright headers. | Aina Niemetz | |
2018-05-17 | Internal propagation for refinement lemmas (#1932) | Andrew Reynolds | |
2018-03-01 | Create infrastructure for sygus modules (#1632) | Andrew Reynolds | |