Where communities thrive


  • Join over 1.5M+ people
  • Join over 100K+ communities
  • Free without limits
  • Create your own community
People
Activity
    Adrien Champion
    @AdrienChampion
    There's one problem left though, z3 prints the tail of the clause as a let binding when it's above a certain length.
    (let ((a!1 (and <tail>))) (=> a!1 <head>))
    I could not find a way to tell it not to do that. @/all Anyone knows whether there's a solution? Or should I just print the clauses "manually"?
    Arie Gurfinkel
    @agurfinkel
    there is a parameter, but it is global for the whole formula, so it will suppress let binders everywhere in the formula
    printing conjuncts separately is more stable
    Adrien Champion
    @AdrienChampion
    Okay, I'll do that then, thanks
    Arie Gurfinkel
    @agurfinkel
    @/all first draft of the format. Please comment: https://chc-comp.github.io/2018/format.html
    Adrien Champion
    @AdrienChampion

    Since we're formatting everything anyway, wouldn't it be simpler to have

    ```

    (Sorry)
    chc_tail    ::=
      | (and (u_predicate var+)* i_formula*)
    (Also note that (u_predicate var*) needs to be changed to (u_predicate var+) everywhere.)
    Adrien Champion
    @AdrienChampion
    It makes rules (and formatting) easier IMHO.
    Sorry to go back to this but looking at the rules I think u_predicate should either always or never be required to be over distinct variables. (I'm fine either way.) I think it would make the rules simpler and less confusing thanks to uniformity.
    Adrien Champion
    @AdrienChampion
    Sorry, for chc_tail I meant
    chc_tail    ::=
      | (and (u_predicate var+)* i_formula)
    Adrien Champion
    @AdrienChampion
    As Arie said a while ago it's not very convenient to discuss this here, I updated the google doc
    https://docs.google.com/document/d/1JL1_3Rnfaa1qyhV-ZiSX1HCPqECtijnEZ8DsCBY_f0M/edit#
    Arie Gurfinkel
    @agurfinkel
    The only significant chance I can spot is that multiple i_formula must be allowed in chc_tail. I've extended the format with that.
    For nullary predicates, there is no agreement right now
    For distinct variables -- the current agreement is that there is no restriction on what the predicates are applied to in the chc_tail, but the head must be applied to distinct variables
    The rationale is that if the head is not applied to distinct variables, this is adds an implicit equality constraint in chc_tail. It is simpler to not have implicit constraints in the tail.
    The same does not apply to the tail because the implicit constraints are entailed by constraints that are already in the tail
    Dejan Jovanović
    @dddejan
    Was that a typo, or does Adrien really want multiple i_formulas in rules? (considering the "Sorry" comment")
    Adrien Champion
    @AdrienChampion

    I actually don't want anything, neither as a participant for my tool or an organizer for the formatting script. Whatever the rules end up being my tool will support them (modulo bug) and I'll modify the script in consequence. I was trying to make the rules simpler.

    Regarding chc_tail my point was simply that we can remove the first two variants and only keep the and one.

    The formatting script produces systems in a fragment a bit more restrictive than the one from the rules, I'll update the google doc shortly if you want to take a look.

    Adrien Champion
    @AdrienChampion
    Done, see the last page of the google doc. I argue these rules are simpler, but again, I have no reason to champion (!) them. They just happen to be how the script works atm.
    Arie Gurfinkel
    @agurfinkel
    @dddejan , I don't think it is a type. I'd like the tail to have things of the form (and (Inv x y) (> x 0) (> y 0)) instead of (and (Inv x y) (and (> x 0) (> y 0)))
    I don't think it makes a difference to any of the tools
    Adrien Champion
    @AdrienChampion
    Is the formatting script expected to support non-SMT-LIB benchmarks such as the following one?
    https://github.com/chc-comp/hcai-bench/blob/master/svcomp/O3/id_i15_o15_false-unreach-call_true-termination.smt2
    z3 does not like it at all...
    Arie Gurfinkel
    @agurfinkel
    yes. that's z3 specific format :)
    Adrien Champion
    @AdrienChampion
    Meaning z3 can parse it?
    Adrien Champion
    @AdrienChampion
    Recent z3 seems to parse it, but I can't get the python api to work on it
    Adrien Champion
    @AdrienChampion
    So upgrading z3py to the most recent version works, but I could not find a simple way to translate the datalog rules to normal chc assertions.
    Anyone knows of a simple way to do that? Or should we just forget about datalog benchmarks?
    Dejan Jovanović
    @dddejan
    @agurfinkel you might as well not have any restrictions on the order of literals too. seems like the running assumption is that everyone is going to use z3 for parsing, which most likely is the case. this means that yes, it makes no difference. i would prefer more structure as it makes it easier to anticipate things when writing a parser (i.e. there is one constraint that constrains the rule), but it's irrelevant because i am not planning on writing one.
    It would be nice to hear from non-SMT people with tools that don't support horn clauses...
    Alberto Griggio
    @agriggio
    I wasn't planning to use Z3, FWIW...
    that would be more work than anticipated
    Adrien Champion
    @AdrienChampion
    By everyone you mean participants? In this case, I'm not using z3 either.
    Arie Gurfinkel
    @agurfinkel
    @AdrienChampion : I've added support for fixedpoint format to one version of your scripts. But ran out of time to submit a PR. You can see the code here: https://github.com/chc-comp/scripts/blob/matteo/format/translate.py
    parse_fp_file()
    as expected, I don't think @agriggio and @AdrienChampion use Z3. This means they have more voice in the format restrictions. I want the format to be as easy as possible to be parsed by all current participants.
    so far, no non-smt folks have expressed interest. We have broadcasted CFC to various conferences, but no response so far. If anyone knows of people I should contact personally, please let me know.
    @jpgallagher, will your tool(s) participate? Are you happy with the current format?
    Adrien Champion
    @AdrienChampion
    @agurfinkel Okay thanks, the code doesn't work but I fixed it locally. I will commit something later in a separate branch and submit a pull request. By the way, shouldn't queries be transformed to (not query) => false?
    Arie Gurfinkel
    @agurfinkel
    I think it's query implies false
    Arie Gurfinkel
    @agurfinkel
    most commonly we have (query Error) and it should be transformed into (=> Error false)
    Adrien Champion
    @AdrienChampion
    Oh okay, so sat in datalog is unsafe, unlike in Horn clauses usually. I was surprised the system I was getting was unsat and the original one was sat.
    Arie Gurfinkel
    @agurfinkel
    yes, which is very confusing especially when you have files in both formats. I routinely spent hours debugging just to discover that again ;)
    Adrien Champion
    @AdrienChampion
    I feel your pain...
    Adrien Champion
    @AdrienChampion
    chc-comp/scripts#2
    The tool works on virtually all the benchmarks on the chc-comp organization.
    Please take a look at test/check_err/*.smt2 (and scripts/check.sh), if you come up with illegal benchmarks that these test files do not cover let me know or submit a PR :D
    Adrien Champion
    @AdrienChampion
    Issues tracking illegal benchmarks:
    • chc-comp/hcai-bench#1
    • chc-comp/kind2-chc-benchmarks#1
    • chc-comp/kind2-chc-benchmarks#2
    • chc-comp/ldv-ant-med#1
    (Illegal in the sense that z3 fails to parse them.)
    Fabio Fioravanti
    @fabiofioravanti
    Hi all. We are also interested in participating. VeriMAP does not currently support input CHCs in SMTLIB format (Prolog-like format only) but we are considering writing a parser.