summaryrefslogtreecommitdiff
path: root/src/theory
AgeCommit message (Expand)Author
2021-04-29Avoid exponential explosion of small constant in CEGQI (#6461)Gereon Kremer
2021-04-28Remove exception headers from options.h (#6456)Gereon Kremer
2021-04-27Add internal support for datatype update (#6450)Andrew Reynolds
2021-04-27Fix refutational soundness bug in quantifier prenexing (#6448)Andrew Reynolds
2021-04-27Bool: Move implementation of type rules to cpp. (#6420)Aina Niemetz
2021-04-26First part of options refactoring (#6428)Gereon Kremer
2021-04-26Fix theoryOf for Boolean equalities (#6444)Andrew Reynolds
2021-04-26Ensure dependency is tracked for all substitutions (#6438)Andrew Reynolds
2021-04-26Do not process looping word equations over sequences (#6434)Andrew Reynolds
2021-04-25Use fast enumeration by default for Boolean predicate synthesis (#6440)Andrew Reynolds
2021-04-24Improve getValue for non-evaluated operators (#6436)Andrew Reynolds
2021-04-23Add assumption-based unsat cores. (#6427)Mathias Preiner
2021-04-23(proof-new) Proofs for sets purification lemmas (#6416)Andrew Reynolds
2021-04-23Add new substitution apply methods fixpoint, sequential, simultaneous (#6429)Andrew Reynolds
2021-04-23Enable strings exp by default for strings specific logics (#6424)Andrew Reynolds
2021-04-23BV: Add proof logging for bit-blasting. (#6373)Aina Niemetz
2021-04-23Move implementation of UF rewriter to cpp (#6393)Andrew Reynolds
2021-04-22Make trust substitution map generate proofs lazily (#6379)Andrew Reynolds
2021-04-22Minor improvements to substitutions (#6380)Andrew Reynolds
2021-04-22Move expand definition from Theory to TheoryRewriter (#6408)Andrew Reynolds
2021-04-21Arithmetic: Move implementation of type rules to cpp. (#6419)Aina Niemetz
2021-04-21UF: Move implementation of type rules to cpp. (#6403)Aina Niemetz
2021-04-21Datatypes: Move implementation of type rules to cpp. (#6418)Aina Niemetz
2021-04-21Goodbye CVC4, hello cvc5! (#6371)Mathias Preiner
2021-04-21Sets: Move implementation of type rules to cpp. (#6401)Aina Niemetz
2021-04-21Arrays: Move implementation of type rules to cpp. (#6407)Aina Niemetz
2021-04-20Split FP expand definitions to own module (#6392)Andrew Reynolds
2021-04-20BV: Move implementation of type rules from header to .cpp. (#6360)Aina Niemetz
2021-04-20Sep: Move implementation of type rules to cpp. (#6402)Aina Niemetz
2021-04-20Quantifiers: Move implementation of type rules to cpp. (#6404)Aina Niemetz
2021-04-20Add InferenceId as resources (#6339)Gereon Kremer
2021-04-20Add guards to disable clang-format around placeholders in templates. (#6375)Aina Niemetz
2021-04-19Fully incorporate quantifiers macros into ppAssert / non-clausal simplificati...Andrew Reynolds
2021-04-15Rename occurrences of CVC4 to CVC5. (#6351)Aina Niemetz
2021-04-14Fix type rule for relations join image (#6349)Andrew Reynolds
2021-04-14Refactor / reimplement statistics (#6162)Gereon Kremer
2021-04-14Rename public and private headers in src/include. (#6352)Aina Niemetz
2021-04-14[unsat-cores] Improving new unsat cores (#6356)Haniel Barbosa
2021-04-14Add internal API methods for pool-based instantiation (#6350)Andrew Reynolds
2021-04-14Add interface for getting relevant assertions (#5131)Andrew Reynolds
2021-04-14Merge equivalent sub-obligations instead of discarding them. (#6353)Abdalrhman Mohamed
2021-04-14Warn about infeasible SyGuS conjectures (#6345)Andrew Reynolds
2021-04-13Add pool instantiation strategy (#6308)Andrew Reynolds
2021-04-13Formalize more skolems (#6307)Andrew Reynolds
2021-04-13Avoid using substitute's input cache after the method call. (#6328)Abdalrhman Mohamed
2021-04-12Bags: Move more implementation of type rule from header to .cpp. (#6336)Aina Niemetz
2021-04-12Strings: Move implementation of type rules from header to .cpp file. (#6334)Aina Niemetz
2021-04-12Fix computation of whether a type is finite (#6312)Andrew Reynolds
2021-04-12Refactor resource manager (#6322)Gereon Kremer
2021-04-12Refactor and update copyright headers. (#6316)Aina Niemetz
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback