git.libre-soc.org Git - cvc5.git/history - src/prop/prop

[cvc5.git] / src / prop / prop_engine.cpp

2021-02-11	Haniel Barbosa	[proof-new] Adding a proof-producing ensure literal...	blob \| commitdiff \| raw
2021-01-28	Andrew Reynolds	Simplify lemma interface (#5819)	blob \| commitdiff \| raw \| diff to current
2021-01-28	Andrew Reynolds	Always theory-preprocess lemmas (#5817)	blob \| commitdiff \| raw \| diff to current
2021-01-24	Andrew Reynolds	Add interface for getting preprocessed term (#5798)	blob \| commitdiff \| raw \| diff to current
2021-01-11	Andrew Reynolds	Merge theory registrar and theory proxy (#5758)	blob \| commitdiff \| raw \| diff to current
2021-01-05	Andrew Reynolds	Remove a few miscellaneous references to the expr layer...	blob \| commitdiff \| raw \| diff to current
2020-12-24	Haniel Barbosa	[proof-new] Only use old proofs for unsat cores if...	blob \| commitdiff \| raw \| diff to current
2020-12-23	Andrew Reynolds	Add option to track and notify from CNF stream (#5708)	blob \| commitdiff \| raw \| diff to current
2020-12-21	Andrew Reynolds	Move ownership of theory preprocessor to TheoryProxy...	blob \| commitdiff \| raw \| diff to current
2020-12-14	Haniel Barbosa	[proof-new] Make prop engine proof producing (#5667)	blob \| commitdiff \| raw \| diff to current
2020-12-14	Haniel Barbosa	[proof-new] Updating interfaces between prop engine...	blob \| commitdiff \| raw \| diff to current
2020-12-11	Haniel Barbosa	[proof-new] Updating theory proxy to new proof infrast...	blob \| commitdiff \| raw \| diff to current
2020-12-09	Andrew Reynolds	Make decision engine independent of AssertionsPipeline...	blob \| commitdiff \| raw \| diff to current
2020-12-03	Andrew Reynolds	(proof-new) Updates to SMT proof manager and SmtEngine...	blob \| commitdiff \| raw \| diff to current
2020-09-25	Haniel Barbosa	Cleaning and documenting cnf stream (#5134)	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-16	Abdalrhman Mohamed	Dump commands in internal code using command printing...	blob \| commitdiff \| raw \| diff to current
2020-09-01	Haniel Barbosa	Removes old proof code (#4964)	blob \| commitdiff \| raw \| diff to current
2020-08-15	Andrew Reynolds	Add finishInit method to PropEngine (#4895)	blob \| commitdiff \| raw \| diff to current
2020-07-30	Andres Noetzli	Python API: Add support for sequences (#4757)	blob \| commitdiff \| raw \| diff to current
2020-06-16	Aina Niemetz	Update copyright headers.	blob \| commitdiff \| raw \| diff to current
2020-04-10	Andrew Reynolds	Towards proper use of resource managers (#4233)	blob \| commitdiff \| raw \| diff to current
2020-03-31	Andrew Reynolds	Remove replay and use-theory options and idl (#4186)	blob \| commitdiff \| raw \| diff to current
2020-03-27	Andres Noetzli	Fix issues with unsat cores and reset-assertions (...	blob \| commitdiff \| raw \| diff to current
2020-03-10	Aina Niemetz	Fix issue with reset-assertions. (#3988)	blob \| commitdiff \| raw \| diff to current
2020-03-05	Aina Niemetz	Move ownership of DecisionEngine into PropEngine. ...	blob \| commitdiff \| raw \| diff to current
2020-03-05	Aina Niemetz	Revert "Move ownership of DecisionEngine into PropEngin...	blob \| commitdiff \| raw \| diff to current
2020-03-05	Andrew Reynolds	Move ownership of DecisionEngine into PropEngine. ...	blob \| commitdiff \| raw \| diff to current
2020-02-26	Andres Noetzli	Remove portfolio leftovers (#3821)	blob \| commitdiff \| raw \| diff to current
2020-02-20	Mathias Preiner	resource manager: Add statistic for every resource...	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-07	Andrew Reynolds	Remove portfolio (#3236)	blob \| commitdiff \| raw \| diff to current
2019-03-26	Aina Niemetz	Update copyright headers.	blob \| commitdiff \| raw \| diff to current
2018-08-17	Andrew Reynolds	Remove support for flipDecision (#2319)	blob \| commitdiff \| raw \| diff to current
2018-06-25	Aina Niemetz	Updated copyright headers.	blob \| commitdiff \| raw \| diff to current
2018-06-09	Andres Noetzli	Reset decisions at SAT level after solving (#2059)	blob \| commitdiff \| raw \| diff to current
2018-01-16	Tim King	Removing more miscellaneous throw specifiers. (#1509)	blob \| commitdiff \| raw \| diff to current
2017-07-07	Mathias Preiner	Update copyright headers.	blob \| commitdiff \| raw \| diff to current
2016-08-24	PaulMeng	Merge remote-tracking branch 'origin/master'	blob \| commitdiff \| raw \| diff to current
2016-07-25	Guy	Merge branch 'master' of https://github.com/CVC4/CVC4	blob \| commitdiff \| raw \| diff to current
2016-07-25	Guy	Proper handling for lemmas that are conjuncts:	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-06-06	guykatzz	Merge pull request #85 from CVC4/master_for_proof_merge	blob \| commitdiff \| raw \| diff to current
2016-06-02	Guy	Merge from proof branch	blob \| commitdiff \| raw \| diff to current
2016-06-02	Guy	Revert "Merging proof branch"	blob \| commitdiff \| raw \| diff to current
2016-06-02	Guy	Merging proof branch	blob \| commitdiff \| raw \| diff to current
2016-04-20	PaulMeng	update from the master	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-04	Tim King	Updating the copyright headers and scripts.	blob \| commitdiff \| raw \| diff to current
2016-03-23	guykatzz	Merge pull request #82 from CVC4/master_for_merge	blob \| commitdiff \| raw \| diff to current
2016-03-23	Guy	squash-merge from proof branch	blob \| commitdiff \| raw \| diff to current
2016-02-02	Tim King	Moving dump., command., model.*, and ite_removal...	blob \| commitdiff \| raw \| diff to current
2016-01-28	Tim King	Adding listeners to Options.	blob \| commitdiff \| raw \| diff to current
2016-01-27	Liana Hadarean	Merged bit-vector and uf proof branch.	blob \| commitdiff \| raw \| diff to current
2016-01-09	Tim King	Adding a new Listener utility class. Changing the Resou...	blob \| commitdiff \| raw \| diff to current
2016-01-09	Tim King	Removing StatisticsRegistry's static functions current...	blob \| commitdiff \| raw \| diff to current
2016-01-06	Tim King	Add SmtGlobals Class	blob \| commitdiff \| raw \| diff to current
2015-12-30	Tim King	Shuffling around public vs. private headers	blob \| commitdiff \| raw \| diff to current
2015-12-15	Tim King	Refactoring Options Handler & Library Cycle Breaking	blob \| commitdiff \| raw \| diff to current
2015-05-29	lianah	changed resource step options to unsigned	blob \| commitdiff \| raw \| diff to current
2015-05-28	Liana Hadarean	added options for controlling resource step-count for...	blob \| commitdiff \| raw \| diff to current
2014-11-27	Tianyi Liang	Merge branch 'master' of github.com:tiliang/CVC4	blob \| commitdiff \| raw \| diff to current
2014-11-17	Liana Hadarean	Resource-limiting work.	blob \| commitdiff \| raw \| diff to current
2014-11-10	Morgan Deters	Merge branch '1.4.x'	blob \| commitdiff \| raw \| diff to current
2014-11-07	Morgan Deters	Merge branch '1.4.x'	blob \| commitdiff \| raw \| diff to current
2014-11-07	Morgan Deters	Merge branch '1.4.x'	blob \| commitdiff \| raw \| diff to current
2014-11-07	Morgan Deters	Merge branch '1.4.x'	blob \| commitdiff \| raw \| diff to current
2014-11-05	Morgan Deters	Merge branch '1.4.x'	blob \| commitdiff \| raw \| diff to current
2014-10-17	Morgan Deters	Merge branch '1.4.x'	blob \| commitdiff \| raw \| diff to current
2014-10-16	Morgan Deters	Merge branch '1.4.x'	blob \| commitdiff \| raw \| diff to current
2014-10-11	Morgan Deters	Merge branch '1.4.x'	blob \| commitdiff \| raw \| diff to current
2014-10-10	Kshitij Bansal	Merge remote-tracking branch 'origin/1.4.x'	blob \| commitdiff \| raw \| diff to current
2014-10-09	Morgan Deters	Merge branch '1.4.x'	blob \| commitdiff \| raw \| diff to current
2014-10-07	Morgan Deters	Fix a resource limiting issue where interruption didn...	blob \| commitdiff \| raw \| diff to current
2014-10-07	Morgan Deters	Merge branch '1.4.x'	blob \| commitdiff \| raw \| diff to current
2014-10-06	Morgan Deters	Merge branch '1.4.x'	blob \| commitdiff \| raw \| diff to current
2014-10-06	Morgan Deters	Merge branch '1.4.x'	blob \| commitdiff \| raw \| diff to current
2014-10-03	Morgan Deters	Merge branch '1.4.x'	blob \| commitdiff \| raw \| diff to current
2014-10-03	Morgan Deters	Merge branch '1.4.x'	blob \| commitdiff \| raw \| diff to current
2014-10-02	Morgan Deters	Merge branch '1.4.x'.	blob \| commitdiff \| raw \| diff to current
2014-09-30	Morgan Deters	Merge branch '1.4.x'	blob \| commitdiff \| raw \| diff to current
2014-09-27	Morgan Deters	Merge branch '1.4.x'	blob \| commitdiff \| raw \| diff to current
2014-09-26	Morgan Deters	Merge branch '1.4.x'	blob \| commitdiff \| raw \| diff to current
2014-09-18	Morgan Deters	Resource spending support in theories (and especially...	blob \| commitdiff \| raw \| diff to current
2014-09-17	Kshitij Bansal	Merge branch '1.4.x' while ignoring commit 8d5eb49.	blob \| commitdiff \| raw \| diff to current
2014-09-17	Kshitij Bansal	Merge branch '1.4.x'	blob \| commitdiff \| raw \| diff to current
2014-08-22	Morgan Deters	Unsat core infrastruture and API (SMT-LIB compliance...	blob \| commitdiff \| raw \| diff to current
2014-07-10	Kshitij Bansal	Merge remote-tracking branch 'origin/master' into segfa...	blob \| commitdiff \| raw \| diff to current
2014-07-01	Morgan Deters	Update copyrights.	blob \| commitdiff \| raw \| diff to current
2014-04-30	Morgan Deters	Mostly resolves bug #561 memory leaks, and more.	blob \| commitdiff \| raw \| diff to current
2014-04-01	Tim King	Merge branch '1.3.x'	blob \| commitdiff \| raw \| diff to current
2014-03-26	Morgan Deters	Merge branch '1.3.x'	blob \| commitdiff \| raw \| diff to current
2014-03-11	Morgan Deters	Merge branch '1.3.x'	blob \| commitdiff \| raw \| diff to current
2014-03-11	Morgan Deters	Merge branch '1.3.x'	blob \| commitdiff \| raw \| diff to current
2014-03-07	Tianyi Liang	Merge branch 'master' of github.com:tiliang/CVC4	blob \| commitdiff \| raw \| diff to current
2014-03-04	Morgan Deters	Don't theory-preprocess under quantifiers; but DO theor...	blob \| commitdiff \| raw \| diff to current
2013-11-06	Tianyi Liang	Merge branch 'master' of github.com:tiliang/CVC4	blob \| commitdiff \| raw \| diff to current
2013-11-04	lianah	Merge branch 'master' of https://github.com/CVC4/CVC4	blob \| commitdiff \| raw \| diff to current
2013-10-08	Liana Hadarean	fixed some bugs	blob \| commitdiff \| raw \| diff to current
2013-09-30	Liana Hadarean	merged golden	blob \| commitdiff \| raw \| diff to current
next

RSS Atom