markusrabe / cadet Goto Github PK

Hello,
Thank you for your tool. I installed it and the tests passed. I created my own file but I don't understand what is wrong in my file, I've got the error :
Is not 2QBF. Currently not supported.
I attached the file : not_working.txt
Thanks for your time.
BoltMaud

This is the error i am getting during the execution of the qdimacs file.
Can you please tell me what the problem is?

I'm wondering if cadet can be applied to quantifier elimination for only exist-quantifer formulas, like ∃ y. $\phi $. If yes, which parameter should be used to generate quantifier elimination results.
I have this problem because when I apply cadet -e to formulas(in QDIMACS) which only contain exist quantifier, it comes to generate aag file like this, which seems not to be right. So I'm wondering if I use cadet in the wrong way or cadet just can't do it, thanks.

aag 0 0 0 1 0
1
o0 There is an assignment to the existentials

Hi, I am wondering if you have extended ID (your work "Incremental Determinization
for Quantifier Elimination and Functional Synthesis" in CAV19) in the current version of cadet?

When I run the command ./configure && make, I get a long error message that ends with:

collect2: error: ld returned 1 exit status
make: *** [Makefile:31: cadet] Error 1

The full error message can be found here.
Am I doing something wrong or is this an actual problem? I am using GCC version 10.3.0 on Ubuntu 21.04.

Hey! I am using UBUNTU to run your tool. I did the cloning of your repository into my local device. I tried to execute the example you gave in Readme.md.
I did the following steps

1. cloned the repository into my PC
2. created a text editor and pasted the QDIMACS format code as it is into the text editor and saved it as new.qdimacs.( does that work?)
3. used the command ./cadet new.qdimacs to execute the file.
   This did not work. I got an error
   bash: ./cadet : no such file of directory

Can you please tell me where I am going wrong?