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

[cvc5.git] / src / theory / arith / theory_arith_private.cpp

2020-11-20	Aina Niemetz	Fix #5493. (#5495)	blob \| commitdiff \| raw
2020-11-20	Aina Niemetz	Fix compiler warnings. (#5493)	blob \| commitdiff \| raw \| diff to current
2020-11-19	Aina Niemetz	Include stddef.h (needed for size_t) in cvc4_public...	blob \| commitdiff \| raw \| diff to current
2020-11-18	Andrew Reynolds	Do not expand definitions of extended arithmetic operat...	blob \| commitdiff \| raw \| diff to current
2020-11-16	Gereon Kremer	Improve accuracy of resource limitation (#4763)	blob \| commitdiff \| raw \| diff to current
2020-10-21	Alex Ozdemir	(proof-new) arith: dedup literals in flattenImpl (...	blob \| commitdiff \| raw \| diff to current
2020-10-15	Alex Ozdemir	(proof-new) TheoryArithPrivate: farkas lemma proof...	blob \| commitdiff \| raw \| diff to current
2020-10-14	Alex Ozdemir	(proof-new) pfs in TheoryArith(Private) explainations...	blob \| commitdiff \| raw \| diff to current
2020-10-14	Alex Ozdemir	(proof-new) pfs for conflicts in TheoryArithPrivate...	blob \| commitdiff \| raw \| diff to current
2020-10-14	Alex Ozdemir	(proof-new) Prove lemmas in Constraint (#5254)	blob \| commitdiff \| raw \| diff to current
2020-10-09	Alex Ozdemir	use right arith explanation fn to fix regressions ...	blob \| commitdiff \| raw \| diff to current
2020-10-09	Alex Ozdemir	(proof-new) proofs for arith-constraint explanations...	blob \| commitdiff \| raw \| diff to current
2020-10-07	Alex Ozdemir	(proof-new) proofs in ee -> arith pipeline (#5215)	blob \| commitdiff \| raw \| diff to current
2020-10-06	Andrew Reynolds	(proof-new) Add interface for trusted substitution...	blob \| commitdiff \| raw \| diff to current
2020-10-03	Andrew Reynolds	Standardization of Theory (#5181)	blob \| commitdiff \| raw \| diff to current
2020-10-02	Andrew Reynolds	Decouple modules from TheoryArithPrivate (#5184)	blob \| commitdiff \| raw \| diff to current
2020-10-02	Alex Ozdemir	(proof-new) New proofs in arith::Constraint::externalEx...	blob \| commitdiff \| raw \| diff to current
2020-10-01	Andrew Reynolds	Update theory of arithmetic to standard check (#5178)	blob \| commitdiff \| raw \| diff to current
2020-09-29	Alex Ozdemir	(proof-new) Add proof managers and eager gens to arith...	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	Andrew Reynolds	Refactor collectModelInfo in TheoryArith (#5027)	blob \| commitdiff \| raw \| diff to current
2020-09-03	Andrew Reynolds	Make ExtTheory independent of Theory (#5010)	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-31	Andrew Reynolds	Simplify interface for computing relevant terms. (...	blob \| commitdiff \| raw \| diff to current
2020-08-17	Andrew Reynolds	Dynamic allocation of equality engine in Theory (#4890)	blob \| commitdiff \| raw \| diff to current
2020-07-27	Andrew Reynolds	(proof-new) Arithmetic operator elim proof producing...	blob \| commitdiff \| raw \| diff to current
2020-07-27	Alex Ozdemir	Consider negation's proof before triggering arith pfs...	blob \| commitdiff \| raw \| diff to current
2020-07-16	Andrew Reynolds	Make ExtTheory a utility and not a member of Theory...	blob \| commitdiff \| raw \| diff to current
2020-06-25	Andrew Reynolds	Update option --nl-ext to enable/disable incremental...	blob \| commitdiff \| raw \| diff to current
2020-06-19	Andrew Reynolds	(proof-new) Split operator elimination from arithmetic...	blob \| commitdiff \| raw \| diff to current
2020-06-16	Aina Niemetz	Update copyright headers.	blob \| commitdiff \| raw \| diff to current
2020-06-05	Andrew Reynolds	(proof-new) Rename ProofSkolemCache to SkolemManager...	blob \| commitdiff \| raw \| diff to current
2020-06-01	Andrew Reynolds	Move non-linear files to src/theory/arith/nl (#4548)	blob \| commitdiff \| raw \| diff to current
2020-05-31	Andres Noetzli	Do not cache operator eliminations in arith (#4542)	blob \| commitdiff \| raw \| diff to current
2020-05-23	Andrew Reynolds	Refactor operator elimination in arithmetic (#4519)	blob \| commitdiff \| raw \| diff to current
2020-05-20	Andrew Reynolds	Do not eliminate variables that are equal to unevaluata...	blob \| commitdiff \| raw \| diff to current
2020-05-19	mudathirmahgoub	Renamed operator CHOICE to WITNESS (#4207)	blob \| commitdiff \| raw \| diff to current
2020-04-08	Andres Noetzli	Perform theory widening eagerly (#4044)	blob \| commitdiff \| raw \| diff to current
2020-03-26	Amalee	Added unit-cube-like test for branch and bound (#3922)	blob \| commitdiff \| raw \| diff to current
2020-03-16	Alex Ozdemir	clang-format	blob \| commitdiff \| raw \| diff to current
2020-03-16	Alex Ozdemir	Fix simplicity check in prop	blob \| commitdiff \| raw \| diff to current
2020-03-16	Alex Ozdemir	Only save farkas+tightening proofs. Error on holes	blob \| commitdiff \| raw \| diff to current
2020-03-09	Andrew Reynolds	Fix type issue in arith rewrite equality (#3972)	blob \| commitdiff \| raw \| diff to current
2020-03-05	Alex Ozdemir	Add a new arith constraint proof rule: IntTightenAP...	blob \| commitdiff \| raw \| diff to current
2020-03-05	Alex Ozdemir	Revert "Add a new arith constraint proof rule: IntTight...	blob \| commitdiff \| raw \| diff to current
2020-03-05	Andres Noetzli	Add a new arith constraint proof rule: IntTightenAP...	blob \| commitdiff \| raw \| diff to current
2020-03-05	Mathias Preiner	Enable -Wshadow and fix warnings. (#3909)	blob \| commitdiff \| raw \| diff to current
2020-02-17	Andrew Reynolds	Fix soundness bug in reduction of integer div/mod...	blob \| commitdiff \| raw \| diff to current
2020-02-04	Alex Ozdemir	Articulate proof-related debug statements in arith...	blob \| commitdiff \| raw \| diff to current
2020-02-03	Andrew Reynolds	Split on model values when repaired model from non...	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-12-05	Andrew Reynolds	Make nonlinear solver intercept model assignments from...	blob \| commitdiff \| raw \| diff to current
2019-11-19	Andres Noetzli	Fix reduction of `sqrt` (#3478)	blob \| commitdiff \| raw \| diff to current
2019-11-18	Andres Noetzli	Use -Wimplicit-fallthrough (#3464)	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-03-26	Aina Niemetz	Update copyright headers.	blob \| commitdiff \| raw \| diff to current
2019-01-03	Alex Ozdemir	[LRA proof] Recording & Printing LRA Proofs (#2758)	blob \| commitdiff \| raw \| diff to current
2018-08-23	Aina Niemetz	Refactor ITE simplification preprocessing pass. (#2360)	blob \| commitdiff \| raw \| diff to current
2018-08-16	Andres Noetzli	Move node algorithms to separate file (#2311)	blob \| commitdiff \| raw \| diff to current
2018-08-08	Andres Noetzli	Require Swig 3 (#2283)	blob \| commitdiff \| raw \| diff to current
2018-07-06	Andrew Reynolds	Split ext theory to own file and document (#1809)	blob \| commitdiff \| raw \| diff to current
2018-06-25	Aina Niemetz	Updated copyright headers.	blob \| commitdiff \| raw \| diff to current
2018-04-03	Andrew Reynolds	Use choice when expanding definitions for inverse trans...	blob \| commitdiff \| raw \| diff to current
2018-02-27	Andrew Reynolds	Option to not use partial function semantics for arithm...	blob \| commitdiff \| raw \| diff to current
2018-02-20	Andrew Reynolds	Minor fixes and additions for transcendental functions...	blob \| commitdiff \| raw \| diff to current
2018-02-14	Andrew Reynolds	Quantifiers subdirectories (#1608)	blob \| commitdiff \| raw \| diff to current
2018-02-07	Andrew Reynolds	Add remaining transcendental functions (#1551)	blob \| commitdiff \| raw \| diff to current
2018-01-23	Tim King	Commenting out throw specifiers for DeltaRationExceptio...	blob \| commitdiff \| raw \| diff to current
2018-01-10	Tim King	Cleaning up throw specifiers on Exception and subclasse...	blob \| commitdiff \| raw \| diff to current
2018-01-08	Tim King	Removes RationalFromDoubleException. Replaces this...	blob \| commitdiff \| raw \| diff to current
2018-01-03	Andrew Reynolds	Global negate (#1466)	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-17	Aina Niemetz	Add random number generator. (#1370)	blob \| commitdiff \| raw \| diff to current
2017-08-31	Andres Noetzli	Use thread_local instead of compiler extensions (#210)	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-10	ajreynol	Merge ntExt branch. Adds support for transcendental...	blob \| commitdiff \| raw \| diff to current
2017-07-07	Mathias Preiner	Update copyright headers.	blob \| commitdiff \| raw \| diff to current
2017-05-31	ajreynol	Minor fix to last commit.	blob \| commitdiff \| raw \| diff to current
2017-05-31	ajreynol	Change to-int, div, int-div skolems from CDAttribute...	blob \| commitdiff \| raw \| diff to current
2017-05-28	Clark Barrett	Merge pull request #164 from CVC4/fix_comp	blob \| commitdiff \| raw \| diff to current
2017-05-26	Tim King	Checking that equalities belong to the arithmetic theor...	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	Clark Barrett	Merge pull request #161 from 4tXJ7f/fix_parser	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	ajreynol	Cleanup handling of division (possible fix for bugs...	blob \| commitdiff \| raw \| diff to current
2017-04-28	ajreynol	Fix bug for real division.	blob \| commitdiff \| raw \| diff to current
2017-04-24	Andrew Reynolds	Merge pull request #152 from timothy-king/delta-rationa...	blob \| commitdiff \| raw \| diff to current
2017-04-22	Tim King	Updating TheoryArithPrivate::getDeltaValue() to eagerly...	blob \| commitdiff \| raw \| diff to current
2017-04-07	ajreynol	Change option names for nl.	blob \| commitdiff \| raw \| diff to current
2017-04-06	Clark Barrett	Merge pull request #143 from FabianWolff/master	blob \| commitdiff \| raw \| diff to current
2017-04-05	ajreynol	Fix bug 698.	blob \| commitdiff \| raw \| diff to current
2017-04-04	ajreynol	Simplify Theory::collectModelInfo interface to not...	blob \| commitdiff \| raw \| diff to current
2017-04-04	Clark Barrett	Merge pull request #141 from 4tXJ7f/remove_def	blob \| commitdiff \| raw \| diff to current
2017-04-03	Andrew Reynolds	Merge pull request #142 from timothy-king/nlAlgMerge	blob \| commitdiff \| raw \| diff to current
2017-04-03	Tim King	Adding a model based axiom instantiation scheme for...	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-25	Tim King	Fixing a potential use after free coming from a pop_bac...	blob \| commitdiff \| raw \| diff to current
next

RSS Atom