projects / cvc5.git / shortlog
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
cvc5.git
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
2021-06-15 Aina Niemetzdocs: Add references instead of links in theory referen... commit | commitdiff | tree
2021-06-15 yoni206An example for a quick start guide (#6686) commit | commitdiff | tree
2021-06-14 Andres NoetzliFinal update to SMT-COMP 2021 options (#6739) commit | commitdiff | tree
2021-06-13 Andrew ReynoldsMinor simplifications to LogicInfo (#6737) commit | commitdiff | tree
2021-06-11 Haniel BarbosaBetter support for HOL parsing and set up (#6697) commit | commitdiff | tree
2021-06-11 Gereon KremerAdd skeleton for new Lazard evaluation (#6732) commit | commitdiff | tree
2021-06-11 Andrew ReynoldsRemove support for lazy BV extended function reductions... commit | commitdiff | tree
2021-06-10 Andrew ReynoldsEnsure bv2nat and int2bv are not rewritten when using... commit | commitdiff | tree
2021-06-10 Mathias Preinersmtcomp: Change some BV configs for SQ and INC track... commit | commitdiff | tree
2021-06-09 Aina Niemetzdocs: Migrate sets and relations theory reference.... commit | commitdiff | tree
2021-06-09 Andres NoetzliMake `--solve-int-as-bv=X` robust to rewriting (#6722) commit | commitdiff | tree
2021-06-09 Andres NoetzliUpdate CVC4 URLs/macros (#6666) commit | commitdiff | tree
2021-06-09 Andres NoetzliReorder ITE rewrites (#6723) commit | commitdiff | tree
2021-06-09 Gereon KremerMake squasing more robust (#6713) commit | commitdiff | tree
2021-06-09 Andrew ReynoldsIntegrate learned literal manager into preprocessing... commit | commitdiff | tree
2021-06-09 Andrew ReynoldsFixes related to printing tuples, define-fun commands... commit | commitdiff | tree
2021-06-09 Gereon KremerPush complex check inside GetInstantiationsCommand... commit | commitdiff | tree
2021-06-09 Andres NoetzliUpdate options for SMT-COMP (#6704) commit | commitdiff | tree
2021-06-09 Ouyancheng[Optimization] support for push/pop (#6706) commit | commitdiff | tree
2021-06-09 Haniel BarbosaRemoving spurious HO checks (#6707) commit | commitdiff | tree
2021-06-09 Gereon KremerRequire statistics for regression (#6714) commit | commitdiff | tree
2021-06-09 Aina Niemetzdocs: Migrate separation logic theory reference. (... commit | commitdiff | tree
2021-06-09 Andres Noetzlidocs: Fix `Kind` description (#6712) commit | commitdiff | tree
2021-06-08 Andrew ReynoldsFix for 2 dimensional dependent bounded quantifiers... commit | commitdiff | tree
2021-06-08 Andrew ReynoldsAdd learned literal manager utility (#6709) commit | commitdiff | tree
next