Open hidenori-shinohara opened 2 years ago
I found a smaller example that produces the exact same issue.
#lang ivy1.7
type my_type_1
type my_type_2 = { val1, val2 }
type my_type_3
interpret my_type_1 -> bv[2]
interpret my_type_3 -> bv[8]
object node(type_1:my_type_1) = {
relation voted(MY_TYPE_2:my_type_2, MY_TYPE_3:my_type_3)
after init {
# Removing this initialization removes the compilation bug.
require voted(MY_TYPE_2, MY_TYPE_3);
}
}
extract executable_runner = node
This seems like a very subtle bug. The order in which my_type_*
's are passed seem to important in reproducing this issue, and it seems that two of them have to interpreted as bit vectors of different sizes and the last one must be an enum. I think ctype_function
and sym_decl
seem related to this issue, but I am not sure.
For reference, my Ivy version is 1.8.22
(f0a63852a8bb960a8bb52aace1902263ed84fd33)
For future reference: one workaround I found is to use bool
instead of the enum type.
I found a similar error in my code-example, and I've raised it in #60 . Could you please elaborate upon the work-around that you identified? How are you using bool
instead of enum type
? Thank you for your help.
@prpr2770 Instead of type_2
I used bool
since type_2
only had two values. The voted
relation was identified by what type of voting it was (prepare
or commit
) and the actual value (=> type_3
). But instead, I used true
to represent prepare
and false
to represent commit
. So instead of voted(prepare, val1)
, I would write voted(true, val1)
. I'm not sure if it works for all cases, but this worked for my particular case. (For instance, if the enum has more than 2 values, I don't think this approach makes sense.)
I ran
ivy_to_cpp target=test isolate=executable_runner build=false executable.ivy
for the following ivy codeand tried to compile it using
clang++ -c -O2 -g -std=c++17 -pthread -I /home/hidenori/ivy/ivy/include -o executable.o executable.cpp
.However, this failed with
It looks like Ivy is confused about the arity of the relation
voted
. For some reason, as denoted in comments, removing parts of the code makes the bug disappear.