summaryrefslogtreecommitdiff
path: root/src/theory/arith
AgeCommit message (Expand)Author
2021-10-29Fix proof of nl lemma for a corner case (#7530)Gereon Kremer
2021-10-29Add PfRule ARITH_POLY_NORM (#7501)Andrew Reynolds
2021-10-27Add comments for arith type rules. (#7488)Gereon Kremer
2021-10-22Fix out-of-sync pruning in CDCAC proofs (#7470)Gereon Kremer
2021-10-22Make CAD proofs user context dependent (#7466)Gereon Kremer
2021-10-22Refactor theory inference manager constructor (#7457)Andrew Reynolds
2021-10-22Fix memory management of `ErrorInformation` (#7388)Andres Noetzli
2021-10-19Fix issue related to sanity checking integer models (#7363)Andrew Reynolds
2021-10-13Make (proof) equality engine use Env (#7336)Andrew Reynolds
2021-10-12fix deprecation of std::iterator (#7332)Ouyancheng
2021-10-06Eliminate more hard coded uses of user context (#7309)Andrew Reynolds
2021-10-05First round of refactoring on NlModel (#7255)Gereon Kremer
2021-09-30Remove usage of static options in arithmetic theory (#7221)Gereon Kremer
2021-09-23Refactor check interface of nonlinear extension (#7235)Gereon Kremer
2021-09-22Eliminate arithmetic proof macros (#7226)Gereon Kremer
2021-09-17Replace write access to options by a local variable (#7207)Gereon Kremer
2021-09-17Minor cleanup related to EnvObj (#7206)Gereon Kremer
2021-09-11Use StatisticsRegistry from Env (#7166)Gereon Kremer
2021-09-09Remove `TheoryState::getEnv()` (#7163)Andres Noetzli
2021-09-09Remove `TheoryState::options()` (#7148)Andres Noetzli
2021-09-08Towards standard usage of ExtendedRewriter (#7145)Andrew Reynolds
2021-09-08Add option for using bound inference for relevant assertions (#7152)Andrew Reynolds
2021-09-07Use `EnvObj` methods instead of `Theory` methods (#7144)Andres Noetzli
2021-09-03EnvObj: Add options(), context(), userContext(). (#7137)Aina Niemetz
2021-09-03theory: Have Theory and TheoryArith* derive from EnvObj. (#7128)Aina Niemetz
2021-08-26Improve integration of nonlinear arithmetic into the arithmetic theory. (#6956)Gereon Kremer
2021-08-25Add missing include (#7067)Gereon Kremer
2021-08-24Uniform treatment of trusted theory inferences in proofs (#7044)Andrew Reynolds
2021-08-20Use Env class in nonlinear extension (#7039)Gereon Kremer
2021-08-19Start using Options via Env in arithmetic (#7032)Gereon Kremer
2021-08-17Replace `Maybe` with `std::optional` (#7005)Andres Noetzli
2021-08-16Push Env class into TheoryState (#7012)Gereon Kremer
2021-08-16Use InferenceManager in ExtTheory (#7006)Gereon Kremer
2021-08-16Make Theory class use Env (#7011)Gereon Kremer
2021-08-04Add missing inference identifiers (#6962)Andrew Reynolds
2021-07-26More updates to arithmetic in preparation for central equality engine (#6927)Andrew Reynolds
2021-07-25Refactor equality engine setup for arithmetic congruence manager (#6902)Andrew Reynolds
2021-07-15Connect the equality solver to theory arith (#6894)Andrew Reynolds
2021-07-15Arithmetic equality solver (#6876)Andrew Reynolds
2021-07-13Add branch and bound lemma if linear arithmetic generates a non-integer assig...Andrew Reynolds
2021-07-12Add branch and bound (#6865)Andrew Reynolds
2021-07-12Add arithmetic preprocess rewrite equality module (#6860)Andrew Reynolds
2021-07-06Integrate Lazard into CAD module (#6812)Gereon Kremer
2021-06-29Add new variants for the CAD projection (#6794)Gereon Kremer
2021-06-28Rewrite POW to POW2 when the base is 2 (#6806)yoni206
2021-06-25pow2 -- final changes (#6800)yoni206
2021-06-24pow2: Adding monotonicity lemma (#6793)yoni206
2021-06-24Fix linear arithmetic for duplicate lemmas in incremental (#6784)Andrew Reynolds
2021-06-24Add CoCoA implementation (#6733)Gereon Kremer
2021-06-23pow2: more implementations (#6756)yoni206
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback