cvc5.git
2021-07-05 Andres Noetzli[Strings] Fix incorrect rewrite (#6837)
2021-07-05 Andrew ReynoldsMake buffered inference manager more robust to backtrac...
2021-07-03 Andres NoetzliFix performance of string regression (#6832)
2021-07-03 Mathias PreinerAdd output tags -o, --output. (#6826)
2021-07-02 Mathias PreinerFix bv assert input reset assertions (#6820)
2021-07-02 Andrew ReynoldsFix rewriter for negative constant seq.nth (#6827)
2021-07-02 Andres NoetzliFix CaDiCaL auto-download on macOS (#6828)
2021-07-02 Gereon KremerRefactor lexer for SMT-LIB in sphinx (#6805)
2021-07-02 Andres NoetzliAdd reverse iterators to `Node`/`TNode` (#6825)
2021-07-01 Andrew ReynoldsAdd recursive function definitions to subsolver in...
2021-07-01 Gereon KremerFix message to show that cadical and symfpu are require...
2021-07-01 Andrew ReynoldsAdd option to limit the number of instantiation rounds...
2021-06-30 Mathias PreinerUse SAT context level for --bv-assert-input instead...
2021-06-30 Gereon KremerUse authored date instead of commit date. (#6815)
2021-06-30 yoni206pow2: new test (#6819)
2021-06-30 Andrew ReynoldsDo not notify during equality engine initialization...
2021-06-30 Andrew ReynoldsDo not apply fmfBound to standard quantifiers when...
2021-06-30 Andrew ReynoldsFix pre vs. post-rewrite in proofs for theory preproces...
2021-06-30 yoni206int-to-bv: correct model values (#6811)
2021-06-29 Gereon KremerAdd new variants for the CAD projection (#6794)
2021-06-29 Mathias PreinerFix statistics in AigBitblaster. (#6810)
2021-06-29 Aina NiemetzFP: Refactor, rewrite and clean up word blasting. ...
2021-06-28 yoni206Rewrite POW to POW2 when the base is 2 (#6806)
2021-06-28 Andrew ReynoldsRename internal string kinds to match API (#6797)
2021-06-28 OuyanchengFurther fix #6453 (#6804)
2021-06-28 Haniel Barbosa[proof] [dot] Make dot printer stateful (#6799)
2021-06-26 yoni206pow2 -- final changes (#6800)
2021-06-25 yoni206pow2: Adding monotonicity lemma (#6793)
2021-06-24 Aina Niemetzapi: getRealValue: Fix printing of integer values....
2021-06-24 Mathias Preinercmake: Add new code coverage targets. (#6796)
2021-06-24 Andrew ReynoldsFix linear arithmetic for duplicate lemmas in increment...
2021-06-24 Gereon KremerAdd CoCoA implementation (#6733)
2021-06-23 Haniel Barbosa[hol] Disable bound fmf when HOL (#6792)
2021-06-23 yoni206pow2: more implementations (#6756)
2021-06-23 Haniel Barbosa[regressions] Adding regression from #5371 (#6791)
2021-06-23 Haniel Barbosa[proofs] [dot] Adding a counter for subproofs (#6735)
2021-06-23 Haniel Barbosa[parser] [hol] Fix parser check for allowing functions...
2021-06-23 Aina Niemetzdocs: Add quickstart guide. (#6782)
2021-06-23 Aina NiemetzFP: Remove sections guarded with undefined macro SYMFPU...
2021-06-23 Andres NoetzliRemove `--tear-down-incremental` (#6745)
2021-06-22 Andrew ReynoldsAvoid full normalization of lambdas in getValue (#6787)
2021-06-22 yoni206python api unit tests for Op (#6785)
2021-06-22 yoni206modular bv2int: Stubs and some implementations (#6760)
2021-06-22 Andrew ReynoldsMinor simplification to equality engine notifications...
2021-06-22 Andrew ReynoldsAlways check legal eliminations in quantified logics...
2021-06-22 Andrew ReynoldsFix type enumeration for non first-class sorts in FMF...
2021-06-22 yoni206Python api unit tests for Result (#6763)
2021-06-22 Andrew ReynoldsFix cases of ITE within regular expressions (#6783)
2021-06-22 Andrew ReynoldsSet up fine grained equality notifications (#6734)
2021-06-21 Mathias PreinerUpdate to CaDiCaL 1.4.1. (#6780)
2021-06-21 Aina Niemetzdocs: Split out and merge C++ class hierarchy. (#6781)
2021-06-21 Andres Noetzli[Attributes] Remove parameter `context_dependent` ...
2021-06-21 Mathias PreinerFix model issues with --bitblast=eager. (#6753)
2021-06-21 mudathirmahgoubAdd Grammar.java to the java API (#6388)
2021-06-21 Mathias PreinerMove cnfConversionTime statistic to CnfStream. (#6769)
2021-06-21 Mathias PreinerMake CaDiCaL a required dependency. (#6761)
2021-06-21 Haniel Barbosa[proof] Fix documentation of array rule (#6770)
2021-06-19 Ying ShengAdding python API test part 5 (#6743)
2021-06-19 Aina Niemetzdocs: Fix config to produce unique Sphinx section label...
2021-06-19 Andres Noetzli[CI] Build with all available cores (#6768)
2021-06-19 Aina Niemetzdocs: Remove 'View page source' link in right corner...
2021-06-18 Mathias PreinerMake CnfStream::toCNF iterative (#6757)
2021-06-18 Andres NoetzliRemove obsolete libpoly patch (#6762)
2021-06-18 Andres NoetzliFix CaDiCaL build on Windows (#6764)
2021-06-18 Andres NoetzliFix build without libpoly (#6759)
2021-06-16 Aina NiemetzMake symfpu a required dependency. (#6749)
2021-06-16 Andres NoetzliArchive SMT-COMP 2021 run scripts (#6748)
2021-06-16 Gereon KremerProperly consider aliases in option handlers (#6683)
2021-06-15 Ouyancheng[Optimization] Use Result in OptimizationResult (#6740)
2021-06-15 yoni206pow2: adding a kind, inference rules, and some implemen...
2021-06-15 Gereon KremerUpdate to a more recent libpoly version. (#6730)
2021-06-15 Gereon KremerAdd cocoalib (#6731)
2021-06-15 Gereon KremerRemove public option wrappers (#6716)
2021-06-15 Aina Niemetzdocs: Fix reference in sep logic reference. (#6747)
2021-06-15 Haniel BarbosaCVC4 -> cvc5 in cpp API examples (#6746)
2021-06-15 Aina Niemetzdocs: Add references instead of links in theory referen...
2021-06-15 yoni206An example for a quick start guide (#6686)
2021-06-14 Andres NoetzliFinal update to SMT-COMP 2021 options (#6739)
2021-06-13 Andrew ReynoldsMinor simplifications to LogicInfo (#6737)
2021-06-11 Haniel BarbosaBetter support for HOL parsing and set up (#6697)
2021-06-11 Gereon KremerAdd skeleton for new Lazard evaluation (#6732)
2021-06-11 Andrew ReynoldsRemove support for lazy BV extended function reductions...
2021-06-10 Andrew ReynoldsEnsure bv2nat and int2bv are not rewritten when using...
2021-06-10 Mathias Preinersmtcomp: Change some BV configs for SQ and INC track...
2021-06-09 Aina Niemetzdocs: Migrate sets and relations theory reference....
2021-06-09 Andres NoetzliMake `--solve-int-as-bv=X` robust to rewriting (#6722)
2021-06-09 Andres NoetzliUpdate CVC4 URLs/macros (#6666)
2021-06-09 Andres NoetzliReorder ITE rewrites (#6723)
2021-06-09 Gereon KremerMake squasing more robust (#6713)
2021-06-09 Andrew ReynoldsIntegrate learned literal manager into preprocessing...
2021-06-09 Andrew ReynoldsFixes related to printing tuples, define-fun commands...
2021-06-09 Gereon KremerPush complex check inside GetInstantiationsCommand...
2021-06-09 Andres NoetzliUpdate options for SMT-COMP (#6704)
2021-06-09 Ouyancheng[Optimization] support for push/pop (#6706)
2021-06-09 Haniel BarbosaRemoving spurious HO checks (#6707)
2021-06-09 Gereon KremerRequire statistics for regression (#6714)
2021-06-09 Aina Niemetzdocs: Migrate separation logic theory reference. (...
2021-06-09 Andres Noetzlidocs: Fix `Kind` description (#6712)
2021-06-08 Andrew ReynoldsFix for 2 dimensional dependent bounded quantifiers...
2021-06-08 Andrew ReynoldsAdd learned literal manager utility (#6709)
next