projects / cvc5.git / history
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
Cleanup in transcendental solver, add ApproximationBounds struct. (#5945)
[cvc5.git] / src / theory /
2021-02-22 Gereon KremerCleanup in transcendental solver, add ApproximationBoun... tree | commitdiff
2021-02-22 Gereon Kremeradd pruneRedundantIntervals (#5950) tree | commitdiff
2021-02-22 Andrew ReynoldsFix datatypes inference manager when proofs are enabled... tree | commitdiff
2021-02-19 Andrew ReynoldsSimplify interface to instantiate (#5926) tree | commitdiff
2021-02-19 Andrew ReynoldsFill in missing inference ids in datatypes theory ... tree | commitdiff
2021-02-19 Andrew ReynoldsRefactoring theory inference process (#5920) tree | commitdiff
2021-02-19 Andrew ReynoldsFix rewrite for contains over replace (#5924) tree | commitdiff
2021-02-19 Andrew ReynoldsRemove string stat for inferences (#5932) tree | commitdiff
2021-02-19 Gereon KremerCleanup of inferences in arithmetic theory (#5927) tree | commitdiff
2021-02-18 Gereon KremerAdd statistic for InferenceId to TheoryInferenceManager... tree | commitdiff
2021-02-18 Gereon KremerAdd InferenceIds for sets theory. (#5900) tree | commitdiff
2021-02-18 Gereon KremerNew InferenceIds for BV theory (#5909) tree | commitdiff
2021-02-18 Andrew ReynoldsDocument UF inferences (#5917) tree | commitdiff
2021-02-18 Andrew ReynoldsEliminate non-static members in term util (#5919) tree | commitdiff
2021-02-18 Andrew ReynoldsMove first order model for full model check to own... tree | commitdiff
2021-02-17 Andrew ReynoldsMove methods from term util to quantifiers registry... tree | commitdiff
2021-02-17 Andrew ReynoldsCompute fact or lemma in datatypes prior to buffering... tree | commitdiff
2021-02-17 Gereon KremerUse InferenceId in sep theory. (#5912) tree | commitdiff
2021-02-17 Gereon KremerTheoryIds for UF theory. (#5901) tree | commitdiff
2021-02-17 Gereon KremerAdd InferenceIds for theory of arrays (#5910) tree | commitdiff
2021-02-17 Gereon KremerAdd InferenceId to buffered inference manager (#5911) tree | commitdiff
2021-02-17 Mathias PreinerAdd bit-level propagation support to BV bitblast solver... tree | commitdiff
2021-02-15 Gereon KremerRemove now obsolete sendLemmas and inferences stat... tree | commitdiff
2021-02-13 Andrew ReynoldsMoving methods from quantifiers engine to quantifiers... tree | commitdiff
2021-02-13 Mathias PreinerProperly set up equality engine for BV bitblast solver... tree | commitdiff
2021-02-11 Gereon KremerMake most methods of TheoryInferenceManager expect... tree | commitdiff
2021-02-11 Gereon KremerAdd InferenceId member to TheoryInference, adapt all... tree | commitdiff
2021-02-11 Gereon KremerMerge InferenceIds into one enum (#5892) tree | commitdiff
2021-02-11 Andrew ReynoldsFix spurious assertion failure in regexp normalization... tree | commitdiff
2021-02-10 Andrew ReynoldsRefactor term registration visitors (#5875) tree | commitdiff
2021-02-10 Andrew ReynoldsFix open proof for factoring lemma (#5885) tree | commitdiff
2021-02-10 Andrew ReynoldsSimplify method for inferring proxy lemmas in strings... tree | commitdiff
2021-02-10 Andrew ReynoldsRemove track instantiations infrastructure (#5883) tree | commitdiff
2021-02-09 Andrew ReynoldsEliminating dependencies from inst utils (#5882) tree | commitdiff
2021-02-09 Andrew ReynoldsMake term database optionally SAT-context-dependent... tree | commitdiff
2021-02-09 Haniel Barbosa[quantifiers] Fix prenex computation (#5879) tree | commitdiff
2021-02-08 Andrew ReynoldsUse quantifiers inference manager for lemma management... tree | commitdiff
2021-02-08 Andrew ReynoldsFix disequality between seq.unit terms (#5880) tree | commitdiff
2021-02-08 Andrew ReynoldsRemove support for inst closure (#5874) tree | commitdiff
2021-02-08 Andrew ReynoldsAvoid spurious traversal of terms during preregistratio... tree | commitdiff
2021-02-06 Andrew ReynoldsDo not combine theories if theory engine needs check... tree | commitdiff
2021-02-05 Andrew ReynoldsMinor cleaning of quantifiers engine (#5858) tree | commitdiff
2021-02-05 Andrew ReynoldsMiscellaneous cleaning in theory engine (#5854) tree | commitdiff
2021-02-04 yoni206Adding an option to optimize polite combination for... tree | commitdiff
2021-02-04 Andrew ReynoldsIntroduce quantifiers registry utility (#5829) tree | commitdiff
2021-02-04 Andrew ReynoldsEliminate equality query dependence on quantifiers... tree | commitdiff
2021-02-03 Mathias PreinerAdd BV solver bitblast. (#5851) tree | commitdiff
2021-02-02 Andrew Reynolds(proof-new) Miscellaneous fixes and regressions (#5841) tree | commitdiff
2021-02-02 Andrew Reynolds(proof-new) Refactor theory preprocessing (#5835) tree | commitdiff
2021-02-02 Andrew ReynoldsCleanup some includes (#5847) tree | commitdiff
2021-02-02 Andrew ReynoldsImprovements for NL traces (#5846) tree | commitdiff
2021-02-01 Andrew ReynoldsEliminate PREPROCESS lemma property (#5827) tree | commitdiff
2021-02-01 Andrew ReynoldsSimplify alpha equivalence module (#5839) tree | commitdiff
2021-02-01 mudathirmahgoubFix BagsRewriter::rewriteUnionDisjoint (#5840) tree | commitdiff
2021-01-30 Andrew ReynoldsFix unguarded call to get representative (#5838) tree | commitdiff
2021-01-29 mudathirmahgoubAdd bag inferences for operators: intersection, duplica... tree | commitdiff
2021-01-29 Andrew Reynolds(proof-new) Distinguish pre vs post rewrites in term... tree | commitdiff
2021-01-28 Andrew ReynoldsReorganize calls to quantifiers engine from SmtEngine... tree | commitdiff
2021-01-28 Andrew ReynoldsSimplify lemma interface (#5819) tree | commitdiff
2021-01-28 Andrew ReynoldsUse standard equality engine information in quantifiers... tree | commitdiff
2021-01-28 Andrew ReynoldsAlways theory-preprocess lemmas (#5817) tree | commitdiff
2021-01-27 Andrew ReynoldsAdd option for whether to filter candidate rewrite... tree | commitdiff
2021-01-27 Andrew ReynoldsSplit pattern term selector from trigger (#5811) tree | commitdiff
2021-01-27 Andrew Reynolds(proof-new) Improvements to quantifiers engine and... tree | commitdiff
2021-01-27 Alex OzdemirThread proofs through arith channels & similar (#5818) tree | commitdiff
2021-01-27 Andrew ReynoldsUse term canonizer utility locally in quantifiers ... tree | commitdiff
2021-01-27 Andrew ReynoldsUse standard conflict mechanism in quantifiers state... tree | commitdiff
2021-01-26 Andrew ReynoldsIntroduce quantifiers inference manager (#5821) tree | commitdiff
2021-01-26 Andrew ReynoldsRemove deprecated quantifiers modules (#5820) tree | commitdiff
2021-01-26 Andrew ReynoldsRefactor quantifiers engine initialization (#5813) tree | commitdiff
2021-01-26 Alex OzdemirAdd proofs to TheoryArithPrivate::propagate (#5812) tree | commitdiff
2021-01-25 mudathirmahgoubRefactor bags::SolverState (#5783) tree | commitdiff
2021-01-25 Andrew ReynoldsEnsure uses of ground terms in triggers are preprocesse... tree | commitdiff
2021-01-25 Andrew ReynoldsSplit inst match generator into multiple files (#5805) tree | commitdiff
2021-01-25 Andrew ReynoldsSplit E-matching strategies to own files (#5807) tree | commitdiff
2021-01-25 mudathirmahgoubrename InferInfo::d_newSkolem to InferInfo::d_skolems... tree | commitdiff
2021-01-24 Andrew Reynolds Initial cleaning of e-matching instantiation strategy... tree | commitdiff
2021-01-24 Andrew ReynoldsInitial cleaning of triggers (#5795) tree | commitdiff
2021-01-24 Andrew ReynoldsInitial cleaning of inst match generator (#5794) tree | commitdiff
2021-01-24 Andrew Reynolds(proof-new) Instantiation list utility (#5768) tree | commitdiff
2021-01-24 Andrew ReynoldsAdd interface for getting preprocessed term (#5798) tree | commitdiff
2021-01-21 Alex Ozdemirarith: Proofs for Diophantine cuts (#5792) tree | commitdiff
2021-01-20 Andrew ReynoldsRefactoring the single invocation solver (#5706) tree | commitdiff
2021-01-20 Andrew ReynoldsFix type issues with relevant domain computation (... tree | commitdiff
2021-01-20 Andrew ReynoldsFix corner case of wrongly applied selector as trigger... tree | commitdiff
2021-01-20 Andrew ReynoldsUse arbitrary ground term assignment for sorts where... tree | commitdiff
2021-01-19 Alex OzdemirImplement proofs for arith BRAB lemmas (#5784) tree | commitdiff
2021-01-15 Andrew ReynoldsImplement --no-strings-lazy-pp as a preprocessing pass... tree | commitdiff
2021-01-14 Andrew ReynoldsUpdates to theory preprocess equality (#5776) tree | commitdiff
2021-01-13 Andrew ReynoldsSplit eager solver from strings solver state (#5775) tree | commitdiff
2021-01-11 Andrew ReynoldsMerge theory registrar and theory proxy (#5758) tree | commitdiff
2021-01-11 Andrew ReynoldsFurther simplifications in preparation for removing... tree | commitdiff
2021-01-11 Andrew ReynoldsRemove extended rewrite for arithmetic (#5760) tree | commitdiff
2021-01-09 mudathirmahgoubFix issue 5513 (#5757) tree | commitdiff
2021-01-08 mudathirmahgoubRename getAntecedent to getPremises (#5754) tree | commitdiff
2021-01-08 mudathirmahgoubAdd bags inference generator (#5731) tree | commitdiff
2021-01-07 Gereon KremerMake sure polynomials are properly factorized in nl... tree | commitdiff
2021-01-06 Andrew ReynoldsAdd new interfaces to term formula removal and theory... tree | commitdiff
2021-01-05 yoni206Adding str.len to triggers (#5746) tree | commitdiff
2020-12-24 Haniel Barbosa[proof-new] Only use old proofs for unsat cores if... tree | commitdiff
next