summaryrefslogtreecommitdiff
path: root/src/theory
AgeCommit message (Expand)Author
2021-02-22Require length-in-conclusion form for strings inferences (#5953)Andrew Reynolds
2021-02-22Add the LazyTreeProofGenerator. (#5948)Gereon Kremer
2021-02-22(proof-new) Add new arithmetic kind INDEXED_ROOT_PREDICATE. (#5949)Gereon Kremer
2021-02-22(proof-new) Add proofs for sine lemmas in the transcendental solver (#5952)Gereon Kremer
2021-02-22Cleanup in transcendental solver, add ApproximationBounds struct. (#5945)Gereon Kremer
2021-02-22add pruneRedundantIntervals (#5950)Gereon Kremer
2021-02-22Fix datatypes inference manager when proofs are enabled (#5937)Andrew Reynolds
2021-02-19Simplify interface to instantiate (#5926)Andrew Reynolds
2021-02-19Fill in missing inference ids in datatypes theory (#5931)Andrew Reynolds
2021-02-19Refactoring theory inference process (#5920)Andrew Reynolds
2021-02-19Fix rewrite for contains over replace (#5924)Andrew Reynolds
2021-02-19Remove string stat for inferences (#5932)Andrew Reynolds
2021-02-19Cleanup of inferences in arithmetic theory (#5927)Gereon Kremer
2021-02-18Add statistic for InferenceId to TheoryInferenceManager. (#5913)Gereon Kremer
2021-02-18Add InferenceIds for sets theory. (#5900)Gereon Kremer
2021-02-18New InferenceIds for BV theory (#5909)Gereon Kremer
2021-02-18Document UF inferences (#5917)Andrew Reynolds
2021-02-17Eliminate non-static members in term util (#5919)Andrew Reynolds
2021-02-17Move first order model for full model check to own file (#5918)Andrew Reynolds
2021-02-17Move methods from term util to quantifiers registry (#5916)Andrew Reynolds
2021-02-17Compute fact or lemma in datatypes prior to buffering (#5914)Andrew Reynolds
2021-02-17Use InferenceId in sep theory. (#5912)Gereon Kremer
2021-02-17TheoryIds for UF theory. (#5901)Gereon Kremer
2021-02-17Add InferenceIds for theory of arrays (#5910)Gereon Kremer
2021-02-17Add InferenceId to buffered inference manager (#5911)Gereon Kremer
2021-02-16Add bit-level propagation support to BV bitblast solver. (#5906)Mathias Preiner
2021-02-15Remove now obsolete sendLemmas and inferences stat from arith::nl (#5903)Gereon Kremer
2021-02-13Moving methods from quantifiers engine to quantifiers state (#5881)Andrew Reynolds
2021-02-13Properly set up equality engine for BV bitblast solver. (#5905)Mathias Preiner
2021-02-11Make most methods of TheoryInferenceManager expect an InferenceId. (#5897)Gereon Kremer
2021-02-11Add InferenceId member to TheoryInference, adapt all derived classes. (#5894)Gereon Kremer
2021-02-11Merge InferenceIds into one enum (#5892)Gereon Kremer
2021-02-11Fix spurious assertion failure in regexp normalization (#5852)Andrew Reynolds
2021-02-10Refactor term registration visitors (#5875)Andrew Reynolds
2021-02-10Fix open proof for factoring lemma (#5885)Andrew Reynolds
2021-02-10Simplify method for inferring proxy lemmas in strings (#5789)Andrew Reynolds
2021-02-09Remove track instantiations infrastructure (#5883)Andrew Reynolds
2021-02-09Eliminating dependencies from inst utils (#5882)Andrew Reynolds
2021-02-09Make term database optionally SAT-context-dependent (#5877)Andrew Reynolds
2021-02-09[quantifiers] Fix prenex computation (#5879)Haniel Barbosa
2021-02-08Use quantifiers inference manager for lemma management (#5867)Andrew Reynolds
2021-02-08Fix disequality between seq.unit terms (#5880)Andrew Reynolds
2021-02-08Remove support for inst closure (#5874)Andrew Reynolds
2021-02-08Avoid spurious traversal of terms during preregistration (#5860)Andrew Reynolds
2021-02-05Do not combine theories if theory engine needs check (#5861)Andrew Reynolds
2021-02-05Minor cleaning of quantifiers engine (#5858)Andrew Reynolds
2021-02-05Miscellaneous cleaning in theory engine (#5854)Andrew Reynolds
2021-02-04Adding an option to optimize polite combination for datatypes (#5856)yoni206
2021-02-04Introduce quantifiers registry utility (#5829)Andrew Reynolds
2021-02-04Eliminate equality query dependence on quantifiers engine (#5831)Andrew Reynolds
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback