summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/sygus/synth_conjecture.h
AgeCommit message (Expand)Author
2021-07-14Move synthesis verification check to own file (#6882)Andrew Reynolds
2021-07-01Add recursive function definitions to subsolver in sygus (#6824)Andrew Reynolds
2021-05-21Update to sygus standard output for check-synth responses (#6521)Andrew Reynolds
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-23Replace old sygus term reconstruction algorithm with a new one. (#5779)Abdalrhman Mohamed
2021-03-09Some more cleanup of includes (#6083)Gereon Kremer
2021-03-09Update copyright headers to 2021. (#6081)Aina Niemetz
2021-02-22Move quantifiers attributes to quantifiers registry (#5929)Andrew Reynolds
2021-02-08Use quantifiers inference manager for lemma management (#5867)Andrew Reynolds
2021-01-26Refactor quantifiers engine initialization (#5813)Andrew Reynolds
2020-11-12Simplify sygus solver and sygus stream (#5389)Andrew Reynolds
2020-11-05Split sygus template inference to its own file (#5388)Andrew Reynolds
2020-09-25Make sygus refinement step more robust to unevaluatable counterexamples (#5102)Andrew Reynolds
2020-09-22Update copyright header script to support CMake and Python files (#5067)Mathias Preiner
2020-06-16Update copyright headers.Aina Niemetz
2020-04-16SyGuS instantiation quantifiers module (#3910)Mathias Preiner
2020-02-24Fixes for quantifiers documentation (#3811)Andrew Reynolds
2020-02-07Interface for example evaluation cache utilities (#3726)Andrew Reynolds
2020-01-31Refactor sygus stats (#3684)Andrew Reynolds
2019-12-06New algorithm for interpolation and abduction based on unsat cores (#3255)Andrew Reynolds
2019-11-04Make check synth solution robust to auxiliary assertions (#3432)Andrew Reynolds
2019-11-04Make getSynthSolution return a Bool (#3306)Andrew Reynolds
2019-09-12Encapsulate synth engine (#3271)Andrew Reynolds
2019-09-04Explicitly pass current sygus solution to exclude (#3209)Andrew Reynolds
2019-08-14Call separate SMT engine for single invocation sygus (#3151)Andrew Reynolds
2019-08-05Remove forward declarations in quantifiers engine (#3156)Andrew Reynolds
2019-04-24Do not use __ prefix for header guards. (#2974)Mathias Preiner
2019-03-26Update copyright headers.Aina Niemetz
2018-11-29 Infrastructure for sygus side conditions (#2729)Andrew Reynolds
2018-11-05Allow partial models with optimized sygus enumeration (#2682)Andrew Reynolds
2018-10-09 Support for basic actively-generated enumerators (#2606)Andrew Reynolds
2018-10-09Allow multiple synthesis conjectures. (#2593)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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback