projects / cvc5.git / history
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
Refactor transcendental solver (#5514)
[cvc5.git] / src / theory / arith /
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
2020-08-20 Andrew ReynoldsAdd TheoryState objects to each Theory (#4920) tree | commitdiff
2020-08-20 Andrew ReynoldsSimplify trigger notifications in equality engine ... tree | commitdiff
2020-08-19 Gereon Kremer(cad solver) Add a partial check method. (#4904) tree | commitdiff
2020-08-17 Andrew ReynoldsDynamic allocation of equality engine in Theory (#4890) tree | commitdiff
2020-08-16 Gereon Kremer(cad solver) Use the current model as initial assignmen... tree | commitdiff
2020-08-14 Andrew ReynoldsSimplify equality engine notifications (#4896) tree | commitdiff
2020-08-14 Gereon KremerInspect roots to avoid certain resultants (Algorithm... tree | commitdiff
2020-08-12 Gereon KremerAdd naive support for integer variables. (#4835) tree | commitdiff
2020-08-12 Gereon KremerFix infinite loop in arith_ite_simp (#4805) tree | commitdiff
2020-08-09 Andrew ReynoldsMake valuation class more robust to null underlying... tree | commitdiff
2020-08-05 Gereon KremerImprove error message for unsupported exponents (#4852) tree | commitdiff
2020-08-05 Gereon KremerAdd dummy returns if libpoly is unavailable. (#4845) tree | commitdiff
2020-08-04 Gereon KremerAdd CAD-based solver (#4834) tree | commitdiff
2020-07-30 Gereon KremerCad implementation (#4774) tree | commitdiff
2020-07-30 Gereon KremerAdds the interface for the CAD-based arithmetic solver... tree | commitdiff
2020-07-28 Andrew ReynoldsUse lemma property enum for OutputChannel::lemma (... tree | commitdiff
2020-07-27 Andrew Reynolds(proof-new) Arithmetic operator elim proof producing... tree | commitdiff
2020-07-27 Alex OzdemirConsider negation's proof before triggering arith pfs... tree | commitdiff
2020-07-21 Gereon KremerPreparations for a CAD-based arithmetic solver (#4762) tree | commitdiff
2020-07-16 Andrew ReynoldsMake ExtTheory a utility and not a member of Theory... tree | commitdiff
2020-07-15 Andrew ReynoldsSimplify entailment check interface (#4744) tree | commitdiff
2020-07-11 Andrew Reynolds(proof-new) Update Theory interface for proof-new ... tree | commitdiff
2020-07-09 Andrew ReynoldsAssociate all lemmas in non-linear arithmetic with... tree | commitdiff
2020-07-08 Andrew ReynoldsImprove and fix secant and tangent lemmas in the transc... tree | commitdiff
2020-07-01 Andrew ReynoldsAdd solver for integer AND (#4681) tree | commitdiff
next