projects / cvc5.git / history
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
Remove CVC language support (#7219)
[cvc5.git] / src / theory /
2021-09-22 Andrew ReynoldsTowards standard usage of evaluator (#7189) tree | commitdiff
2021-09-22 Andrew ReynoldsAdd extensionality option for strings disequalities... tree | commitdiff
2021-09-22 Aina Niemetzarrays: Use EnvObj::rewrite and EnvObj::options. (... tree | commitdiff
2021-09-22 Aina Niemetzarrays: Move type enumerator implementation to .cpp... tree | commitdiff
2021-09-22 Gereon KremerEliminate arithmetic proof macros (#7226) tree | commitdiff
2021-09-21 Andres NoetzliFix handling of conversions between FP and reals (... tree | commitdiff
2021-09-20 Aina NiemetzTheoryModel: Use EnvObj::rewrite instead of Rewriter... tree | commitdiff
2021-09-17 Andres NoetzliUse a single `NodeManager` per thread (#7204) tree | commitdiff
2021-09-17 Gereon KremerReplace write access to options by a local variable... tree | commitdiff
2021-09-17 Gereon KremerMinor cleanup related to EnvObj (#7206) tree | commitdiff
2021-09-16 Andrew ReynoldsFix relevant domain for parametric operators (#7198) tree | commitdiff
2021-09-15 Andrew ReynoldsMinor changes to E-matching utilities (#7062) tree | commitdiff
2021-09-15 Andrew ReynoldsEliminate global access to options:: from quantifiers... tree | commitdiff
2021-09-14 Mathias Preinerbv: Unify bit-blasting code for udiv and urem. (#7188) tree | commitdiff
2021-09-14 Mathias Preinerproofs: Properly track pre- and post-rewrites in bbAtom... tree | commitdiff
2021-09-13 Andres NoetzliRemove context getters from `TheoryState` (#7174) tree | commitdiff
2021-09-13 Andrew ReynoldsConnect difficulty manager to TheoryEngine (#7161) tree | commitdiff
2021-09-13 Aina NiemetzFP: Rename FpConverter to FpWordBlaster. (#7170) tree | commitdiff
2021-09-11 Gereon KremerUse StatisticsRegistry from Env (#7166) tree | commitdiff
2021-09-11 Mathias Preinerbv: Move IsPowerOfTwo rule to preprocessing pass and... tree | commitdiff
2021-09-10 Aina NiemetzFP: Enable caching in the theory inference manager... tree | commitdiff
2021-09-10 Mathias Preinerbv: Use EnvObj::rewrite() and EnvObj::options() in... tree | commitdiff
2021-09-10 Aina NiemetzFP: Use EnvObj::rewrite() and options() in theory_fp... tree | commitdiff
2021-09-10 Aina NiemetzFP: Do not send trivial lemmas. (#7167) tree | commitdiff
2021-09-10 Andres NoetzliUse C++17 attributes (#7154) tree | commitdiff
2021-09-10 Mathias Preinerbv: Use EnvObj::rewrite() and EnvObj::options() in... tree | commitdiff
2021-09-09 Andres NoetzliRemove `TheoryState::getEnv()` (#7163) tree | commitdiff
2021-09-09 Andrew ReynoldsAdd difficulty manager (#7151) tree | commitdiff
2021-09-09 Andrew ReynoldsDisable shared selectors for quantified logics without... tree | commitdiff
2021-09-09 Andres NoetzliRemove `TheoryState::options()` (#7148) tree | commitdiff
2021-09-09 Andrew ReynoldsRemove deprecated SyGuS method evaluateWithUnfolding... tree | commitdiff
2021-09-08 Andrew ReynoldsImprove pre-skolemization, move quantifiers preprocess... tree | commitdiff
2021-09-08 Andrew ReynoldsTowards standard usage of ExtendedRewriter (#7145) tree | commitdiff
2021-09-08 Andrew ReynoldsAdd option for using bound inference for relevant asser... tree | commitdiff
2021-09-08 Andrew ReynoldsUse rewriteViaMethod instead of accessing builtin proof... tree | commitdiff
2021-09-07 Andres NoetzliUse `EnvObj` methods instead of `Theory` methods (... tree | commitdiff
2021-09-07 Aina Niemetzsygus: Eliminate calls to Rewriter::rewrite. (#7142) tree | commitdiff
2021-09-03 Aina NiemetzEnvObj: Add options(), context(), userContext(). (... tree | commitdiff
2021-09-03 MikolasJanotaAvoiding duplicate search in maps (#7055) tree | commitdiff
2021-09-03 Aina Niemetzsygus: Make more classes derive from EnvObj. (#7140) tree | commitdiff
2021-09-03 Andrew ReynoldsStandardize Rewriter::rewriteViaMethod call (#7119) tree | commitdiff
2021-09-03 Andrew ReynoldsMake quantifier module classes derive from EnvObj ... tree | commitdiff
2021-09-03 Aina Niemetzsygus: Make CeSingleInv derive from EnvObj. (#7136) tree | commitdiff
2021-09-03 Aina Niemetztheory: Have more classes in theory with reference... tree | commitdiff
2021-09-03 Aina Niemetztheory: Have Theory and TheoryArith* derive from EnvObj... tree | commitdiff
2021-09-02 Andrew ReynoldsRemove more instances of ufHo (#7087) tree | commitdiff
2021-09-02 Andres NoetzliRemove unused `Backtracker` (#7115) tree | commitdiff
2021-09-02 Andres Noetzli[Unit Tests] Fix bags rewrite test (#7114) tree | commitdiff
2021-09-02 Aina Niemetzrewriter: Make rewriteEqualityExt non-static. (#7110) tree | commitdiff
2021-09-01 Aina NiemetzClean up TheoryEngine header according to code style... tree | commitdiff
2021-09-01 Aina Niemetzrewriter: Make registerTheoryRewriter non-static. ... tree | commitdiff
2021-09-01 Aina Niemetzrewriter: Make clearCaches non-static. (#7100) tree | commitdiff
2021-09-01 Andrew ReynoldsLazy proof reconstruction for strings theory solver... tree | commitdiff
2021-08-31 Aina Niemetzbv: Remove dump=bv-rewrites. (#7099) tree | commitdiff
2021-08-31 yoni206bv-to-int-module: implementations and stubs for transla... tree | commitdiff
2021-08-31 Andrew ReynoldsFix normal forms context-dependent simplification for... tree | commitdiff
2021-08-30 mudathirmahgoubAdd kind BAG_MAP and its type rule to bags (#6503) tree | commitdiff
2021-08-30 Andrew ReynoldsFix proof equality engine for "no-explain" premises... tree | commitdiff
2021-08-30 Andrew ReynoldsFix quantifiers dynamic split module for parametric... tree | commitdiff
2021-08-27 Andrew ReynoldsExpand definitions in sygus operators at the SMT level... tree | commitdiff
2021-08-27 Andrew ReynoldsAdd missing methods to Solver API for models (#7052) tree | commitdiff
2021-08-26 Andrew ReynoldsEliminate currentSmtEngine for subsolver calls (#7068) tree | commitdiff
2021-08-26 Andrew ReynoldsMake datatype selector expansion to its own accessible... tree | commitdiff
2021-08-26 Gereon KremerImprove integration of nonlinear arithmetic into the... tree | commitdiff
2021-08-26 Gereon KremerConsolidate language types (#7065) tree | commitdiff
2021-08-25 Gereon KremerAdd missing include (#7067) tree | commitdiff
2021-08-25 Andrew ReynoldsEliminate calls to currentSmtEngine (#7060) tree | commitdiff
2021-08-24 Andrew ReynoldsSplit higher-order term database (#7045) tree | commitdiff
2021-08-24 Andrew ReynoldsRefactor enumerator management in synth conjecture... tree | commitdiff
2021-08-24 yoni206bv-to-int: more implementations (#7051) tree | commitdiff
2021-08-24 Andrew ReynoldsUniform treatment of trusted theory inferences in proof... tree | commitdiff
2021-08-23 Andrew ReynoldsFix non-deterministism in quantified datatypes expansio... tree | commitdiff
2021-08-23 Andrew ReynoldsPurify substitutions in strings proof reconstruction... tree | commitdiff
2021-08-23 Andrew ReynoldsGeneralize inequality elimination in quantifiers rewrit... tree | commitdiff
2021-08-23 Andrew ReynoldsFix single invocation partition for higher-order (... tree | commitdiff
2021-08-22 Andrew ReynoldsPrenex quantified formulas with user annotations by... tree | commitdiff
2021-08-20 Andrew ReynoldsSimplify how user-provided quantifier attributes are... tree | commitdiff
2021-08-20 Andrew ReynoldsMore refactoring of set defaults (#7043) tree | commitdiff
2021-08-20 Andrew ReynoldsEliminate eager model building (#7038) tree | commitdiff
2021-08-20 Gereon KremerUse Env class in nonlinear extension (#7039) tree | commitdiff
2021-08-19 Andrew ReynoldsCatch cases where recursive functions reference functio... tree | commitdiff
2021-08-19 Gereon KremerStart using Options via Env in arithmetic (#7032) tree | commitdiff
2021-08-18 Gereon Kremermove collectAssertedTerms back to the theory class... tree | commitdiff
2021-08-18 Andres NoetzliMinor fixes of policy for eliminating quantifiers ... tree | commitdiff
2021-08-17 Andres NoetzliReplace `Maybe` with `std::optional` (#7005) tree | commitdiff
2021-08-17 Andrew ReynoldsRefactoring theory-specific variable elimination in... tree | commitdiff
2021-08-17 Andrew ReynoldsFix policy for eliminating quantified formulas (#7017) tree | commitdiff
2021-08-17 Andrew ReynoldsMake theory BV use central eq engine when option is... tree | commitdiff
2021-08-17 Andrew ReynoldsCosmetic improvements to theory datatypes (#7020) tree | commitdiff
2021-08-17 Andrew ReynoldsImprove conversion to skolems in expression miner ... tree | commitdiff
2021-08-17 Gereon KremerPush Env class into TheoryState (#7012) tree | commitdiff
2021-08-16 Gereon KremerUse InferenceManager in ExtTheory (#7006) tree | commitdiff
2021-08-16 Gereon KremerMake Theory class use Env (#7011) tree | commitdiff
2021-08-16 Andres Noetzli[Strings] Make fact detection more robust (#7007) tree | commitdiff
2021-08-05 Andrew ReynoldsFix policy for rewriting string equalities (#6916) tree | commitdiff
2021-08-04 Andrew ReynoldsAdd inference ids for remainder of sygus solver (#6977) tree | commitdiff
2021-08-04 Haniel BarbosaImprove error messages for UF catching higher-order... tree | commitdiff
2021-08-04 Mathias Preinersyqi: Add debug information for dumping instantiations... tree | commitdiff
2021-08-04 Andrew ReynoldsAdd optional debug information for dumping instantiatio... tree | commitdiff
2021-08-04 Andrew ReynoldsAdd missing inference identifiers (#6962) tree | commitdiff
next