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

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

2021-01-26	Andrew Reynolds	Introduce quantifiers inference manager (#5821)	blob \| commitdiff \| raw
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-15	Andrew Reynolds	Move trigger trie to own file (#5680)	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-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-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-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-06-16	Aina Niemetz	Update copyright headers.	blob \| commitdiff \| raw \| diff to current
2020-03-20	Andrew Reynolds	Make handling of illegal internal representatives in...	blob \| commitdiff \| raw \| diff to current
2020-02-19	Andrew Reynolds	Delay enumerative instantiation if theory engine does...	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-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-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-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-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-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-07-03	Andrew Reynolds	Remove miscellaneous dead and unused code from quantifi...	blob \| commitdiff \| raw \| diff to current
2018-06-25	Aina Niemetz	Updated copyright headers.	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-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-02	Haniel Barbosa	Option to check solutions produced by SyGuS solver...	blob \| commitdiff \| raw \| diff to current
2017-12-06	Andres Noetzli	Remove CDChunkList (#1414)	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-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-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-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
2017-05-15	Andrew Reynolds	Merge pull request #159 from 4tXJ7f/fix_set_types	blob \| commitdiff \| raw \| diff to current
2017-05-15	Andrew Reynolds	Merge pull request #158 from 4tXJ7f/fix_sets_rewriter	blob \| commitdiff \| raw \| diff to current
2017-05-15	Andrew Reynolds	Merge pull request #157 from 4tXJ7f/fix_iterator	blob \| commitdiff \| raw \| diff to current
2017-05-15	ajreynol	Make conflict-based instantiation abort if a ground...	blob \| commitdiff \| raw \| diff to current
2017-03-29	ajreynol	Add quantifiers options related to model and master...	blob \| commitdiff \| raw \| diff to current
2017-03-27	Clark Barrett	Merge pull request #137 from 4tXJ7f/throw_quals	blob \| commitdiff \| raw \| diff to current
2017-03-27	Tim King	Making ppNotifyAssertions take a const vector.	blob \| commitdiff \| raw \| diff to current
2017-01-04	Andrew Reynolds	Merge pull request #122 from 4tXJ7f/fix_lfsc_str	blob \| commitdiff \| raw \| diff to current
2017-01-04	guykatzz	Merge pull request #120 from 4tXJ7f/fix_f_pp_holes	blob \| commitdiff \| raw \| diff to current
2017-01-04	Andrew Reynolds	Merge pull request #121 from 4tXJ7f/fix_lfsc_mem_leaks	blob \| commitdiff \| raw \| diff to current
2016-12-29	Tim King	Adding a destructor to InstantiationNotify.	blob \| commitdiff \| raw \| diff to current
2016-12-07	guykatzz	Merge branch 'master' of https://github.com/CVC4/CVC4	blob \| commitdiff \| raw \| diff to current
2016-12-07	ajreynol	Refactoring, generalization of bounded inference module...	blob \| commitdiff \| raw \| diff to current
2016-11-21	ajreynol	Refactoring related to track instantiation option.	blob \| commitdiff \| raw \| diff to current
2016-11-03	ajreynol	Add priorities to getNextDecision. Properly handle...	blob \| commitdiff \| raw \| diff to current
2016-10-28	ajreynol	Add get instantiations utilities to API.	blob \| commitdiff \| raw \| diff to current
2016-10-11	Paul Meng	Merge branch 'origin' of https://github.com/CVC4/CVC4.git	blob \| commitdiff \| raw \| diff to current
2016-10-01	Tim King	Merge pull request #93 from timothy-king/clang-format	blob \| commitdiff \| raw \| diff to current
2016-09-29	ajreynol	Address some coverity warnings, add another stat.	blob \| commitdiff \| raw \| diff to current
2016-09-29	ajreynol	Minor cleanup and additions to quantifiers statistics.	blob \| commitdiff \| raw \| diff to current
2016-09-14	ajreynol	Lemma cache in theory sep. Minor optimization for sets...	blob \| commitdiff \| raw \| diff to current
2016-09-02	Tim King	Merge pull request #91 from timothy-king/no-throw	blob \| commitdiff \| raw \| diff to current
2016-09-01	ajreynol	Updates to cbqi. New strategy --cbqi-nested-qe to...	blob \| commitdiff \| raw \| diff to current
2016-08-26	ajreynol	Basic support for EPR+CBQI. Minor cleanup.	blob \| commitdiff \| raw \| diff to current
2016-08-25	ajreynol	Minor cleanup preprocessing, add ppNotifyAssertions.	blob \| commitdiff \| raw \| diff to current
2016-08-24	PaulMeng	Merge remote-tracking branch 'origin/master'	blob \| commitdiff \| raw \| diff to current
2016-07-26	Guy	Merge branch 'master' of https://github.com/CVC4/CVC4	blob \| commitdiff \| raw \| diff to current
2016-07-26	ajreynol	Add option to minimize sygus solutions based on using...	blob \| commitdiff \| raw \| diff to current
2016-07-19	ajreynol	Add infrastructure for tracking instantiation lemmas...	blob \| commitdiff \| raw \| diff to current
2016-07-05	PaulMeng	Merge branch 'master' of https://github.com/CVC4/CVC4.git	blob \| commitdiff \| raw \| diff to current
2016-05-15	ajreynol	Work on --sygus-direct-eval. Minor optimizations, updat...	blob \| commitdiff \| raw \| diff to current
2016-05-06	ajreynol	Minor clean up, fixes related to sygus.	blob \| commitdiff \| raw \| diff to current
2016-05-05	ajreynol	Compute term indices lazily in TermDb. Optimization...	blob \| commitdiff \| raw \| diff to current
2016-04-28	ajreynol	More work on inst propagate. Optimization for qcf...	blob \| commitdiff \| raw \| diff to current
2016-04-20	PaulMeng	update from the master	blob \| commitdiff \| raw \| diff to current
2016-04-13	ajreynol	Minor improvements for alpha equivalence and partial...	blob \| commitdiff \| raw \| diff to current
2016-04-12	ajreynol	Optimizations for QCF to check relevant domain of varia...	blob \| commitdiff \| raw \| diff to current
2016-04-10	ajreynol	More work on instantiation propagation. Enable external...	blob \| commitdiff \| raw \| diff to current
2016-04-09	Guy	Merge branch 'master' of https://github.com/CVC4/CVC4	blob \| commitdiff \| raw \| diff to current
2016-04-09	ajreynol	Minor refactoring of entailment tests and quantifiers...	blob \| commitdiff \| raw \| diff to current
2016-04-07	ajreynol	Refactor trigger selection, revisions to --relational...	blob \| commitdiff \| raw \| diff to current
next

RSS Atom