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