Add difficulty manager (#7151)
[cvc5.git] / src /
2021-09-09 Andrew ReynoldsAdd difficulty manager (#7151)
2021-09-09 Andrew ReynoldsAdd difficulty post-processor (#7150)
2021-09-09 Andrew ReynoldsDisable shared selectors for quantified logics without...
2021-09-09 Andres NoetzliRemove `TheoryState::options()` (#7148)
2021-09-09 Andrew ReynoldsRemove deprecated SyGuS method evaluateWithUnfolding...
2021-09-08 Andrew ReynoldsAdd Lfsc print channel utilities (#7123)
2021-09-08 Andrew ReynoldsImprove pre-skolemization, move quantifiers preprocess...
2021-09-08 Gereon KremerRefactor options::set() (#7138)
2021-09-08 Gereon KremerWork on comments (#7139)
2021-09-08 Gereon KremerA couple of minor cleanups (#7141)
2021-09-08 Gereon KremerRefactor code generation for options.h/.cpp (#7126)
2021-09-08 Andrew ReynoldsTowards standard usage of ExtendedRewriter (#7145)
2021-09-08 Andrew ReynoldsAdd option for using bound inference for relevant asser...
2021-09-08 Andrew ReynoldsAdd LFSC side condition conversion utility for list...
2021-09-08 mudathirmahgoubAdd Datatype.java to the Java API (#6389)
2021-09-08 mudathirmahgoubAdd DatatypeConstructor.java, DatatypeConstructorDecl...
2021-09-08 Andrew ReynoldsUse rewriteViaMethod instead of accessing builtin proof...
2021-09-07 Andrew ReynoldsRefactoring of proof manager initialization (#7073)
2021-09-07 Andres NoetzliUse `EnvObj` methods instead of `Theory` methods (...
2021-09-07 Aina Niemetzsygus: Eliminate calls to Rewriter::rewrite. (#7142)
2021-09-07 Andrew ReynoldsRefactoring and fixes of set defaults for quantifiers...
2021-09-03 Aina NiemetzEnvObj: Add options(), context(), userContext(). (...
2021-09-03 MikolasJanotaAvoiding duplicate search in maps (#7055)
2021-09-03 Aina Niemetzsygus: Make more classes derive from EnvObj. (#7140)
2021-09-03 Gereon KremerRefactor option sanitizations (#7129)
2021-09-03 Andrew ReynoldsStandardize Rewriter::rewriteViaMethod call (#7119)
2021-09-03 Gereon KremerCheck that alternate is only set for bool (#7125)
2021-09-03 Gereon KremerRefactor options::get() and options::getNames() (#7135)
2021-09-03 Andrew ReynoldsMake quantifier module classes derive from EnvObj ...
2021-09-03 Aina Niemetzsygus: Make CeSingleInv derive from EnvObj. (#7136)
2021-09-03 Andrew ReynoldsEliminate backwards ref to SmtEngine from abduction...
2021-09-03 Aina Niemetztheory: Have more classes in theory with reference...
2021-09-03 Aina Niemetztheory: Have Theory and TheoryArith* derive from EnvObj...
2021-09-03 Gereon KremerRemove "experimental" options (#7124)
2021-09-03 Aina Niemetzpp: Have PreprocessingPassContext derive from EnvObj...
2021-09-02 Andrew ReynoldsAdd LFSC node converter (#6944)
2021-09-02 Gereon KremerRefactor options handlers (#7080)
2021-09-02 Andres Noetzli[Unit Tests] Fix shell test for Editline (#7117)
2021-09-02 Aina NiemetzEnvObj: Restrict access. (#7121)
2021-09-02 Gereon KremerAdd API check whether option in getOptionInfo() exists...
2021-09-02 Gereon KremerDriver & Options cleanup (#7109)
2021-09-02 Andrew ReynoldsRemove more instances of ufHo (#7087)
2021-09-02 Gereon KremerRemove options::getAll() (#7111)
2021-09-02 Andrew ReynoldsImplement lazy proof checking modes (#7106)
2021-09-02 Aina NiemetzRemove PreprocessingPassContext::getSmt(). (#7118)
2021-09-02 Andres NoetzliRemove unused `Backtracker` (#7115)
2021-09-02 Andres Noetzli[Unit Tests] Fix bags rewrite test (#7114)
2021-09-02 Aina Niemetzpp: Derive PreprocessingPass from EnvObj. (#7112)
2021-09-02 Aina NiemetzEnable sygus-inst for FP, NIA and NRA. (#7098)
2021-09-02 Aina Niemetzrewriter: Make rewriteEqualityExt non-static. (#7110)
2021-09-02 Aina NiemetzAdd class EnvObj. (#7113)
2021-09-01 Aina NiemetzClean up and document PP context. (#7102)
2021-09-01 Aina NiemetzClean up TheoryEngine header according to code style...
2021-09-01 Haniel Barbosa[proof] [sat] Fix lost reference to reason when process...
2021-09-01 Andrew ReynoldsPrint response to get-model using the API (#7084)
2021-09-01 Aina Niemetzrewriter: Make registerTheoryRewriter non-static. ...
2021-09-01 Andrew ReynoldsFix issues with cyclic proofs due to double SYMM applic...
2021-09-01 Gereon KremerMake driver::totalTime a TimerStat (#7089)
2021-09-01 Gereon KremerNo longer use direct access to options in driver (...
2021-09-01 Aina Niemetzrewriter: Make clearCaches non-static. (#7100)
2021-09-01 Andrew ReynoldsLazy proof reconstruction for strings theory solver...
2021-08-31 Aina Niemetzbv: Remove dump=bv-rewrites. (#7099)
2021-08-31 Gereon KremerMake sure modes are sorted in ModeInfo (#7097)
2021-08-31 yoni206bv-to-int-module: implementations and stubs for transla...
2021-08-31 Andrew ReynoldsFix normal forms context-dependent simplification for...
2021-08-31 Andrew ReynoldsMake regular expression sort not closed enumerable...
2021-08-30 Gereon KremerAdd API function to obtain information about a single...
2021-08-30 mudathirmahgoubAdd kind BAG_MAP and its type rule to bags (#6503)
2021-08-30 Andrew ReynoldsFurther refactoring of set defaults for incompatibility...
2021-08-30 Gereon KremerRefactor filename handling (#7088)
2021-08-30 Andrew ReynoldsFix proof equality engine for "no-explain" premises...
2021-08-30 yoni206python docs for Datatype-related classes (#7058)
2021-08-30 Andrew ReynoldsFix quantifiers dynamic split module for parametric...
2021-08-27 Gereon KremerAdd Driver options (#7078)
2021-08-27 Gereon KremerHandle languages as strings in driver (#7074)
2021-08-27 Andrew ReynoldsExpand definitions in sygus operators at the SMT level...
2021-08-27 Andrew ReynoldsAdd n-ary match trie utility (#6909)
2021-08-27 Andrew ReynoldsAdd missing methods to Solver API for models (#7052)
2021-08-27 yoni206Add `isNull` to cpp api tests, python api, and python...
2021-08-26 Andrew ReynoldsEliminate currentSmtEngine for subsolver calls (#7068)
2021-08-26 Andrew ReynoldsDump models for isNotEntailed results (#7071)
2021-08-26 Andrew ReynoldsMake datatype selector expansion to its own accessible...
2021-08-26 Gereon KremerImprove integration of nonlinear arithmetic into the...
2021-08-26 Mathias Preinerint2bv: Fix conversion of signed bit-vector values...
2021-08-26 Gereon KremerConsolidate language types (#7065)
2021-08-25 Gereon KremerAdd missing include (#7067)
2021-08-25 Andrew ReynoldsEliminate calls to currentSmtEngine (#7060)
2021-08-24 Andrew ReynoldsSplit higher-order term database (#7045)
2021-08-24 Andrew ReynoldsRefactor enumerator management in synth conjecture...
2021-08-24 yoni206bv-to-int: more implementations (#7051)
2021-08-24 Andrew ReynoldsTop-level structure for set defaults (#7047)
2021-08-24 Andrew ReynoldsUniform treatment of trusted theory inferences in proof...
2021-08-24 Andrew ReynoldsMiscellaneous changes from proof-new (#7042)
2021-08-23 Andrew ReynoldsFix non-deterministism in quantified datatypes expansio...
2021-08-23 Andrew ReynoldsPurify substitutions in strings proof reconstruction...
2021-08-23 Andrew ReynoldsGeneralize inequality elimination in quantifiers rewrit...
2021-08-23 Andrew ReynoldsFix single invocation partition for higher-order (...
2021-08-23 Gereon KremerMove options parsing code to main (#7054)
2021-08-23 yoni206Adding parameters to Datatype python API documentation...
2021-08-23 Aina Niemetzapi: Require size argument for mkBitVector. (#6998)
next