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

[zafer-esen]

Thanks! I had a look now, and I actually get the correct encoding (i.e., 6 < b + 1 for the weaker encoding and b + 1 != 6 for the stronger one) when I run Eldarica with the -logSimplified option. I use the command eld Main_5.smt2 -logSimplified > Main_5_simplified.horn.

I tried it with both Main_5.smt2 files from the archives that you've shared. This works for me with both the Nightly and the 2.0.6 releases of Eldarica. Can you tell me how to reproduce the incorrect simplified encoding you sent in the first archive (ex-asadi.zip)? If the simplified encoding was generated from JayHorn, it might be better to move this discussion over there as well.

[sepideha]

Thanks @zafer-esen for checking that. Now I got the latest version and the encoding seems correct, thanks so much! After running your last command I get the following clauses after simplification:

<Main: void main(JayArray_java_lang_String)>_Block4(P54, P35) :- 0 >= P54 - 3 + 3 & P22 >= 0 & P42 >= 0 & P12 >= 0 & P42 >= 0 & P16 >= 0 & P42 >= 0 & P12 >= 0 & P42 >= 0 & P42 >= 0 & P42 >= 0 & P12 >= 0 & P42 >= 0 & P42 >= 0 & P42 >= 0 & P12 >= 0 & P42 >= 0 & P35 = P54 - 3.
<Main: void main(JayArray_java_lang_String)>_Block5(P10, P18) :- <Main: void main(JayArray_java_lang_String)>_Block4(P10, P18), P10 >= 5.
<Main: void main(JayArray_java_lang_String)>_Block4(P6, P8) :- <Main: void main(JayArray_java_lang_String)>_Block4(P6 - 1, P8), P6 - 1 < 5.
<Main: void main(JayArray_java_lang_String)>_Block5(P55, P24) :- <Main: void main(JayArray_java_lang_String)>_Block5(P55, P24 - 1), P24 - 1 < P55.

Although I see room for further simplification, for instance P42 >= 0 appeared 10 times in the first clause.

Also a minor point: the use of & and , would be useful if unified.

[zafer-esen]

@sepideha Glad to see that worked out!

There is some ongoing work in the constraint simplifier, which should also reduce the number of duplicate conjuncts. You are right about the printing of connectives, there shouldn't be any &s in the Prolog-style output. I will try to look into this, but this might end up being more involved to get it right, due to the constraints currently being printed by Princess.