projects / cvc5.git / history
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
FloatingPoint: Separate out symFPU glue code. (#5492)
[cvc5.git] / src / theory /
2020-11-20 Aina NiemetzFloatingPoint: Separate out symFPU glue code. (#5492) tree | commitdiff
2020-11-20 Aina NiemetzFix #5493. (#5495) tree | commitdiff
2020-11-20 Andrew ReynoldsSupport nested quantifier elimination for get-qe comman... tree | commitdiff
2020-11-20 Aina NiemetzFix compiler warnings. (#5493) tree | commitdiff
2020-11-20 Gereon Kremer(proof-new) Replace LazyCDProofSet by generic CDProofSe... tree | commitdiff
2020-11-20 Gereon KremerAllow to pass ProofGenerator to arithmetic inference... tree | commitdiff
2020-11-19 Andrew ReynoldsEnable new implementation of CEGQI based on nested... tree | commitdiff
2020-11-19 Aina NiemetzInclude stddef.h (needed for size_t) in cvc4_public... tree | commitdiff
2020-11-19 Andrew ReynoldsAdd nested quantifier elimination module (#5422) 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-18 Aina NiemetzFloatingPoint: Clean up and document header, format... 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-14 Andrew ReynoldsFix double conflict in extended string solver (#5435) tree | commitdiff
2020-11-13 Andrew Reynolds(proof-new) Enable proofs for datatypes (#5436) tree | commitdiff
2020-11-13 Andrew ReynoldsMake regular expression difference left associative... tree | commitdiff
2020-11-12 Andrew ReynoldsSimplify sygus solver and sygus stream (#5389) tree | commitdiff
2020-11-12 Andrew Reynolds(proof-new) Separate explanation stages in proof equali... tree | commitdiff
2020-11-12 Andrew ReynoldsFix redundant refinement lemma in sygus solver (#5399) tree | commitdiff
2020-11-12 Andrew Reynolds(proof-new) Proofs for skolemization (#5339) tree | commitdiff
2020-11-12 Andrew Reynolds(proof-new) Fix true explanations of propagations in... tree | commitdiff
2020-11-12 Andrew Reynolds(proof-new) Add datatypes inference to proof constructo... tree | commitdiff
2020-11-11 Andrew ReynoldsRewrite witness terms at prerewrite (#5419) tree | commitdiff
2020-11-11 Andrew ReynoldsFix preregistration in TheorySep before declare-heap... tree | commitdiff
2020-11-10 Andrew ReynoldsDo not mark extended functions as reduced based on... tree | commitdiff
2020-11-10 Andrew ReynoldsMake mkGroundTerm deterministic (#5347) tree | commitdiff
2020-11-10 Andrew ReynoldsAdd proper support for the declare-heap command for... tree | commitdiff
2020-11-09 Andrew ReynoldsDo not regress explanations of datatype lemmas (#5376) tree | commitdiff
2020-11-06 mudathirmahgoubFix issue #5342 (#5349) tree | commitdiff
2020-11-06 Andrew Reynolds(proof-new) Miscellaneous changes to strings for proofs... tree | commitdiff
2020-11-06 Andrew ReynoldsSplit sygus template inference to its own file (#5388) tree | commitdiff
2020-11-05 mudathirmahgoubRemove mkSingleton from the API (#5366) tree | commitdiff
2020-11-04 Andres NoetzliAdd constants from equality engine evaluation to model... tree | commitdiff
2020-11-03 Andrew ReynoldsReset built model flag at presolve in nonlinear (#5386) tree | commitdiff
2020-11-03 Andrew ReynoldsMove sygus qe preproc to its own file (#5375) tree | commitdiff
2020-11-02 Andrew ReynoldsUpdate strings proxy variable map to be context indepen... tree | commitdiff
2020-10-30 Gereon KremerUse BoundInference in nonlinear extension (#5359) tree | commitdiff
2020-10-30 Andrew ReynoldsUpdate api::Sort to use TypeNode instead of Type (... tree | commitdiff
2020-10-29 Andrew ReynoldsSet strings pending conflict flag (#5364) tree | commitdiff
2020-10-29 mudathirmahgoubAdd mkInteger to the API (#5274) tree | commitdiff
2020-10-29 Andrew Reynolds(proof-new) Update the strings inference manager for... tree | commitdiff
2020-10-28 Andrew ReynoldsRemove more uses of Expr (#5357) 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 Abdalrhman MohamedRefactor DeclareSygusVarCommand and SynthFunCommand... tree | commitdiff
2020-10-27 Gereon KremerEnable --nl-cad by default (#5345) tree | commitdiff
2020-10-27 mudathirmahgoubAdd DUPICATE_REMOVAL operator to bags (#5336) tree | commitdiff
2020-10-26 Andrew Reynolds(proof-new) Add datatypes proof checker (#5340) tree | commitdiff
2020-10-26 Andrew ReynoldsSend external equalities from collapse selector as... tree | commitdiff
2020-10-24 mudathirmahgoubFix issue 5271 (#5335) tree | commitdiff
2020-10-24 Haniel Barbosa[proof-new] Fix n-ary kind handling in EqEngine explana... tree | commitdiff
2020-10-23 Andrew ReynoldsApply alpha equivalence to annotated quantified formula... tree | commitdiff
2020-10-23 Andrew ReynoldsChange datatypes lemma policy for equalities not coming... tree | commitdiff
2020-10-23 Andrew ReynoldsFix related to preregistering boolean term variables... tree | commitdiff
2020-10-22 Andrew ReynoldsRemove unused equality engine types (#5319) tree | commitdiff
2020-10-22 mudathirmahgoubFix issue 5309 (#5327) tree | commitdiff
2020-10-22 Andrew Reynolds(proof-new) Make theory preprocessor user-context depen... tree | commitdiff
2020-10-21 Gereon Kremer(proof-new) Make circuit propagator proof producing... tree | commitdiff
2020-10-21 mudathirmahgoubImplement bags evaluator (#5322) tree | commitdiff
2020-10-21 Alex Ozdemir(proof-new) arith: dedup literals in flattenImpl (... tree | commitdiff
2020-10-21 mudathirmahgoubAdd operator MakeBagOp for constructing bags (#5209) tree | commitdiff
2020-10-21 Abdalrhman MohamedAdd finishInit for getInterpol and getAbduct. (#5316) tree | commitdiff
2020-10-21 Andrew Reynolds(proof-new) Fixes for proofs in rewriter (#5307) tree | commitdiff
2020-10-20 Aina NiemetzFix compiler warnings. (#5305) tree | commitdiff
2020-10-20 Gereon Kremer(proof-new) Add proofs for circuit propagator (#5301) tree | commitdiff
2020-10-20 Andrew Reynolds(proof-new) Update add lazy step interface in LazyCDPro... tree | commitdiff
2020-10-20 Andrew ReynoldsFix miscellaneous warnings (#5256) tree | commitdiff
2020-10-20 Andrew ReynoldsMake seq.nth a trigger kind (#5314) tree | commitdiff
2020-10-20 Gereon KremerHandle rewrite to bool in BoundInference (#5311) tree | commitdiff
2020-10-20 yoni206Expand `seq.nth` lazily (#5287) tree | commitdiff
2020-10-19 Haniel Barbosa[proof-new] Fixing resolution proof checker (#5262) tree | commitdiff
2020-10-19 Andrew ReynoldsSafer version of pending lemma processing in inference... tree | commitdiff
2020-10-18 Andrew Reynolds (proof-new) Witness axiom reconstruction for purificat... tree | commitdiff
2020-10-18 Andrew Reynolds(proof-new) Implementation of trust substitution (... tree | commitdiff
2020-10-18 Andrew Reynolds(proof-new) More features for SMT proof post-processor... tree | commitdiff
2020-10-18 Andrew Reynolds(proof-new) Improvements for theory engine (#5292) tree | commitdiff
2020-10-16 Andrew ReynoldsRefactor SMT-level model object (#5277) tree | commitdiff
2020-10-16 Andrew ReynoldsCatch more cases of nested recursion in datatypes ... tree | commitdiff
2020-10-16 Andrew ReynoldsAdd inference enumeration to datatypes (#5275) tree | commitdiff
2020-10-15 Alex Ozdemir(proof-new) TheoryArithPrivate: farkas lemma proof... tree | commitdiff
2020-10-14 mudathirmahgoubFix issue #5269 (#5270) 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 Haniel Barbosausing NOT_NOT_ELIM rather than macros to do double... tree | commitdiff
2020-10-14 Alex Ozdemir(proof-new) Prove lemmas in Constraint (#5254) tree | commitdiff
2020-10-14 Andrew Reynolds(proof-new) Simplifications for proof rule checker... tree | commitdiff
2020-10-14 Andrew Reynolds (proof-new) Miscellaneous minor improvements and fixes... tree | commitdiff
2020-10-13 Andrew Reynolds(proof-new) New rules for Booleans (#5243) tree | commitdiff
2020-10-13 yoni206bv2int: improving bvand tables (#5235) tree | commitdiff
2020-10-12 Andrew ReynoldsRemove uf-ss-totality option (#5251) tree | commitdiff
2020-10-12 Andrew ReynoldsEliminate uses of Expr in SmtEngine interface (#5240) tree | commitdiff
2020-10-11 Mathias PreinerSyGuS instantiation modes (#5228) 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
next