projects / cvc5.git / shortlog
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
cvc5.git
2021-07-12 Andres NoetzliFix ANTLR build on CMake <3.11 (#6864) commit | commitdiff | tree
2021-07-12 Andrew ReynoldsAdd arithmetic preprocess rewrite equality module ... commit | commitdiff | tree
2021-07-12 Andrew ReynoldsAdd trace for combination splits (#6862) commit | commitdiff | tree
2021-07-12 Andres NoetzliUse default visibility for `cvc5::Exception` (#6856) commit | commitdiff | tree
2021-07-12 Andrew ReynoldsImprovements to debug check model (#6861) commit | commitdiff | tree
2021-07-09 Haniel Barbosatest also with default cores (#6858) commit | commitdiff | tree
2021-07-09 Andres NoetzliMake regression test `issue4971-0` more robust (#6857) commit | commitdiff | tree
2021-07-09 Andres NoetzliUse newer config.sub to fix build on Apple M1 (#6854) commit | commitdiff | tree
2021-07-09 Andrew ReynoldsFix sets cardinality inference involving equivalent... commit | commitdiff | tree
2021-07-09 Andrew ReynoldsImplement stop-only for new justification heuristic... commit | commitdiff | tree
2021-07-08 Andrew ReynoldsDisable ordering heuristic for justification by default... commit | commitdiff | tree
2021-07-08 makaimannAdd script to build wheel for pycvc5 (#6839) commit | commitdiff | tree
2021-07-08 Haniel Barbosa[proof] [dot] Print let map (of terms in proof) as... commit | commitdiff | tree
2021-07-07 Haniel Barbosa[unsat cores] Adding regressions from #4971 (#6852) commit | commitdiff | tree
2021-07-07 Aina Niemetzpow2: Update NEWS. (#6851) commit | commitdiff | tree
2021-07-07 Aina NiemetzRename operator pow2 to int.pow2. (#6849) commit | commitdiff | tree
2021-07-07 Andrew ReynoldsFix regressions for competition build (#6846) commit | commitdiff | tree
2021-07-07 Andrew ReynoldsStandard output for trigger selection (#6841) commit | commitdiff | tree
2021-07-06 Gereon KremerIntegrate Lazard into CAD module (#6812) commit | commitdiff | tree
2021-07-06 Andrew ReynoldsIntegrate learned rewrite preprocessing pass (#6840) commit | commitdiff | tree
2021-07-06 Andrew ReynoldsAdd implementation of learned rewrite pass (#6843) commit | commitdiff | tree
2021-07-06 Andrew ReynoldsAdd learned rewrite preprocessing pass (#6842) commit | commitdiff | tree
2021-07-06 Haniel BarbosaPorting C++ API examples to SMT-LIB examples (#6789) commit | commitdiff | tree
2021-07-06 OuyanchengAdd some printing functions for OptimizationObjective... commit | commitdiff | tree
2021-07-06 Gereon KremerAdd doc page about transcendentals (#6755) commit | commitdiff | tree
2021-07-05 Andres Noetzli[Strings] Fix incorrect rewrite (#6837) commit | commitdiff | tree
2021-07-05 Andrew ReynoldsMake buffered inference manager more robust to backtrac... commit | commitdiff | tree
2021-07-03 Andres NoetzliFix performance of string regression (#6832) commit | commitdiff | tree
2021-07-03 Mathias PreinerAdd output tags -o, --output. (#6826) commit | commitdiff | tree
2021-07-02 Mathias PreinerFix bv assert input reset assertions (#6820) commit | commitdiff | tree
2021-07-02 Andrew ReynoldsFix rewriter for negative constant seq.nth (#6827) commit | commitdiff | tree
2021-07-02 Andres NoetzliFix CaDiCaL auto-download on macOS (#6828) commit | commitdiff | tree
2021-07-02 Gereon KremerRefactor lexer for SMT-LIB in sphinx (#6805) commit | commitdiff | tree
2021-07-02 Andres NoetzliAdd reverse iterators to `Node`/`TNode` (#6825) commit | commitdiff | tree
2021-07-01 Andrew ReynoldsAdd recursive function definitions to subsolver in... commit | commitdiff | tree
2021-07-01 Gereon KremerFix message to show that cadical and symfpu are require... commit | commitdiff | tree
2021-07-01 Andrew ReynoldsAdd option to limit the number of instantiation rounds... commit | commitdiff | tree
2021-06-30 Mathias PreinerUse SAT context level for --bv-assert-input instead... commit | commitdiff | tree
2021-06-30 Gereon KremerUse authored date instead of commit date. (#6815) commit | commitdiff | tree
2021-06-30 yoni206pow2: new test (#6819) commit | commitdiff | tree
2021-06-30 Andrew ReynoldsDo not notify during equality engine initialization... commit | commitdiff | tree
2021-06-30 Andrew ReynoldsDo not apply fmfBound to standard quantifiers when... commit | commitdiff | tree
2021-06-30 Andrew ReynoldsFix pre vs. post-rewrite in proofs for theory preproces... commit | commitdiff | tree
2021-06-30 yoni206int-to-bv: correct model values (#6811) commit | commitdiff | tree
2021-06-29 Gereon KremerAdd new variants for the CAD projection (#6794) commit | commitdiff | tree
2021-06-29 Mathias PreinerFix statistics in AigBitblaster. (#6810) commit | commitdiff | tree
2021-06-29 Aina NiemetzFP: Refactor, rewrite and clean up word blasting. ... commit | commitdiff | tree
2021-06-28 yoni206Rewrite POW to POW2 when the base is 2 (#6806) commit | commitdiff | tree
2021-06-28 Andrew ReynoldsRename internal string kinds to match API (#6797) commit | commitdiff | tree
2021-06-28 OuyanchengFurther fix #6453 (#6804) commit | commitdiff | tree
2021-06-28 Haniel Barbosa[proof] [dot] Make dot printer stateful (#6799) commit | commitdiff | tree
2021-06-26 yoni206pow2 -- final changes (#6800) commit | commitdiff | tree
2021-06-25 yoni206pow2: Adding monotonicity lemma (#6793) commit | commitdiff | tree
2021-06-24 Aina Niemetzapi: getRealValue: Fix printing of integer values.... commit | commitdiff | tree
2021-06-24 Mathias Preinercmake: Add new code coverage targets. (#6796) commit | commitdiff | tree
2021-06-24 Andrew ReynoldsFix linear arithmetic for duplicate lemmas in increment... commit | commitdiff | tree
2021-06-24 Gereon KremerAdd CoCoA implementation (#6733) commit | commitdiff | tree
2021-06-23 Haniel Barbosa[hol] Disable bound fmf when HOL (#6792) commit | commitdiff | tree
2021-06-23 yoni206pow2: more implementations (#6756) commit | commitdiff | tree
2021-06-23 Haniel Barbosa[regressions] Adding regression from #5371 (#6791) commit | commitdiff | tree
2021-06-23 Haniel Barbosa[proofs] [dot] Adding a counter for subproofs (#6735) commit | commitdiff | tree
2021-06-23 Haniel Barbosa[parser] [hol] Fix parser check for allowing functions... commit | commitdiff | tree
2021-06-23 Aina Niemetzdocs: Add quickstart guide. (#6782) commit | commitdiff | tree
2021-06-23 Aina NiemetzFP: Remove sections guarded with undefined macro SYMFPU... commit | commitdiff | tree
2021-06-23 Andres NoetzliRemove `--tear-down-incremental` (#6745) commit | commitdiff | tree
2021-06-22 Andrew ReynoldsAvoid full normalization of lambdas in getValue (#6787) commit | commitdiff | tree
2021-06-22 yoni206python api unit tests for Op (#6785) commit | commitdiff | tree
2021-06-22 yoni206modular bv2int: Stubs and some implementations (#6760) commit | commitdiff | tree
2021-06-22 Andrew ReynoldsMinor simplification to equality engine notifications... commit | commitdiff | tree
2021-06-22 Andrew ReynoldsAlways check legal eliminations in quantified logics... commit | commitdiff | tree
2021-06-22 Andrew ReynoldsFix type enumeration for non first-class sorts in FMF... commit | commitdiff | tree
2021-06-22 yoni206Python api unit tests for Result (#6763) commit | commitdiff | tree
2021-06-22 Andrew ReynoldsFix cases of ITE within regular expressions (#6783) commit | commitdiff | tree
2021-06-22 Andrew ReynoldsSet up fine grained equality notifications (#6734) commit | commitdiff | tree
2021-06-21 Mathias PreinerUpdate to CaDiCaL 1.4.1. (#6780) commit | commitdiff | tree
2021-06-21 Aina Niemetzdocs: Split out and merge C++ class hierarchy. (#6781) commit | commitdiff | tree
2021-06-21 Andres Noetzli[Attributes] Remove parameter `context_dependent` ... commit | commitdiff | tree
2021-06-21 Mathias PreinerFix model issues with --bitblast=eager. (#6753) commit | commitdiff | tree
2021-06-21 mudathirmahgoubAdd Grammar.java to the java API (#6388) commit | commitdiff | tree
2021-06-21 Mathias PreinerMove cnfConversionTime statistic to CnfStream. (#6769) commit | commitdiff | tree
2021-06-21 Mathias PreinerMake CaDiCaL a required dependency. (#6761) commit | commitdiff | tree
2021-06-21 Haniel Barbosa[proof] Fix documentation of array rule (#6770) commit | commitdiff | tree
2021-06-19 Ying ShengAdding python API test part 5 (#6743) commit | commitdiff | tree
2021-06-19 Aina Niemetzdocs: Fix config to produce unique Sphinx section label... commit | commitdiff | tree
2021-06-19 Andres Noetzli[CI] Build with all available cores (#6768) commit | commitdiff | tree
2021-06-19 Aina Niemetzdocs: Remove 'View page source' link in right corner... commit | commitdiff | tree
2021-06-18 Mathias PreinerMake CnfStream::toCNF iterative (#6757) commit | commitdiff | tree
2021-06-18 Andres NoetzliRemove obsolete libpoly patch (#6762) commit | commitdiff | tree
2021-06-18 Andres NoetzliFix CaDiCaL build on Windows (#6764) commit | commitdiff | tree
2021-06-18 Andres NoetzliFix build without libpoly (#6759) commit | commitdiff | tree
2021-06-16 Aina NiemetzMake symfpu a required dependency. (#6749) commit | commitdiff | tree
2021-06-16 Andres NoetzliArchive SMT-COMP 2021 run scripts (#6748) commit | commitdiff | tree
2021-06-16 Gereon KremerProperly consider aliases in option handlers (#6683) commit | commitdiff | tree
2021-06-15 Ouyancheng[Optimization] Use Result in OptimizationResult (#6740) commit | commitdiff | tree
2021-06-15 yoni206pow2: adding a kind, inference rules, and some implemen... commit | commitdiff | tree
2021-06-15 Gereon KremerUpdate to a more recent libpoly version. (#6730) commit | commitdiff | tree
2021-06-15 Gereon KremerAdd cocoalib (#6731) commit | commitdiff | tree
2021-06-15 Gereon KremerRemove public option wrappers (#6716) commit | commitdiff | tree
2021-06-15 Aina Niemetzdocs: Fix reference in sep logic reference. (#6747) commit | commitdiff | tree
2021-06-15 Haniel BarbosaCVC4 -> cvc5 in cpp API examples (#6746) commit | commitdiff | tree
next