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                 :            :  * "Ouroborous" test: does cvc5 read its own output?
      11                 :            :  *
      12                 :            :  * The "Ouroborous" test, named after the serpent that swallows its
      13                 :            :  * own tail, ensures that cvc5 can parse some input, output it again
      14                 :            :  * (in any of its languages) and then parse it again.  The result of
      15                 :            :  * the first parse must be equal to the result of the second parse;
      16                 :            :  * both strings and expressions are compared for equality.
      17                 :            :  *
      18                 :            :  * To add a new test, simply add a call to runTestString() under
      19                 :            :  * runTest(), below.  If you don't specify an input language,
      20                 :            :  * LANG_SMTLIB_V2 is used.  If your example depends on symbolic constants,
      21                 :            :  * you'll need to declare them in the "declarations" global, just
      22                 :            :  * below, in SMT-LIBv2 form (but they're good for all languages).
      23                 :            :  */
      24                 :            : 
      25                 :            : #include <cvc5/cvc5.h>
      26                 :            : #include <cvc5/cvc5_parser.h>
      27                 :            : 
      28                 :            : #include <cassert>
      29                 :            : #include <iostream>
      30                 :            : #include <string>
      31                 :            : 
      32                 :            : using namespace cvc5;
      33                 :            : using namespace cvc5::internal;
      34                 :            : using namespace cvc5::parser;
      35                 :            : 
      36                 :            : int runTest();
      37                 :            : 
      38                 :          1 : int main()
      39                 :            : {
      40                 :            :   try
      41                 :            :   {
      42                 :          1 :     return runTest();
      43                 :            :   }
      44         [ -  - ]:          0 :   catch (cvc5::CVC5ApiException& e)
      45                 :            :   {
      46                 :          0 :     std::cerr << e.getMessage() << std::endl;
      47                 :          0 :   }
      48                 :          0 :   catch (...)
      49                 :            :   {
      50                 :          0 :     std::cerr << "non-cvc5 exception thrown" << std::endl;
      51                 :          0 :   }
      52                 :          0 :   return 1;
      53                 :            : }
      54                 :            : 
      55                 :         12 : std::string parse(std::string instr,
      56                 :            :                   std::string input_language,
      57                 :            :                   std::string output_language)
      58                 :            : {
      59         [ -  + ]:         12 :   assert(input_language == "smt2");
      60         [ -  + ]:         12 :   assert(output_language == "smt2");
      61                 :            : 
      62                 :            :   std::string declarations =
      63                 :            :       "(set-logic ALL)\n"
      64                 :            :       "(declare-sort U 0)\n"
      65                 :            :       "(declare-fun f (U) U)\n"
      66                 :            :       "(declare-fun x () U)\n"
      67                 :            :       "(declare-fun y () U)\n"
      68                 :            :       "(assert (= (f x) x))\n"
      69                 :         12 :       "(declare-fun a () (Array U (Array U U)))\n";
      70                 :            : 
      71                 :         12 :   cvc5::TermManager tm;
      72                 :         12 :   cvc5::Solver solver(tm);
      73                 :            : 
      74                 :         12 :   modes::InputLanguage ilang = modes::InputLanguage::SMT_LIB_2_6;
      75                 :            : 
      76                 :         12 :   solver.setOption("input-language", input_language);
      77                 :         12 :   solver.setOption("output-language", output_language);
      78                 :         12 :   SymbolManager symman(tm);
      79                 :         12 :   InputParser parser(&solver, &symman);
      80                 :         12 :   std::stringstream ss;
      81                 :         12 :   ss << declarations;
      82                 :         12 :   parser.setStreamInput(ilang, ss, "internal-buffer");
      83                 :            :   // we don't need to execute the commands, but we DO need to parse them to
      84                 :            :   // get the declarations
      85                 :         12 :   std::stringstream tmp;
      86                 :         12 :   Command c;
      87                 :            :   while (true)
      88                 :            :   {
      89                 :         96 :     c = parser.nextCommand();
      90         [ +  + ]:         96 :     if (c.isNull())
      91                 :            :     {
      92                 :         12 :       break;
      93                 :            :     }
      94                 :            :     // invoke the command, which may bind symbols
      95                 :         84 :     c.invoke(&solver, &symman, tmp);
      96                 :            :   }
      97         [ -  + ]:         12 :   assert(parser.done());  // parser should be done
      98                 :         12 :   std::stringstream ssi;
      99                 :         12 :   ssi << instr;
     100                 :         12 :   parser.setStreamInput(ilang, ss, "internal-buffer");
     101                 :         12 :   cvc5::Term e = parser.nextTerm();
     102                 :         12 :   std::string s = e.toString();
     103         [ -  + ]:         12 :   assert(parser.nextTerm().isNull());  // next expr should be null
     104                 :         24 :   return s;
     105                 :         12 : }
     106                 :            : 
     107                 :          6 : std::string translate(std::string instr,
     108                 :            :                       std::string input_language,
     109                 :            :                       std::string output_language)
     110                 :            : {
     111         [ -  + ]:          6 :   assert(input_language == "smt2");
     112         [ -  + ]:          6 :   assert(output_language == "smt2");
     113                 :            : 
     114                 :          6 :   std::cout << "==============================================" << std::endl
     115                 :            :             << "translating from " << input_language << " to "
     116                 :          6 :             << output_language << " this string:" << std::endl
     117                 :          6 :             << instr << std::endl;
     118                 :         12 :   std::string outstr = parse(instr, input_language, output_language);
     119                 :          6 :   std::cout << "got this:" << std::endl
     120                 :          6 :             << outstr << std::endl
     121                 :          6 :             << "reparsing as " << output_language << std::endl;
     122                 :         12 :   std::string poutstr = parse(outstr, output_language, output_language);
     123         [ -  + ]:          6 :   assert(outstr == poutstr);
     124                 :          6 :   std::cout << "got same expressions " << outstr << " and " << poutstr
     125                 :          6 :             << std::endl
     126                 :          6 :             << "==============================================" << std::endl;
     127                 :         12 :   return outstr;
     128                 :          6 : }
     129                 :            : 
     130                 :          3 : void runTestString(std::string instr, std::string instr_language)
     131                 :            : {
     132                 :          3 :   std::cout << std::endl
     133                 :          3 :             << "starting with: " << instr << std::endl
     134                 :          3 :             << "   in language " << instr_language << std::endl;
     135                 :          6 :   std::string smt2str = translate(instr, instr_language, "smt2");
     136                 :          3 :   std::cout << "in SMT2      : " << smt2str << std::endl;
     137                 :          6 :   std::string outstr = translate(smt2str, "smt2", "smt2");
     138                 :          3 :   std::cout << "to SMT2 : " << outstr << std::endl << std::endl;
     139                 :            : 
     140         [ -  + ]:          3 :   assert(outstr == smt2str);  // differences in output
     141                 :          3 : }
     142                 :            : 
     143                 :          1 : int32_t runTest()
     144                 :            : {
     145                 :          1 :   runTestString("(= (f (f y)) x)", "smt2");
     146                 :          1 :   runTestString("(= ((_ extract 2 1) (bvnot (bvadd #b000 #b011))) #b10)",
     147                 :            :                 "smt2");
     148                 :          1 :   runTestString("((_ extract 2 0) (bvnot (bvadd (bvmul #b001 #b011) #b011)))",
     149                 :            :                 "smt2");
     150                 :          1 :   return 0;
     151                 :            : }