projects / cvc5.git / history
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
Fix GLPK linking (#7357)
[cvc5.git] / src /
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 Niemetzpp: Derive PreprocessingPass from EnvObj. (#7112) tree | commitdiff
2021-09-02 Aina NiemetzEnable sygus-inst for FP, NIA and NRA. (#7098) tree | commitdiff
2021-09-02 Aina Niemetzrewriter: Make rewriteEqualityExt non-static. (#7110) tree | commitdiff
2021-09-02 Aina NiemetzAdd class EnvObj. (#7113) tree | commitdiff
2021-09-01 Aina NiemetzClean up and document PP context. (#7102) tree | commitdiff
2021-09-01 Aina NiemetzClean up TheoryEngine header according to code style... tree | commitdiff
2021-09-01 Haniel Barbosa[proof] [sat] Fix lost reference to reason when process... tree | commitdiff
2021-09-01 Andrew ReynoldsPrint response to get-model using the API (#7084) tree | commitdiff
2021-09-01 Aina Niemetzrewriter: Make registerTheoryRewriter non-static. ... tree | commitdiff
2021-09-01 Andrew ReynoldsFix issues with cyclic proofs due to double SYMM applic... tree | commitdiff
2021-09-01 Gereon KremerMake driver::totalTime a TimerStat (#7089) tree | commitdiff
2021-09-01 Gereon KremerNo longer use direct access to options in driver (... 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 Gereon KremerMake sure modes are sorted in ModeInfo (#7097) 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-31 Andrew ReynoldsMake regular expression sort not closed enumerable... tree | commitdiff
2021-08-30 Gereon KremerAdd API function to obtain information about a single... tree | commitdiff
2021-08-30 mudathirmahgoubAdd kind BAG_MAP and its type rule to bags (#6503) tree | commitdiff
2021-08-30 Andrew ReynoldsFurther refactoring of set defaults for incompatibility... tree | commitdiff
2021-08-30 Gereon KremerRefactor filename handling (#7088) tree | commitdiff
2021-08-30 Andrew ReynoldsFix proof equality engine for "no-explain" premises... tree | commitdiff
2021-08-30 yoni206python docs for Datatype-related classes (#7058) tree | commitdiff
2021-08-30 Andrew ReynoldsFix quantifiers dynamic split module for parametric... tree | commitdiff
2021-08-27 Gereon KremerAdd Driver options (#7078) tree | commitdiff
2021-08-27 Gereon KremerHandle languages as strings in driver (#7074) tree | commitdiff
2021-08-27 Andrew ReynoldsExpand definitions in sygus operators at the SMT level... tree | commitdiff
2021-08-27 Andrew ReynoldsAdd n-ary match trie utility (#6909) tree | commitdiff
2021-08-27 Andrew ReynoldsAdd missing methods to Solver API for models (#7052) tree | commitdiff
2021-08-27 yoni206Add `isNull` to cpp api tests, python api, and python... tree | commitdiff
2021-08-26 Andrew ReynoldsEliminate currentSmtEngine for subsolver calls (#7068) tree | commitdiff
2021-08-26 Andrew ReynoldsDump models for isNotEntailed results (#7071) 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 Mathias Preinerint2bv: Fix conversion of signed bit-vector values... 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 ReynoldsTop-level structure for set defaults (#7047) tree | commitdiff
2021-08-24 Andrew ReynoldsUniform treatment of trusted theory inferences in proof... tree | commitdiff
2021-08-24 Andrew ReynoldsMiscellaneous changes from proof-new (#7042) 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-23 Gereon KremerMove options parsing code to main (#7054) tree | commitdiff
2021-08-23 yoni206Adding parameters to Datatype python API documentation... tree | commitdiff
2021-08-23 Aina Niemetzapi: Require size argument for mkBitVector. (#6998) tree | commitdiff
2021-08-23 Gereon KremerUse options correctly in competition mode (#7053) tree | commitdiff
2021-08-22 Andrew ReynoldsSimplify model printing modes (#7049) tree | commitdiff
2021-08-22 Andrew ReynoldsPrenex quantified formulas with user annotations by... tree | commitdiff
2021-08-20 Gereon KremerMake driver use options from the solver (#6930) tree | commitdiff
2021-08-20 Andrew ReynoldsSimplify how user-provided quantifier attributes are... tree | commitdiff
2021-08-20 mudathirmahgoubAdd Term.java to the Java API (#6330) tree | commitdiff
2021-08-20 Andrew ReynoldsMore refactoring of set defaults (#7043) tree | commitdiff
2021-08-20 Andrew ReynoldsSupport sygus standard command syntax set-feature ... 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-20 Gereon KremerAdd CVC5ApiOptionException (#6992) tree | commitdiff
2021-08-19 Andres NoetzliRemove `--(no-)interactive-prompt` (#7022) tree | commitdiff
2021-08-19 Andrew ReynoldsCatch cases where recursive functions reference functio... tree | commitdiff
2021-08-19 Andrew ReynoldsSplit proof final callback to its own file (#6984) tree | commitdiff
2021-08-19 Andrew ReynoldsRefactor proof output for TPTP (#7029) tree | commitdiff
2021-08-19 Gereon KremerStart using Options via Env in arithmetic (#7032) tree | commitdiff
2021-08-19 Haniel Barbosa[unsat cores] [proofs] Revert test about when to explai... 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-18 Andrew ReynoldsMake TheoryProxy use Env, simplify initialization of... tree | commitdiff
2021-08-17 Andres NoetzliReplace `Maybe` with `std::optional` (#7005) tree | commitdiff
2021-08-17 Andrew ReynoldsMake SmtEngineState use Env (#7028) 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 Andrew ReynoldsInitial refactoring of set defaults (#7021) 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-16 Andrew V. JonesCorrect copyright print for GLPK (#7015) tree | commitdiff
2021-08-13 Gereon KremerRefactor setDefaults to use an options object (#6994) tree | commitdiff
2021-08-10 Gereon KremerSimplify generation of option module code. (#6995) tree | commitdiff
2021-08-09 Andres NoetzliSupport older CMake versions (#7003) tree | commitdiff
2021-08-06 Gereon KremerMerge options cmake into general cmake file (#6989) tree | commitdiff
2021-08-06 Gereon KremerClear options manager (#6991) tree | commitdiff
2021-08-05 Alex OzdemirNormalize val in BitVector(val_str, base) (#6955) tree | commitdiff
2021-08-05 Andrew ReynoldsGeneralize term canonizer for type classes (#6895) tree | commitdiff
2021-08-05 Andrew ReynoldsFix policy for rewriting string equalities (#6916) tree | commitdiff
2021-08-04 Gereon KremerConsolidate solver resets (#6986) tree | commitdiff
2021-08-04 Andrew ReynoldsProper printing of proofs in the internal calculus... tree | commitdiff
2021-08-04 Andrew ReynoldsFix policy for merging subproofs (#6981) tree | commitdiff
2021-08-04 Diego Della Rocca... [proof] [dot] Fix comments on dot printer (#6983) tree | commitdiff
next