cvc5.git
2022-05-31 Andrew ReynoldsMake subs minimize utility robust to non-constant evalu...
2022-05-31 Gereon KremerFix issues with to_real around coverings solver (#8837)
2022-05-31 Gereon KremerFix FindCaDiCaL script (#8838)
2022-05-31 yoni206Update to GoogleTest 1.11.0 (#8813)
2022-05-27 Andrew ReynoldsEliminate more static options accesses (#8832)
2022-05-27 Andrew ReynoldsEliminate static options access for central ee (#8823)
2022-05-27 Andrew ReynoldsEliminate static options access in skolemize (#8831)
2022-05-27 Andrew ReynoldsFix mixed arithmetic issue in relevant domain (#8826)
2022-05-27 Andrew ReynoldsEliminate static options access in BV inverter (#8829)
2022-05-27 Andrew ReynoldsMake Rewriter::rewrite non-static (#8828)
2022-05-26 Andrew ReynoldsUse function array constants in HO solver (#8818)
2022-05-26 Gereon KremerMake sure phase-shift lemma is properly typed (#8824)
2022-05-25 Andrew ReynoldsEliminate some static options access (#8795)
2022-05-25 Haniel Barbosa[proofs] [alethe] Remove static call to options from...
2022-05-25 Andrew ReynoldsAdd model-based quantifier instantiation (#8729)
2022-05-25 Andrew ReynoldsEliminate static access to dtSharedSelectors (#8804)
2022-05-25 Andrew ReynoldsEliminate more static options accesses (#8802)
2022-05-24 Andrew ReynoldsIntroduce function array constant (#8793)
2022-05-24 Andrew ReynoldsFix subtype issues in proofs for nonlinear solver ...
2022-05-24 Aina Niemetzbv: Disable rule ExtractArith. (#8816)
2022-05-24 mudathirmahgoubAdd table.group operator (#8731)
2022-05-24 Andrew ReynoldsAdd declareOracleFun to API (#8794)
2022-05-23 Andrew ReynoldsRemove spurious assertion in isLegalElimination (#8812)
2022-05-23 Andrew ReynoldsMake model core robust to when we cannot show the model...
2022-05-22 Mathias Preinerbv: Add resource limits support for CaDiCaL. (#8788)
2022-05-22 Andrew ReynoldsSimplification of smt2 printer for type ascriptions...
2022-05-21 Andrew ReynoldsMove smt_util to preprocessing/util (#8799)
2022-05-21 Andrew ReynoldsReenable assertion in skolem definition manager (#8797)
2022-05-21 Andrew ReynoldsAdd option to send all instantiations in a bounded...
2022-05-21 Gereon KremerAdd cross-compilation for arm64 on macOS (#8758)
2022-05-20 Andrew ReynoldsMore removing of unused code (#8806)
2022-05-20 vinciusbTrying to break cycles when printing a .dot DAG (#8698)
2022-05-20 vinciusbNew way to identify THEORY_LEMMA clusters when printing...
2022-05-19 Andrew ReynoldsMinor deleting of unused code (#8800)
2022-05-19 Andrew ReynoldsAdd options and regressions to increase coverage (...
2022-05-18 Andrew ReynoldsBasic cleanup of sep theory (#8790)
2022-05-18 Andrew ReynoldsMake skolem definition manager robust to definitions...
2022-05-18 Andrew ReynoldsEliminate subtypes (#8783)
2022-05-17 Andrew ReynoldsRefactor declare oracle command (#8742)
2022-05-17 Andrew ReynoldsMinor cleanup of datatypes theory (#8791)
2022-05-17 Andrew ReynoldsFix LFSC proof construction for concat clash of sequenc...
2022-05-17 Mathias Preinerdocs: Remove references to checkEntailed(). (#8789)
2022-05-17 Andrew ReynoldsGeneralize pto constraint tracking for multiple heaps...
2022-05-17 Ying ShengAdd getInterpolant with a grammar in the unit test...
2022-05-17 yoni206new test for resolved issue (#8784)
2022-05-16 Andrew ReynoldsLast remaining fixes for eliminating subtyping (#8772)
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...
next