test/system/smt2_compliance.cpp

   1 /*********************                                                        */
   2 /*! \file smt2_compliance.cpp
   3  ** \verbatim
   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
  11  **
  12  ** \brief A test of SMT-LIBv2 commands, checks for compliant output
  13  **
  14  ** A test of SMT-LIBv2 commands, checks for compliant output.
  15  **/
  16
  17 #include <iostream>
  18 #include <sstream>
  19 #include <cassert>
  20
  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"
  27
  28 using namespace CVC4;
  29 using namespace CVC4::parser;
  30 using namespace std;
  31
  32 void testGetInfo(SmtEngine& smt, const char* s);
  33
  34 int main() {
  35   Options opts;
  36   opts.set(options::inputLanguage, language::input::LANG_SMTLIB_V2);
  37   opts.set(options::outputLanguage, language::output::LANG_SMTLIB_V2);
  38
  39   cout << Expr::setlanguage(language::output::LANG_SMTLIB_V2);
  40
  41   ExprManager em(opts);
  42   SmtEngine smt(&em);
  43
  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");
  55
  56   return 0;
  57 }
  58
  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();
  62   assert(p != NULL);
  63   Command* c = p->nextCommand();
  64   assert(c != NULL);
  65   cout << c << endl;
  66   stringstream ss;
  67   c->invoke(&smt, ss);
  68   assert(p->nextCommand() == NULL);
  69   delete p;
  70
  71   cout << ss.str() << endl << endl;
  72 }