summaryrefslogtreecommitdiff
path: root/src/theory
AgeCommit message (Expand)Author
2021-03-03(proof-new) Simplifications to arithmetic operator elimination and preprocess...Andrew Reynolds
2021-03-03More cleanup of includes to reduce compilation times (#6037)Gereon Kremer
2021-03-03Remove uses of SExpr class. (#6035)Abdalrhman Mohamed
2021-03-03Add tuple projection operator (#5904)mudathirmahgoub
2021-03-02Remove non-ASCII characters from source files. (#6039)Mathias Preiner
2021-03-02Add aarch64 (ARM64) cross-compile support. (#6033)Mathias Preiner
2021-03-02Fix nightly errors. (#6034)Mathias Preiner
2021-03-02Introduce quantifiers term registry (#5983)Andrew Reynolds
2021-03-02Clean up includes to reduce compile times (#6031)Gereon Kremer
2021-02-27google test: theory: Migrate theory_white. (#6006)Aina Niemetz
2021-02-25(proof-new) Fix regular expression unfolding under substitution (#5958)Andrew Reynolds
2021-02-26Move (optional) rewrite from TrustSubstitutionMap to SubstitutionMap. (#5992)Gereon Kremer
2021-02-25Datatypes lemmas: share only external types (#5997)yoni206
2021-02-24Enable -Werror. (#5969)Mathias Preiner
2021-02-24(proof-new) Add proofs for CAD solver (#5981)Gereon Kremer
2021-02-23Add state and inference manager to inst match generator (#5968)Andrew Reynolds
2021-02-23Add interface to TheoryState for sort inference and facts (#5967)Andrew Reynolds
2021-02-23Add proof for mult sign lemma (#5966)Gereon Kremer
2021-02-23Add proof for monomial bounds check (#5965)Gereon Kremer
2021-02-23(proof-new) Add proof generator for CAD solver (#5964)Gereon Kremer
2021-02-22Add trans secant proofs. (#5957)Gereon Kremer
2021-02-22Explanation of failure for instantiate, use in enumerative instantiation (#5951)Andrew Reynolds
2021-02-22Eliminate raw use of output channel and valuation in quantifiers (#5933)Andrew Reynolds
2021-02-22Move quantifiers attributes to quantifiers registry (#5929)Andrew Reynolds
2021-02-22(proof-new) Change proof-new option to proof (#5955)Andrew Reynolds
2021-02-22(proof-new) Add proofs for exponential functions (#5956)Gereon Kremer
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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback