Where communities thrive


  • Join over 1.5M+ people
  • Join over 100K+ communities
  • Free without limits
  • Create your own community
People
Activity
    leo
    @leonardoalt:matrix.org
    [m]
    I'm of course not sure how useful the benchmarks I could contribute would be, but worse case NIA-Arrays-ADT-BV. BV could be stripped out, and I guess I would need to guarantee that the benchmarks are rather LIA
    nonlinear clauses, quantifier free bodies
    but in general I see the value of a "best effort" category, not sure how practical/important that is for the competition
    Grigory Fedyukovich
    @grigoryfedyukovich
    There are new benchmarks for LIA-Lin-Arrays with quantified bodies (and therefore, quantified solutions) from Vienna people (check their paper at FMCAD'20). We've converted them to CHCs.
    Philipp Ruemmer
    @pruemmer
    ok, it would be great to upload all available benchmarks on github, we can then see which tracks make sense!
    for NIA-Array-ADT-BV, I suspect few solvers will qualify ;-)
    Philipp Ruemmer
    @pruemmer

    Hi all,

    the following solvers have registered for CHC-COMP 2021:

    Golem: LIA-Lin, LRA-TS, LRA-TS-parallel
    Spacer: LIA-Lin, LIA-NonLin, LIA-Lin-Arrays, LIA-NonLin-Arrays, LRA-TS, LRA-TS-parallel, ADT-NonLin
    RegInv: ADT-NonLin
    PCSat: LIA-Lin, LIA-NonLin, ADT-NonLin
    Ultimate TreeAutomizer: LIA-Lin, LIA-NonLin, LIA-Lin-Arrays, LIA-NonLin-Arrays, LRA-TS, LRA-TS-parallel
    Ultimate UniHorn: LIA-Lin, LIA-NonLin, LIA-Lin-Arrays, LIA-NonLin-Arrays, LRA-TS, LRA-TS-parallel
    Eldarica (HC): LIA-Lin, LIA-NonLin, LIA-Lin-Arrays, LIA-NonLin-Arrays, ADT-NonLin

    We removed the ADT-Lin track, since we could not put together a useful set of benchmarks for this track.

    The deadline for sending us the final version of the solvers is March 18.

    You can find example benchmarks in the CHC space on StarExec, https://www.starexec.org/starexec/secure/explore/spaces.jsp?id=442129

    Regards, Grigory & Philipp

    Philipp Ruemmer
    @pruemmer
    Correction: the name of “RegInv” changed to “RInGen”
    leo
    @leonardoalt:matrix.org
    [m]
    Hi there!
    I started uploading some benchmarks from my tool that folks might find useful:
    https://github.com/leonardoalt/chc_benchmarks_solidity
    How about an Industry track for next CHC comp? 😬
    That would mean: every SMT theory is available, nonlinear clauses too.
    Currently only Spacer and Eldarica can solve these benchmarks, but maybe the competition would incentivize other solvers to get there?
    Grigory Fedyukovich
    @grigoryfedyukovich
    Thanks, Leo! So it's a combination of theories, I guess? Can you list them here?
    IMHO, we need at least three solvers to register for a track. And Spacer next year will not compete since Hari is one of the organizers.
    leo
    @leonardoalt:matrix.org
    [m]
    NIA, Arrays, ADTs (only tuples, non-recursive), potentially BV but that I can remove, nonlinear clauses
    Grigory Fedyukovich
    @grigoryfedyukovich
    If you unfold tuples and get rid of BV, that would be just NIA+Arrays, so maybe that will make them more approachable by other solvers. Also, what kind of NIA? I could not find *, div, or mod there.
    3 replies
    Hari Govind V K
    @hgvk94
    I am hoping that Eldarica can participate instead of Spacer.
    leo
    @leonardoalt:matrix.org
    [m]
    Regarding tuples, that's true. That would make my encoding a lot more complicated though, not sure I have the current bandwidth to make that change in my code. Maybe eventually we'll have a pre-processing tool that does that pass, since that might be useful for other applications as well besides mine.
    Yea that's true, the actual code only has linear division and mod, and after some equality propagation the horn code too.
    Ah wait, you're talking about abi, you're right.
    It's a single benchmark but it's a lot more meaningful though. The application it comes from currently holds 37 billion usd, whereas my thousands of unit tests hold nothing haha
    1 reply
    leo
    @leonardoalt:matrix.org
    [m]
    How so?
    (it's public code and that info is also public, if that's what you're referring to)
    1 reply
    leo
    @leonardoalt:matrix.org
    [m]
    I'll see what I can do about unfolding the tuples, would make sense in general.
    1 reply
    If you use Matrix/Element you can!
    (Gitter channels are also Matrix channels now after it was bought)
    2 replies
    leo
    @leonardoalt:matrix.org
    [m]
    Yea true, I remember Gitter had that but always found it kinda buggy.
    1 reply
    You can use both, one for emojis one for threads.
    Yurii Kostyukov
    @Columpio
    Hello, everyone. We are now going to make SAT/UNSAT validator for CHC-COMP with our students. As we have seen, there are some tools for that already on https://github.com/chc-comp/chc-tools
    However, there is no chc_is_refute actually and chc_is_model does not work even for examples/ from repository (it gives Z3 parsing error)
    Could anyone elaborate on that? What's the status of chc_is_refute and chc_is_model?
    1 reply