cvc5.git
2021-08-16 Gereon KremerMake Theory class use Env (#7011)
2021-08-16 Andres Noetzli[Strings] Make fact detection more robust (#7007)
2021-08-16 Andrew V. JonesAdd check for static libraries when compiling CryptoMin...
2021-08-16 Andrew V. JonesCorrect copyright print for GLPK (#7015)
2021-08-13 Gereon KremerRefactor setDefaults to use an options object (#6994)
2021-08-10 Andres NoetzliDisable external initialization of `thread_local` varia...
2021-08-10 Gereon KremerSimplify generation of option module code. (#6995)
2021-08-09 Andrew V. JonesCreate grouping of tests that exercise '--use-approx...
2021-08-09 Andres NoetzliSupport older CMake versions (#7003)
2021-08-06 Gereon KremerMerge options cmake into general cmake file (#6989)
2021-08-06 Gereon KremerClear options manager (#6991)
2021-08-05 Alex OzdemirNormalize val in BitVector(val_str, base) (#6955)
2021-08-05 Andrew ReynoldsGeneralize term canonizer for type classes (#6895)
2021-08-05 Andres Noetzli[Unit Tests] Add missing include (#6990)
2021-08-05 Andrew ReynoldsFix policy for rewriting string equalities (#6916)
2021-08-05 Gereon KremerNo longer call solver constructor with an options objec...
2021-08-04 Gereon KremerConsolidate solver resets (#6986)
2021-08-04 Andrew ReynoldsProper printing of proofs in the internal calculus...
2021-08-04 Andrew ReynoldsFix policy for merging subproofs (#6981)
2021-08-04 Diego Della... [proof] [dot] Fix comments on dot printer (#6983)
2021-08-04 Andrew ReynoldsAdd inference ids for remainder of sygus solver (#6977)
2021-08-04 Haniel BarbosaImprove error messages for UF catching higher-order...
2021-08-04 Mathias Preinersyqi: Add debug information for dumping instantiations...
2021-08-04 Andrew ReynoldsAdd optional debug information for dumping instantiatio...
2021-08-04 Aina NiemetzUpdate bug_report.md
2021-08-04 Andrew ReynoldsAdd containsAssumption proof utility (#6953)
2021-08-04 Gereon KremerRefactor managed streams (#6934)
2021-08-04 Gereon KremerAdd API function to get list of option names (#6971)
2021-08-04 Gereon KremerReplace numeric predicates by explicit minimum and...
2021-08-04 Andrew ReynoldsAdd missing inference identifiers (#6962)
2021-08-04 Haniel Barbosa[proof] Add getProof to API and use it in GetProofComma...
2021-08-04 Alex OzdemirAdd IEEE-BV-to-FP to external-to-internal mapping in...
2021-08-04 Andrew ReynoldsRemove dependencies on smt engine in smt solver (#6965)
2021-08-03 Gereon KremerUse int64_t, uint64_t or double for all numeric options...
2021-08-03 Andrew ReynoldsRefactor shared solver to use theory builtin inference...
2021-08-03 Andrew ReynoldsRemove "inUnsatCore" flag throughout (#6964)
2021-08-03 Gereon KremerProperly honor --stats-all and --stats-expert when...
2021-08-02 Aina NiemetzAdd 'REQUIRES: poly' to regression. (#6966)
2021-08-02 Mathias Preinerbv: Enable equality engine for bitblast-internal. ...
2021-07-31 Gereon KremerPerform statistics printing via the API (#6952)
2021-07-30 Gereon KremerAllow changing certain options while solving (#6945)
2021-07-30 Andrew ReynoldsSimplify smt2 printer (#6954)
2021-07-29 Gereon KremerIntegrate installation instructions into documentation...
2021-07-29 Aina Niemetzquickstart: Add python example to docs. (#6949)
2021-07-29 Haniel Barbosa[proofs] Set BV solver to better proof-producing one...
2021-07-29 yoni206Python quick start example (#6939)
2021-07-29 Andrew ReynoldsIntegrate central equality engine approach into theory...
2021-07-29 Andrew ReynoldsMinor updates to shared terms database for central...
2021-07-28 makaimannFixes for building python wheels on manylinux2014 ...
2021-07-28 Andrew ReynoldsMinor changes to arrays in preparation for central...
2021-07-28 Gereon KremerOnly use libedit on tty inputs (#6946)
2021-07-28 Andres NoetzliPrint link to docs preview (#6922)
2021-07-28 Andrew ReynoldsMake extended rewriter methods const (#6948)
2021-07-27 Mathias Preinerbv: Refactor getEqualityStatus and use for both bitblas...
2021-07-27 Mathias Preinerproof: Add eqrange expansion rule. (#6936)
2021-07-27 Andrew ReynoldsTrack instantiation reasons in proofs (#6935)
2021-07-27 Andrew ReynoldsAdd basic LFSC utilities (#6879)
2021-07-27 Andrew ReynoldsMove enum value generator to own file (#6941)
2021-07-27 Andrew ReynoldsMinor fix for term database + central equality engine...
2021-07-27 Andrew ReynoldsRevert change to regression (#6940)
2021-07-27 Andrew ReynoldsMake all dependencies in the fast enumerator optional...
2021-07-27 Andrew ReynoldsAdd print expression utility (#6880)
2021-07-27 Andres NoetzliAdd regression for fixed `str.indexof_re` issue (#6938)
2021-07-27 Andrew ReynoldsMinor changes from proof-new (#6937)
2021-07-27 Andrew ReynoldsMiscellaneous fixes from proof-new (#6914)
2021-07-27 Andrew ReynoldsAdd proof letify utility (#6881)
2021-07-27 Andrew ReynoldsFix eq proof conversion for constant merged parameteriz...
2021-07-27 Andrew ReynoldsDefault equality proofs for bags and separation logic...
2021-07-27 Andrew ReynoldsAdd sygus enumerator callback (#6923)
2021-07-26 Gereon KremerMove public options functions to separate file (#6671)
2021-07-26 Andrew ReynoldsEnable default equality proofs for sets (#6931)
2021-07-26 Andrew ReynoldsMore updates to arithmetic in preparation for central...
2021-07-25 Andrew ReynoldsChanges to datatypes in preparation for central equalit...
2021-07-25 Andrew ReynoldsRefactor equality engine setup for arithmetic congruenc...
2021-07-24 Andres NoetzliFix CLN build (#6920)
2021-07-23 Andres NoetzliConfiguration: Indicate dependencies being built (...
2021-07-23 Andres NoetzliFix CoCoA build for newer compilers (#6919)
2021-07-23 Aina NiemetzFP: Add option to word-blast more lazily. (#6904)
2021-07-22 Andrew ReynoldsSimplify computation of relevant terms in datatypes...
2021-07-22 Andrew ReynoldsAdd the central equality engine manager (#6893)
2021-07-22 Andrew ReynoldsMiscellaneous changes in preparation for central equali...
2021-07-22 Andres NoetzliAdd support for minimal unsat cores (#4605)
2021-07-22 Andrew ReynoldsPreparation for carry the rewrite rule database in...
2021-07-22 mudathirmahgoubAdd std::vector<Term> Op:: getIndices() and operator...
2021-07-20 Haniel Barbosa[AUTHORS] Add CVC4 as part of CVC series (#6907)
2021-07-20 Andres NoetzliANTLR3: Install into `CMAKE_INSTALL_LIBDIR` (#6912)
2021-07-19 Andrew V. Jones'CryptoMiniSat_LIBRARIES' should respect lib/lib64...
2021-07-19 Andrew V. Jones'ANTLR3_RUNTIME' should respect lib/lib64 (#6906)
2021-07-18 Andrew ReynoldsAdd n-ary term utilities (#6896)
2021-07-16 Andrew ReynoldsDo not exhaustive instantiation when FMF is disabled...
2021-07-16 Andres Noetzli[Unit Tests] Avoid linking against external libs (...
2021-07-16 Andres Noetzli[Unit Tests] Reenable `top_scope_context_obj` (#6892)
2021-07-15 Andrew ReynoldsFix context for proofs of instantiations (#6890)
2021-07-15 Andrew ReynoldsDistinguish quantifiers preprocess as its own proof...
2021-07-15 Andrew ReynoldsConnect the equality solver to theory arith (#6894)
2021-07-15 Andrew ReynoldsArithmetic equality solver (#6876)
2021-07-15 Andrew ReynoldsMove master equality engine notification to own file...
2021-07-15 Andrew ReynoldsAdd node converter utility (#6878)
2021-07-15 Mathias Preinerbv: Disable bv-assert-input if proofs are enabled....
2021-07-15 Mathias Preinerbv: Rename BBSimple to NodeBitblaster. (#6891)
next