summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/sygus/cegis.h
AgeCommit message (Collapse)Author
2021-05-13Add std::hash overloads for Node, TNode and TypeNode. (#6534)Mathias Preiner
Eliminates NodeHashFunction, TNodeHashFunction and TypeNodeHashFunction.
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-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
2020-02-10Use example evaluation cache instead of sygus PBE (#3733)Andrew Reynolds
2020-02-07Interface for example evaluation cache utilities (#3726)Andrew Reynolds
This adds interfaces in synth_conjecture for getting an ExampleEvalCache, per enumerator. It also adds a specialization `checkRefinementEvalLemmas` of `getRefinementEvalLemmas` in the cegis module, which does evaluation on CEGIS refinement lemmas without structural generalization. This function will be used as an alternative to `getRefinementEvalLemmas` for fast enumerators. The next PR will update all utilities to use ExampleEvalCache instead of SygusPbe for evaluating examples.
2019-11-21Evaluation unfolding for symbolic SyGuS constructors (#3483)Andrew Reynolds
2019-10-14Apply sygus repair constant techniques restricted to refinement lemmas (#3386)Andrew Reynolds
2019-08-23 Pass synthesis conjecture to sygus modules (#3212)Andrew Reynolds
2019-04-24Do not use __ prefix for header guards. (#2974)Mathias Preiner
Fixes 2887.
2019-03-26Update copyright headers.Aina Niemetz
2018-10-03Add actively generated sygus enumerators (#2552)Andrew Reynolds
2018-09-27Infrastructure for using active enumerators in sygus modules (#2547)Andrew Reynolds
2018-09-18Move and rename sygus solver classes (#2488)Andrew Reynolds
2018-07-30Fix several spelling errors (#2231)FabianWolff
2018-06-25Updated copyright headers.Aina Niemetz
2018-06-20Fix warnings and enable -Wnon-virtual-dtor warning (#2079)Andres Noetzli
This commit fixes warnings for an unused variable, comparison of two different types and add virtual destructors to classes that were previously missing them. It also enables the -Wnon-virtual-dtor warning which warns about any class definition with virtual methods that does not have a virtual destructor (except if the destructor is protected). This flag is supported by both clang and GCC and not enabled by default.
2018-05-25Reenable repair const (#1983)Andrew Reynolds
2018-05-22Repair constants using symbolic constructors (#1960)Andrew Reynolds
2018-05-21Refactor sygus eval unfold (#1946)Andrew Reynolds
2018-05-17Cegis-specific infrastructure (#1933)Andrew Reynolds
2018-05-17Internal propagation for refinement lemmas (#1932)Andrew Reynolds
2018-05-03Make CegisUnif default to Cegis when no unif used (#1836)Haniel Barbosa
2018-03-02Simplify sygus wrt miniscoping (#1634)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