Printing CHCs after they have been simplified in Eldarica

[sepideha]

I ran CHCs of a small java program using Eldarica. With-log option I noticed that in preprocessing phase initial 96 clauses were simplified to 9 clauses and then solved. I am wondering if there is a way in Eldarica to print CHCs after they have been simplified, i.e, to print only 9 clauses?
#Question

[pruemmer]

Hi Sepideh, yes, you can get the simplified clauses using the option -logSimplified Philipp

[sepideha]

Great, thanks!

[sepideha]

Thanks @pruemmer! Is there an option to print the simplified clauses in smt2 format, not prolog?

[zafer-esen]

If it is possible to use the latest committed version, the simplified clauses can now be printed in SMT-LIB format using the option -logSimplifiedSMT.

[sepideha]

Thanks @zafer-esen, I used the latest nightly build, very helpful! Would be great if this option appears in the official release as well.

[sepideha]

Thanks @zafer-esen and another followup feature request on this! It'd be great if the simplified clauses in SMT-LIB format are printed in a way that they are parsable & solvable by Eldarica. When printing the simplified clauses, is it possible to print/dump simplified CHCs with their declarations in SMT-LIB format?

[zafer-esen]

Thanks for the feedback @sepideha! -logSimplifiedSMT option should now produce a complete SMT-LIB output (including the declarations). We are planning to include this option in the official release as well, but for now you can probably use it again through the nightly build. If you are building from source you will also need to update Princess to the latest nightly version (sbt clean & sbt update).

[sepideha]

Cool! thank for the quick action on it @zafer-esen!

[pruemmer]

Hi,
I just noticed an issue with the -logSimplifiedSMT option: when it is used for problems that use Booleans, the output will contain also a datatype definition that shouldn't be there:

[...]
(declare-datatype bool (
(true)
(false)
))
[...]

This datatype only exists internally, it should not be printed.

Philipp

[sepideha]

Thanks for the update! I also have one question in the encoding:
Here is the small java program:

    public class Main {
        public static int a;
        public static int b;
        public static void main(String[] args) {
             java.util.Random random = new java.util.Random(-5);
             int nondet = random.nextInt(); 
             if(nondet > 0) return; //assume nondet <=0 
                     a = nondet;
                     b = nondet - 3;
                     while( a< 5 ){
                          a++;
                     }
                   while(b < a){
                          b++;
                     }
                   b++;
                   assert(b <= 6);
       }
   }`

and here is the simplified clause that Eldarica prints:

Clauses after preprocessing:

   <Block4(P54, P35) :- 0 >= P54 & P22 >= 0  & P16 >= 0 & P12 >= 0 & P42 >= 0   & P35 = P54 - 3.
   <Block5(P10, P18) :- <Block4(P10, P18), P10 >= 5.
   <Block4(P6, P8) :- <Block4(P6 - 1, P8), P6  < 6.
   <Block5(P55, P24) :- <Block5(P55, P24 - 1), P24 - 1 < P55.
   false :- <Block5(P32, P19), 6 < P19 & P19 >= P32.

I think the b++ in the last line was not encoded, I believe the last clause should be : false :- <Block5(P32, P19), 6 < P19+1 & P19 >= P32. Do I miss something?

Sepideh

[zafer-esen]

Hi, I just noticed an issue with the -logSimplifiedSMT option: when it is used for problems that use Booleans, the output will contain also a datatype definition that shouldn't be there:

[...] (declare-datatype bool ( (true) (false) )) [...]

This datatype only exists internally, it should not be printed.

Philipp

This was an issue coming from the SMT lineariser in Princess, should be fixed now.

[zafer-esen]

@sepideha Could you share the encoding of the Java program (in SMT) you passed to Eldarica for simplification?

[sepideha]

I am sharing all the original 5 SMT encodings generated by JayHorn, and also the simplified SMT encoding by Eldarica.
ex-asadi.zip

[zafer-esen]

Yes there seems to be a bug somewhere, but I am not sure if this is a problem coming from the original encoding in JayHorn or a bug during simplification in Eldarica. It is a bit difficult for me to debug due to the size of the clauses in the original encoding, which might already be containing this bug. Does JayHorn return sat/safe if you would use the stronger assertion b == 6? Could you send me the original encoding with this assertion? I can check if it is satisfiable without some of the preprocessors.

[sepideha]

The stronger assert is reported safe by jayHorn as in the attachment.
stronger.zip