GCC Code Coverage Report
Directory: . Exec Total Coverage
File: test/api/ouroborous.cpp Lines: 72 79 91.1 %
Date: 2021-03-22 Branches: 127 253 50.2 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file ouroborous.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Aina Niemetz, Morgan Deters, Christopher L. Conway
6
 ** This file is part of the CVC4 project.
7
 ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
8
 ** in the top-level source directory and their institutional affiliations.
9
 ** All rights reserved.  See the file COPYING in the top-level source
10
 ** directory for licensing information.\endverbatim
11
 **
12
 ** \brief "Ouroborous" test: does CVC4 read its own output?
13
 **
14
 ** The "Ouroborous" test, named after the serpent that swallows its
15
 ** own tail, ensures that CVC4 can parse some input, output it again
16
 ** (in any of its languages) and then parse it again.  The result of
17
 ** the first parse must be equal to the result of the second parse;
18
 ** both strings and expressions are compared for equality.
19
 **
20
 ** To add a new test, simply add a call to runTestString() under
21
 ** runTest(), below.  If you don't specify an input language,
22
 ** LANG_SMTLIB_V2 is used.  If your example depends on variables,
23
 ** you'll need to declare them in the "declarations" global, just
24
 ** below, in SMT-LIBv2 form (but they're good for all languages).
25
 **/
26
27
#include <cassert>
28
#include <iostream>
29
#include <string>
30
31
#include "api/cvc4cpp.h"
32
#include "options/set_language.h"
33
#include "parser/parser.h"
34
#include "parser/parser_builder.h"
35
#include "smt/command.h"
36
37
using namespace CVC4;
38
using namespace CVC4::parser;
39
using namespace CVC4::language;
40
41
int runTest();
42
43
1
int main()
44
{
45
  try
46
  {
47
1
    return runTest();
48
  }
49
  catch (api::CVC4ApiException& e)
50
  {
51
    std::cerr << e.getMessage() << std::endl;
52
  }
53
  catch (parser::ParserException& e)
54
  {
55
    std::cerr << e.getMessage() << std::endl;
56
  }
57
  catch (...)
58
  {
59
    std::cerr << "non-cvc4 exception thrown" << std::endl;
60
  }
61
  return 1;
62
}
63
64
24
std::string parse(std::string instr,
65
                  std::string input_language,
66
                  std::string output_language)
67
{
68
24
  assert(input_language == "smt2" || input_language == "cvc4");
69
24
  assert(output_language == "smt2" || output_language == "cvc4");
70
71
48
  std::string declarations;
72
73
24
  if (input_language == "smt2")
74
  {
75
13
    declarations =
76
        "\
77
  (declare-sort U 0)\n\
78
  (declare-fun f (U) U)\n\
79
  (declare-fun x () U)\n\
80
  (declare-fun y () U)\n\
81
  (assert (= (f x) x))\n\
82
  (declare-fun a () (Array U (Array U U)))\n\
83
  ";
84
  }
85
  else
86
  {
87
11
    declarations =
88
        "\
89
      U: TYPE;\n\
90
      f: U -> U;\n\
91
      x,y: U;\n\
92
      a: ARRAY U OF (ARRAY U OF U);\n\
93
      ASSERT f(x) = x;\n\
94
  ";
95
  }
96
97
48
  api::Solver solver;
98
  InputLanguage ilang =
99
24
      input_language == "smt2" ? input::LANG_SMTLIB_V2 : input::LANG_CVC4;
100
101
24
  solver.setOption("input-language", input_language);
102
24
  solver.setOption("output-language", output_language);
103
48
  SymbolManager symman(&solver);
104
48
  Parser* parser = ParserBuilder(&solver, &symman, "internal-buffer")
105
24
                       .withStringInput(declarations)
106
24
                       .withInputLanguage(ilang)
107
24
                       .build();
108
  // we don't need to execute the commands, but we DO need to parse them to
109
  // get the declarations
110
170
  while (Command* c = parser->nextCommand())
111
  {
112
146
    delete c;
113
146
  }
114
24
  assert(parser->done());  // parser should be done
115
24
  parser->setInput(Input::newStringInput(ilang, instr, "internal-buffer"));
116
48
  api::Term e = parser->nextExpression();
117
24
  std::string s = e.toString();
118
24
  assert(parser->nextExpression().isNull());  // next expr should be null
119
24
  delete parser;
120
48
  return s;
121
}
122
123
12
std::string translate(std::string instr,
124
                      std::string input_language,
125
                      std::string output_language)
126
{
127
12
  assert(input_language == "smt2" || input_language == "cvc4");
128
12
  assert(output_language == "smt2" || output_language == "cvc4");
129
130
12
  std::cout << "==============================================" << std::endl
131
12
            << "translating from "
132
12
            << (input_language == "smt2" ? input::LANG_SMTLIB_V2
133
12
                                         : input::LANG_CVC4)
134
12
            << " to "
135
12
            << (output_language == "smt2" ? output::LANG_SMTLIB_V2
136
12
                                          : output::LANG_CVC4)
137
12
            << " this string:" << std::endl
138
12
            << instr << std::endl;
139
12
  std::string outstr = parse(instr, input_language, output_language);
140
12
  std::cout << "got this:" << std::endl
141
12
            << outstr << std::endl
142
12
            << "reparsing as "
143
12
            << (output_language == "smt2" ? input::LANG_SMTLIB_V2
144
12
                                          : input::LANG_CVC4)
145
12
            << std::endl;
146
24
  std::string poutstr = parse(outstr, output_language, output_language);
147
12
  assert(outstr == poutstr);
148
12
  std::cout << "got same expressions " << outstr << " and " << poutstr
149
12
            << std::endl
150
12
            << "==============================================" << std::endl;
151
24
  return outstr;
152
}
153
154
4
void runTestString(std::string instr, std::string instr_language)
155
{
156
4
  std::cout << std::endl
157
4
            << "starting with: " << instr << std::endl
158
4
            << "   in language " << input::LANG_SMTLIB_V2 << std::endl;
159
8
  std::string smt2str = translate(instr, instr_language, "smt2");
160
4
  std::cout << "in SMT2      : " << smt2str << std::endl;
161
8
  std::string cvcstr = translate(smt2str, "smt2", "cvc4");
162
4
  std::cout << "in CVC       : " << cvcstr << std::endl;
163
8
  std::string outstr = translate(cvcstr, "cvc4", "smt2");
164
4
  std::cout << "back to SMT2 : " << outstr << std::endl << std::endl;
165
166
4
  assert(outstr == smt2str);  // differences in output
167
4
}
168
169
1
int32_t runTest()
170
{
171
1
  runTestString("(= (f (f y)) x)", "smt2");
172
1
  runTestString("~BVPLUS(3, 0bin00, 0bin11)[2:1] = 0bin10", "cvc4");
173
1
  runTestString("~BVPLUS(3, BVMULT(2, 0bin01, 0bin11), 0bin11)[2:0]", "cvc4");
174
1
  runTestString("a[x][y] = a[y][x]", "cvc4");
175
1
  return 0;
176
3
}