cvc5.git
2022-05-16 Haniel Barbosa[proofs] Generalize handling of constants merged in...
2022-05-16 Haniel BarbosaRename equality engine trace to print E-graph (#8780)
2022-05-15 Andrew ReynoldsEliminate the use of CAST_TO_REAL (#8759)
2022-05-15 Andrew ReynoldsEliminate ops for parameterized type constructors ...
2022-05-13 Andrew ReynoldsMake arith substitute its own utility (#8765)
2022-05-13 Amalee WilsonAdd heap-trail partitioning strategy, checks between...
2022-05-13 Andrew ReynoldsFixes and improvement for IAND solver (#8771)
2022-05-13 Andrew ReynoldsEliminate use of getBaseType (#8764)
2022-05-13 Andrew ReynoldsAdd utilities in preparation for supporting str.nth...
2022-05-13 Andrew ReynoldsFix debug failures in LFSC proofs due to curried arithm...
2022-05-13 Andrew ReynoldsRefactor logic exceptions during preregistration for...
2022-05-13 Gereon KremerUpdate CoCoALib version (#8757)
2022-05-13 Andrew ReynoldsMinor refactoring for sep theory (#8753)
2022-05-12 Andrew ReynoldsFix type of null terminator for ADD/MULT for LFSC ...
2022-05-12 Andrew ReynoldsEliminate use of subtypes from remainder of type rules...
2022-05-12 Andrew ReynoldsPreserve types in rewriter and make core type rules...
2022-05-12 Haniel Barbosa[docs] Marking internal comment in proofs docs (#8747)
2022-05-12 Gereon KremerMake regular options access const (#8754)
2022-05-11 Gereon KremerRemove --build from GMP configure line (#8752)
2022-05-11 Andrew ReynoldsRelax an assertion in the evaluator (#8751)
2022-05-10 Gereon KremerEnsure substitutions in nonlinear solver are properly...
2022-05-10 Gereon KremerFix some issues with the Python API tests (#8746)
2022-05-10 Gereon KremerAdd test coverage for almost everything from the Java...
2022-05-10 Gereon KremerCompress debug symbols to make libcvc5 smaller (#8743)
2022-05-09 Andrew ReynoldsImprovements for evaluation in model (#8738)
2022-05-09 Andrew ReynoldsDo not depend on subtyping for APPLY_UF in TPTP parser...
2022-05-09 Andrew ReynoldsAdd unit tests for getInstantiations (#8741)
2022-05-07 Andrew ReynoldsDo not rely on subtyping in real-to-int preprocessing...
2022-05-07 Abdalrhman... Disable proof testers for delicate regressions. (#8735)
2022-05-07 Andrew ReynoldsMore preparation for strict type rules (#8733)
2022-05-07 Andrew ReynoldsFix proofs for ppAssert for theory Bool (#8708)
2022-05-06 Andrew ReynoldsFallback for sequential substitution proof reconstructi...
2022-05-06 Andrew ReynoldsEliminate arithmetic subtyping for (dis)equalities...
2022-05-06 Andrew ReynoldsSeparate ill-typed portion of arith models (#8734)
2022-05-06 Andrew ReynoldsFix LFSC side condition for matching premise of concat_...
2022-05-05 Gereon KremerAdd test coverage for almost everything from the Python...
2022-05-05 Andrew ReynoldsPreparation for making equality strictly typed (#8728)
2022-05-05 Andrew ReynoldsFix cache in learned rewrite preprocessing pass (#8725)
2022-05-05 Andrew ReynoldsFix more issues with subtypes in regressions (#8727)
2022-05-05 mudathirmahgoubAdd operators table.aggr and table.join (#8681)
2022-05-05 Andrew ReynoldsUse purification for set comprehension reduction (...
2022-05-04 Andres NoetzliImprove finding Python library/includes (#8718)
2022-05-04 yoni206fix link to `Testing cvc5` in `INSTALL.md` (#8675)
2022-05-04 Andrew ReynoldsMake equality solver the entry point for all equality...
2022-05-04 Gereon KremerMake printStatisticsSafe public (#8721)
2022-05-04 Andrew ReynoldsAdd declareOracleFun interface to SolverEngine (#8622)
2022-05-04 Andrew ReynoldsRefactor oracles using new std::function backend (...
2022-05-04 Andrew ReynoldsRemove unecessary calls to equality engine from congrue...
2022-05-04 Gereon KremerRemove obsolete private methods from API (#8716)
2022-05-04 Andrew ReynoldsFix rewrite for to_real in division by zero (#8714)
2022-05-04 Andrew ReynoldsAdd support for oracle constant nodes (#8707)
2022-05-03 Andrew ReynoldsFix LFSC node converter for 0-ary tuples (#8706)
2022-05-03 Andres NoetzliUpdate LFSC version (#8713)
2022-05-03 Andrew ReynoldsUse (non-recursive) unpurified form instead of original...
2022-05-03 Aina Niemetzdocs: Some fixes in options docs. (#8710)
2022-05-03 Andrew ReynoldsChange option name for mbqi in fmf (#8701)
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)
next