9 #include "options/options.h"
10 #include "expr/expr.h"
11 #include "expr/command.h"
12 #include "parser/parser.h"
13 #include "parser/parser_builder.h"
14 #include "smt/smt_engine.h"
18 using namespace CVC4::parser
;
19 using namespace CVC4::options
;
20 using namespace CVC4::theory
;
22 int main(int argc
, char* argv
[])
26 string
input(argv
[1]);
28 // Create the expression manager
30 options
.set(inputLanguage
, language::input::LANG_SMTLIB_V2
);
31 ExprManager
exprManager(options
);
33 cout
<< Expr::setlanguage(language::output::LANG_SMTLIB_V2
) << Expr::setdepth(-1);
36 ParserBuilder
parserBuilder(&exprManager
, input
, options
);
37 Parser
* parser
= parserBuilder
.build();
39 // Smt manager for simplifications
40 SmtEngine
engine(&exprManager
);
42 // Variables and assertions
43 vector
<BoolExpr
> assertions
;
46 while ((cmd
= parser
->nextCommand())) {
48 AssertCommand
* assert = dynamic_cast<AssertCommand
*>(cmd
);
50 Expr normalized
= engine
.simplify(assert->getExpr());
51 cout
<< "(assert " << normalized
<< ")" << endl
;
56 CheckSatCommand
* checksat
= dynamic_cast<CheckSatCommand
*>(cmd
);
66 cout
<< "(check-sat)" << endl
;
68 // Get rid of the parser