summaryrefslogtreecommitdiff
path: root/src/theory
AgeCommit message (Expand)Author
2021-05-16New reduction for str.substrnewSubstrAndres Noetzli
2021-05-14bv: Assert input facts on user-level 0. (#6515)Mathias Preiner
2021-05-13Add std::hash overloads for Node, TNode and TypeNode. (#6534)Mathias Preiner
2021-05-12Ensure sequences of Booleans generate Boolean term variable skolems when appl...Andrew Reynolds
2021-05-10Unify top-level substitutions and model substitutions (#6499)Andrew Reynolds
2021-05-07Add support for datatype update (#6449)Andrew Reynolds
2021-05-07Simplifications to expand definitions (#6487)Andrew Reynolds
2021-05-06[proof-new] Updating documentation for Subs/Rw ids (#6502)Haniel Barbosa
2021-05-06Discard duplicate terms in patterns (#6501)Andrew Reynolds
2021-05-06Use constant folding for evaluating BV eager atom (#6494)Andrew Reynolds
2021-05-05Do not have quantifiers model inherit from theory model (#6493)Andrew Reynolds
2021-05-04Move env into smt solver, theory engine, prop engine (#6486)Andrew Reynolds
2021-05-04FP: Move removal of generic to_fp operations to rewriter. (#6480)Aina Niemetz
2021-05-04FP: Move type check from expandDefinitions. (#6479)Aina Niemetz
2021-05-03FP: Rewrite to_fp conversion from signed bit-vector. (#6472)Aina Niemetz
2021-04-30bv: Refactor ppAssert and move to TheoryBV. (#6470)Mathias Preiner
2021-04-30Add parameter name for argument `isPreRewrite` for FP rewrites. (#6469)Aina Niemetz
2021-04-30Use substitutions for implementing defined functions (#6437)Andrew Reynolds
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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback