summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/sygus/term_database_sygus.h
AgeCommit message (Expand)Author
2021-05-13Add std::hash overloads for Node, TNode and TypeNode. (#6534)Mathias Preiner
2021-04-14Rename public and private headers in src/include. (#6352)Aina Niemetz
2021-04-12Refactor and update copyright headers. (#6316)Aina Niemetz
2021-04-09Rename CVC4__ header guards to CVC5__. (#6326)Aina Niemetz
2021-04-01Rename namespace CVC5 to cvc5. (#6258)Aina Niemetz
2021-03-31Rename namespace CVC4 to CVC5. (#6249)Aina Niemetz
2021-03-15Reorganizing initialization of term registry in quantifiers (#6127)Andrew Reynolds
2021-03-09Update copyright headers to 2021. (#6081)Aina Niemetz
2021-03-02Introduce quantifiers term registry (#5983)Andrew Reynolds
2021-01-26Introduce quantifiers inference manager (#5821)Andrew Reynolds
2021-01-26Refactor quantifiers engine initialization (#5813)Andrew Reynolds
2020-09-22Update copyright header script to support CMake and Python files (#5067)Mathias Preiner
2020-07-14Remove sygus print callback (#4727)Andrew Reynolds
2020-06-16Update copyright headers.Aina Niemetz
2020-05-19Fix cached free variable identifiers in sygus term database (#4394)Andrew Reynolds
2020-01-30Example minimize evaluation utility. (#3671)Andrew Reynolds
2020-01-07Update any-constant and normalization policies for sygus grammars (#3583)Andrew Reynolds
2019-12-12Use the node-level datatypes API (#3556)Andrew Reynolds
2019-11-21Evaluation unfolding for symbolic SyGuS constructors (#3483)Andrew Reynolds
2019-11-06Support for SyGuS PBE + recursive functions (#3433)Andrew Reynolds
2019-11-04Eliminate deprecated utility function from sygus (#3431)Andrew Reynolds
2019-11-01Eagerly beta reduce during sygus to builtin term conversion (#3418)Andrew Reynolds
2019-09-16Sygus type info class (#3187)Andrew Reynolds
2019-08-14Minor cleaning of sygus term database (#3159)Andrew Reynolds
2019-06-11Do not require sygus constructors to be flattened (#3049)Andrew Reynolds
2019-04-24Do not use __ prefix for header guards. (#2974)Mathias Preiner
2019-03-26Update copyright headers.Aina Niemetz
2018-11-06Incorporate static PBE symmetry breaking lemmas into SygusEnumerator (#2690)Andrew Reynolds
2018-11-05Change default sygus enumeration mode to auto (#2689)Andrew Reynolds
2018-10-31Add optimized sygus enumeration (#2677)Andrew Reynolds
2018-10-09 Support for basic actively-generated enumerators (#2606)Andrew Reynolds
2018-09-27Infrastructure for using active enumerators in sygus modules (#2547)Andrew Reynolds
2018-09-24Infrastructure for variable agnostic sygus enumerators (#2511)Andrew Reynolds
2018-09-18Move and rename sygus solver classes (#2488)Andrew Reynolds
2018-08-07Document/refactor datatypes sygus simple symmetry breaking (#2233)Andrew Reynolds
2018-07-17sygusComp 2018: updates to sygus term database (#2170)Andrew Reynolds
2018-06-27Synthesize candidate-rewrites from standard inputs (#1918)Andrew Reynolds
2018-06-26sygusComp2018: Add evaluator (#2090)Andres Noetzli
2018-06-25Updated copyright headers.Aina Niemetz
2018-05-28Builtin evaluation functions for sygus (#1991)Andrew Reynolds
2018-05-24Improve simple constant symmetry breaking for sygus (#1977)Andrew Reynolds
2018-05-22Repair constants using symbolic constructors (#1960)Andrew Reynolds
2018-05-21Refactor sygus eval unfold (#1946)Andrew Reynolds
2018-05-18Unified fairness scheme for cegis unif (#1941)Andrew Reynolds
2018-05-17Catch type errors in sygus grammars for lambda (define-fun) constructors (#1937)Andrew Reynolds
2018-05-17Internal propagation for refinement lemmas (#1932)Andrew Reynolds
2018-05-10Exclude Boolean connectives from ITE conditions in SygusUnifStrat (#1900)Andrew Reynolds
2018-05-10Sygus repair constants (#1812)Andrew Reynolds
2018-03-20Minor refactor datatypes sygus (#1673)Andrew Reynolds
2018-03-06Refactor symmetry breaking in datatypes sygus (#1640)Andrew Reynolds
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback