593123426a898cf62658251c9f194fb527711829
1 /********************* */
2 /*! \file smt2_compliance.cpp
4 ** Original author: Morgan Deters
5 ** Major contributors: none
6 ** Minor contributors (to current version): none
7 ** This file is part of the CVC4 project.
8 ** Copyright (c) 2009-2014 New York University and The University of Iowa
9 ** See the file COPYING in the top-level source directory for licensing
10 ** information.\endverbatim
12 ** \brief A test of SMT-LIBv2 commands, checks for compliant output
14 ** A test of SMT-LIBv2 commands, checks for compliant output.
21 #include "smt/options.h"
22 #include "parser/parser.h"
23 #include "expr/expr_manager.h"
24 #include "expr/command.h"
25 #include "smt/smt_engine.h"
26 #include "parser/parser_builder.h"
29 using namespace CVC4::parser
;
32 void testGetInfo(SmtEngine
& smt
, const char* s
);
36 opts
.set(options::inputLanguage
, language::input::LANG_SMTLIB_V2
);
37 opts
.set(options::outputLanguage
, language::output::LANG_SMTLIB_V2
);
39 cout
<< Expr::setlanguage(language::output::LANG_SMTLIB_V2
);
44 testGetInfo(smt
, ":error-behavior");
45 testGetInfo(smt
, ":name");
46 testGetInfo(smt
, ":authors");
47 testGetInfo(smt
, ":version");
48 testGetInfo(smt
, ":status");
49 testGetInfo(smt
, ":reason-unknown");
50 testGetInfo(smt
, ":arbitrary-undefined-keyword");
51 testGetInfo(smt
, ":56");// legal
52 testGetInfo(smt
, ":<=");// legal
53 testGetInfo(smt
, ":->");// legal
54 testGetInfo(smt
, ":all-statistics");
59 void testGetInfo(SmtEngine
& smt
, const char* s
) {
60 ParserBuilder
pb(smt
.getExprManager(), "<internal>", smt
.getExprManager()->getOptions());
61 Parser
* p
= pb
.withStringInput(string("(get-info ") + s
+ ")").build();
63 Command
* c
= p
->nextCommand();
68 assert(p
->nextCommand() == NULL
);
71 cout
<< ss
.str() << endl
<< endl
;