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/options.h" |
22 |
|
#include "options/set_language.h" |
23 |
|
#include "parser/parser.h" |
24 |
|
#include "parser/parser_builder.h" |
25 |
|
#include "smt/command.h" |
26 |
|
#include "smt/smt_engine.h" |
27 |
|
|
28 |
|
using namespace cvc5; |
29 |
|
using namespace cvc5::parser; |
30 |
|
using namespace std; |
31 |
|
|
32 |
|
void testGetInfo(api::Solver* solver, const char* s); |
33 |
|
|
34 |
1 |
int main() |
35 |
|
{ |
36 |
2 |
Options opts; |
37 |
1 |
opts.setInputLanguage(language::input::LANG_SMTLIB_V2); |
38 |
1 |
opts.setOutputLanguage(language::output::LANG_SMTLIB_V2); |
39 |
|
|
40 |
1 |
cout << language::SetLanguage(language::output::LANG_SMTLIB_V2); |
41 |
|
|
42 |
|
std::unique_ptr<api::Solver> solver = |
43 |
2 |
std::unique_ptr<api::Solver>(new api::Solver(&opts)); |
44 |
1 |
testGetInfo(solver.get(), ":error-behavior"); |
45 |
1 |
testGetInfo(solver.get(), ":name"); |
46 |
1 |
testGetInfo(solver.get(), ":authors"); |
47 |
1 |
testGetInfo(solver.get(), ":version"); |
48 |
1 |
testGetInfo(solver.get(), ":status"); |
49 |
1 |
testGetInfo(solver.get(), ":reason-unknown"); |
50 |
1 |
testGetInfo(solver.get(), ":arbitrary-undefined-keyword"); |
51 |
1 |
testGetInfo(solver.get(), ":56"); // legal |
52 |
1 |
testGetInfo(solver.get(), ":<="); // legal |
53 |
1 |
testGetInfo(solver.get(), ":->"); // legal |
54 |
1 |
testGetInfo(solver.get(), ":all-statistics"); |
55 |
|
|
56 |
1 |
return 0; |
57 |
|
} |
58 |
|
|
59 |
11 |
void testGetInfo(api::Solver* solver, const char* s) |
60 |
|
{ |
61 |
22 |
std::unique_ptr<SymbolManager> symman(new SymbolManager(solver)); |
62 |
|
|
63 |
|
std::unique_ptr<Parser> p( |
64 |
22 |
ParserBuilder(solver, symman.get(), solver->getOptions()).build()); |
65 |
33 |
p->setInput(Input::newStringInput(language::input::LANG_SMTLIB_V2, |
66 |
22 |
string("(get-info ") + s + ")", |
67 |
|
"<internal>")); |
68 |
11 |
assert(p != NULL); |
69 |
11 |
Command* c = p->nextCommand(); |
70 |
11 |
assert(c != NULL); |
71 |
11 |
cout << c << endl; |
72 |
22 |
stringstream ss; |
73 |
11 |
c->invoke(solver, symman.get(), ss); |
74 |
11 |
assert(p->nextCommand() == NULL); |
75 |
11 |
delete c; |
76 |
11 |
cout << ss.str() << endl << endl; |
77 |
14 |
} |