summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/sygus/synth_engine.cpp
AgeCommit message (Expand)Author
2020-08-20Split QuantElimSolver from SmtEngine (#4919)Andrew Reynolds
2020-07-07Transfer ownership of internal Options from NodeManager to SmtEngine (#4682)Andrew Reynolds
2020-06-29Make ExprManager constructor private (#4669)Andres Noetzli
2020-06-16Update copyright headers.Aina Niemetz
2020-04-20Make option names related to CEGQI consistent (#4316)Andrew Reynolds
2020-03-20Handle failures for sygus QE preprocess (#4072)Andrew Reynolds
2020-03-05Enable -Wshadow and fix warnings. (#3909)Mathias Preiner
2020-03-03Standardize the interface for SMT engine subsolvers (#3836)Andrew Reynolds
2020-02-19Delay enumerative instantiation if theory engine does not need check (#3774)Andrew Reynolds
2020-01-31Refactor sygus stats (#3684)Andrew Reynolds
2019-11-27Enable sygusRecFun by default and fixes SyGuS+RecFun+HO issues (#3502)Haniel Barbosa
2019-11-21Evaluation unfolding for symbolic SyGuS constructors (#3483)Andrew Reynolds
2019-11-06Support for SyGuS PBE + recursive functions (#3433)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-08-14Call separate SMT engine for single invocation sygus (#3151)Andrew Reynolds
2019-08-05Remove forward declarations in quantifiers engine (#3156)Andrew Reynolds
2019-03-26Update copyright headers.Aina Niemetz
2019-03-19Sygus abduction feature (#2744)Andrew Reynolds
2018-11-27Improve cegqi engine trace. (#2714)Andrew Reynolds
2018-10-19Sygus streaming non-implied predicates (#2660)Andrew Reynolds
2018-10-09 Support for basic actively-generated enumerators (#2606)Andrew Reynolds
2018-10-09Allow multiple synthesis conjectures. (#2593)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