projects / cvc5.git / history
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
Updates to theory preprocess equality (#5776)
[cvc5.git] / src / theory / arith /
2021-01-14 Andrew ReynoldsUpdates to theory preprocess equality (#5776) tree | commitdiff
2021-01-07 Gereon KremerMake sure polynomials are properly factorized in nl... tree | commitdiff
2020-12-23 Gereon KremerAdd proofs for nonlinear sign lemmas. (#5707) tree | commitdiff
2020-12-22 Andrew ReynoldsMake theory preprocess rewrite equalities a preprocessi... tree | commitdiff
2020-12-21 Gereon KremerAdd proof for pi bound lemma (#5709) tree | commitdiff
2020-12-21 Gereon KremerAdd proof for sine shift lemmas. (#5710) tree | commitdiff
2020-12-21 Gereon Kremer(proof-new) Make nl-ext factoring lemmas proof producin... tree | commitdiff
2020-12-18 Gereon Kremer(proof-new) Setup proof infrastructure for transcendent... tree | commitdiff
2020-12-18 Gereon KremerAdd proof checker for nl tangent lemma (#5704) tree | commitdiff
2020-12-18 Alex OzdemirBugfix: proofs for props of non-normal arith lits ... tree | commitdiff
2020-12-18 Gereon Kremer(proof-new) Add proof for tangent plane lemmas (#5700) tree | commitdiff
2020-12-18 Gereon KremerAdd proof for split zero check. (#5699) tree | commitdiff
2020-12-17 Gereon KremerAlways consider rewritten lemmas for caching. (#5696) tree | commitdiff
2020-12-17 Gereon Kremer(proof-new) Prepare nonlinear extension and nl-ext... tree | commitdiff
2020-12-10 Gereon KremerFixed a bunch of clang warnings. (#5637) tree | commitdiff
2020-12-09 Gereon KremerSplit initial exp lemma into separate lemmas. (#5622) tree | commitdiff
2020-12-07 makaimannAdd bitwise refinement mode for IAND (#5328) tree | commitdiff
2020-12-07 Gereon KremerRefactor initial phase of transcendental solver (#5599) tree | commitdiff
2020-12-07 Andrew ReynoldsDo not expand theory definitions at the beginning of... tree | commitdiff
2020-12-03 Aina NiemetzUpdate copyright headers. tree | commitdiff
2020-12-02 Aina NiemetzRename macro Message to CVC4Message. (#5576) tree | commitdiff
2020-12-01 Gereon KremerRefactor transcendental solver (#5539) tree | commitdiff
2020-11-30 Andrew ReynoldsRemove includes for old API from internal code (#5536) tree | commitdiff
2020-11-26 Gereon KremerMake CAD solver work for empty set of assertions (... tree | commitdiff
2020-11-25 Gereon KremerFix transcendental secant plane lemmas (#5525) tree | commitdiff
2020-11-25 Gereon KremerRefactor transcendental solver (#5514) tree | commitdiff
2020-11-20 Aina NiemetzFix #5493. (#5495) tree | commitdiff
2020-11-20 Aina NiemetzFix compiler warnings. (#5493) tree | commitdiff
2020-11-20 Gereon KremerAllow to pass ProofGenerator to arithmetic inference... tree | commitdiff
2020-11-19 Aina NiemetzInclude stddef.h (needed for size_t) in cvc4_public... tree | commitdiff
2020-11-19 Andrew ReynoldsFix issues related to eliminating extended arithmetic... tree | commitdiff
2020-11-18 Andrew ReynoldsDo not expand definitions of extended arithmetic operat... tree | commitdiff
2020-11-17 Gereon KremerFix tangent plane lemmas (#5455) tree | commitdiff
2020-11-16 Gereon KremerRefactor tangent plane lemmas (#5449) tree | commitdiff
2020-11-16 Gereon KremerImprove accuracy of resource limitation (#4763) tree | commitdiff
2020-11-05 mudathirmahgoubRemove mkSingleton from the API (#5366) tree | commitdiff
2020-11-03 Andrew ReynoldsReset built model flag at presolve in nonlinear (#5386) tree | commitdiff
2020-10-30 Gereon KremerUse BoundInference in nonlinear extension (#5359) tree | commitdiff
2020-10-29 mudathirmahgoubAdd mkInteger to the API (#5274) tree | commitdiff
2020-10-28 Andrew ReynoldsFixes for unconstrained variables in nonlinear model... tree | commitdiff
2020-10-28 Gereon KremerSplit NlSolver in multiple subsolvers (#5315) tree | commitdiff
2020-10-28 Andrew ReynoldsAdd rewrites for div/mod in the arithmetic rewriter... tree | commitdiff
2020-10-27 Gereon KremerEnable --nl-cad by default (#5345) tree | commitdiff
2020-10-21 Alex Ozdemir(proof-new) arith: dedup literals in flattenImpl (... tree | commitdiff
2020-10-20 Gereon KremerHandle rewrite to bool in BoundInference (#5311) tree | commitdiff
2020-10-15 Alex Ozdemir(proof-new) TheoryArithPrivate: farkas lemma proof... tree | commitdiff
2020-10-14 yoni206bv2int: implementing the iand-sum mode (#5265) tree | commitdiff
2020-10-14 Alex Ozdemir(proof-new) debug statements & docs for INT_TRUST ... tree | commitdiff
2020-10-14 Alex Ozdemir(proof-new) pfs in TheoryArith(Private) explainations... tree | commitdiff
2020-10-14 Andrew ReynoldsGuard uses of printing approximations for constants... tree | commitdiff
2020-10-14 Alex Ozdemir(proof-new) pfs for conflicts in TheoryArithPrivate... tree | commitdiff
2020-10-14 Alex Ozdemir(proof-new) Prove lemmas in Constraint (#5254) tree | commitdiff
2020-10-13 yoni206bv2int: improving bvand tables (#5235) tree | commitdiff
2020-10-11 Gereon KremerAdd conversion of poly polynomial to cvc node. (#5218) tree | commitdiff
2020-10-10 yoni206bv2int: bvand translation code move (#5227) tree | commitdiff
2020-10-09 Alex Ozdemiruse right arith explanation fn to fix regressions ... tree | commitdiff
2020-10-09 Alex Ozdemir(proof-new) proofs for arith-constraint explanations... tree | commitdiff
2020-10-07 Alex Ozdemir(proof-new) proofs in ee -> arith pipeline (#5215) tree | commitdiff
2020-10-07 Gereon KremerMake sure conflicts are not rewritten (in arithmetic... tree | commitdiff
2020-10-06 Alex Ozdemir(proof-new) proofs for ArithCongMan -> ee facts (#5207) tree | commitdiff
2020-10-06 Andrew Reynolds(proof-new) Add interface for trusted substitution... tree | commitdiff
2020-10-06 Andrew ReynoldsAdd arithmetic preprocess module (#5188) tree | commitdiff
2020-10-03 Andrew ReynoldsStandardization of Theory (#5181) tree | commitdiff
2020-10-02 Andrew ReynoldsDecouple modules from TheoryArithPrivate (#5184) tree | commitdiff
2020-10-02 Alex Ozdemir(proof-new) New proofs in arith::Constraint::externalEx... tree | commitdiff
2020-10-01 Andrew ReynoldsUpdate theory of arithmetic to standard check (#5178) tree | commitdiff
2020-10-01 Gereon KremerAllow to use the initial assignment for CAD (#5177) tree | commitdiff
2020-09-30 Gereon KremerRemove too strict assertion to allow for approximate... tree | commitdiff
2020-09-30 Gereon KremerAdd missing includes. (#5170) tree | commitdiff
2020-09-30 Gereon KremerAdd strategy for nonlinear extension (#5160) tree | commitdiff
2020-09-29 Alex Ozdemir(proof-new) Add proof managers and eager gens to arith... tree | commitdiff
2020-09-29 Gereon KremerClean up nonlinear extension (#5149) tree | commitdiff
2020-09-29 Alex OzdemirAdd utilities for arith/proof_checker and build it... tree | commitdiff
2020-09-28 Gereon KremerAdd new arithmetic BoundInference class (#5148) tree | commitdiff
2020-09-26 Gereon KremerUse inference manager for nl_solver (#5125) tree | commitdiff
2020-09-23 Gereon KremerMake IAND solver use inference manager. (#5126) tree | commitdiff
2020-09-22 Andres NoetzliFix compilation without LibPoly (#5118) tree | commitdiff
2020-09-22 Mathias PreinerUpdate copyright header script to support CMake and... tree | commitdiff
2020-09-22 Gereon KremerICP-based solver for nonlinear arithmetic (#5017) tree | commitdiff
2020-09-17 Gereon Kremer(cad-solver) Fix square-free-basis computation (#5085) tree | commitdiff
2020-09-17 Gereon KremerUse new inference manager in transcendental solver... tree | commitdiff
2020-09-16 Andrew ReynoldsRefactor collectModelInfo in TheoryArith (#5027) tree | commitdiff
2020-09-04 Andrew ReynoldsAdd asLemma flag to theory inference process (#5030) tree | commitdiff
2020-09-04 Haniel BarbosaFix non-lib-poly-build issues (#5028) tree | commitdiff
2020-09-04 Gereon KremerUse arith::InferenceManager for CAD lemmas (#5015) tree | commitdiff
2020-09-03 Gereon KremerBasic integration of arith::InferenceManager (#4999) tree | commitdiff
2020-09-03 Gereon KremerMake nonlinear extension (more) deterministic (#4996) tree | commitdiff
2020-09-03 Andrew ReynoldsMake ExtTheory independent of Theory (#5010) tree | commitdiff
2020-09-02 Gereon KremerUse std::unique_ptr instead of std::shared_ptr for... tree | commitdiff
2020-09-02 Gereon KremerAdd ArithLemma and arith::InferenceManager (#4960) tree | commitdiff
2020-09-01 Haniel BarbosaRemoves old proof code (#4964) tree | commitdiff
2020-09-01 Alex OzdemirAdd arithmetic-specific, runtime, proof-macros. (#4992) tree | commitdiff
2020-09-01 FabianWolffFix spelling errors (#4977) tree | commitdiff
2020-08-31 Andrew ReynoldsSimplify interface for computing relevant terms. (... tree | commitdiff
2020-08-28 Andrew ReynoldsReplace Theory::Set with TheoryIdSet (#4959) tree | commitdiff
2020-08-28 Gereon Kremer(cad-solver) Fixed excluding lemma generation. (#4958) tree | commitdiff
2020-08-28 Gereon KremerMake iand lemmas use proper Inference types. (#4956) tree | commitdiff
2020-08-24 Andrew ReynoldsDo not use relevance during non-linear check model... tree | commitdiff
2020-08-24 Andrew ReynoldsExtend the standard Theory template based on equality... tree | commitdiff
2020-08-21 Andrew ReynoldsConnect the relevance manager to TheoryEngine and use... tree | commitdiff
next