git.libre-soc.org Git - cvc5.git/history - src/theory/quantifiers/sygus/synth

[cvc5.git] / src / theory / quantifiers / sygus / synth_conjecture.h

2021-02-08	Andrew Reynolds	Use quantifiers inference manager for lemma management...	blob \| commitdiff \| raw
2021-01-26	Andrew Reynolds	Refactor quantifiers engine initialization (#5813)	blob \| commitdiff \| raw \| diff to current
2020-11-12	Andrew Reynolds	Simplify sygus solver and sygus stream (#5389)	blob \| commitdiff \| raw \| diff to current
2020-11-06	Andrew Reynolds	Split sygus template inference to its own file (#5388)	blob \| commitdiff \| raw \| diff to current
2020-09-25	Andrew Reynolds	Make sygus refinement step more robust to unevaluatable...	blob \| commitdiff \| raw \| diff to current
2020-09-22	Mathias Preiner	Update copyright header script to support CMake and...	blob \| commitdiff \| raw \| diff to current
2020-06-16	Aina Niemetz	Update copyright headers.	blob \| commitdiff \| raw \| diff to current
2020-04-17	Mathias Preiner	SyGuS instantiation quantifiers module (#3910)	blob \| commitdiff \| raw \| diff to current
2020-02-24	Andrew Reynolds	Fixes for quantifiers documentation (#3811)	blob \| commitdiff \| raw \| diff to current
2020-02-08	Andrew Reynolds	Interface for example evaluation cache utilities (...	blob \| commitdiff \| raw \| diff to current
2020-01-31	Andrew Reynolds	Refactor sygus stats (#3684)	blob \| commitdiff \| raw \| diff to current
2019-12-06	Andrew Reynolds	New algorithm for interpolation and abduction based...	blob \| commitdiff \| raw \| diff to current
2019-11-04	Andrew Reynolds	Make check synth solution robust to auxiliary assertion...	blob \| commitdiff \| raw \| diff to current
2019-11-04	Andrew Reynolds	Make getSynthSolution return a Bool (#3306)	blob \| commitdiff \| raw \| diff to current
2019-09-12	Andrew Reynolds	Encapsulate synth engine (#3271)	blob \| commitdiff \| raw \| diff to current
2019-09-05	Andrew Reynolds	Explicitly pass current sygus solution to exclude ...	blob \| commitdiff \| raw \| diff to current
2019-08-14	Andrew Reynolds	Call separate SMT engine for single invocation sygus...	blob \| commitdiff \| raw \| diff to current
2019-08-05	Andrew Reynolds	Remove forward declarations in quantifiers engine ...	blob \| commitdiff \| raw \| diff to current
2019-04-24	Mathias Preiner	Do not use __ prefix for header guards. (#2974)	blob \| commitdiff \| raw \| diff to current
2019-03-26	Aina Niemetz	Update copyright headers.	blob \| commitdiff \| raw \| diff to current
2018-11-29	Andrew Reynolds	Infrastructure for sygus side conditions (#2729)	blob \| commitdiff \| raw \| diff to current
2018-11-05	Andrew Reynolds	Allow partial models with optimized sygus enumeration...	blob \| commitdiff \| raw \| diff to current
2018-10-09	Andrew Reynolds	Support for basic actively-generated enumerators ...	blob \| commitdiff \| raw \| diff to current
2018-10-09	Andrew Reynolds	Allow multiple synthesis conjectures. (#2593)	blob \| commitdiff \| raw \| diff to current
2018-10-03	Andrew Reynolds	Add actively generated sygus enumerators (#2552)	blob \| commitdiff \| raw \| diff to current
2018-09-27	Andrew Reynolds	Infrastructure for using active enumerators in sygus...	blob \| commitdiff \| raw \| diff to current
2018-09-25	Andrew Reynolds	Allow partial models for multiple sygus enumerators...	blob \| commitdiff \| raw \| diff to current
2018-09-18	Andrew Reynolds	Move and rename sygus solver classes (#2488)	blob \| commitdiff \| raw \| diff to current

RSS Atom