cvc5.git
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 Gereon KremerFix a subtle issues with squashing the docs-ci history...
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)
2021-08-23 Gereon KremerUse options correctly in competition mode (#7053)
2021-08-22 Andrew ReynoldsSimplify model printing modes (#7049)
2021-08-22 Andrew ReynoldsPrenex quantified formulas with user annotations by...
2021-08-20 Gereon KremerMake driver use options from the solver (#6930)
2021-08-20 Andrew ReynoldsSimplify how user-provided quantifier attributes are...
2021-08-20 mudathirmahgoubAdd Term.java to the Java API (#6330)
2021-08-20 Andrew ReynoldsMore refactoring of set defaults (#7043)
2021-08-20 Andrew ReynoldsSupport sygus standard command syntax set-feature ...
2021-08-20 Andrew ReynoldsEliminate eager model building (#7038)
2021-08-20 Gereon KremerUse Env class in nonlinear extension (#7039)
2021-08-20 Gereon KremerAdd CVC5ApiOptionException (#6992)
2021-08-19 yoni206Make the python quickstart example run using ctest...
2021-08-19 yoni206Add python quick start guide (#7024)
2021-08-19 Andres NoetzliRemove `--(no-)interactive-prompt` (#7022)
2021-08-19 Andrew ReynoldsCatch cases where recursive functions reference functio...
2021-08-19 Andrew ReynoldsSplit proof final callback to its own file (#6984)
2021-08-19 Andrew ReynoldsRefactor proof output for TPTP (#7029)
2021-08-19 Gereon KremerStart using Options via Env in arithmetic (#7032)
2021-08-19 Haniel Barbosa[unsat cores] [proofs] Revert test about when to explai...
2021-08-18 Gereon Kremermove collectAssertedTerms back to the theory class...
2021-08-18 Andres NoetzliMinor fixes of policy for eliminating quantifiers ...
2021-08-18 Andrew ReynoldsMake TheoryProxy use Env, simplify initialization of...
2021-08-17 Andres NoetzliReplace `Maybe` with `std::optional` (#7005)
2021-08-17 Andrew ReynoldsMake SmtEngineState use Env (#7028)
2021-08-17 Andrew ReynoldsRefactoring theory-specific variable elimination in...
2021-08-17 Andrew ReynoldsFix policy for eliminating quantified formulas (#7017)
2021-08-17 Andrew ReynoldsMake theory BV use central eq engine when option is...
2021-08-17 Andrew ReynoldsCosmetic improvements to theory datatypes (#7020)
2021-08-17 Andrew ReynoldsImprove conversion to skolems in expression miner ...
2021-08-17 Andrew ReynoldsInitial refactoring of set defaults (#7021)
2021-08-17 Gereon KremerPush Env class into TheoryState (#7012)
2021-08-16 Gereon KremerUse InferenceManager in ExtTheory (#7006)
2021-08-16 Gereon KremerMake Theory class use Env (#7011)
2021-08-16 Andres Noetzli[Strings] Make fact detection more robust (#7007)
2021-08-16 Andrew V. JonesAdd check for static libraries when compiling CryptoMin...
2021-08-16 Andrew V. JonesCorrect copyright print for GLPK (#7015)
2021-08-13 Gereon KremerRefactor setDefaults to use an options object (#6994)
2021-08-10 Andres NoetzliDisable external initialization of `thread_local` varia...
2021-08-10 Gereon KremerSimplify generation of option module code. (#6995)
2021-08-09 Andrew V. JonesCreate grouping of tests that exercise '--use-approx...
2021-08-09 Andres NoetzliSupport older CMake versions (#7003)
2021-08-06 Gereon KremerMerge options cmake into general cmake file (#6989)
2021-08-06 Gereon KremerClear options manager (#6991)
2021-08-05 Alex OzdemirNormalize val in BitVector(val_str, base) (#6955)
2021-08-05 Andrew ReynoldsGeneralize term canonizer for type classes (#6895)
2021-08-05 Andres Noetzli[Unit Tests] Add missing include (#6990)
2021-08-05 Andrew ReynoldsFix policy for rewriting string equalities (#6916)
2021-08-05 Gereon KremerNo longer call solver constructor with an options objec...
2021-08-04 Gereon KremerConsolidate solver resets (#6986)
2021-08-04 Andrew ReynoldsProper printing of proofs in the internal calculus...
2021-08-04 Andrew ReynoldsFix policy for merging subproofs (#6981)
2021-08-04 Diego Della... [proof] [dot] Fix comments on dot printer (#6983)
2021-08-04 Andrew ReynoldsAdd inference ids for remainder of sygus solver (#6977)
2021-08-04 Haniel BarbosaImprove error messages for UF catching higher-order...
2021-08-04 Mathias Preinersyqi: Add debug information for dumping instantiations...
2021-08-04 Andrew ReynoldsAdd optional debug information for dumping instantiatio...
2021-08-04 Aina NiemetzUpdate bug_report.md
2021-08-04 Andrew ReynoldsAdd containsAssumption proof utility (#6953)
2021-08-04 Gereon KremerRefactor managed streams (#6934)
2021-08-04 Gereon KremerAdd API function to get list of option names (#6971)
2021-08-04 Gereon KremerReplace numeric predicates by explicit minimum and...
2021-08-04 Andrew ReynoldsAdd missing inference identifiers (#6962)
2021-08-04 Haniel Barbosa[proof] Add getProof to API and use it in GetProofComma...
2021-08-04 Alex OzdemirAdd IEEE-BV-to-FP to external-to-internal mapping in...
2021-08-04 Andrew ReynoldsRemove dependencies on smt engine in smt solver (#6965)
next