(parametric datatypes API) Unexpected sort of APPLY_SELECTOR term.

[aniemetz]

cvc5/cvc5@9b81d04da42615642c2fd4ec6b4637862848ae0a murxla/murxla@446feb874766b3ed98eeb8af3e245f66718fcff8

The following API sequence creates an APPLY_SELECTOR on an instantiated parametric mutually recursive DT, where cvc5 returns the non-instantiated sort via getSort(), which shouldn't be the case.

TEST_F(TestApiBlackSolver, foo)
{
  Sort s1 = d_solver.getBooleanSort();

  Sort u1 = d_solver.mkSortConstructorSort("_x0", 1);
  Sort u2 = d_solver.mkSortConstructorSort("_x1", 1);
  Sort p1 = d_solver.mkParamSort("_x4");
  Sort p2 = d_solver.mkParamSort("_x27");

  DatatypeDecl dtdecl1 = d_solver.mkDatatypeDecl("_x0", p1);
  DatatypeConstructorDecl ctordecl1 = d_solver.mkDatatypeConstructorDecl("_x18");
  ctordecl1.addSelector("_x17", u2.instantiate({p2}));
  dtdecl1.addConstructor(ctordecl1);

  DatatypeDecl dtdecl2 = d_solver.mkDatatypeDecl("_x1", p2);
  DatatypeConstructorDecl ctordecl2 = d_solver.mkDatatypeConstructorDecl("_x41");
  ctordecl2.addSelector("_x40", u1.instantiate({p1}));
  dtdecl2.addConstructor(ctordecl2);

  std::vector<Sort> dt_sorts = d_solver.mkDatatypeSorts({dtdecl1, dtdecl2}, {u1, u2});
  Sort s8 = dt_sorts[1].instantiate({s1});
  Term t895 = d_solver.mkConst(s8, "_x374");
  Term t896 = d_solver.mkTerm(
      APPLY_SELECTOR,
      t895.getSort().getDatatype().getSelector("_x40").getSelectorTerm(),
      t895);
  std::cout << "dt_sorts[0].instantiate({s1}): " << dt_sorts[0].instantiate({s1}).toString() << std::endl;
  std::cout << "t896.getSort(): " << t896.getSort().toString() << std::endl;
  ASSERT_FALSE(t895.getSort().isSortConstructor());
  ASSERT_EQ(dt_sorts[0].instantiate({s1}), t896.getSort());
}

The ASSERT_EQ fails. The sort strings are:

dt_sorts[0].instantiate({s1}): (_x0 Bool)                                 
t896.getSort(): (_x0 _x4)  

Note that the issue here is that u2 and u1 are instantiated with the wrong parameter sorts (they are out of scope). It should be

ctordecl1.addSelector("_x17", u2.instantiate({p1}));
ctordecl2.addSelector("_x40", u1.instantiate({p2}));

We should guard against this.

[ajreynol]

This is a longer term goal, we should make a special "parameter" sort which would give us a way of ensuring that all sorts are in scope.