projects / cvc5.git / history
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
Clean up occurrences of SmtEngine in comments. (#7349)
[cvc5.git] / src / theory /
2021-10-12 Aina NiemetzClean up occurrences of SmtEngine in comments. (#7349) tree | commitdiff
2021-10-12 Andrew ReynoldsMinor cleaning of instantiation utilities (#7334) tree | commitdiff
2021-10-12 Andrew ReynoldsSimplify skolemization in sygus solver (#7331) tree | commitdiff
2021-10-12 Ouyanchengfix deprecation of std::iterator (#7332) tree | commitdiff
2021-10-11 Aina NiemetzRename SmtScope to SolverEngineScope. (#7284) tree | commitdiff
2021-10-09 Gereon KremerRemove static accesses to options where EnvObj is used... tree | commitdiff
2021-10-07 Andrew ReynoldsUse skolem lemma in prop layer interfaces (#7320) tree | commitdiff
2021-10-07 Andrew ReynoldsMake the cardinality of the alphabet of strings configu... tree | commitdiff
2021-10-07 Andrew ReynoldsMiscellaneous fixes from proof-new (#7313) tree | commitdiff
2021-10-07 Andrew ReynoldsFast exit for string extended equality rewriter (#7312) tree | commitdiff
2021-10-06 Andrew ReynoldsEliminate more hard coded uses of user context (#7309) tree | commitdiff
2021-10-05 Gereon KremerFirst round of refactoring on NlModel (#7255) tree | commitdiff
2021-10-04 Andrew ReynoldsRefactor internally generated bounded quantified formul... tree | commitdiff
2021-10-04 Andrew ReynoldsMove isFiniteType from theory engine to Env (#7287) tree | commitdiff
2021-10-04 Andrew ReynoldsEliminating static calls to rewriter in quantifiers... tree | commitdiff
2021-10-04 Andrew ReynoldsEliminating static calls to rewriter from strings ... tree | commitdiff
2021-10-01 Andrew ReynoldsUpdate theory preprocessor to use Env (#7288) tree | commitdiff
2021-10-01 Andrew ReynoldsMake preregistration safe for uninterpreted constants... tree | commitdiff
2021-10-01 Andrew ReynoldsUse the proper evaluator for optimized SyGuS datatype... tree | commitdiff
2021-10-01 Aina NiemetzRename SmtEngine to SolverEngine. (#7282) tree | commitdiff
2021-09-30 Aina NiemetzRename files smt_engine.(cpp|h) to solver_engine.(cpp... tree | commitdiff
2021-09-30 Mathias Preinerbv: Refactor ppRewrite and move to TheoryBV. (#7271) tree | commitdiff
2021-09-30 Andrew ReynoldsMake theory engine modules use Env (#7277) tree | commitdiff
2021-09-30 Andrew ReynoldsSimplify the syntax and representation of the separatio... tree | commitdiff
2021-09-30 Gereon KremerRemove usage of static options in arithmetic theory... tree | commitdiff
2021-09-29 Abdalrhman MohamedRemove support for extended `(check-sat <term>)` comman... tree | commitdiff
2021-09-29 Andrew ReynoldsProperly restrict PBE symmetry breaking for abduction... tree | commitdiff
2021-09-29 Andrew ReynoldsAdd the strings array solver (#7232) tree | commitdiff
2021-09-24 Andrew ReynoldsEliminate calls to Rewriter::rewrite from strings entai... tree | commitdiff
2021-09-23 Andrew ReynoldsGeneralize string enumerator for fixed length sequences... tree | commitdiff
2021-09-23 Gereon KremerEliminate Output macro in favor of simple Env functions... tree | commitdiff
2021-09-23 Lachnitt[proofs] Alethe: Translate THEORY_REWRITE (#7236) tree | commitdiff
2021-09-23 Gereon KremerRefactor check interface of nonlinear extension (#7235) tree | commitdiff
2021-09-23 Andrew ReynoldsMore uses of EnvObj (#7230) tree | commitdiff
2021-09-23 Abdalrhman MohamedUse `|` to print quoted strings in `set-info` command... tree | commitdiff
2021-09-23 Andrew ReynoldsImplement alpha equivalence proofs (#7066) tree | commitdiff
2021-09-22 Andrew ReynoldsMake cegqi subsolvers EnvObj (#7205) tree | commitdiff
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
next