Where communities thrive


  • Join over 1.5M+ people
  • Join over 100K+ communities
  • Free without limits
  • Create your own community
People
Activity
    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.
    Adrien Champion
    @AdrienChampion
    Awesome! Let us know if you have questions/remarks on the format
    Fabio Fioravanti
    @fabiofioravanti
    Sure! I'm editing the Google doc adding assumptions that are spread over the conversation
    Arie Gurfinkel
    @agurfinkel
    @fabiofioravanti : the current format is summarized at https://chc-comp.github.io/2018/format.html
    it should include everything from our discussions
    a script to translate arbitrary files to this format is: https://github.com/chc-comp/scripts
    it should not be too difficult to extend the script to convert to prolog-like format. I believe @jpgallagher has a z3-based converter from SMT-LIB constraints to prolog
    if you have benchmarks (in any format) please let me know so that I can include them. The best way is either a link to an archive or a github repo
    Fabio Fioravanti
    @fabiofioravanti
    Thanks Arie. John has kindly shared his converter with us (thank you again @jpgallagher). We will either extend that converter or write a native Prolog parser. We also intend to contribute some benchmarks. Is there a deadline for submitting them?
    Arie Gurfinkel
    @agurfinkel
    Fantastic! Given that this is our first time organizing the competition, there are no strict deadlines. We are waiting for comments until April 2nd. Throughout April, I'll start going over the rules again and getting people to try their tools and benchmarks on StarExec. Provided that everything works smoothly, we can wait until the last minute to finalize competition benchmarks and run the tools.
    Of course, earlier is better, especially if your benchmarks are in your format and will require conversion to smt-lib
    Please let me know if there are any issues for you with our current format. We have tried to make it as simple and as inclusive as possible. But since all of our tools are smt-lib based, we are not sure what complications others might encounter.
    Fabio Fioravanti
    @fabiofioravanti
    Thanks for your comprehension... we will try to adhere to the current format. Our tools can output CHCs in SMTLIB format but not read them yet
    Fabio Fioravanti
    @fabiofioravanti
    Now looking at let-binders. Reading the gdrive doc it seems that all participants use them... are there any further specs about their format and occurrence?
    According to the current grammar they can be used in i_formulas only, right? do let-binders occur at top-level only? can they be nested ?
    Philipp Ruemmer
    @pruemmer
    Hi Fabio ... yes, let binders would only occur in i_formula, and in many benchmarks they should not actually be necessary
    the syntax and semantics follows the one in SMT-LIB, p27 in http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2017-07-18.pdf
    let binders are very commonly nested when they occur
    Fabio Fioravanti
    @fabiofioravanti

    Hi Philipp. Thanks for your answer.

    Can we make some assumptions on the variables occurring in let-binders?

    For example, given the term (let ((x1 t1)...(xn tn)) t )
    the SMT-LIB standard requires that x1...xn are distinct variables but does not say anything about their occurrence in t1...tn.

    Thus a term (let ((x y) (y x)) (> x y)) is legal and equivalent to (> y x).

    Can we assume that variables x1...xn do not occur in t1...tn?
    This would simplify the management of let-binders
    and allow us to manage the parallel bindings in a sequential manner.

    Philipp Ruemmer
    @pruemmer
    In let ((x y) (y x)), technically there are two different variables with name "x" (and two called "y")
    I suppose one could add the simplification in the format that identifiers are not reused (the variables bound by let all have distinct and unique names)
    Fabio Fioravanti
    @fabiofioravanti
    Indeed...
    in the more general form let-binders require a more sophisticated treatment (f.e. for assigning distinct names to the two distinct variables with the same name)
    Arie Gurfinkel
    @agurfinkel
    I don't see the complexity in handling parallel binders. After traversing a let-binder, you have a map {xi -> ti}, you traverse the body of the let statement and replace every occurrence of xi by ti. You do not recurse into the occurrence that was replaced.
    The only complication is the scope introduced by multiple let binders, but that simply means you keep a stack of {xi->ti} maps
    Fabio Fioravanti
    @fabiofioravanti
    Everything could be implemented, of course. Just wondering whether purely parallel let-binders are actually needed or we can make some simplifying assumptions
    Arie Gurfinkel
    @agurfinkel
    I'm worried that simplifying assumptions will make things harder
    Fabio Fioravanti
    @fabiofioravanti
    So.. they would not be simplifying :-)
    Arie Gurfinkel
    @agurfinkel
    what are you trying to actually do? Let-binders are there to ensure that the syntactic representation of an expression is the same as its in memory DAG-representation. If you implement rewriting that eliminates let-binders, the formulas will explode exponentially.
    You have two choices: (a) replace let binders by new existentially quantified variables. That is, rewrite each let as an equality. and (b) write a parser that keeps track of current binding while building the expressions
    (b) seems easier and more robust in presence of nested let binders
    if you want to flatten the formula to remove let binders you can probably use one of many smt-lib parsers to do that.
    but, again, this would explode the size of the formula dramatically
    Fabio Fioravanti
    @fabiofioravanti
    Ok. Thanks. We will try to manage let-binders in their general form ... or we could end asking you to create a separate track with no binders :-)
    Arie Gurfinkel
    @agurfinkel
    The actual benchmarks use binders only to minimize the representation. You might want to look at a few examples. Even without making a restriction in the rules, your assumptions are probably true of all our current benchmarks.
    Fabio Fioravanti
    @fabiofioravanti
    I see.. thanks again
    Grigory Fedyukovich
    @grigoryfedyukovich
    Hey, we need to amend the format to support ADTs. One thing that is missing (at least) is declare-datatype or declare-datatypes
    Philipp Ruemmer
    @pruemmer
    Yes, true; but I think only those two statements are missing?
    Everything else is covered in the “interpreted formulas” part
    Grigory Fedyukovich
    @grigoryfedyukovich
    OK, but do we want to include (recursive) functions for specific ADTs, like length of list? Also, SMT-Lib has some specific support for lists, and we need to be clear if we want to use it, or we require a definition of lists in each benchmark.
    Philipp Ruemmer
    @pruemmer
    I would not include define-fun or define-fun-rec in the format; we can still collect benchmarks of this kind, but not use them in the competition this year.
    [If we are ambitious, we could add a translator from recursive functions to CHCs.]
    SMT-LIB does not support lists directly, this is an extension of Z3, and I think we should not have lists as a pre-defined theory. Where relevant, we can define lists as an ADT.
    Grigory Fedyukovich
    @grigoryfedyukovich
    OK, maybe it is an extension of Z3 rather than an SMT-LIB feature.