mean tests fail

[Stephen Siegel]

At least one of the mean tests fails. Others may pass, but only by luck, and need to be examined closely.

At least part of the problem is the way mixed integer/real arithmetic is dealt with. In simplify mode, the symbolic package seems to convert something like 1+2.0 back to an integer 3 (instead of 3.0), and this is carried forward into the value package.

The correctness of integer operations should be carefully checked.

[Stephen Siegel]

See what happens to the value of s at this step:

begin State 9
  onStack = true;
  seen = true;
  pathCondition : ((0<=(X0+-2))&&((0<=((X0*-1)+2))&&(0<=(X0+-1))))
  begin model state
    begin shared variables
      N = X0 (int);
      a = X1 (int[X0]);
      s = undefined (real);
    end shared variables;
    begin process 0
      begin stack frame 0
        function : main;
        location : 5;
        i = 2 (int);
        x = (X1[1]+X1[0]) (int);
      end stack frame 0;
    end process 0;
  end model state
end State 9

Step 10: State 9 -- meanSpec_2.mmp line 16 [main@5->main@6] "s = x / N;" -> State 10

begin State 10
  onStack = true;
  seen = true;
  pathCondition : ((0<=(X0+-2))&&((0<=((X0*-1)+2))&&(0<=(X0+-1))))
  begin model state
    begin shared variables
      N = X0 (int);
      a = X1 (int[X0]);
      s = (X1[1]+X1[0]) (int);
    end shared variables;
    begin process 0
      begin stack frame 0
        function : main;
        location : 6;
        i = 2 (int);
        x = (X1[1]+X1[0]) (int);
      end stack frame 0;
    end process 0;
  end model state
end State 10

This is testCompareIgnoreSimplify.

[Stephen Siegel]

Note that CVC3 does not support integer division. (It is the same as real division.) I you want to support it, you need to do something like introduce a new integer variable and add two constraints involving that variable and the quotient.

However, that does not explain the problem with this example. Even after switching over to reals, the same error occurs. There seems to be a problem with simplify.

[ywei]

I got a CVC3 exception like this:
cvc3.Cvc3Exception: Arithmetic error: not positive integer exponent in (X0 ^-1)

at cvc3.ValidityChecker.jniSimplify(Native Method)
at cvc3.ValidityChecker.simplify(ValidityChecker.java:1304)
at edu.udel.cis.vsl.minimp.symbolic.prover.CVC3TheoremProver.simplify(CVC3TheoremProver.java:597)
at edu.udel.cis.vsl.minimp.symbolic.SymUniverse.equalsExpression(SymUniverse.java:1059)
at edu.udel.cis.vsl.minimp.dynamic.impl.DynamicFactory.equals(DynamicFactory.java:214)
at edu.udel.cis.vsl.minimp.verify.IF.InnerPredicate.holdsAt(InnerPredicate.java:122)
at edu.udel.cis.vsl.minimp.verify.IF.InnerPredicate.holdsAt(InnerPredicate.java:1)
at edu.udel.cis.vsl.minimp.search.DfsSearcher.search(DfsSearcher.java:105)
at edu.udel.cis.vsl.minimp.search.DfsSearcher.search(DfsSearcher.java:93)
at edu.udel.cis.vsl.minimp.verify.IF.OuterPredicate.holdsAt(OuterPredicate.java:257)
at edu.udel.cis.vsl.minimp.verify.IF.OuterPredicate.holdsAt(OuterPredicate.java:1)
at edu.udel.cis.vsl.minimp.search.DfsSearcher.search(DfsSearcher.java:105)
at edu.udel.cis.vsl.minimp.search.DfsSearcher.search(DfsSearcher.java:93)
at edu.udel.cis.vsl.minimp.verify.Comparison.compare(Comparison.java:80)
at edu.udel.cis.vsl.minimp.verify.Comparison.compare(Comparison.java:29)
at edu.udel.cis.vsl.minimp.MiniMP.compareEquivalence(MiniMP.java:466)
at edu.udel.cis.vsl.minimp.MiniMP.main(MiniMP.java:485)

It occurs when CVC3 tried to compare X1[0]/X0 + X1[1]/X0 == X1[1]*0.5 + X1[0]*0.5.
I tried the interactive CVC3, the problem persisted. And it seemed that CVC3 would convert expression like "1/(X0^{1)" into "X0}-1" so even if I typed in "1/(X0^{1)" in the command line, it still crashed. I also modified symbolic universe to convert expression like "X0}-1" to "1/(X0^{1)" but it didn't work.}

[ywei]

Bug fixed. The JUnit test now passes.