summaryrefslogtreecommitdiff
path: root/src/theory/inference_id.cpp
AgeCommit message (Expand)Author
2021-11-01Fix upwards closure for relations (#7515)Andrew Reynolds
2021-10-31Fix soundess issue for bags with negative multiplicity (#7539)mudathirmahgoub
2021-10-27Fix model unsoundness for relation join (#7511)Andrew Reynolds
2021-10-25Add inference for count map (#7264)mudathirmahgoub
2021-10-24Add new eager conflict detection in strings for integer equivalence classes (...Andrew Reynolds
2021-09-29Add the strings array solver (#7232)Andrew Reynolds
2021-09-22Add extensionality option for strings disequalities (#7229)Andrew Reynolds
2021-08-16Use InferenceManager in ExtTheory (#7006)Gereon Kremer
2021-08-04Add inference ids for remainder of sygus solver (#6977)Andrew Reynolds
2021-08-04Add optional debug information for dumping instantiations (#6950)Andrew Reynolds
2021-08-04Add missing inference identifiers (#6962)Andrew Reynolds
2021-07-27Track instantiation reasons in proofs (#6935)Andrew Reynolds
2021-07-26Enable default equality proofs for sets (#6931)Andrew Reynolds
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-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-13Add pool instantiation strategy (#6308)Andrew Reynolds
2021-04-12Refactor and update copyright headers. (#6316)Aina Niemetz
2021-04-09Add missing InferenceIds to toString (#6320)Gereon Kremer
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-11Introduce inference ids for quantifier instantiation (#6119)Andrew Reynolds
2021-03-11Direct lemmas and inference ids for sygus extension (#5960)Andrew Reynolds
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-03-03More cleanup of includes to reduce compilation times (#6037)Gereon Kremer
2021-02-19Fill in missing inference ids in datatypes theory (#5931)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 InferenceIds for sets theory. (#5900)Gereon Kremer
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