summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/sygus/sygus_module.cpp
AgeCommit message (Collapse)Author
2021-04-12Refactor and update copyright headers. (#6316)Aina Niemetz
2021-04-01Rename namespace CVC5 to cvc5. (#6258)Aina Niemetz
2021-03-31Rename namespace CVC4 to CVC5. (#6249)Aina Niemetz
2021-03-31Eliminate 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-29Eliminate the use of quantifiers engine in sygus solver (#6232)Andrew Reynolds
2021-03-09Update copyright headers to 2021. (#6081)Aina Niemetz
2021-02-22Eliminate 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-22Update 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-16Update copyright headers.Aina Niemetz
2019-08-05Remove forward declarations in quantifiers engine (#3156)Andrew Reynolds
2019-03-26Update copyright headers.Aina Niemetz
2018-09-18Move and rename sygus solver classes (#2488)Andrew Reynolds
2018-06-25Updated copyright headers.Aina Niemetz
2018-05-17Internal propagation for refinement lemmas (#1932)Andrew Reynolds
2018-03-01Create infrastructure for sygus modules (#1632)Andrew Reynolds
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback