summaryrefslogtreecommitdiff
path: root/src/theory
AgeCommit message (Expand)Author
2021-09-23Implement alpha equivalence proofs (#7066)Andrew Reynolds
2021-09-22Make cegqi subsolvers EnvObj (#7205)Andrew Reynolds
2021-09-22Towards standard usage of evaluator (#7189)Andrew Reynolds
2021-09-22Add extensionality option for strings disequalities (#7229)Andrew Reynolds
2021-09-22arrays: Use EnvObj::rewrite and EnvObj::options. (#7217)Aina Niemetz
2021-09-22arrays: Move type enumerator implementation to .cpp. (#7216)Aina Niemetz
2021-09-22Eliminate arithmetic proof macros (#7226)Gereon Kremer
2021-09-20Fix handling of conversions between FP and reals (#7149)Andres Noetzli
2021-09-20TheoryModel: Use EnvObj::rewrite instead of Rewriter::rewrite. (#7215)Aina Niemetz
2021-09-17Use a single `NodeManager` per thread (#7204)Andres Noetzli
2021-09-17Replace write access to options by a local variable (#7207)Gereon Kremer
2021-09-17Minor cleanup related to EnvObj (#7206)Gereon Kremer
2021-09-16Fix relevant domain for parametric operators (#7198)Andrew Reynolds
2021-09-15Minor changes to E-matching utilities (#7062)Andrew Reynolds
2021-09-15Eliminate global access to options:: from quantifiers rewriter (#7192)Andrew Reynolds
2021-09-14bv: Unify bit-blasting code for udiv and urem. (#7188)Mathias Preiner
2021-09-14proofs: Properly track pre- and post-rewrites in bbAtom(). (#7147)Mathias Preiner
2021-09-13Remove context getters from `TheoryState` (#7174)Andres Noetzli
2021-09-13Connect difficulty manager to TheoryEngine (#7161)Andrew Reynolds
2021-09-13FP: Rename FpConverter to FpWordBlaster. (#7170)Aina Niemetz
2021-09-11Use StatisticsRegistry from Env (#7166)Gereon Kremer
2021-09-11bv: Move IsPowerOfTwo rule to preprocessing pass and use EnvObj. (#7179)Mathias Preiner
2021-09-10FP: Enable caching in the theory inference manager. (#7168)Aina Niemetz
2021-09-10bv: Use EnvObj::rewrite() and EnvObj::options() in NodeBitblaster. (#7172)Mathias Preiner
2021-09-10FP: Use EnvObj::rewrite() and options() in theory_fp. (#7169)Aina Niemetz
2021-09-10FP: Do not send trivial lemmas. (#7167)Aina Niemetz
2021-09-10Use C++17 attributes (#7154)Andres Noetzli
2021-09-10bv: Use EnvObj::rewrite() and EnvObj::options() in BvSolver. (#7171)Mathias Preiner
2021-09-09Remove `TheoryState::getEnv()` (#7163)Andres Noetzli
2021-09-09Add difficulty manager (#7151)Andrew Reynolds
2021-09-09Disable shared selectors for quantified logics without SyGuS (#7156)Andrew Reynolds
2021-09-09Remove `TheoryState::options()` (#7148)Andres Noetzli
2021-09-08Remove deprecated SyGuS method evaluateWithUnfolding (#7155)Andrew Reynolds
2021-09-08Improve pre-skolemization, move quantifiers preprocess to own file (#7153)Andrew Reynolds
2021-09-08Towards standard usage of ExtendedRewriter (#7145)Andrew Reynolds
2021-09-08Add option for using bound inference for relevant assertions (#7152)Andrew Reynolds
2021-09-08Use rewriteViaMethod instead of accessing builtin proof checker (#7146)Andrew Reynolds
2021-09-07Use `EnvObj` methods instead of `Theory` methods (#7144)Andres Noetzli
2021-09-07sygus: Eliminate calls to Rewriter::rewrite. (#7142)Aina Niemetz
2021-09-03EnvObj: Add options(), context(), userContext(). (#7137)Aina Niemetz
2021-09-03Avoiding duplicate search in maps (#7055)MikolasJanota
2021-09-03sygus: Make more classes derive from EnvObj. (#7140)Aina Niemetz
2021-09-03Standardize Rewriter::rewriteViaMethod call (#7119)Andrew Reynolds
2021-09-03Make quantifier module classes derive from EnvObj (#7132)Andrew Reynolds
2021-09-03sygus: Make CeSingleInv derive from EnvObj. (#7136)Aina Niemetz
2021-09-03theory: Have more classes in theory with reference to Env derive from EnvObj....Aina Niemetz
2021-09-03theory: Have Theory and TheoryArith* derive from EnvObj. (#7128)Aina Niemetz
2021-09-02Remove more instances of ufHo (#7087)Andrew Reynolds
2021-09-02Remove unused `Backtracker` (#7115)Andres Noetzli
2021-09-02[Unit Tests] Fix bags rewrite test (#7114)Andres Noetzli
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback