projects / cvc5.git / shortlog
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
cvc5.git
2022-05-04 Andrew ReynoldsRefactor oracles using new std::function backend (... commit | commitdiff | tree
2022-05-04 Andrew ReynoldsRemove unecessary calls to equality engine from congrue... commit | commitdiff | tree
2022-05-04 Gereon KremerRemove obsolete private methods from API (#8716) commit | commitdiff | tree
2022-05-04 Andrew ReynoldsFix rewrite for to_real in division by zero (#8714) commit | commitdiff | tree
2022-05-04 Andrew ReynoldsAdd support for oracle constant nodes (#8707) commit | commitdiff | tree
2022-05-03 Andrew ReynoldsFix LFSC node converter for 0-ary tuples (#8706) commit | commitdiff | tree
2022-05-03 Andres NoetzliUpdate LFSC version (#8713) commit | commitdiff | tree
2022-05-03 Andrew ReynoldsUse (non-recursive) unpurified form instead of original... commit | commitdiff | tree
2022-05-03 Aina Niemetzdocs: Some fixes in options docs. (#8710) commit | commitdiff | tree
2022-05-03 Andrew ReynoldsChange option name for mbqi in fmf (#8701) commit | commitdiff | tree
2022-05-03 Andrew ReynoldsSimplify representation of datatypes at the TypeNode... commit | commitdiff | tree
2022-05-03 Andrew ReynoldsFinal preparation for CONST_INTEGER (#8700) commit | commitdiff | tree
2022-05-03 Andrew ReynoldsMigrate basic EqualityEngine management from Congruence... commit | commitdiff | tree
2022-05-02 Amalee WilsonAdd strict-cube and decision-trail partitioning strateg... commit | commitdiff | tree
2022-05-02 Andrew ReynoldsMore robust treatment of flattening in arith rewriter... commit | commitdiff | tree
2022-05-02 Andrew ReynoldsMake arith msum utility agnostic to Int (#8694) commit | commitdiff | tree
2022-05-02 Gereon KremerAdd missing tests for some corners of the API (#8688) commit | commitdiff | tree
2022-05-02 Aina Niemetzdocs: Do not use explicit line numbers in literalinclud... commit | commitdiff | tree
2022-05-02 Andrew ReynoldsFurther refactoring in preparation for CONST_INTEGER... commit | commitdiff | tree
2022-05-02 Andrew ReynoldsFix tuple printing in LFSC (#8696) commit | commitdiff | tree
2022-04-29 Andrew ReynoldsProperly represent Tuples in the TypeNode AST (#8648) commit | commitdiff | tree
2022-04-29 Andres NoetzliAdd simple type rule for real-or-int arguments (#8685) commit | commitdiff | tree
2022-04-29 Gereon KremerReplace mkConst(CONST_RATIONAL) by mkConstReal (#8686) commit | commitdiff | tree
2022-04-29 Andrew ReynoldsTowards proper usage of TO_REAL (#8680) commit | commitdiff | tree
2022-04-29 Andres NoetzliDocument non-standard string operators (#8679) commit | commitdiff | tree
2022-04-29 Andrew ReynoldsEnsure mkConstInt is used on integral rationals only... commit | commitdiff | tree
2022-04-29 Andrew ReynoldsRefactor interfaces for E-matching (#8665) commit | commitdiff | tree
2022-04-29 Andrew ReynoldsMake extended rewriter use standard Subs utility (... commit | commitdiff | tree
2022-04-29 Abdalrhman... Add an option to enable all testers. (#8676) commit | commitdiff | tree
2022-04-29 yoni206Add missing parenthesis for bags documentation (#8673) commit | commitdiff | tree
2022-04-29 Gereon KremerAdd unit test for code not exposed by java API (#8678) commit | commitdiff | tree
2022-04-29 Gereon KremerAdd unit test for code not exposed by python API (... commit | commitdiff | tree
2022-04-29 Gereon KremerAdd some missing API tests (#8669) commit | commitdiff | tree
2022-04-28 Gereon KremerMove tests around (#8670) commit | commitdiff | tree
2022-04-28 yoni206int-blaster: not allowing higher order functions (... commit | commitdiff | tree
2022-04-28 Andrew ReynoldsMove datatype split inference scheme to its own method... commit | commitdiff | tree
2022-04-28 Andrew ReynoldsClean code for datatypes split (#8667) commit | commitdiff | tree
2022-04-28 Andrew ReynoldsMake labelled separation logic asserts preserve labels... commit | commitdiff | tree
2022-04-28 Andrey Andreyevich... Fix PyUnicode_AsWideCharString signature (#8522) commit | commitdiff | tree
2022-04-28 Gereon KremerAdd resource limiting to coverings solver (#8672) commit | commitdiff | tree
2022-04-27 Andrew ReynoldsAdd option to apply constant propagation for all learne... commit | commitdiff | tree
2022-04-27 Andrew ReynoldsRefactoring of initial lemmas in datatypes (#8666) commit | commitdiff | tree
2022-04-27 Andrew ReynoldsMinor improvements for entailment test (#8663) commit | commitdiff | tree
2022-04-26 Andrew ReynoldsMinor improvements to quantifiers utilities (#8661) commit | commitdiff | tree
2022-04-26 Andrew ReynoldsMake IndexTrie take nodes (#8649) commit | commitdiff | tree
2022-04-26 Andrew ReynoldsMove rep set iterator to its own file (#8647) commit | commitdiff | tree
2022-04-26 Andrew ReynoldsRefactor InstMatch (#8646) commit | commitdiff | tree
2022-04-26 Andrew ReynoldsRefactor mkRep option for instantiation (#8657) commit | commitdiff | tree
2022-04-26 Gereon KremerAdd some missing resultants in the coverings solver... commit | commitdiff | tree
2022-04-26 Andrew ReynoldsSimplify internal represenation of uninterpreted sorts... commit | commitdiff | tree
2022-04-26 Andres NoetzliFix GMP cross-compilation when Wine installed (#8645) commit | commitdiff | tree
2022-04-26 Andrew ReynoldsSimplify internal representation of instantiated sorts... commit | commitdiff | tree
2022-04-25 Andres Noetzli[Regressions] Use Wine for Windows builds (#8652) commit | commitdiff | tree
2022-04-25 Andrew ReynoldsMove VTS term cache to term registry (#8656) commit | commitdiff | tree
2022-04-25 Andrew ReynoldsOption exception for quantified bit-vectors + eager... commit | commitdiff | tree
2022-04-25 Andrew ReynoldsMake BVInstantiatorUtil an EnvObj (#8633) commit | commitdiff | tree
2022-04-25 Abdalrhman... Add custom targets for specific testers. (#8653) commit | commitdiff | tree
2022-04-23 Andrew ReynoldsMinor cleanup of NodeManager (#8650) commit | commitdiff | tree
2022-04-22 Andrew ReynoldsAdd `deep-restart` option (#8644) commit | commitdiff | tree
2022-04-21 Abdalrhman... Add tester for LFSC printer. (#8606) commit | commitdiff | tree
2022-04-21 Andres Noetzli[Seq] Remove `SkolemCache::mkSkolemSeqNth()` (#8643) commit | commitdiff | tree
2022-04-21 mudathirmahgoubAdd bag.partition evaluation (#8637) commit | commitdiff | tree
2022-04-20 Andrew ReynoldsAdd utilities in preparation for deep restarts (#8642) commit | commitdiff | tree
2022-04-20 Andres NoetzliRemove unused `SEQ_NTH_TOTAL` kind (#8048) commit | commitdiff | tree
2022-04-20 Andres NoetzliImprove handling of `(push)` and `(pop)` (#8641) commit | commitdiff | tree
2022-04-20 Andrew ReynoldsAdd declare-oracle-fun command (#8621) commit | commitdiff | tree
2022-04-20 Andrew ReynoldsMinor simplifications for datatype selector triggers... commit | commitdiff | tree
2022-04-20 yoni206int-blaster: direct support for bvcomp (#8640) commit | commitdiff | tree
2022-04-20 yoni206Remove redundant assertion in int-blaster (#8639) commit | commitdiff | tree
2022-04-20 Andrew ReynoldsUpdates to zero level learner (#8597) commit | commitdiff | tree
2022-04-19 Andrew ReynoldsAvoid trivial equalities in explanation of SETS_CARD_CY... commit | commitdiff | tree
2022-04-19 Andrew ReynoldsSimplify implementation of subtype methods in TypeNode... commit | commitdiff | tree
2022-04-19 mudathirmahgoubAdd table.project evaluator (#8632) commit | commitdiff | tree
2022-04-19 Andrew ReynoldsMove linear arithmetic solver to theory::arith::linear... commit | commitdiff | tree
2022-04-19 Andrew ReynoldsGeneralize concat conflict for sequences in LFSC (... commit | commitdiff | tree
2022-04-18 Abdalrhman... Remove instances of `check-proofs` in regressions.... commit | commitdiff | tree
2022-04-18 Andrew ReynoldsAdd some missing FP symbols to LFSC (#8629) commit | commitdiff | tree
2022-04-18 Andrew ReynoldsDistinguish name variants for types in LFSC node conver... commit | commitdiff | tree
2022-04-18 Andrew ReynoldsMake more utilities distinguish Int and Real (#8626) commit | commitdiff | tree
2022-04-18 Andrew ReynoldsSimplify management of separation logic heap (#8580) commit | commitdiff | tree
2022-04-18 Andres NoetzliRemove support for unused `declare-*` commands (#8623) commit | commitdiff | tree
2022-04-14 Andrew ReynoldsFix internal type issue for congruence over quantifiers... commit | commitdiff | tree
2022-04-14 Andrew ReynoldsImplement internal support for (definitional) satisfiab... commit | commitdiff | tree
2022-04-14 Andrew ReynoldsMake LFSC printer robust to internal types (#8616) commit | commitdiff | tree
2022-04-14 Andrew ReynoldsImplement internal support for synthesis modulo oracles... commit | commitdiff | tree
2022-04-14 Andrew ReynoldsRemove static calls to rewrite involving array constant... commit | commitdiff | tree
2022-04-14 Andrew ReynoldsImprovements to phase shifting + purification lemmas... commit | commitdiff | tree
2022-04-14 Amalee WilsonRevised partitioning (#8143) commit | commitdiff | tree
2022-04-14 vinciusb[proofs] [dot] New way to traverse the proof when print... commit | commitdiff | tree
2022-04-14 Andrew ReynoldsIntegrate oracle checker into quantifiers term registry... commit | commitdiff | tree
2022-04-14 Andrew ReynoldsFix spurious assertion involving subtypes (#8611) commit | commitdiff | tree
2022-04-14 Andrew ReynoldsUpdate LFSC version (#8614) commit | commitdiff | tree
2022-04-13 mudathirmahgoubAdd Relation and Table types to SMTLib parser (#8605) commit | commitdiff | tree
2022-04-13 Andrew ReynoldsFix type issue for FP constants in LFSC node converter... commit | commitdiff | tree
2022-04-12 Andrew ReynoldsFix spurious assertion failure caused by subtyping... commit | commitdiff | tree
2022-04-12 Andrew ReynoldsFix type issue for LFSC null terminator (#8607) commit | commitdiff | tree
2022-04-12 Andrew ReynoldsAdd oracle checker utility (#8603) commit | commitdiff | tree
2022-04-12 Andrew ReynoldsAdd oracle caller utility (#8599) commit | commitdiff | tree
2022-04-12 Andrew ReynoldsMaking some benchmarks SMT-LIB compliant for subtypes... commit | commitdiff | tree
2022-04-12 Andrew ReynoldsFix more misuses of arithmetic subtypes (#8601) commit | commitdiff | tree
next