Age | Commit message (Collapse) | Author | |
---|---|---|---|
2021-05-13 | Add std::hash overloads for Node, TNode and TypeNode. (#6534) | Mathias Preiner | |
Eliminates NodeHashFunction, TNodeHashFunction and TypeNodeHashFunction. | |||
2021-04-14 | Rename public and private headers in src/include. (#6352) | Aina Niemetz | |
2021-04-12 | Refactor and update copyright headers. (#6316) | Aina Niemetz | |
2021-04-09 | Rename CVC4__ header guards to CVC5__. (#6326) | Aina Niemetz | |
2021-04-01 | Rename namespace CVC5 to cvc5. (#6258) | Aina Niemetz | |
2021-03-31 | Rename namespace CVC4 to CVC5. (#6249) | Aina Niemetz | |
2021-03-29 | Eliminate the use of quantifiers engine in sygus solver (#6232) | Andrew Reynolds | |
2021-03-09 | Update copyright headers to 2021. (#6081) | Aina Niemetz | |
2021-02-22 | Eliminate 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-22 | Update 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-16 | Update copyright headers. | Aina Niemetz | |
2020-02-10 | Use example evaluation cache instead of sygus PBE (#3733) | Andrew Reynolds | |
2020-02-07 | Interface 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-21 | Evaluation unfolding for symbolic SyGuS constructors (#3483) | Andrew Reynolds | |
2019-10-14 | Apply 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-24 | Do not use __ prefix for header guards. (#2974) | Mathias Preiner | |
Fixes 2887. | |||
2019-03-26 | Update copyright headers. | Aina Niemetz | |
2018-10-03 | Add actively generated sygus enumerators (#2552) | Andrew Reynolds | |
2018-09-27 | Infrastructure for using active enumerators in sygus modules (#2547) | Andrew Reynolds | |
2018-09-18 | Move and rename sygus solver classes (#2488) | Andrew Reynolds | |
2018-07-30 | Fix several spelling errors (#2231) | FabianWolff | |
2018-06-25 | Updated copyright headers. | Aina Niemetz | |
2018-06-20 | Fix 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-25 | Reenable repair const (#1983) | Andrew Reynolds | |
2018-05-22 | Repair constants using symbolic constructors (#1960) | Andrew Reynolds | |
2018-05-21 | Refactor sygus eval unfold (#1946) | Andrew Reynolds | |
2018-05-17 | Cegis-specific infrastructure (#1933) | Andrew Reynolds | |
2018-05-17 | Internal propagation for refinement lemmas (#1932) | Andrew Reynolds | |
2018-05-03 | Make CegisUnif default to Cegis when no unif used (#1836) | Haniel Barbosa | |
2018-03-02 | Simplify sygus wrt miniscoping (#1634) | Andrew Reynolds | |
2018-03-01 | Create infrastructure for sygus modules (#1632) | Andrew Reynolds | |