summaryrefslogtreecommitdiff
path: root/src/theory/inference_id.h
AgeCommit message (Expand)Author
2021-07-15bv: Rename lazy solver to layered solver. (#6889)Mathias Preiner
2021-07-14bv: Rename simple solver to bitblast-internal. (#6888)Mathias Preiner
2021-07-12Add trace for combination splits (#6862)Andrew Reynolds
2021-06-25pow2 -- final changes (#6800)yoni206
2021-06-24pow2: Adding monotonicity lemma (#6793)yoni206
2021-06-15pow2: adding a kind, inference rules, and some implementations in the pow2 so...yoni206
2021-05-19Add more missing inference ids (#6313)Andrew Reynolds
2021-04-14Rename public and private headers in src/include. (#6352)Aina Niemetz
2021-04-13Add pool instantiation strategy (#6308)Andrew Reynolds
2021-04-12Refactor and update copyright headers. (#6316)Aina Niemetz
2021-04-09Rename CVC4__ header guards to CVC5__. (#6326)Aina Niemetz
2021-04-08Add identifiers for sources of incompleteness (#6311)Andrew Reynolds
2021-04-01Rename namespace CVC5 to cvc5. (#6258)Aina Niemetz
2021-03-31Rename namespace CVC4 to CVC5. (#6249)Aina Niemetz
2021-03-31Add missing inference ids (#6242)Andrew Reynolds
2021-03-21Clean up remaining raw uses of output channel (#6161)Andrew Reynolds
2021-03-16Further standardization of strings statistics (#6128)Andrew Reynolds
2021-03-11Make linear arithmetic use its inference manager (#5934)Gereon Kremer
2021-03-11Introduce inference ids for quantifier instantiation (#6119)Andrew Reynolds
2021-03-11Direct lemmas and inference ids for sygus extension (#5960)Andrew Reynolds
2021-03-09Some more cleanup of includes (#6083)Gereon Kremer
2021-03-09Update copyright headers to 2021. (#6081)Aina Niemetz
2021-03-08(proof-new) Prepare arithmetic for changes to ppRewrite (#6063)Andrew Reynolds
2021-02-22Eliminate raw use of output channel and valuation in quantifiers (#5933)Andrew Reynolds
2021-02-19Fill in missing inference ids in datatypes theory (#5931)Andrew Reynolds
2021-02-19Cleanup of inferences in arithmetic theory (#5927)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-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-11Merge InferenceIds into one enum (#5892)Gereon Kremer
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback