hasVar() for level 1

[winnieros]

Hello, I noticed a potential bug with the hasVar() method for level 1 nodes. Here is a code snipped where hasVar() on level 1 returns false but if I transform the same node to a level 0 node and check if it contains the same variable it returns true:

Texpr1VarNode x = new Texpr1VarNode("x"); Environment environment = new Environment(new String[]{"x"},new String[]{}); Preconditions.checkArgument(!x.hasVar("x")); \\ I would expect true for x.hasVar("x") Texpr0Node xZero = x.toTexpr0Node(environment); Preconditions.checkArgument(xZero.hasDim(environment.dimOfVar("x")));

Thanks!

[antoinemine]

Thanks for the report.

Could you see if #95 fixes this issue on your side?

[winnieros]

I checked it out, but the fix doesn't change the outcome.

[antoinemine]

This is strange. This fixes the problem for me on your example. Do you have a full program. The following code:

Texpr1VarNode x = new Texpr1VarNode("x");
Environment environment = new Environment(new String[]{"x"},new String[]{}); 
System.out.println(x.hasVar("x"));
Texpr0Node xZero = x.toTexpr0Node(environment);
System.out.println(xZero.hasDim(environment.dimOfVar("x")));

returns true true, which is expected. Do you have a more complete example where it fails?

[winnieros]

Mhm wierd. Same code gives me false true.

[antoinemine]

Sorry, it will be difficult for me to fix the issue if I cannot reproduce it... Any additional information would be welcome.

[winnieros]

Okay, sorry, sure. I try to give as much information as I can. I included the Apron library into JavaSMT (https://github.com/sosy-lab/java-smt/tree/314-adding-the-abstract-numeric-domains-of-the-apron-library-as-smt-solver). The bug occurred firstly in the class https://github.com/sosy-lab/java-smt/blob/314-adding-the-abstract-numeric-domains-of-the-apron-library-as-smt-solver/src/org/sosy_lab/java_smt/solvers/apron/ApronModel.java line 246 ff.

 private ApronNode getComplexValue(ApronNode pNode){
    Texpr1Node node = pNode.getNode();
    List<String> modelVars = new ArrayList<>();
    for (ValueAssignment assignment:model) {
      String modelVar = assignment.getName();
      StringVar apronVar = new StringVar(modelVar);
      ApronNode toSub = (ApronNode) assignment.getValueAsFormula();
      Texpr1Node toSubT = toSub.getNode();
      //hasVar() only works for Texpr0Node
      Texpr0Node zeroNode = node.toTexpr0Node(prover.getAbstract1().getEnvironment());
      boolean hasVarZero =
          zeroNode.hasDim(prover.getAbstract1().getEnvironment().dimOfVar(modelVar));
      if(hasVarZero){
...

So I wrote some Tests (https://github.com/sosy-lab/java-smt/blob/314-adding-the-abstract-numeric-domains-of-the-apron-library-as-smt-solver/src/org/sosy_lab/java_smt/solvers/apron/ApronNativeApiTest.java) line 109 ff.

  @Test
  public void hasVarTest(){
    //code form github
    Texpr1VarNode x = new Texpr1VarNode("x");
    Environment environment = new Environment(new String[]{"x"},new String[]{});
    System.out.println(x.hasVar("x"));
    Texpr0Node xZero = x.toTexpr0Node(environment);
    System.out.println(xZero.hasDim(environment.dimOfVar("x")));

    //has Texpr1VarNode "x"?
    Texpr1VarNode x1 = new Texpr1VarNode("x");
    Environment environment1 = new Environment(new String[]{"x"},new String[]{"y"});
    assertTrue(!x1.hasVar("x")); //should be true
    assertFalse(x1.hasVar("y"));
    Texpr0Node xZero1 = x.toTexpr0Node(environment1);
    assertTrue(xZero1.hasDim(environment1.dimOfVar("x")));
    assertFalse(xZero1.hasDim(environment1.dimOfVar("y")));

    //has x+x "x"?
    Texpr1BinNode xPlusx = new Texpr1BinNode(Texpr1BinNode.OP_ADD, x, x);
    assertTrue(!xPlusx.hasVar("x")); //should be true
    Texpr0Node zeroxPlusx = xPlusx.toTexpr0Node(environment);
    assertTrue(zeroxPlusx.hasDim(environment.dimOfVar("x")));
  }

After your proposed fix I changed the branch of the Apron library but the tests still don't work. I hope this can help you.