projects / cvc5.git / shortlog
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
cvc5.git
2021-08-23 Andrew ReynoldsPurify substitutions in strings proof reconstruction... commit | commitdiff | tree
2021-08-23 Andrew ReynoldsGeneralize inequality elimination in quantifiers rewrit... commit | commitdiff | tree
2021-08-23 Andrew ReynoldsFix single invocation partition for higher-order (... commit | commitdiff | tree
2021-08-23 Gereon KremerMove options parsing code to main (#7054) commit | commitdiff | tree
2021-08-23 yoni206Adding parameters to Datatype python API documentation... commit | commitdiff | tree
2021-08-23 Aina Niemetzapi: Require size argument for mkBitVector. (#6998) commit | commitdiff | tree
2021-08-23 Gereon KremerUse options correctly in competition mode (#7053) commit | commitdiff | tree
2021-08-22 Andrew ReynoldsSimplify model printing modes (#7049) commit | commitdiff | tree
2021-08-22 Andrew ReynoldsPrenex quantified formulas with user annotations by... commit | commitdiff | tree
2021-08-20 Gereon KremerMake driver use options from the solver (#6930) commit | commitdiff | tree
2021-08-20 Andrew ReynoldsSimplify how user-provided quantifier attributes are... commit | commitdiff | tree
2021-08-20 mudathirmahgoubAdd Term.java to the Java API (#6330) commit | commitdiff | tree
2021-08-20 Andrew ReynoldsMore refactoring of set defaults (#7043) commit | commitdiff | tree
2021-08-20 Andrew ReynoldsSupport sygus standard command syntax set-feature ... commit | commitdiff | tree
2021-08-20 Andrew ReynoldsEliminate eager model building (#7038) commit | commitdiff | tree
2021-08-20 Gereon KremerUse Env class in nonlinear extension (#7039) commit | commitdiff | tree
2021-08-20 Gereon KremerAdd CVC5ApiOptionException (#6992) commit | commitdiff | tree
2021-08-19 yoni206Make the python quickstart example run using ctest... commit | commitdiff | tree
2021-08-19 yoni206Add python quick start guide (#7024) commit | commitdiff | tree
2021-08-19 Andres NoetzliRemove `--(no-)interactive-prompt` (#7022) commit | commitdiff | tree
2021-08-19 Andrew ReynoldsCatch cases where recursive functions reference functio... commit | commitdiff | tree
2021-08-19 Andrew ReynoldsSplit proof final callback to its own file (#6984) commit | commitdiff | tree
2021-08-19 Andrew ReynoldsRefactor proof output for TPTP (#7029) commit | commitdiff | tree
2021-08-19 Gereon KremerStart using Options via Env in arithmetic (#7032) commit | commitdiff | tree
2021-08-19 Haniel Barbosa[unsat cores] [proofs] Revert test about when to explai... commit | commitdiff | tree
2021-08-18 Gereon Kremermove collectAssertedTerms back to the theory class... commit | commitdiff | tree
2021-08-18 Andres NoetzliMinor fixes of policy for eliminating quantifiers ... commit | commitdiff | tree
2021-08-18 Andrew ReynoldsMake TheoryProxy use Env, simplify initialization of... commit | commitdiff | tree
2021-08-17 Andres NoetzliReplace `Maybe` with `std::optional` (#7005) commit | commitdiff | tree
2021-08-17 Andrew ReynoldsMake SmtEngineState use Env (#7028) commit | commitdiff | tree
2021-08-17 Andrew ReynoldsRefactoring theory-specific variable elimination in... commit | commitdiff | tree
2021-08-17 Andrew ReynoldsFix policy for eliminating quantified formulas (#7017) commit | commitdiff | tree
2021-08-17 Andrew ReynoldsMake theory BV use central eq engine when option is... commit | commitdiff | tree
2021-08-17 Andrew ReynoldsCosmetic improvements to theory datatypes (#7020) commit | commitdiff | tree
2021-08-17 Andrew ReynoldsImprove conversion to skolems in expression miner ... commit | commitdiff | tree
2021-08-17 Andrew ReynoldsInitial refactoring of set defaults (#7021) commit | commitdiff | tree
2021-08-17 Gereon KremerPush Env class into TheoryState (#7012) commit | commitdiff | tree
2021-08-16 Gereon KremerUse InferenceManager in ExtTheory (#7006) commit | commitdiff | tree
2021-08-16 Gereon KremerMake Theory class use Env (#7011) commit | commitdiff | tree
2021-08-16 Andres Noetzli[Strings] Make fact detection more robust (#7007) commit | commitdiff | tree
2021-08-16 Andrew V. JonesAdd check for static libraries when compiling CryptoMin... commit | commitdiff | tree
2021-08-16 Andrew V. JonesCorrect copyright print for GLPK (#7015) commit | commitdiff | tree
2021-08-13 Gereon KremerRefactor setDefaults to use an options object (#6994) commit | commitdiff | tree
2021-08-10 Andres NoetzliDisable external initialization of `thread_local` varia... commit | commitdiff | tree
2021-08-10 Gereon KremerSimplify generation of option module code. (#6995) commit | commitdiff | tree
2021-08-09 Andrew V. JonesCreate grouping of tests that exercise '--use-approx... commit | commitdiff | tree
2021-08-09 Andres NoetzliSupport older CMake versions (#7003) commit | commitdiff | tree
2021-08-06 Gereon KremerMerge options cmake into general cmake file (#6989) commit | commitdiff | tree
2021-08-06 Gereon KremerClear options manager (#6991) commit | commitdiff | tree
2021-08-05 Alex OzdemirNormalize val in BitVector(val_str, base) (#6955) commit | commitdiff | tree
2021-08-05 Andrew ReynoldsGeneralize term canonizer for type classes (#6895) commit | commitdiff | tree
2021-08-05 Andres Noetzli[Unit Tests] Add missing include (#6990) commit | commitdiff | tree
2021-08-05 Andrew ReynoldsFix policy for rewriting string equalities (#6916) commit | commitdiff | tree
2021-08-05 Gereon KremerNo longer call solver constructor with an options objec... commit | commitdiff | tree
2021-08-04 Gereon KremerConsolidate solver resets (#6986) commit | commitdiff | tree
2021-08-04 Andrew ReynoldsProper printing of proofs in the internal calculus... commit | commitdiff | tree
2021-08-04 Andrew ReynoldsFix policy for merging subproofs (#6981) commit | commitdiff | tree
2021-08-04 Diego Della... [proof] [dot] Fix comments on dot printer (#6983) commit | commitdiff | tree
2021-08-04 Andrew ReynoldsAdd inference ids for remainder of sygus solver (#6977) commit | commitdiff | tree
2021-08-04 Haniel BarbosaImprove error messages for UF catching higher-order... commit | commitdiff | tree
2021-08-04 Mathias Preinersyqi: Add debug information for dumping instantiations... commit | commitdiff | tree
2021-08-04 Andrew ReynoldsAdd optional debug information for dumping instantiatio... commit | commitdiff | tree
2021-08-04 Aina NiemetzUpdate bug_report.md commit | commitdiff | tree
2021-08-04 Andrew ReynoldsAdd containsAssumption proof utility (#6953) commit | commitdiff | tree
2021-08-04 Gereon KremerRefactor managed streams (#6934) commit | commitdiff | tree
2021-08-04 Gereon KremerAdd API function to get list of option names (#6971) commit | commitdiff | tree
2021-08-04 Gereon KremerReplace numeric predicates by explicit minimum and... commit | commitdiff | tree
2021-08-04 Andrew ReynoldsAdd missing inference identifiers (#6962) commit | commitdiff | tree
2021-08-04 Haniel Barbosa[proof] Add getProof to API and use it in GetProofComma... commit | commitdiff | tree
2021-08-04 Alex OzdemirAdd IEEE-BV-to-FP to external-to-internal mapping in... commit | commitdiff | tree
2021-08-04 Andrew ReynoldsRemove dependencies on smt engine in smt solver (#6965) commit | commitdiff | tree
2021-08-03 Gereon KremerUse int64_t, uint64_t or double for all numeric options... commit | commitdiff | tree
2021-08-03 Andrew ReynoldsRefactor shared solver to use theory builtin inference... commit | commitdiff | tree
2021-08-03 Andrew ReynoldsRemove "inUnsatCore" flag throughout (#6964) commit | commitdiff | tree
2021-08-03 Gereon KremerProperly honor --stats-all and --stats-expert when... commit | commitdiff | tree
2021-08-02 Aina NiemetzAdd 'REQUIRES: poly' to regression. (#6966) commit | commitdiff | tree
2021-08-02 Mathias Preinerbv: Enable equality engine for bitblast-internal. ... commit | commitdiff | tree
2021-07-31 Gereon KremerPerform statistics printing via the API (#6952) commit | commitdiff | tree
2021-07-30 Gereon KremerAllow changing certain options while solving (#6945) commit | commitdiff | tree
2021-07-30 Andrew ReynoldsSimplify smt2 printer (#6954) commit | commitdiff | tree
2021-07-29 Gereon KremerIntegrate installation instructions into documentation... commit | commitdiff | tree
2021-07-29 Aina Niemetzquickstart: Add python example to docs. (#6949) commit | commitdiff | tree
2021-07-29 Haniel Barbosa[proofs] Set BV solver to better proof-producing one... commit | commitdiff | tree
2021-07-29 yoni206Python quick start example (#6939) commit | commitdiff | tree
2021-07-29 Andrew ReynoldsIntegrate central equality engine approach into theory... commit | commitdiff | tree
2021-07-29 Andrew ReynoldsMinor updates to shared terms database for central... commit | commitdiff | tree
2021-07-28 makaimannFixes for building python wheels on manylinux2014 ... commit | commitdiff | tree
2021-07-28 Andrew ReynoldsMinor changes to arrays in preparation for central... commit | commitdiff | tree
2021-07-28 Gereon KremerOnly use libedit on tty inputs (#6946) commit | commitdiff | tree
2021-07-28 Andres NoetzliPrint link to docs preview (#6922) commit | commitdiff | tree
2021-07-28 Andrew ReynoldsMake extended rewriter methods const (#6948) commit | commitdiff | tree
2021-07-27 Mathias Preinerbv: Refactor getEqualityStatus and use for both bitblas... commit | commitdiff | tree
2021-07-27 Mathias Preinerproof: Add eqrange expansion rule. (#6936) commit | commitdiff | tree
2021-07-27 Andrew ReynoldsTrack instantiation reasons in proofs (#6935) commit | commitdiff | tree
2021-07-27 Andrew ReynoldsAdd basic LFSC utilities (#6879) commit | commitdiff | tree
2021-07-27 Andrew ReynoldsMove enum value generator to own file (#6941) commit | commitdiff | tree
2021-07-27 Andrew ReynoldsMinor fix for term database + central equality engine... commit | commitdiff | tree
2021-07-27 Andrew ReynoldsRevert change to regression (#6940) commit | commitdiff | tree
2021-07-27 Andrew ReynoldsMake all dependencies in the fast enumerator optional... commit | commitdiff | tree
2021-07-27 Andrew ReynoldsAdd print expression utility (#6880) commit | commitdiff | tree
next