summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/sygus/sygus_pbe.cpp
AgeCommit message (Collapse)Author
2021-04-12Refactor and update copyright headers. (#6316)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-09Some more cleanup of includes (#6083)Gereon Kremer
This PR does some more cleanup of the includes.
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-08-25Replace 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-16Update copyright headers.Aina Niemetz
2020-02-26Initial work towards -Wshadow (#3817)Andrew Reynolds
2020-02-10Use example evaluation cache instead of sygus PBE (#3733)Andrew Reynolds
2020-02-03Example inference utility (#3670)Andrew Reynolds
2020-01-22Fix check for subtypes in sygus PBE (#3640)Andrew Reynolds
2020-01-14Generalize example-based sym breaking to conjectures with constant function ↵Andrew Reynolds
apps (#3605)
2020-01-07Update any-constant and normalization policies for sygus grammars (#3583)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-08-23 Pass synthesis conjecture to sygus modules (#3212)Andrew Reynolds
2019-03-26Update copyright headers.Aina Niemetz
2018-12-04Apply extended rewriting on PBE static symmetry breaking. (#2735)Andrew Reynolds
2018-11-21Cache evaluations for PBE (#2699)Andrew Reynolds
2018-11-21Quickly 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-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-10-05Update default options for sygus (#2586)Andrew Reynolds
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-24Allow partial models for multiple sygus enumerators (#2499)Andrew Reynolds
2018-09-18Move and rename sygus solver classes (#2488)Andrew Reynolds
2018-08-03Eliminate option for sygus UF evaluation functions (#2262)Andrew Reynolds
2018-07-23Fix warning in sygus PBE (#2190)Andrew Reynolds
2018-07-18 sygusComp2018: pbe multi-enumerator fairness option (#2178)Andrew Reynolds
2018-06-25Updated copyright headers.Aina Niemetz
2018-05-28Builtin evaluation functions for sygus (#1991)Andrew Reynolds
2018-05-17Internal propagation for refinement lemmas (#1932)Andrew Reynolds
2018-05-16Improve 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-10Exclude Boolean connectives from ITE conditions in SygusUnifStrat (#1900)Andrew Reynolds
2018-05-10Static learn redundant operators in CegisUnif (#1899)Haniel Barbosa
2018-05-09Better option names for PBE (#1891)Andrew Reynolds
2018-04-29Allow multiple functions in sygus unif approaches (#1831)Andrew Reynolds
2018-03-27Make sygus pbe use sygus unif utility (#1724)Andrew Reynolds
2018-03-27Make sygus unif utility (#1720)Andrew Reynolds
2018-03-26Documentation and simplifications for PBE (#1677)Andrew Reynolds
2018-03-06Refactor symmetry breaking in datatypes sygus (#1640)Andrew Reynolds
2018-03-01Create infrastructure for sygus modules (#1632)Andrew Reynolds
2018-02-14Quantifiers subdirectories (#1608)Andrew Reynolds
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback