projects / cvc5.git / history
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
Reimplement support for relational triggers (#7063)
[cvc5.git] / src / theory /
2021-10-20 Andrew ReynoldsReimplement support for relational triggers (#7063) tree | commitdiff
2021-10-20 Andrew ReynoldsDo not make assumption about model for Boolean variable... tree | commitdiff
2021-10-20 Andrew ReynoldsMake proofs of rewrites robust to use in internal subso... tree | commitdiff
2021-10-20 Andrew ReynoldsAdd basic regular expression type enumerator (#7416) tree | commitdiff
2021-10-19 Andrew ReynoldsSupport sequences of fixed finite cardinality (#7371) tree | commitdiff
2021-10-19 Andrew ReynoldsFix issue related to sanity checking integer models... tree | commitdiff
2021-10-18 Abdalrhman MohamedMove check for experimental arrays features to `theory_... tree | commitdiff
2021-10-15 Andrew ReynoldsFix issues related to proofs of lemmas with duplicate... tree | commitdiff
2021-10-14 Andrew ReynoldsSplit entailment check from term database (#7342) tree | commitdiff
2021-10-14 Andrew ReynoldsFix quantifiers variable elimination for parametric... tree | commitdiff
2021-10-13 Andrew ReynoldsEliminate uses of rewrite from datatypes theory (#7354) tree | commitdiff
2021-10-13 Andrew ReynoldsMake (proof) equality engine use Env (#7336) tree | commitdiff
2021-10-12 Andrew ReynoldsSimplify refinement in sygus solver (#7343) tree | commitdiff
2021-10-12 Andrew ReynoldsEliminate calls to currentResourceManager (#7350) tree | commitdiff
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
next