projects / cvc5.git / shortlog
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
cvc5.git
2022-07-19 Andrew ReynoldsGlobal negate requires quantifiers (#8957) commit | commitdiff | tree
2022-07-18 Andrew ReynoldsFix global-declarations with abduction (#8961) commit | commitdiff | tree
2022-07-18 mudathirmahgoubFix issue 8959 (#8962) commit | commitdiff | tree
2022-07-13 Jacob Lifshayfix incorrect 64-bit detection -- powerpc64le doesn... main commit | commitdiff | tree
2022-07-11 Andrew ReynoldsMove bv arith conversions to arith (#8945) commit | commitdiff | tree
2022-07-11 Andres Noetzli[IntToBV] Add check for unsupported operators (#8949) commit | commitdiff | tree
2022-07-09 Andres NoetzliRemove `--strings-unified-vspt` option (#8947) commit | commitdiff | tree
2022-07-09 Andrew ReynoldsEliminate static options accesses in sygus (#8943) commit | commitdiff | tree
2022-07-09 Andrew ReynoldsAdd scripts for casc j11 (#8941) commit | commitdiff | tree
2022-07-09 Andrew ReynoldsEliminate static options access in proof utilities... commit | commitdiff | tree
2022-07-09 Andrew ReynoldsFix issues with mixed types in relevant domain (#8901) commit | commitdiff | tree
2022-07-08 Andrew ReynoldsDo not use sygus-inst for internal bounded quantifiers... commit | commitdiff | tree
2022-07-07 Andrew ReynoldsFix casting for arith msum (#8940) commit | commitdiff | tree
2022-07-07 Andrew ReynoldsFix mod elimination in learned rewrite preprocessing... commit | commitdiff | tree
2022-07-07 Andrew ReynoldsDo not eagerly preprocess seq.nth (#8937) commit | commitdiff | tree
2022-07-07 Andrew ReynoldsRevert usage of seq.nth in reductions (#8939) commit | commitdiff | tree
2022-07-07 Andrew ReynoldsFix pto handling for heaps that are not a subset of... commit | commitdiff | tree
2022-07-06 mudathirmahgoubAdd rel.project operator to sets (#8929) commit | commitdiff | tree
2022-07-06 Andres NoetzliUpdate SMT-COMP scripts (#8930) commit | commitdiff | tree
2022-06-30 Andres NoetzliRemove `Theory::postsolve()` (#8924) commit | commitdiff | tree
2022-06-30 Andrew ReynoldsRemove spurious pto singleton inference (#8925) commit | commitdiff | tree
2022-06-30 Andres Noetzli[SMT-COMP] Update use of `--decision` option (#8922) commit | commitdiff | tree
2022-06-30 Andrew ReynoldsFix injectivity inferences for seq.nth applied to strin... commit | commitdiff | tree
2022-06-30 Andrew ReynoldsFix type issue in substitutions from covering solver... commit | commitdiff | tree
2022-06-30 mudathirmahgoubAdd set.aggr operator to sets (#8878) commit | commitdiff | tree
2022-06-29 Andrew ReynoldsFix reduction for seq.nth for strings (#8919) commit | commitdiff | tree
2022-06-29 Andrew ReynoldsFix model construction for str.unit (#8917) commit | commitdiff | tree
2022-06-28 mudathirmahgoubAdd rel.group operator to sets (#8876) commit | commitdiff | tree
2022-06-27 Andres NoetzliMove `SymbolManager` and `SymbolTable` to parser (... commit | commitdiff | tree
2022-06-27 Andres Noetzli[Docs] Update `EnumDocumenter` for newer Sphinx (#8914) commit | commitdiff | tree
2022-06-27 Andrew ReynoldsRevert change in lemma order in prop engine (#8911) commit | commitdiff | tree
2022-06-23 mudathirmahgoubAdd inference rules for table.group (#8819) commit | commitdiff | tree
2022-06-23 Andres NoetzliRemove `CommandSequence` command (#8904) commit | commitdiff | tree
2022-06-23 Andres NoetzliMove non-stream options out of `printer_options.toml... commit | commitdiff | tree
2022-06-23 Andrew ReynoldsFix explanation for strings unit oob inference (#8908) commit | commitdiff | tree
2022-06-23 mudathirmahgoubAdd set.fold operator (#8867) commit | commitdiff | tree
2022-06-23 Andres NoetzliFix rewrite for `(to_int real.pi)` (#8907) commit | commitdiff | tree
2022-06-23 Andrew ReynoldsFix handling of injectivity for str.unit (#8899) commit | commitdiff | tree
2022-06-22 mudathirmahgoubprint run_process command (#8859) commit | commitdiff | tree
2022-06-22 Andres NoetzliRemove `Command::clone()` (#8903) commit | commitdiff | tree
2022-06-22 Andres NoetzliSimplify printing of command results (#8902) commit | commitdiff | tree
2022-06-22 mudathirmahgoubAvoid quoting symbols already surrounded with vertical... commit | commitdiff | tree
2022-06-22 Andrew ReynoldsFix sort inference for equality over finite types ... commit | commitdiff | tree
2022-06-22 mudathirmahgoubAdd type to uninterpreted constant values (#8891) commit | commitdiff | tree
2022-06-22 Andres Noetzli[Parser] Rename generated `.c` to `.cpp` files (#8894) commit | commitdiff | tree
2022-06-21 Andres NoetzliRemove unused `DeclarationSequence` command (#8892) commit | commitdiff | tree
2022-06-18 mudathirmahgoubRemove redundant projection operators (#8889) commit | commitdiff | tree
2022-06-17 Andres NoetzliAdd support for operators with same payload (#8886) commit | commitdiff | tree
2022-06-16 Andres Noetzli[CMake] Remove redundant code (#8885) commit | commitdiff | tree
2022-06-15 Andres NoetzliDisable parser regression for competition builds (... commit | commitdiff | tree
2022-06-15 Andres Noetzli[Regressions] Disable ASan on slow regression (#8882) commit | commitdiff | tree
2022-06-14 Andres Noetzli[CMake] Fix `install()` commands (#8879) commit | commitdiff | tree
2022-06-13 Aina Niemetzbv sat solvers: Update CaDiCaL and Kissat to most recen... commit | commitdiff | tree
2022-06-13 Gereon KremerInfrastructure for portfolio solving (#8709) commit | commitdiff | tree
2022-06-10 Andres Noetzli[Win64] Use `CC_FOR_BUILD` when compiling GMP (#8874) commit | commitdiff | tree
2022-06-09 Andres Noetzli[Java API] Do not link JNI libraries (#8870) commit | commitdiff | tree
2022-06-07 Haniel BarbosaMove slow regression (#8866) commit | commitdiff | tree
2022-06-07 Andrew ReynoldsAllow mixed int/real equalities in non-strict parsing... commit | commitdiff | tree
2022-06-07 mudathirmahgoubAdd set.filter operator and its inference rules (#8856) commit | commitdiff | tree
2022-06-07 Mathias PreinerRemove redundant options headers from TPTP parser.... commit | commitdiff | tree
2022-06-07 Andrew ReynoldsAdd str.unit to LFSC signature (#8862) commit | commitdiff | tree
2022-06-07 mudathirmahgoubAdd set.map signature to lfsc (#8860) commit | commitdiff | tree
2022-06-07 Andrew ReynoldsUse STRING_NTH in strings reductions and eliminate... commit | commitdiff | tree
2022-06-06 Andres Noetzli[CMake] Improve FindGMP (#8846) commit | commitdiff | tree
2022-06-06 Abdalrhman... Disable `lfsc` tester if `proof` tester is disabled... commit | commitdiff | tree
2022-06-06 Andrew ReynoldsAdd MBQI to SMT comp script (#8858) commit | commitdiff | tree
2022-06-06 mudathirmahgoubAdd declareOracleFun to the Java API (#8815) commit | commitdiff | tree
2022-06-05 Andrew ReynoldsDisable LFSC for regression with learned rewrite (... commit | commitdiff | tree
2022-06-04 Andrew ReynoldsFix corner case of interpolants from conjectures with... commit | commitdiff | tree
2022-06-03 mudathirmahgoubAdd inference rules for set.map operator (#8849) commit | commitdiff | tree
2022-06-03 Andrew ReynoldsFix check for whether a term contains an uninterpreted... commit | commitdiff | tree
2022-06-03 Andrew ReynoldsDisable arithmetic static learning when unsat cores... commit | commitdiff | tree
2022-06-03 Andrew ReynoldsEliminate static options access from pattern term selec... commit | commitdiff | tree
2022-06-02 Andrew ReynoldsPreparation for SEQ_NTH applied to strings (#8779) commit | commitdiff | tree
2022-06-02 Haniel Barbosa[proofs] [sat] [cores] Fix unsat cores based on the... commit | commitdiff | tree
2022-06-02 Andrew ReynoldsFix missing conclusion for sep pto neg prop (#8844) commit | commitdiff | tree
2022-06-02 yoni206Restricting the bit-width in int-to-bv (#8814) commit | commitdiff | tree
2022-06-02 yoni206Disable arrays in eager bit-blasting (#8785) commit | commitdiff | tree
2022-06-01 Andrew ReynoldsMake interpolation robust to conjectures with no shared... commit | commitdiff | tree
2022-06-01 Gereon KremerRefactor how options are passed to the printer (#8827) commit | commitdiff | tree
2022-05-31 Andrew ReynoldsMake subs minimize utility robust to non-constant evalu... commit | commitdiff | tree
2022-05-31 Gereon KremerFix issues with to_real around coverings solver (#8837) commit | commitdiff | tree
2022-05-31 Gereon KremerFix FindCaDiCaL script (#8838) commit | commitdiff | tree
2022-05-31 yoni206Update to GoogleTest 1.11.0 (#8813) commit | commitdiff | tree
2022-05-27 Andrew ReynoldsEliminate more static options accesses (#8832) commit | commitdiff | tree
2022-05-27 Andrew ReynoldsEliminate static options access for central ee (#8823) commit | commitdiff | tree
2022-05-27 Andrew ReynoldsEliminate static options access in skolemize (#8831) commit | commitdiff | tree
2022-05-27 Andrew ReynoldsFix mixed arithmetic issue in relevant domain (#8826) commit | commitdiff | tree
2022-05-27 Andrew ReynoldsEliminate static options access in BV inverter (#8829) commit | commitdiff | tree
2022-05-27 Andrew ReynoldsMake Rewriter::rewrite non-static (#8828) commit | commitdiff | tree
2022-05-26 Andrew ReynoldsUse function array constants in HO solver (#8818) commit | commitdiff | tree
2022-05-26 Gereon KremerMake sure phase-shift lemma is properly typed (#8824) commit | commitdiff | tree
2022-05-25 Andrew ReynoldsEliminate some static options access (#8795) commit | commitdiff | tree
2022-05-25 Haniel Barbosa[proofs] [alethe] Remove static call to options from... commit | commitdiff | tree
2022-05-25 Andrew ReynoldsAdd model-based quantifier instantiation (#8729) commit | commitdiff | tree
2022-05-25 Andrew ReynoldsEliminate static access to dtSharedSelectors (#8804) commit | commitdiff | tree
2022-05-25 Andrew ReynoldsEliminate more static options accesses (#8802) commit | commitdiff | tree
2022-05-24 Andrew ReynoldsIntroduce function array constant (#8793) commit | commitdiff | tree
2022-05-24 Andrew ReynoldsFix subtype issues in proofs for nonlinear solver ... commit | commitdiff | tree
2022-05-24 Aina Niemetzbv: Disable rule ExtractArith. (#8816) commit | commitdiff | tree
next