projects / cvc5.git / shortlog
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
cvc5.git
2021-07-25 Andrew ReynoldsChanges to datatypes in preparation for central equalit... commit | commitdiff | tree
2021-07-25 Andrew ReynoldsRefactor equality engine setup for arithmetic congruenc... commit | commitdiff | tree
2021-07-24 Andres NoetzliFix CLN build (#6920) commit | commitdiff | tree
2021-07-23 Andres NoetzliConfiguration: Indicate dependencies being built (... commit | commitdiff | tree
2021-07-23 Andres NoetzliFix CoCoA build for newer compilers (#6919) commit | commitdiff | tree
2021-07-23 Aina NiemetzFP: Add option to word-blast more lazily. (#6904) commit | commitdiff | tree
2021-07-22 Andrew ReynoldsSimplify computation of relevant terms in datatypes... commit | commitdiff | tree
2021-07-22 Andrew ReynoldsAdd the central equality engine manager (#6893) commit | commitdiff | tree
2021-07-22 Andrew ReynoldsMiscellaneous changes in preparation for central equali... commit | commitdiff | tree
2021-07-22 Andres NoetzliAdd support for minimal unsat cores (#4605) commit | commitdiff | tree
2021-07-22 Andrew ReynoldsPreparation for carry the rewrite rule database in... commit | commitdiff | tree
2021-07-22 mudathirmahgoubAdd std::vector<Term> Op:: getIndices() and operator... commit | commitdiff | tree
2021-07-20 Haniel Barbosa[AUTHORS] Add CVC4 as part of CVC series (#6907) commit | commitdiff | tree
2021-07-20 Andres NoetzliANTLR3: Install into `CMAKE_INSTALL_LIBDIR` (#6912) commit | commitdiff | tree
2021-07-19 Andrew V. Jones'CryptoMiniSat_LIBRARIES' should respect lib/lib64... commit | commitdiff | tree
2021-07-19 Andrew V. Jones'ANTLR3_RUNTIME' should respect lib/lib64 (#6906) commit | commitdiff | tree
2021-07-18 Andrew ReynoldsAdd n-ary term utilities (#6896) commit | commitdiff | tree
2021-07-16 Andrew ReynoldsDo not exhaustive instantiation when FMF is disabled... commit | commitdiff | tree
2021-07-16 Andres Noetzli[Unit Tests] Avoid linking against external libs (... commit | commitdiff | tree
2021-07-16 Andres Noetzli[Unit Tests] Reenable `top_scope_context_obj` (#6892) commit | commitdiff | tree
2021-07-15 Andrew ReynoldsFix context for proofs of instantiations (#6890) commit | commitdiff | tree
2021-07-15 Andrew ReynoldsDistinguish quantifiers preprocess as its own proof... commit | commitdiff | tree
2021-07-15 Andrew ReynoldsConnect the equality solver to theory arith (#6894) commit | commitdiff | tree
2021-07-15 Andrew ReynoldsArithmetic equality solver (#6876) commit | commitdiff | tree
2021-07-15 Andrew ReynoldsMove master equality engine notification to own file... commit | commitdiff | tree
2021-07-15 Andrew ReynoldsAdd node converter utility (#6878) commit | commitdiff | tree
2021-07-15 Mathias Preinerbv: Disable bv-assert-input if proofs are enabled.... commit | commitdiff | tree
2021-07-15 Mathias Preinerbv: Rename BBSimple to NodeBitblaster. (#6891) commit | commitdiff | tree
2021-07-15 Mathias Preinerbv: Rename lazy solver to layered solver. (#6889) commit | commitdiff | tree
2021-07-15 Mathias Preinerbv: Rename simple solver to bitblast-internal. (#6888) commit | commitdiff | tree
2021-07-14 Haniel Barbosa[proof] Fix open proof issues in SAT proof (#6887) commit | commitdiff | tree
2021-07-14 Haniel BarbosaAdd option that exercises the previously buggy behavior... commit | commitdiff | tree
2021-07-14 Haniel BarbosaGeneralize congruence handling for HO in eq proofs... commit | commitdiff | tree
2021-07-14 Andrew ReynoldsFix for context on input proof generator (#6873) commit | commitdiff | tree
2021-07-14 Andrew ReynoldsMove synthesis verification check to own file (#6882) commit | commitdiff | tree
2021-07-14 Andrew ReynoldsRefactor setup of proof equality engine for central... commit | commitdiff | tree
2021-07-14 Andrew ReynoldsFix models for sequences of infinite element type ... commit | commitdiff | tree
2021-07-14 Gereon KremerClean up option usage in command executor (#6844) commit | commitdiff | tree
2021-07-14 Mathias PreinerAdd missing space for check macro error messages. ... commit | commitdiff | tree
2021-07-14 Mathias Preinerbv: Add missing BV_EAGER_ATOM proof rule. (#6874) commit | commitdiff | tree
2021-07-13 Mathias Preinerbv: Simplify BV_BITBLAST_* proof rules. (#6871) commit | commitdiff | tree
2021-07-13 Haniel Barbosa[rewriter] Add rewrite to order IFF (equality for Boole... commit | commitdiff | tree
2021-07-13 Mathias Preinerbv: Do not rewrite below BV leafs in BBProof's TConvPro... commit | commitdiff | tree
2021-07-13 Andrew ReynoldsAdd branch and bound lemma if linear arithmetic generat... commit | commitdiff | tree
2021-07-13 Mathias Preinerbv: Expand bitblast proof steps in the proof post proce... commit | commitdiff | tree
2021-07-12 Andrew ReynoldsAdd branch and bound (#6865) commit | commitdiff | tree
2021-07-12 Andrew ReynoldsFix for learned rewrite pass, add regression (#6850) commit | commitdiff | tree
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
next