summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/sygus/term_database_sygus.cpp
AgeCommit message (Expand)Author
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-25Use fast enumeration by default for Boolean predicate synthesis (#6440)Andrew Reynolds
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-25Add missing includes. (#6207)Gereon Kremer
2021-03-15Reorganizing initialization of term registry in quantifiers (#6127)Andrew Reynolds
2021-03-09Update copyright headers to 2021. (#6081)Aina Niemetz
2021-03-03More cleanup of includes to reduce compilation times (#6037)Gereon Kremer
2021-03-02Introduce quantifiers term registry (#5983)Andrew Reynolds
2021-03-02Clean up includes to reduce compile times (#6031)Gereon Kremer
2021-02-22Eliminate raw use of output channel and valuation in quantifiers (#5933)Andrew Reynolds
2021-02-17Eliminate non-static members in term util (#5919)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-30Fix null case for sygus printing (#4793)Andrew Reynolds
2020-07-17Enumerate shapes feature in fast sygus enumerator (#4742)Andrew Reynolds
2020-07-14Remove sygus print callback (#4727)Andrew Reynolds
2020-06-16Update copyright headers.Aina Niemetz
2020-06-12Move sygus datatype utility functions to their own file (#4595)Andrew Reynolds
2020-05-19Fix cached free variable identifiers in sygus term database (#4394)Andrew Reynolds
2020-04-12Fixes for extended rewriter (#4278)Andrew Reynolds
2020-03-05Enable -Wshadow and fix warnings. (#3909)Mathias Preiner
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-17Generate code for options with modes. (#3561)Mathias Preiner
2019-12-16Fix evaluator for non-evaluatable nodes (#3575)Andrew Reynolds
2019-12-12Use the node-level datatypes API (#3556)Andrew Reynolds
2019-12-11Fix CEGIS refinement for recursive functions evaluation (#3555)Andrew Reynolds
2019-12-06Optimize the rewriter for DT_SYGUS_EVAL (#3529)Andrew Reynolds
2019-11-27Enable sygusRecFun by default and fixes SyGuS+RecFun+HO issues (#3502)Haniel Barbosa
2019-11-21Evaluation unfolding for symbolic SyGuS constructors (#3483)Andrew Reynolds
2019-11-15Introduce SyGuS datatype API (#3465)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-10-30Unify CVC4_CHECK/CVC4_DCHECK/AlwaysAssert/Assert. (#3366)Mathias Preiner
2019-10-17 Move datatype utility functions to own file (#3397)Andrew Reynolds
2019-09-16Sygus type info class (#3187)Andrew Reynolds
2019-08-14Minor cleaning of sygus term database (#3159)Andrew Reynolds
2019-07-19Fixes for sygus with datatypes (#3103)Andrew Reynolds
2019-06-11Do not require sygus constructors to be flattened (#3049)Andrew Reynolds
2019-04-29Optimization for evaluation with unfolding (#2979)Andrew Reynolds
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-11-05Allow partial models with optimized sygus enumeration (#2682)Andrew Reynolds
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback