cvc5.git
2022-06-27 Andres NoetzliMove `SymbolManager` and `SymbolTable` to parser (...
2022-06-27 Andres Noetzli[Docs] Update `EnumDocumenter` for newer Sphinx (#8914)
2022-06-27 Andrew ReynoldsRevert change in lemma order in prop engine (#8911)
2022-06-23 mudathirmahgoubAdd inference rules for table.group (#8819)
2022-06-23 Andres NoetzliRemove `CommandSequence` command (#8904)
2022-06-23 Andres NoetzliMove non-stream options out of `printer_options.toml...
2022-06-23 Andrew ReynoldsFix explanation for strings unit oob inference (#8908)
2022-06-23 mudathirmahgoubAdd set.fold operator (#8867)
2022-06-23 Andres NoetzliFix rewrite for `(to_int real.pi)` (#8907)
2022-06-23 Andrew ReynoldsFix handling of injectivity for str.unit (#8899)
2022-06-22 mudathirmahgoubprint run_process command (#8859)
2022-06-22 Andres NoetzliRemove `Command::clone()` (#8903)
2022-06-22 Andres NoetzliSimplify printing of command results (#8902)
2022-06-22 mudathirmahgoubAvoid quoting symbols already surrounded with vertical...
2022-06-22 Andrew ReynoldsFix sort inference for equality over finite types ...
2022-06-22 mudathirmahgoubAdd type to uninterpreted constant values (#8891)
2022-06-22 Andres Noetzli[Parser] Rename generated `.c` to `.cpp` files (#8894)
2022-06-21 Andres NoetzliRemove unused `DeclarationSequence` command (#8892)
2022-06-18 mudathirmahgoubRemove redundant projection operators (#8889)
2022-06-17 Andres NoetzliAdd support for operators with same payload (#8886)
2022-06-16 Andres Noetzli[CMake] Remove redundant code (#8885)
2022-06-15 Andres NoetzliDisable parser regression for competition builds (...
2022-06-15 Andres Noetzli[Regressions] Disable ASan on slow regression (#8882)
2022-06-14 Andres Noetzli[CMake] Fix `install()` commands (#8879)
2022-06-13 Aina Niemetzbv sat solvers: Update CaDiCaL and Kissat to most recen...
2022-06-13 Gereon KremerInfrastructure for portfolio solving (#8709)
2022-06-10 Andres Noetzli[Win64] Use `CC_FOR_BUILD` when compiling GMP (#8874)
2022-06-09 Andres Noetzli[Java API] Do not link JNI libraries (#8870)
2022-06-07 Haniel BarbosaMove slow regression (#8866)
2022-06-07 Andrew ReynoldsAllow mixed int/real equalities in non-strict parsing...
2022-06-07 mudathirmahgoubAdd set.filter operator and its inference rules (#8856)
2022-06-07 Mathias PreinerRemove redundant options headers from TPTP parser....
2022-06-07 Andrew ReynoldsAdd str.unit to LFSC signature (#8862)
2022-06-07 mudathirmahgoubAdd set.map signature to lfsc (#8860)
2022-06-07 Andrew ReynoldsUse STRING_NTH in strings reductions and eliminate...
2022-06-06 Andres Noetzli[CMake] Improve FindGMP (#8846)
2022-06-06 Abdalrhman... Disable `lfsc` tester if `proof` tester is disabled...
2022-06-06 Andrew ReynoldsAdd MBQI to SMT comp script (#8858)
2022-06-06 mudathirmahgoubAdd declareOracleFun to the Java API (#8815)
2022-06-05 Andrew ReynoldsDisable LFSC for regression with learned rewrite (...
2022-06-04 Andrew ReynoldsFix corner case of interpolants from conjectures with...
2022-06-03 mudathirmahgoubAdd inference rules for set.map operator (#8849)
2022-06-03 Andrew ReynoldsFix check for whether a term contains an uninterpreted...
2022-06-03 Andrew ReynoldsDisable arithmetic static learning when unsat cores...
2022-06-03 Andrew ReynoldsEliminate static options access from pattern term selec...
2022-06-02 Andrew ReynoldsPreparation for SEQ_NTH applied to strings (#8779)
2022-06-02 Haniel Barbosa[proofs] [sat] [cores] Fix unsat cores based on the...
2022-06-02 Andrew ReynoldsFix missing conclusion for sep pto neg prop (#8844)
2022-06-02 yoni206Restricting the bit-width in int-to-bv (#8814)
2022-06-02 yoni206Disable arrays in eager bit-blasting (#8785)
2022-06-01 Andrew ReynoldsMake interpolation robust to conjectures with no shared...
2022-06-01 Gereon KremerRefactor how options are passed to the printer (#8827)
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)
next