GCC Code Coverage Report
Directory: . Exec Total Coverage
File: test/api/smt2_compliance.cpp Lines: 33 33 100.0 %
Date: 2021-03-22 Branches: 45 90 50.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file smt2_compliance.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Aina Niemetz, Morgan Deters, Tim King
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 A test of SMT-LIBv2 commands, checks for compliant output
13
 **
14
 ** A test of SMT-LIBv2 commands, checks for compliant output.
15
 **/
16
17
#include <cassert>
18
#include <iostream>
19
#include <sstream>
20
21
#include "api/cvc4cpp.h"
22
#include "options/options.h"
23
#include "options/set_language.h"
24
#include "parser/parser.h"
25
#include "parser/parser_builder.h"
26
#include "smt/command.h"
27
#include "smt/smt_engine.h"
28
29
using namespace CVC4;
30
using namespace CVC4::parser;
31
using namespace std;
32
33
void testGetInfo(api::Solver* solver, const char* s);
34
35
1
int main()
36
{
37
2
  Options opts;
38
1
  opts.setInputLanguage(language::input::LANG_SMTLIB_V2);
39
1
  opts.setOutputLanguage(language::output::LANG_SMTLIB_V2);
40
41
1
  cout << language::SetLanguage(language::output::LANG_SMTLIB_V2);
42
43
  std::unique_ptr<api::Solver> solver =
44
2
      std::unique_ptr<api::Solver>(new api::Solver(&opts));
45
1
  testGetInfo(solver.get(), ":error-behavior");
46
1
  testGetInfo(solver.get(), ":name");
47
1
  testGetInfo(solver.get(), ":authors");
48
1
  testGetInfo(solver.get(), ":version");
49
1
  testGetInfo(solver.get(), ":status");
50
1
  testGetInfo(solver.get(), ":reason-unknown");
51
1
  testGetInfo(solver.get(), ":arbitrary-undefined-keyword");
52
1
  testGetInfo(solver.get(), ":56");  // legal
53
1
  testGetInfo(solver.get(), ":<=");  // legal
54
1
  testGetInfo(solver.get(), ":->");  // legal
55
1
  testGetInfo(solver.get(), ":all-statistics");
56
57
1
  return 0;
58
}
59
60
11
void testGetInfo(api::Solver* solver, const char* s)
61
{
62
22
  std::unique_ptr<SymbolManager> symman(new SymbolManager(solver));
63
64
22
  ParserBuilder pb(solver, symman.get(), "<internal>", solver->getOptions());
65
11
  Parser* p = pb.withStringInput(string("(get-info ") + s + ")").build();
66
11
  assert(p != NULL);
67
11
  Command* c = p->nextCommand();
68
11
  assert(c != NULL);
69
11
  cout << c << endl;
70
22
  stringstream ss;
71
11
  c->invoke(solver, symman.get(), ss);
72
11
  assert(p->nextCommand() == NULL);
73
11
  delete p;
74
11
  delete c;
75
11
  cout << ss.str() << endl << endl;
76
14
}