summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/sygus/synth_engine.cpp
AgeCommit message (Expand)Author
2021-03-31Rename namespace CVC4 to CVC5. (#6249)Aina Niemetz
2021-03-31Eliminate dependencies on quantifiers engine in internal quantifiers code (#6...Andrew Reynolds
2021-03-30Miscellaneous elimination of dependencies on quantifiers engine (#6238)Andrew Reynolds
2021-03-29Eliminate the use of quantifiers engine in sygus solver (#6232)Andrew Reynolds
2021-03-26Pass term registry to quantifiers modules (#6216)Andrew Reynolds
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
2021-02-22Move quantifiers attributes to quantifiers registry (#5929)Andrew Reynolds
2021-02-17Add InferenceId to buffered inference manager (#5911)Gereon Kremer
2021-02-08Use quantifiers inference manager for lemma management (#5867)Andrew Reynolds
2021-02-04Introduce quantifiers registry utility (#5829)Andrew Reynolds
2021-02-02Cleanup some includes (#5847)Andrew Reynolds
2021-01-26Use standard conflict mechanism in quantifiers state (#5822)Andrew Reynolds
2021-01-26Introduce quantifiers inference manager (#5821)Andrew Reynolds
2021-01-26Refactor quantifiers engine initialization (#5813)Andrew Reynolds
2020-12-02Update copyright headers.Aina Niemetz
2020-11-12Simplify sygus solver and sygus stream (#5389)Andrew Reynolds
2020-11-02Move sygus qe preproc to its own file (#5375)Andrew Reynolds
2020-09-27Fix sygus quantifier elimination preprocess for multiple functions (#5130)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-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