summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/sygus/sygus_enumerator.cpp
AgeCommit message (Expand)Author
2021-11-12Remove `ConstantMap<Rational>` (#7635)Andres Noetzli
2021-09-22Towards standard usage of evaluator (#7189)Andrew Reynolds
2021-08-24Refactor enumerator management in synth conjecture (#6942)Andrew Reynolds
2021-07-27Make all dependencies in the fast enumerator optional (#6918)Andrew Reynolds
2021-05-13Add std::hash overloads for Node, TNode and TypeNode. (#6534)Mathias Preiner
2021-04-12Fix computation of whether a type is finite (#6312)Andrew Reynolds
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-09Some more cleanup of includes (#6083)Gereon Kremer
2021-03-09Update copyright headers to 2021. (#6081)Aina Niemetz
2021-03-02Clean up includes to reduce compile times (#6031)Gereon Kremer
2020-09-22Update copyright header script to support CMake and Python files (#5067)Mathias Preiner
2020-07-17Enumerate shapes feature in fast sygus enumerator (#4742)Andrew Reynolds
2020-06-16Update copyright headers.Aina Niemetz
2020-04-20Make option names related to CEGQI consistent (#4316)Andrew Reynolds
2020-04-16SyGuS instantiation quantifiers module (#3910)Mathias Preiner
2020-03-05Enable -Wshadow and fix warnings. (#3909)Mathias Preiner
2020-02-19Fix symmetry breaking for multiple sygus types (#3775)Andrew Reynolds
2020-02-16Fix simple issue with cache (#3762)Andrew Reynolds
2020-02-10Use example evaluation cache instead of sygus PBE (#3733)Andrew Reynolds
2020-02-07Statistics for fast enumerator (#3699)Andrew Reynolds
2020-01-31Minor refactoring of constructor classes in fast enumerator (#3685)Andrew Reynolds
2020-01-08Fix backtracking issue in sygus fast enumerator (#3593)Andrew Reynolds
2019-12-12Use the node-level datatypes API (#3556)Andrew Reynolds
2019-11-29Fix fast SyGuS enumeration for interpreted constants (#3501)Andrew Reynolds
2019-10-17 Move datatype utility functions to own file (#3397)Andrew Reynolds
2019-03-26Update copyright headers.Aina Niemetz
2019-03-19Fix fairness issue with fast sygus enumerator (#2873)Andrew Reynolds
2019-03-14Generalize sygus-rr-verify for fast enumerator (#2829)Andrew Reynolds
2018-11-21Cache evaluations for PBE (#2699)Andrew Reynolds
2018-11-06Incorporate static PBE symmetry breaking lemmas into SygusEnumerator (#2690)Andrew Reynolds
2018-11-05Fix coverity warnings in sygus enumerator (#2687)Andrew Reynolds
2018-11-05Allow partial models with optimized sygus enumeration (#2682)Andrew Reynolds
2018-11-04 Implement option to turn off symmetry breaking for basic enumerators (#2686)Andrew Reynolds
2018-10-31Add optimized sygus enumeration (#2677)Andrew Reynolds
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback