Solver does not report anything... about thoth HOT 11 CLOSED

Hey, thanks for reporting. We will take a look asap ;)

from thoth.

@acmLL It should be good now, can you try again?
don't forget to install the new version 0.7.0 with pip install .

from thoth.

Hey, pventuzelo. Thanks for the update. I tried the same code and got this

thoth local test.json -d
// Function 0
func main.sum2{}(x : felt, y : felt){
v4 = v0_x + v1_y
ret
}

// Function 1
func main.main{output_ptr : felt*}(){
sum2(v6_callers_function_frame, v7_return_instruction)
v8 = v7_return_instruction - 10
if (v8 == 0) {
v9 = v5_output_ptr
ret

}
v10 = v5_output_ptr
ret

}

Then I run thoth local test.json -a assignations and got this

[Optimization] Assignations

• v4 = v0_x + v1_y
• v8 = v7_return_instruction + -10
• v9 = v5_output_ptr
• v10 = v5_output_ptr

Finally, I run thoth local test.json --symbolic -function main.test_symbolic_execution -constraint v8==0 v4==10 -solve v7_return_instruction v_0x v1_y

but thoth returned nothing. Did I make some mistake? Best regards!

P.S.: Is there any chance to connect v4 and v7_return_instruction as the same variable? Because in this way I just have to propose v8==0 and ask the solver to find v0_x and v1_y...

from thoth.

Hello !

If you run

 thoth local test.json --symbolic -function main.test_symbolic_execution -constraint v4==10 -solve v_0x v1_y

and

 thoth local test.json --symbolic -function main.test_symbolic_execution -constraint v8==0 -solve v7_return_instruction 

It should now return the result with the changes applied in #114.

from thoth.

Hi, Rog3rSm1th. When I run thoth local test.json --symbolic -function main.test_symbolic_execution -constraint v4==10 -solve v_0x v1_y, I get nothing. But when I run thoth local test.json --symbolic -function main.sum2 -constraint v4==10 -solve v_0x v1_y, it returns correctly. However, I cannot get a similar behavior for thoth local test.json --symbolic -function main.test_symbolic_execution -constraint v8==0 -solve v7_return_instruction. With this command, it returns nothing. And with this modified one thoth local test.json --symbolic -function main.main -constraint v8==0 -solve v7_return_instruction (I do not know it this modified version makes sense but it is similar to the case sum2 except for the parameters), it returns "No solution". Regards

from thoth.

it should be good with the last commit ;)
thx

from thoth.

Unfortunately, it is not pventuzelo :-(. I deleted the thoth folder right now and reinstalled it again. And my above is being repeated. I can get the values in the function sum2 if I reference it specifically in the command instead of the general -function main.test_symbolic_execution. But I get a "No solution" in the case of __main__main :-( Thanks!

from thoth.

I added the example you are trying to use to the tests here. Using symbolic execution I can now solve the constraints with these commands:

thoth local ./tests/json_files/cairo_0/cairo_test_symbolic_execution_5.json --symbolic -function __main__.sum2 -constraint v4==10 -solve v0_x v1_y           
v0_x: 10
v1_y: 0

thoth local ./tests/json_files/cairo_0/cairo_test_symbolic_execution_5.json --symbolic -function __main__.main -constraint v8==0 -solve v7_return_instruction
v7_return_instruction: 10

I hope this helps!

from thoth.

Thanks, Rog3rSm1th! For some reason...

(cairo_venv) acmLL@MacBook-Air thoth % thoth local ./tests/json_files/cairo_0/cairo_test_symbolic_execution_5.json --symbolic -function main.main -constraint v8==0 -solve v7_return_instruction
No solution

Do you know what can be the problem with my installation? Best!

from thoth.

Did you reinstall thoth ? also can you send me the file you use ?

from thoth.

Yes, Rog3rSm1th. I reinstalled it.
test.cairo.zip

from thoth.