cvc5.git
2021-07-12 Andrew ReynoldsAdd trace for combination splits (#6862)
2021-07-12 Andres NoetzliUse default visibility for `cvc5::Exception` (#6856)
2021-07-12 Andrew ReynoldsImprovements to debug check model (#6861)
2021-07-09 Haniel Barbosatest also with default cores (#6858)
2021-07-09 Andres NoetzliMake regression test `issue4971-0` more robust (#6857)
2021-07-09 Andres NoetzliUse newer config.sub to fix build on Apple M1 (#6854)
2021-07-09 Andrew ReynoldsFix sets cardinality inference involving equivalent...
2021-07-09 Andrew ReynoldsImplement stop-only for new justification heuristic...
2021-07-08 Andrew ReynoldsDisable ordering heuristic for justification by default...
2021-07-08 makaimannAdd script to build wheel for pycvc5 (#6839)
2021-07-08 Haniel Barbosa[proof] [dot] Print let map (of terms in proof) as...
2021-07-07 Haniel Barbosa[unsat cores] Adding regressions from #4971 (#6852)
2021-07-07 Aina Niemetzpow2: Update NEWS. (#6851)
2021-07-07 Aina NiemetzRename operator pow2 to int.pow2. (#6849)
2021-07-07 Andrew ReynoldsFix regressions for competition build (#6846)
2021-07-07 Andrew ReynoldsStandard output for trigger selection (#6841)
2021-07-06 Gereon KremerIntegrate Lazard into CAD module (#6812)
2021-07-06 Andrew ReynoldsIntegrate learned rewrite preprocessing pass (#6840)
2021-07-06 Andrew ReynoldsAdd implementation of learned rewrite pass (#6843)
2021-07-06 Andrew ReynoldsAdd learned rewrite preprocessing pass (#6842)
2021-07-06 Haniel BarbosaPorting C++ API examples to SMT-LIB examples (#6789)
2021-07-06 OuyanchengAdd some printing functions for OptimizationObjective...
2021-07-06 Gereon KremerAdd doc page about transcendentals (#6755)
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)
next