diff options
Diffstat (limited to 'test/api')
| -rw-r--r-- | test/api/ouroborous.cpp | 206 |
1 files changed, 122 insertions, 84 deletions
diff --git a/test/api/ouroborous.cpp b/test/api/ouroborous.cpp index 1a23acd29..ca8adaf4d 100644 --- a/test/api/ouroborous.cpp +++ b/test/api/ouroborous.cpp @@ -2,9 +2,9 @@ /*! \file ouroborous.cpp ** \verbatim ** Top contributors (to current version): - ** Morgan Deters, Andrew Reynolds, Tim King + ** Aina Niemetz, Morgan Deters, Christopher L. Conway ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim @@ -25,7 +25,6 @@ **/ #include <iostream> -#include <sstream> #include <string> #include "api/cvc4cpp.h" @@ -39,101 +38,140 @@ using namespace CVC4; using namespace CVC4::parser; using namespace CVC4::language; -using namespace std; - -const string declarations = "\ -(declare-sort U 0)\n\ -(declare-fun f (U) U)\n\ -(declare-fun x () U)\n\ -(declare-fun y () U)\n\ -(assert (= (f x) x))\n\ -(declare-fun a () (Array U (Array U U)))\n\ -"; - -Parser* psr = NULL; int runTest(); -int main() { - try { +int main() +{ + try + { return runTest(); - } catch(Exception& e) { - cerr << e << endl; - } catch(...) { - cerr << "non-cvc4 exception thrown." << endl; + } + catch (api::CVC4ApiException& e) + { + std::cerr << e.getMessage() << std::endl; + } + catch (parser::ParserException& e) + { + std::cerr << e.getMessage() << std::endl; + } + catch (...) + { + std::cerr << "non-cvc4 exception thrown" << std::endl; } return 1; } -string translate(string in, InputLanguage inlang, OutputLanguage outlang) { - cout << "==============================================" << endl - << "translating from " << inlang << " to " << outlang << " this string:" << endl - << in << endl; - psr->setInput(Input::newStringInput(inlang, in, "internal-buffer")); - Expr e = psr->nextExpression().getExpr(); - stringstream ss; - ss << language::SetLanguage(outlang) << expr::ExprSetDepth(-1) << e; - assert(psr->nextExpression().isNull());// next expr should be null - assert(psr->done());// parser should be done - string s = ss.str(); - cout << "got this:" << endl - << s << endl - << "reparsing as " << outlang << endl; - - psr->setInput(Input::newStringInput(toInputLanguage(outlang), s, "internal-buffer")); - Expr f = psr->nextExpression().getExpr(); - assert(e == f); - cout << "got same expressions " << e.getId() << " and " << f.getId() << endl - << "==============================================" << endl; - - return s; -} - -void runTestString(std::string instr, InputLanguage instrlang = input::LANG_SMTLIB_V2) { - cout << endl - << "starting with: " << instr << endl - << " in language " << instrlang << endl; - string smt2 = translate(instr, instrlang, output::LANG_SMTLIB_V2); - cout << "in SMT2 : " << smt2 << endl; - /* -- SMT-LIBv1 doesn't have a functional printer yet - string smt1 = translate(smt2, input::LANG_SMTLIB_V2, output::LANG_SMTLIB); - cout << "in SMT1 : " << smt1 << endl; - */ - string cvc = translate(smt2, input::LANG_SMTLIB_V2, output::LANG_CVC4); - cout << "in CVC : " << cvc << endl; - string out = translate(cvc, input::LANG_CVC4, output::LANG_SMTLIB_V2); - cout << "back to SMT2 : " << out << endl << endl; - - assert(out == smt2);// differences in output -} - - -int runTest() { - std::unique_ptr<api::Solver> solver = - std::unique_ptr<api::Solver>(new api::Solver()); - std::unique_ptr<SymbolManager> symman(new SymbolManager(solver.get())); - psr = ParserBuilder(solver.get(), symman.get(), "internal-buffer") - .withStringInput(declarations) - .withInputLanguage(input::LANG_SMTLIB_V2) - .build(); +std::string parse(std::string instr, + std::string input_language, + std::string output_language) +{ + assert(input_language == "smt2" || input_language == "cvc4"); + assert(output_language == "smt2" || output_language == "cvc4"); + + std::string declarations; + + if (input_language == "smt2") + { + declarations = + "\ + (declare-sort U 0)\n\ + (declare-fun f (U) U)\n\ + (declare-fun x () U)\n\ + (declare-fun y () U)\n\ + (assert (= (f x) x))\n\ + (declare-fun a () (Array U (Array U U)))\n\ + "; + } + else + { + declarations = + "\ + U: TYPE;\n\ + f: U -> U;\n\ + x,y: U;\n\ + a: ARRAY U OF (ARRAY U OF U);\n\ + ASSERT f(x) = x;\n\ + "; + } - // we don't need to execute them, but we DO need to parse them to + api::Solver solver; + InputLanguage ilang = + input_language == "smt2" ? input::LANG_SMTLIB_V2 : input::LANG_CVC4; + + solver.setOption("input-language", input_language); + solver.setOption("output-language", output_language); + SymbolManager symman(&solver); + Parser* parser = ParserBuilder(&solver, &symman, "internal-buffer") + .withStringInput(declarations) + .withInputLanguage(ilang) + .build(); + // we don't need to execute the commands, but we DO need to parse them to // get the declarations - while(Command* c = psr->nextCommand()) { + while (Command* c = parser->nextCommand()) + { delete c; } + assert(parser->done()); // parser should be done + parser->setInput(Input::newStringInput(ilang, instr, "internal-buffer")); + api::Term e = parser->nextExpression(); + std::string s = e.toString(); + assert(parser->nextExpression().isNull()); // next expr should be null + delete parser; + return s; +} - assert(psr->done());// parser should be done - - cout << expr::ExprSetDepth(-1); - - runTestString("(= (f (f y)) x)"); - runTestString("~BVPLUS(3, 0bin00, 0bin11)[2:1] = 0bin10", input::LANG_CVC4); - runTestString("~BVPLUS(3, BVMULT(2, 0bin01, 0bin11), 0bin11)[2:0]", input::LANG_CVC4); - runTestString("a[x][y] = a[y][x]", input::LANG_CVC4); +std::string translate(std::string instr, + std::string input_language, + std::string output_language) +{ + assert(input_language == "smt2" || input_language == "cvc4"); + assert(output_language == "smt2" || output_language == "cvc4"); + + std::cout << "==============================================" << std::endl + << "translating from " + << (input_language == "smt2" ? input::LANG_SMTLIB_V2 + : input::LANG_CVC4) + << " to " + << (output_language == "smt2" ? output::LANG_SMTLIB_V2 + : output::LANG_CVC4) + << " this string:" << std::endl + << instr << std::endl; + std::string outstr = parse(instr, input_language, output_language); + std::cout << "got this:" << std::endl + << outstr << std::endl + << "reparsing as " + << (output_language == "smt2" ? input::LANG_SMTLIB_V2 + : input::LANG_CVC4) + << std::endl; + std::string poutstr = parse(outstr, output_language, output_language); + assert(outstr == poutstr); + std::cout << "got same expressions " << outstr << " and " << poutstr + << std::endl + << "==============================================" << std::endl; + return outstr; +} - delete psr; - psr = NULL; +void runTestString(std::string instr, std::string instr_language) +{ + std::cout << std::endl + << "starting with: " << instr << std::endl + << " in language " << input::LANG_SMTLIB_V2 << std::endl; + std::string smt2str = translate(instr, instr_language, "smt2"); + std::cout << "in SMT2 : " << smt2str << std::endl; + std::string cvcstr = translate(smt2str, "smt2", "cvc4"); + std::cout << "in CVC : " << cvcstr << std::endl; + std::string outstr = translate(cvcstr, "cvc4", "smt2"); + std::cout << "back to SMT2 : " << outstr << std::endl << std::endl; + + assert(outstr == smt2str); // differences in output +} +int32_t runTest() +{ + runTestString("(= (f (f y)) x)", "smt2"); + runTestString("~BVPLUS(3, 0bin00, 0bin11)[2:1] = 0bin10", "cvc4"); + runTestString("~BVPLUS(3, BVMULT(2, 0bin01, 0bin11), 0bin11)[2:0]", "cvc4"); + runTestString("a[x][y] = a[y][x]", "cvc4"); return 0; } |