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