Age | Commit message (Collapse) | Author | |
---|---|---|---|
2021-04-12 | Refactor and update copyright headers. (#6316) | 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 | Some more cleanup of includes (#6083) | Gereon Kremer | |
This PR does some more cleanup of the includes. | |||
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-08-25 | Replace Expr-level datatype with Node-level DType (#4875) | Andrew Reynolds | |
This PR makes two simultaneous changes: The new API uses Node-level DType instead of Expr-level Datatype. This required converting 2 of the last remaining calls in the parser that used Expr to use the new API. Internally constructed datatypes (e.g. for sygus) use Node-level DType instead of Expr-level Datatype. Note this required moving a block of code for handling a corner case of sygus from Datatype -> DType. This PR removes : ExprManger::mkDatatypeType. The Expr-level datatype itself. This PR removes all references to its include file. It also updates one remaining unit test from Expr -> Node. This PR will enable further removal of other datatype-specific things in the Expr layer. | |||
2020-06-16 | Update copyright headers. | Aina Niemetz | |
2020-02-26 | Initial work towards -Wshadow (#3817) | Andrew Reynolds | |
2020-02-10 | Use example evaluation cache instead of sygus PBE (#3733) | Andrew Reynolds | |
2020-02-03 | Example inference utility (#3670) | Andrew Reynolds | |
2020-01-22 | Fix check for subtypes in sygus PBE (#3640) | Andrew Reynolds | |
2020-01-14 | Generalize example-based sym breaking to conjectures with constant function ↵ | Andrew Reynolds | |
apps (#3605) | |||
2020-01-07 | Update any-constant and normalization policies for sygus grammars (#3583) | Andrew Reynolds | |
2019-10-30 | Unify CVC4_CHECK/CVC4_DCHECK/AlwaysAssert/Assert. (#3366) | Mathias Preiner | |
2019-10-17 | Move datatype utility functions to own file (#3397) | Andrew Reynolds | |
2019-08-23 | Pass synthesis conjecture to sygus modules (#3212) | Andrew Reynolds | |
2019-03-26 | Update copyright headers. | Aina Niemetz | |
2018-12-04 | Apply extended rewriting on PBE static symmetry breaking. (#2735) | Andrew Reynolds | |
2018-11-21 | Cache evaluations for PBE (#2699) | Andrew Reynolds | |
2018-11-21 | Quickly recognize when PBE conjectures are infeasible (#2718) | Andrew Reynolds | |
Recognizes when the conjecture has conflicting I/O pairs. Also includes a minor change to the default behavior of PBE. This change broke a delicate regression array_search_2, which I fixed by adding some additional options to make it more robust. After this PR, we immediately find 4/7 unsolved in PBE strings of sygusComp 2018 to be infeasible. | |||
2018-11-06 | Incorporate static PBE symmetry breaking lemmas into SygusEnumerator (#2690) | Andrew Reynolds | |
2018-11-05 | Change default sygus enumeration mode to auto (#2689) | Andrew Reynolds | |
2018-10-31 | Add optimized sygus enumeration (#2677) | Andrew Reynolds | |
2018-10-09 | Support for basic actively-generated enumerators (#2606) | Andrew Reynolds | |
2018-10-05 | Update default options for sygus (#2586) | Andrew Reynolds | |
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-24 | Allow partial models for multiple sygus enumerators (#2499) | Andrew Reynolds | |
2018-09-18 | Move and rename sygus solver classes (#2488) | Andrew Reynolds | |
2018-08-03 | Eliminate option for sygus UF evaluation functions (#2262) | Andrew Reynolds | |
2018-07-23 | Fix warning in sygus PBE (#2190) | Andrew Reynolds | |
2018-07-18 | sygusComp2018: pbe multi-enumerator fairness option (#2178) | Andrew Reynolds | |
2018-06-25 | Updated copyright headers. | Aina Niemetz | |
2018-05-28 | Builtin evaluation functions for sygus (#1991) | Andrew Reynolds | |
2018-05-17 | Internal propagation for refinement lemmas (#1932) | Andrew Reynolds | |
2018-05-16 | Improve the separation resolution scheme in cegis unif (#1931) | Andrew Reynolds | |
2018-05-14 | Incorporating dynamic condition enumeration into cegis unif (#1916) | Andrew Reynolds | |
2018-05-10 | Exclude Boolean connectives from ITE conditions in SygusUnifStrat (#1900) | Andrew Reynolds | |
2018-05-10 | Static learn redundant operators in CegisUnif (#1899) | Haniel Barbosa | |
2018-05-09 | Better option names for PBE (#1891) | Andrew Reynolds | |
2018-04-29 | Allow multiple functions in sygus unif approaches (#1831) | Andrew Reynolds | |
2018-03-27 | Make sygus pbe use sygus unif utility (#1724) | Andrew Reynolds | |
2018-03-27 | Make sygus unif utility (#1720) | Andrew Reynolds | |
2018-03-26 | Documentation and simplifications for PBE (#1677) | Andrew Reynolds | |
2018-03-06 | Refactor symmetry breaking in datatypes sygus (#1640) | Andrew Reynolds | |
2018-03-01 | Create infrastructure for sygus modules (#1632) | Andrew Reynolds | |
2018-02-14 | Quantifiers subdirectories (#1608) | Andrew Reynolds | |