diff options
author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2012-07-10 15:24:22 +0000 |
---|---|---|
committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2012-07-10 15:24:22 +0000 |
commit | ff5ecc85124857dccb6fa6ed542bb90e678bdc77 (patch) | |
tree | 1ae254a832b4f93666a81d8b3a07340066b24a7a /examples/nra-translate/smt2todreal.cpp | |
parent | 00af00c419b965ed26fff540a565dee748c7e4ed (diff) |
* fixing the simple_vc_cxx.cpp compile issue (no more Integer constants)
* adding as examples the programs i used to translate nonlinear smt2 problems to other formats
Diffstat (limited to 'examples/nra-translate/smt2todreal.cpp')
-rw-r--r-- | examples/nra-translate/smt2todreal.cpp | 66 |
1 files changed, 66 insertions, 0 deletions
diff --git a/examples/nra-translate/smt2todreal.cpp b/examples/nra-translate/smt2todreal.cpp new file mode 100644 index 000000000..34e28bb75 --- /dev/null +++ b/examples/nra-translate/smt2todreal.cpp @@ -0,0 +1,66 @@ +#include <string> +#include <iostream> +#include <typeinfo> +#include <cassert> +#include <vector> +#include <map> + +#include "util/options.h" +#include "expr/expr.h" +#include "expr/command.h" +#include "parser/parser.h" +#include "parser/parser_builder.h" +#include "smt/smt_engine.h" + +using namespace std; +using namespace CVC4; +using namespace CVC4::parser; + +int main(int argc, char* argv[]) +{ + + // Get the filename + string input(argv[1]); + + // Create the expression manager + Options options; + options.inputLanguage = language::input::LANG_SMTLIB_V2; + options.outputLanguage = language::output::LANG_SMTLIB_V2; + ExprManager exprManager(options); + + cout << Expr::dag(0) << Expr::setdepth(-1); + + // Create the parser + ParserBuilder parserBuilder(&exprManager, input, options); + Parser* parser = parserBuilder.build(); + + // Smt manager for simplifications + SmtEngine engine(&exprManager); + + // Variables and assertions + std::map<Expr, unsigned> variables; + vector<string> info_tags; + vector<string> info_data; + vector<BoolExpr> assertions; + + Command* cmd; + while ((cmd = parser->nextCommand())) { + + DeclareFunctionCommand* declare = dynamic_cast<DeclareFunctionCommand*>(cmd); + if (declare) { + cout << "[-10000, 10000] " << declare->getSymbol() << ";" << endl; + } + + AssertCommand* assert = dynamic_cast<AssertCommand*>(cmd); + if (assert) { + cout << assert->getExpr() << ";" << endl; + } + + delete cmd; + } + + // Get rid of the parser + delete parser; +} + + |