projects
/
cvc5.git
/ shortlog
commit
grep
author
committer
pickaxe
?
search:
re
summary
| shortlog |
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
cvc5.git
2022-07-18
Andrew Reynolds
Fix global-declarations with abduction (#8961)
commit
|
commitdiff
|
tree
2022-07-18
mudathirmahgoub
Fix issue 8959 (#8962)
commit
|
commitdiff
|
tree
2022-07-13
Jacob Lifshay
fix incorrect 64-bit detection -- powerpc64le doesn...
main
commit
|
commitdiff
|
tree
2022-07-11
Andrew Reynolds
Move 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 Noetzli
Remove `--strings-unified-vspt` option (#8947)
commit
|
commitdiff
|
tree
2022-07-09
Andrew Reynolds
Eliminate static options accesses in sygus (#8943)
commit
|
commitdiff
|
tree
2022-07-09
Andrew Reynolds
Add scripts for casc j11 (#8941)
commit
|
commitdiff
|
tree
2022-07-09
Andrew Reynolds
Eliminate static options access in proof utilities...
commit
|
commitdiff
|
tree
2022-07-09
Andrew Reynolds
Fix issues with mixed types in relevant domain (#8901)
commit
|
commitdiff
|
tree
2022-07-08
Andrew Reynolds
Do not use sygus-inst for internal bounded quantifiers...
commit
|
commitdiff
|
tree
2022-07-07
Andrew Reynolds
Fix casting for arith msum (#8940)
commit
|
commitdiff
|
tree
2022-07-07
Andrew Reynolds
Fix mod elimination in learned rewrite preprocessing...
commit
|
commitdiff
|
tree
2022-07-07
Andrew Reynolds
Do not eagerly preprocess seq.nth (#8937)
commit
|
commitdiff
|
tree
2022-07-07
Andrew Reynolds
Revert usage of seq.nth in reductions (#8939)
commit
|
commitdiff
|
tree
2022-07-07
Andrew Reynolds
Fix pto handling for heaps that are not a subset of...
commit
|
commitdiff
|
tree
2022-07-06
mudathirmahgoub
Add rel.project operator to sets (#8929)
commit
|
commitdiff
|
tree
2022-07-06
Andres Noetzli
Update SMT-COMP scripts (#8930)
commit
|
commitdiff
|
tree
2022-06-30
Andres Noetzli
Remove `Theory::postsolve()` (#8924)
commit
|
commitdiff
|
tree
2022-06-30
Andrew Reynolds
Remove 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 Reynolds
Fix injectivity inferences for seq.nth applied to strin...
commit
|
commitdiff
|
tree
2022-06-30
Andrew Reynolds
Fix type issue in substitutions from covering solver...
commit
|
commitdiff
|
tree
2022-06-30
mudathirmahgoub
Add set.aggr operator to sets (#8878)
commit
|
commitdiff
|
tree
2022-06-29
Andrew Reynolds
Fix reduction for seq.nth for strings (#8919)
commit
|
commitdiff
|
tree
2022-06-29
Andrew Reynolds
Fix model construction for str.unit (#8917)
commit
|
commitdiff
|
tree
2022-06-28
mudathirmahgoub
Add rel.group operator to sets (#8876)
commit
|
commitdiff
|
tree
2022-06-27
Andres Noetzli
Move `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 Reynolds
Revert change in lemma order in prop engine (#8911)
commit
|
commitdiff
|
tree
2022-06-23
mudathirmahgoub
Add inference rules for table.group (#8819)
commit
|
commitdiff
|
tree
2022-06-23
Andres Noetzli
Remove `CommandSequence` command (#8904)
commit
|
commitdiff
|
tree
2022-06-23
Andres Noetzli
Move non-stream options out of `printer_options.toml...
commit
|
commitdiff
|
tree
2022-06-23
Andrew Reynolds
Fix explanation for strings unit oob inference (#8908)
commit
|
commitdiff
|
tree
2022-06-23
mudathirmahgoub
Add set.fold operator (#8867)
commit
|
commitdiff
|
tree
2022-06-23
Andres Noetzli
Fix rewrite for `(to_int real.pi)` (#8907)
commit
|
commitdiff
|
tree
2022-06-23
Andrew Reynolds
Fix handling of injectivity for str.unit (#8899)
commit
|
commitdiff
|
tree
2022-06-22
mudathirmahgoub
print run_process command (#8859)
commit
|
commitdiff
|
tree
2022-06-22
Andres Noetzli
Remove `Command::clone()` (#8903)
commit
|
commitdiff
|
tree
2022-06-22
Andres Noetzli
Simplify printing of command results (#8902)
commit
|
commitdiff
|
tree
2022-06-22
mudathirmahgoub
Avoid quoting symbols already surrounded with vertical...
commit
|
commitdiff
|
tree
2022-06-22
Andrew Reynolds
Fix sort inference for equality over finite types ...
commit
|
commitdiff
|
tree
2022-06-22
mudathirmahgoub
Add 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 Noetzli
Remove unused `DeclarationSequence` command (#8892)
commit
|
commitdiff
|
tree
2022-06-18
mudathirmahgoub
Remove redundant projection operators (#8889)
commit
|
commitdiff
|
tree
2022-06-17
Andres Noetzli
Add 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 Noetzli
Disable 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 Niemetz
bv sat solvers: Update CaDiCaL and Kissat to most recen...
commit
|
commitdiff
|
tree
2022-06-13
Gereon Kremer
Infrastructure 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 Barbosa
Move slow regression (#8866)
commit
|
commitdiff
|
tree
2022-06-07
Andrew Reynolds
Allow mixed int/real equalities in non-strict parsing...
commit
|
commitdiff
|
tree
2022-06-07
mudathirmahgoub
Add set.filter operator and its inference rules (#8856)
commit
|
commitdiff
|
tree
2022-06-07
Mathias Preiner
Remove redundant options headers from TPTP parser....
commit
|
commitdiff
|
tree
2022-06-07
Andrew Reynolds
Add str.unit to LFSC signature (#8862)
commit
|
commitdiff
|
tree
2022-06-07
mudathirmahgoub
Add set.map signature to lfsc (#8860)
commit
|
commitdiff
|
tree
2022-06-07
Andrew Reynolds
Use 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 Reynolds
Add MBQI to SMT comp script (#8858)
commit
|
commitdiff
|
tree
2022-06-06
mudathirmahgoub
Add declareOracleFun to the Java API (#8815)
commit
|
commitdiff
|
tree
2022-06-05
Andrew Reynolds
Disable LFSC for regression with learned rewrite (...
commit
|
commitdiff
|
tree
2022-06-04
Andrew Reynolds
Fix corner case of interpolants from conjectures with...
commit
|
commitdiff
|
tree
2022-06-03
mudathirmahgoub
Add inference rules for set.map operator (#8849)
commit
|
commitdiff
|
tree
2022-06-03
Andrew Reynolds
Fix check for whether a term contains an uninterpreted...
commit
|
commitdiff
|
tree
2022-06-03
Andrew Reynolds
Disable arithmetic static learning when unsat cores...
commit
|
commitdiff
|
tree
2022-06-03
Andrew Reynolds
Eliminate static options access from pattern term selec...
commit
|
commitdiff
|
tree
2022-06-02
Andrew Reynolds
Preparation 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 Reynolds
Fix missing conclusion for sep pto neg prop (#8844)
commit
|
commitdiff
|
tree
2022-06-02
yoni206
Restricting the bit-width in int-to-bv (#8814)
commit
|
commitdiff
|
tree
2022-06-02
yoni206
Disable arrays in eager bit-blasting (#8785)
commit
|
commitdiff
|
tree
2022-06-01
Andrew Reynolds
Make interpolation robust to conjectures with no shared...
commit
|
commitdiff
|
tree
2022-06-01
Gereon Kremer
Refactor how options are passed to the printer (#8827)
commit
|
commitdiff
|
tree
2022-05-31
Andrew Reynolds
Make subs minimize utility robust to non-constant evalu...
commit
|
commitdiff
|
tree
2022-05-31
Gereon Kremer
Fix issues with to_real around coverings solver (#8837)
commit
|
commitdiff
|
tree
2022-05-31
Gereon Kremer
Fix FindCaDiCaL script (#8838)
commit
|
commitdiff
|
tree
2022-05-31
yoni206
Update to GoogleTest 1.11.0 (#8813)
commit
|
commitdiff
|
tree
2022-05-27
Andrew Reynolds
Eliminate more static options accesses (#8832)
commit
|
commitdiff
|
tree
2022-05-27
Andrew Reynolds
Eliminate static options access for central ee (#8823)
commit
|
commitdiff
|
tree
2022-05-27
Andrew Reynolds
Eliminate static options access in skolemize (#8831)
commit
|
commitdiff
|
tree
2022-05-27
Andrew Reynolds
Fix mixed arithmetic issue in relevant domain (#8826)
commit
|
commitdiff
|
tree
2022-05-27
Andrew Reynolds
Eliminate static options access in BV inverter (#8829)
commit
|
commitdiff
|
tree
2022-05-27
Andrew Reynolds
Make Rewriter::rewrite non-static (#8828)
commit
|
commitdiff
|
tree
2022-05-26
Andrew Reynolds
Use function array constants in HO solver (#8818)
commit
|
commitdiff
|
tree
2022-05-26
Gereon Kremer
Make sure phase-shift lemma is properly typed (#8824)
commit
|
commitdiff
|
tree
2022-05-25
Andrew Reynolds
Eliminate 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 Reynolds
Add model-based quantifier instantiation (#8729)
commit
|
commitdiff
|
tree
2022-05-25
Andrew Reynolds
Eliminate static access to dtSharedSelectors (#8804)
commit
|
commitdiff
|
tree
2022-05-25
Andrew Reynolds
Eliminate more static options accesses (#8802)
commit
|
commitdiff
|
tree
2022-05-24
Andrew Reynolds
Introduce function array constant (#8793)
commit
|
commitdiff
|
tree
2022-05-24
Andrew Reynolds
Fix subtype issues in proofs for nonlinear solver ...
commit
|
commitdiff
|
tree
2022-05-24
Aina Niemetz
bv: Disable rule ExtractArith. (#8816)
commit
|
commitdiff
|
tree
2022-05-24
mudathirmahgoub
Add table.group operator (#8731)
commit
|
commitdiff
|
tree
next