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

[cvc5.git] / src / theory / quantifiers_engine.cpp

2021-02-02	Andrew Reynolds	Cleanup some includes (#5847)	blob \| commitdiff \| raw
2021-02-01	Andrew Reynolds	Eliminate PREPROCESS lemma property (#5827)	blob \| commitdiff \| raw \| diff to current
2021-01-28	Andrew Reynolds	Use standard equality engine information in quantifiers...	blob \| commitdiff \| raw \| diff to current
2021-01-27	Andrew Reynolds	(proof-new) Improvements to quantifiers engine and...	blob \| commitdiff \| raw \| diff to current
2021-01-27	Andrew Reynolds	Use term canonizer utility locally in quantifiers ...	blob \| commitdiff \| raw \| diff to current
2021-01-27	Andrew Reynolds	Use standard conflict mechanism in quantifiers state...	blob \| commitdiff \| raw \| diff to current
2021-01-26	Andrew Reynolds	Introduce quantifiers inference manager (#5821)	blob \| commitdiff \| raw \| diff to current
2021-01-26	Andrew Reynolds	Refactor quantifiers engine initialization (#5813)	blob \| commitdiff \| raw \| diff to current
2020-12-23	Andrew Reynolds	Remove quant EPR option (#5716)	blob \| commitdiff \| raw \| diff to current
2020-12-16	Andrew Reynolds	Mark quantifier instantiations as needs justify (#5684)	blob \| commitdiff \| raw \| diff to current
2020-12-01	Andrew Reynolds	More fixes for quantifier elimination (#5533)	blob \| commitdiff \| raw \| diff to current
2020-11-19	Andrew Reynolds	Enable new implementation of CEGQI based on nested...	blob \| commitdiff \| raw \| diff to current
2020-11-12	Andrew Reynolds	(proof-new) Proofs for skolemization (#5339)	blob \| commitdiff \| raw \| diff to current
2020-10-01	Mathias Preiner	Add additional ground terms to SyGuS instantiation...	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-09-15	Andrew Reynolds	Move quantifiers engine private to own file (#5053)	blob \| commitdiff \| raw \| diff to current
2020-09-08	Andrew Reynolds	Eliminate a custom use of TheorySep in quantifiers...	blob \| commitdiff \| raw \| diff to current
2020-09-03	Andrew Reynolds	Minor cleanup of quantifiers engine (#4994)	blob \| commitdiff \| raw \| diff to current
2020-09-03	Andrew Reynolds	(proof-new) Support proofs of quantifier instantiation...	blob \| commitdiff \| raw \| diff to current
2020-09-01	Haniel Barbosa	Removes old proof code (#4964)	blob \| commitdiff \| raw \| diff to current
2020-09-01	FabianWolff	Fix spelling errors (#4977)	blob \| commitdiff \| raw \| diff to current
2020-08-26	Andrew Reynolds	Connect combination engine to theory engine (#4940)	blob \| commitdiff \| raw \| diff to current
2020-08-21	Andrew Reynolds	Connect the relevance manager to TheoryEngine and use...	blob \| commitdiff \| raw \| diff to current
2020-08-18	Andrew Reynolds	Quantifiers engine stores a pointer to the master equal...	blob \| commitdiff \| raw \| diff to current
2020-08-11	Andrew Reynolds	Remove instantiation model true option (#4861)	blob \| commitdiff \| raw \| diff to current
2020-07-28	Andrew Reynolds	Use lemma property enum for OutputChannel::lemma (...	blob \| commitdiff \| raw \| diff to current
2020-07-14	Andrew Reynolds	Debug instantiations output (#4739)	blob \| commitdiff \| raw \| diff to current
2020-07-13	Andrew Reynolds	Statistics on instantiations per quantified formula...	blob \| commitdiff \| raw \| diff to current
2020-06-30	Andrew Reynolds	Simplify quantifiers strategy for when to apply last...	blob \| commitdiff \| raw \| diff to current
2020-06-16	Aina Niemetz	Update copyright headers.	blob \| commitdiff \| raw \| diff to current
2020-04-21	Andrew Reynolds	Make option names related to CEGQI consistent (#4316)	blob \| commitdiff \| raw \| diff to current
2020-04-17	Mathias Preiner	SyGuS instantiation quantifiers module (#3910)	blob \| commitdiff \| raw \| diff to current
2020-04-15	Andrew Reynolds	Abort if in conflict in enumerative instantiation ...	blob \| commitdiff \| raw \| diff to current
2020-03-11	Andrew Reynolds	Remove partial instantiation for local theory extension...	blob \| commitdiff \| raw \| diff to current
2020-03-10	Andrew Reynolds	Only register sygus terms to unfold if option is set...	blob \| commitdiff \| raw \| diff to current
2020-03-10	Andrew Reynolds	Rename sygus option name (#3977)	blob \| commitdiff \| raw \| diff to current
2020-03-10	Andrew Reynolds	Remove instantiation propagator infrastructure (#3975)	blob \| commitdiff \| raw \| diff to current
2020-02-19	Andrew Reynolds	Delay enumerative instantiation if theory engine does...	blob \| commitdiff \| raw \| diff to current
2020-02-14	Andrew Reynolds	Remove quantifiers rewrite rules infrastructure (#3754)	blob \| commitdiff \| raw \| diff to current
2019-12-17	Mathias Preiner	Generate code for options with modes. (#3561)	blob \| commitdiff \| raw \| diff to current
2019-11-27	Haniel Barbosa	Enable sygusRecFun by default and fixes SyGuS+RecFun...	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-10-30	Mathias Preiner	Unify CVC4_CHECK/CVC4_DCHECK/AlwaysAssert/Assert. ...	blob \| commitdiff \| raw \| diff to current
2019-09-18	Andrew Reynolds	Decouple fmf-bound and finite-model-find (#3297)	blob \| commitdiff \| raw \| diff to current
2019-09-17	Andrew Reynolds	Encapsulate relevant domain (#3293)	blob \| commitdiff \| raw \| diff to current
2019-09-16	Andrew Reynolds	Remove equality inference option for quantifiers (...	blob \| commitdiff \| raw \| diff to current
2019-09-12	Andrew Reynolds	Encapsulate synth engine (#3271)	blob \| commitdiff \| raw \| diff to current
2019-09-12	Andrew Reynolds	Refactoring finite bounds in Quantifiers Engine (#3261)	blob \| commitdiff \| raw \| diff to current
2019-09-11	Andrew Reynolds	Infrastructure for instantiation rewriter (#3262)	blob \| commitdiff \| raw \| diff to current
2019-09-05	Andrew Reynolds	Refactoring CEGQI interface (#3239)	blob \| commitdiff \| raw \| diff to current
2019-08-17	Andrew Reynolds	Move quantifiers relevance module inside E-matching...	blob \| commitdiff \| raw \| diff to current
2019-08-12	Andrew Reynolds	Give rewrite engine pointer to conflict-based instanti...	blob \| commitdiff \| raw \| diff to current
2019-08-08	Andrew Reynolds	Reorganize includes for quantifiers engine (#3169)	blob \| commitdiff \| raw \| diff to current
2019-08-05	Andrew Reynolds	Remove forward declarations in quantifiers engine ...	blob \| commitdiff \| raw \| diff to current
2019-08-01	Andrew Reynolds	Move some generic utilities out of quantifiers (#3139)	blob \| commitdiff \| raw \| diff to current
2019-03-26	Aina Niemetz	Update copyright headers.	blob \| commitdiff \| raw \| diff to current
2018-12-11	Andrew Reynolds	Remove alternate versions of mbqi (#2742)	blob \| commitdiff \| raw \| diff to current
2018-09-18	Andrew Reynolds	Move and rename sygus solver classes (#2488)	blob \| commitdiff \| raw \| diff to current
2018-09-18	Andrew Reynolds	Clean remaining references to getNextDecisionRequest...	blob \| commitdiff \| raw \| diff to current
2018-09-17	Andrew Reynolds	Move inst_strategy_cbqi to inst_strategy_cegqi (#2477)	blob \| commitdiff \| raw \| diff to current
2018-09-10	Andrew Reynolds	Squash implementation of counterexample-guided instanti...	blob \| commitdiff \| raw \| diff to current
2018-08-28	Andrew Reynolds	Split term canonize utility to own file and document...	blob \| commitdiff \| raw \| diff to current
2018-08-25	Andrew Reynolds	Clean up quantifiers engine initialization. (#2371)	blob \| commitdiff \| raw \| diff to current
2018-08-22	Andrew Reynolds	More unused code elimination (#2358)	blob \| commitdiff \| raw \| diff to current
2018-08-21	Andrew Reynolds	More unused code elimination (#2339)	blob \| commitdiff \| raw \| diff to current
2018-07-03	Andrew Reynolds	Remove miscellaneous dead and unused code from quantifi...	blob \| commitdiff \| raw \| diff to current
2018-06-28	Andrew Reynolds	Split and document ceg theory instantiators (#2094)	blob \| commitdiff \| raw \| diff to current
2018-06-26	Andrew Reynolds	Remove unnecessary code in register quantifier internal...	blob \| commitdiff \| raw \| diff to current
2018-06-25	Aina Niemetz	Updated copyright headers.	blob \| commitdiff \| raw \| diff to current
2018-06-01	Andrew Reynolds	Fix quantifiers conflict lemma handling (#2043)	blob \| commitdiff \| raw \| diff to current
2018-06-01	Andrew Reynolds	Reduce before preregister. (#2025)	blob \| commitdiff \| raw \| diff to current
2018-05-30	Andrew Reynolds	Fixes for quantifiers + incremental (#2009)	blob \| commitdiff \| raw \| diff to current
2018-05-27	Andrew Reynolds	Fix cegqi assertions for quantified non-linear cases...	blob \| commitdiff \| raw \| diff to current
2018-05-21	Andrew Reynolds	Refactor sygus eval unfold (#1946)	blob \| commitdiff \| raw \| diff to current
2018-03-23	Andrew Reynolds	Remove unused code (#1700)	blob \| commitdiff \| raw \| diff to current
2018-03-06	Andrew Reynolds	Simplify initialization of quantifiers engine (#1641)	blob \| commitdiff \| raw \| diff to current
2018-02-14	Andrew Reynolds	Quantifiers subdirectories (#1608)	blob \| commitdiff \| raw \| diff to current
2018-02-02	Haniel Barbosa	Option to check solutions produced by SyGuS solver...	blob \| commitdiff \| raw \| diff to current
2017-12-08	Andrew Reynolds	Make collect model info return a Bool (#1421)	blob \| commitdiff \| raw \| diff to current
2017-11-25	Andrew Reynolds	(Refactor) Instantiate utility (#1387)	blob \| commitdiff \| raw \| diff to current
2017-11-15	Andrew Reynolds	Make QEffort an enum (#1366)	blob \| commitdiff \| raw \| diff to current
2017-11-09	Andrew Reynolds	Decouple sygus term database and term database. (...	blob \| commitdiff \| raw \| diff to current
2017-11-02	Andrew Reynolds	(Move-only) Split quant util (#1306)	blob \| commitdiff \| raw \| diff to current
2017-11-01	Andrew Reynolds	(Refactor) Split term util (#1303)	blob \| commitdiff \| raw \| diff to current
2017-10-28	Andrew Reynolds	(Move only) Move enumerative instantiation strategy...	blob \| commitdiff \| raw \| diff to current
2017-10-28	Andrew Reynolds	Document term db (#1220)	blob \| commitdiff \| raw \| diff to current
2017-10-27	Andrew Reynolds	Refactor theory model (#1236)	blob \| commitdiff \| raw \| diff to current
2017-10-10	Andres Noetzli	Fix memory leak in quantifiers engine (#1219)	blob \| commitdiff \| raw \| diff to current
2017-10-10	Andrew Reynolds	Split term database (#1206)	blob \| commitdiff \| raw \| diff to current
2017-09-29	Andrew Reynolds	Simplify representation of inversion Skolems for bv...	blob \| commitdiff \| raw \| diff to current
2017-09-27	Andrew Reynolds	Minor fixes for partial quantifier elimination. (#1147)	blob \| commitdiff \| raw \| diff to current
2017-08-24	Andrew Reynolds	Merge pull request #191 from timothy-king/cleanup-regexp	blob \| commitdiff \| raw \| diff to current
2017-08-17	ajreynol	Add mbqi interleave option, change option fs-inst to...	blob \| commitdiff \| raw \| diff to current
2017-07-21	Tim King	Merge branch 'master' into cleanup-regexp	blob \| commitdiff \| raw \| diff to current
2017-07-21	Tim King	Moving from the gnu extensions for hash maps to the...	blob \| commitdiff \| raw \| diff to current
2017-07-07	Mathias Preiner	Update copyright headers.	blob \| commitdiff \| raw \| diff to current
2017-06-01	ajreynol	Minor optimizations related to cbqi.	blob \| commitdiff \| raw \| diff to current
2017-05-17	Clark Barrett	Merge pull request #155 from makaimann/conditional_coverage	blob \| commitdiff \| raw \| diff to current
2017-05-16	Andrew Reynolds	Merge pull request #156 from 4tXJ7f/fix_safe_print	blob \| commitdiff \| raw \| diff to current
next

RSS Atom