projects / cvc5.git / shortlog
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
cvc5.git
2021-08-04 Haniel Barbosa[proof] Add getProof to API and use it in GetProofComma... commit | commitdiff | tree
2021-08-04 Alex OzdemirAdd IEEE-BV-to-FP to external-to-internal mapping in... commit | commitdiff | tree
2021-08-04 Andrew ReynoldsRemove dependencies on smt engine in smt solver (#6965) commit | commitdiff | tree
2021-08-03 Gereon KremerUse int64_t, uint64_t or double for all numeric options... commit | commitdiff | tree
2021-08-03 Andrew ReynoldsRefactor shared solver to use theory builtin inference... commit | commitdiff | tree
2021-08-03 Andrew ReynoldsRemove "inUnsatCore" flag throughout (#6964) commit | commitdiff | tree
2021-08-03 Gereon KremerProperly honor --stats-all and --stats-expert when... commit | commitdiff | tree
2021-08-02 Aina NiemetzAdd 'REQUIRES: poly' to regression. (#6966) commit | commitdiff | tree
2021-08-02 Mathias Preinerbv: Enable equality engine for bitblast-internal. ... commit | commitdiff | tree
2021-07-31 Gereon KremerPerform statistics printing via the API (#6952) commit | commitdiff | tree
2021-07-30 Gereon KremerAllow changing certain options while solving (#6945) commit | commitdiff | tree
2021-07-30 Andrew ReynoldsSimplify smt2 printer (#6954) commit | commitdiff | tree
2021-07-29 Gereon KremerIntegrate installation instructions into documentation... commit | commitdiff | tree
2021-07-29 Aina Niemetzquickstart: Add python example to docs. (#6949) commit | commitdiff | tree
2021-07-29 Haniel Barbosa[proofs] Set BV solver to better proof-producing one... commit | commitdiff | tree
2021-07-29 yoni206Python quick start example (#6939) commit | commitdiff | tree
2021-07-29 Andrew ReynoldsIntegrate central equality engine approach into theory... commit | commitdiff | tree
2021-07-29 Andrew ReynoldsMinor updates to shared terms database for central... commit | commitdiff | tree
2021-07-28 makaimannFixes for building python wheels on manylinux2014 ... commit | commitdiff | tree
2021-07-28 Andrew ReynoldsMinor changes to arrays in preparation for central... commit | commitdiff | tree
2021-07-28 Gereon KremerOnly use libedit on tty inputs (#6946) commit | commitdiff | tree
2021-07-28 Andres NoetzliPrint link to docs preview (#6922) commit | commitdiff | tree
2021-07-28 Andrew ReynoldsMake extended rewriter methods const (#6948) commit | commitdiff | tree
2021-07-27 Mathias Preinerbv: Refactor getEqualityStatus and use for both bitblas... commit | commitdiff | tree
2021-07-27 Mathias Preinerproof: Add eqrange expansion rule. (#6936) commit | commitdiff | tree
2021-07-27 Andrew ReynoldsTrack instantiation reasons in proofs (#6935) commit | commitdiff | tree
2021-07-27 Andrew ReynoldsAdd basic LFSC utilities (#6879) commit | commitdiff | tree
2021-07-27 Andrew ReynoldsMove enum value generator to own file (#6941) commit | commitdiff | tree
2021-07-27 Andrew ReynoldsMinor fix for term database + central equality engine... commit | commitdiff | tree
2021-07-27 Andrew ReynoldsRevert change to regression (#6940) commit | commitdiff | tree
2021-07-27 Andrew ReynoldsMake all dependencies in the fast enumerator optional... commit | commitdiff | tree
2021-07-27 Andrew ReynoldsAdd print expression utility (#6880) commit | commitdiff | tree
2021-07-27 Andres NoetzliAdd regression for fixed `str.indexof_re` issue (#6938) commit | commitdiff | tree
2021-07-27 Andrew ReynoldsMinor changes from proof-new (#6937) commit | commitdiff | tree
2021-07-27 Andrew ReynoldsMiscellaneous fixes from proof-new (#6914) commit | commitdiff | tree
2021-07-27 Andrew ReynoldsAdd proof letify utility (#6881) commit | commitdiff | tree
2021-07-27 Andrew ReynoldsFix eq proof conversion for constant merged parameteriz... commit | commitdiff | tree
2021-07-27 Andrew ReynoldsDefault equality proofs for bags and separation logic... commit | commitdiff | tree
2021-07-27 Andrew ReynoldsAdd sygus enumerator callback (#6923) commit | commitdiff | tree
2021-07-26 Gereon KremerMove public options functions to separate file (#6671) commit | commitdiff | tree
2021-07-26 Andrew ReynoldsEnable default equality proofs for sets (#6931) commit | commitdiff | tree
2021-07-26 Andrew ReynoldsMore updates to arithmetic in preparation for central... commit | commitdiff | tree
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
next