Branch data     Line data    Source code

       1                 :            : /******************************************************************************
       2                 :            :  * This file is part of the cvc5 project.
       3                 :            :  *
       4                 :            :  * Copyright (c) 2009-2026 by the authors listed in the file AUTHORS
       5                 :            :  * in the top-level source directory and their institutional affiliations.
       6                 :            :  * All rights reserved.  See the file COPYING in the top-level source
       7                 :            :  * directory for licensing information.
       8                 :            :  * ****************************************************************************
       9                 :            :  *
      10                 :            :  * Test for project issue #581
      11                 :            :  *
      12                 :            :  */
      13                 :            : #include <cvc5/cvc5.h>
      14                 :            : 
      15                 :            : using namespace cvc5;
      16                 :          1 : int main(void)
      17                 :            : {
      18                 :          1 :   TermManager tm;
      19                 :          1 :   Solver solver(tm);
      20                 :          1 :   solver.setOption("incremental", "false");
      21                 :          1 :   solver.setOption("sets-exp", "true");
      22                 :          1 :   solver.setOption("produce-interpolants", "true");
      23                 :          2 :   DatatypeDecl d0 = tm.mkDatatypeDecl("_dt0");
      24                 :          2 :   DatatypeConstructorDecl dtcd1 = tm.mkDatatypeConstructorDecl("_cons8");
      25                 :          1 :   d0.addConstructor(dtcd1);
      26                 :          1 :   Sort s2 = tm.mkParamSort("_p2");
      27                 :          1 :   Sort s3 = tm.mkParamSort("_p3");
      28                 :          4 :   DatatypeDecl d4 = tm.mkDatatypeDecl("_dt1", {s2, s3});
      29                 :          2 :   DatatypeConstructorDecl dtcd5 = tm.mkDatatypeConstructorDecl("_cons14");
      30                 :          2 :   Sort s6 = tm.mkUnresolvedDatatypeSort("_dt4", 3);
      31                 :          5 :   Sort s7 = s6.instantiate({s2, s2, s2});
      32                 :          1 :   dtcd5.addSelector("_sel9", s7);
      33                 :          1 :   dtcd5.addSelectorSelf("_sel10");
      34                 :          1 :   dtcd5.addSelectorSelf("_sel11");
      35                 :          2 :   Sort s8 = tm.mkUnresolvedDatatypeSort("_dt0", 0);
      36                 :          1 :   dtcd5.addSelector("_sel12", s8);
      37                 :          1 :   dtcd5.addSelectorSelf("_sel13");
      38                 :          1 :   d4.addConstructor(dtcd5);
      39                 :          2 :   DatatypeConstructorDecl dtcd9 = tm.mkDatatypeConstructorDecl("_cons19");
      40                 :          1 :   dtcd9.addSelector("_sel15", s2);
      41                 :          1 :   dtcd9.addSelectorSelf("_sel16");
      42                 :          1 :   dtcd9.addSelector("_sel17", s8);
      43                 :          1 :   dtcd9.addSelector("_sel18", s8);
      44                 :          1 :   d4.addConstructor(dtcd9);
      45                 :          2 :   DatatypeConstructorDecl dtcd10 = tm.mkDatatypeConstructorDecl("_cons25");
      46                 :          1 :   dtcd10.addSelector("_sel20", s3);
      47                 :          1 :   dtcd10.addSelector("_sel21", s3);
      48                 :          1 :   dtcd10.addSelector("_sel22", s3);
      49                 :          1 :   dtcd10.addSelector("_sel23", s3);
      50                 :          1 :   dtcd10.addSelector("_sel24", s3);
      51                 :          1 :   d4.addConstructor(dtcd10);
      52                 :          2 :   DatatypeConstructorDecl dtcd11 = tm.mkDatatypeConstructorDecl("_cons31");
      53                 :          1 :   dtcd11.addSelector("_sel26", s2);
      54                 :          5 :   Sort s12 = s6.instantiate({s3, s2, s2});
      55                 :          1 :   dtcd11.addSelector("_sel27", s12);
      56                 :          5 :   Sort s13 = s6.instantiate({s3, s2, s3});
      57                 :          1 :   dtcd11.addSelector("_sel28", s13);
      58                 :          1 :   dtcd11.addSelector("_sel29", s2);
      59                 :          1 :   dtcd11.addSelector("_sel30", s3);
      60                 :          1 :   d4.addConstructor(dtcd11);
      61                 :          1 :   Sort s14 = tm.mkParamSort("_p5");
      62                 :          1 :   Sort s15 = tm.mkParamSort("_p6");
      63                 :          1 :   Sort s16 = tm.mkParamSort("_p7");
      64                 :          5 :   DatatypeDecl d17 = tm.mkDatatypeDecl("_dt4", {s14, s15, s16});
      65                 :          2 :   DatatypeConstructorDecl dtcd18 = tm.mkDatatypeConstructorDecl("_cons32");
      66                 :          1 :   d17.addConstructor(dtcd18);
      67                 :          2 :   DatatypeConstructorDecl dtcd19 = tm.mkDatatypeConstructorDecl("_cons35");
      68                 :          2 :   Sort s20 = tm.mkUnresolvedDatatypeSort("_dt0", 0);
      69                 :          1 :   dtcd19.addSelector("_sel33", s20);
      70                 :          1 :   dtcd19.addSelectorSelf("_sel34");
      71                 :          1 :   d17.addConstructor(dtcd19);
      72                 :          2 :   DatatypeConstructorDecl dtcd21 = tm.mkDatatypeConstructorDecl("_cons39");
      73                 :          1 :   dtcd21.addSelectorSelf("_sel36");
      74                 :          2 :   Sort s22 = tm.mkUnresolvedDatatypeSort("_dt1", 2);
      75                 :          4 :   Sort s23 = s22.instantiate({s16, s16});
      76                 :          1 :   dtcd21.addSelector("_sel37", s23);
      77                 :          1 :   dtcd21.addSelector("_sel38", s15);
      78                 :          1 :   d17.addConstructor(dtcd21);
      79                 :          2 :   DatatypeConstructorDecl dtcd24 = tm.mkDatatypeConstructorDecl("_cons44");
      80                 :          1 :   dtcd24.addSelectorSelf("_sel40");
      81                 :          1 :   dtcd24.addSelector("_sel41", s15);
      82                 :          1 :   dtcd24.addSelector("_sel42", s20);
      83                 :          1 :   dtcd24.addSelector("_sel43", s16);
      84                 :          1 :   d17.addConstructor(dtcd24);
      85                 :          5 :   std::vector<Sort> v25 = tm.mkDatatypeSorts({d0, d4, d17});
      86                 :          1 :   Sort s26 = v25[0];
      87                 :          1 :   Sort s27 = v25[1];
      88                 :          1 :   Sort s28 = v25[2];
      89                 :          1 :   Sort s29 = tm.mkSetSort(s26);
      90                 :          1 :   Term t30 = tm.mkConst(s29, "_x46");
      91                 :          1 :   Term t31 = tm.mkUniverseSet(s29);
      92                 :          1 :   Term t32 = tm.mkVar(s29, "_f49_0");
      93                 :          1 :   Term t33 = tm.mkVar(s29, "_f49_1");
      94                 :          1 :   Term t34 = tm.mkVar(s29, "_f49_2");
      95                 :          3 :   Term t35 = tm.mkTerm(Kind::SET_CHOOSE, {t34});
      96                 :          4 :   Term t36 = tm.mkTerm(Kind::SET_INSERT, {t35, t30});
      97                 :          5 :   Sort s37 = tm.mkFunctionSort({s29, s29, s29}, s29);
      98                 :          5 :   Term t38 = solver.defineFun("_f49", {t32, t33, t34}, s29, t36, true);
      99                 :          6 :   Term t39 = tm.mkTerm(Kind::APPLY_UF, {t38, t30, t30, t30});
     100                 :          1 :   Op o40 = tm.mkOp(Kind::SET_MINUS);
     101                 :          4 :   Term t41 = tm.mkTerm(o40, {t30, t30});
     102                 :          1 :   Op o42 = tm.mkOp(Kind::SET_IS_SINGLETON);
     103                 :          3 :   Term t43 = tm.mkTerm(o42, {t31});
     104                 :          1 :   Sort s44 = t43.getSort();
     105                 :          1 :   Op o45 = tm.mkOp(Kind::EQUAL);
     106                 :          1 :   Term t46 = t39.eqTerm(t41);
     107                 :          1 :   Term t47 = t46.xorTerm(t43);
     108                 :          1 :   solver.assertFormula(t43);
     109                 :          1 :   Term t48 = solver.getInterpolant(t47);
     110                 :            : 
     111                 :          1 :   return 0;
     112                 :          1 : }