examples/nra-translate/smt2toredlog.cpp

   1 /*********************                                                        */
   2 /*! \file smt2toredlog.cpp
   3  ** \verbatim
   4  ** Original author: Dejan Jovanovic
   5  ** Major contributors: none
   6  ** Minor contributors (to current version): Morgan Deters
   7  ** This file is part of the CVC4 project.
   8  ** Copyright (c) 2009-2013  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 [[ Add one-line brief description here ]]
  13  **
  14  ** [[ Add lengthier description here ]]
  15  ** \todo document this file
  16  **/
  17
  18 #include <string>
  19 #include <iostream>
  20 #include <typeinfo>
  21 #include <cassert>
  22 #include <vector>
  23 #include <map>
  24
  25
  26 #include "options/options.h"
  27 #include "expr/expr.h"
  28 #include "expr/command.h"
  29 #include "parser/parser.h"
  30 #include "parser/parser_builder.h"
  31 #include "smt/smt_engine.h"
  32
  33 using namespace std;
  34 using namespace CVC4;
  35 using namespace CVC4::parser;
  36 using namespace CVC4::options;
  37
  38 void translate_to_redlog(
  39         string input,
  40         string command,
  41         const vector<string>& info_tags,
  42         const vector<string>& info_data,
  43         const map<Expr, unsigned>& variables,
  44         const vector<Expr>& assertions);
  45
  46 int main(int argc, char* argv[])
  47 {
  48
  49   // Get the filename
  50   string input(argv[1]);
  51   // Get the redlog command
  52   string command(argv[2]);
  53
  54   // Create the expression manager
  55   Options options;
  56   options.set(inputLanguage, language::input::LANG_SMTLIB_V2);
  57   ExprManager exprManager(options);
  58
  59   // Create the parser
  60   ParserBuilder parserBuilder(&exprManager, input, options);
  61   Parser* parser = parserBuilder.build();
  62
  63   // Smt manager for simplifications
  64   SmtEngine engine(&exprManager);
  65
  66   // Variables and assertions
  67   std::map<Expr, unsigned> variables;
  68   vector<string> info_tags;
  69   vector<string> info_data;
  70   vector<Expr> assertions;
  71
  72   Command* cmd;
  73   while ((cmd = parser->nextCommand())) {
  74
  75     SetInfoCommand* setinfo = dynamic_cast<SetInfoCommand*>(cmd);
  76     if (setinfo) {
  77       info_tags.push_back(setinfo->getFlag());
  78       info_data.push_back(setinfo->getSExpr().getValue());
  79       delete cmd;
  80       continue;
  81     }
  82
  83     DeclareFunctionCommand* declare = dynamic_cast<DeclareFunctionCommand*>(cmd);
  84     if (declare) {
  85       string name = declare->getSymbol();
  86       Expr var = parser->getVariable(name);
  87       unsigned n = variables.size();
  88       variables[var] = n;
  89       delete cmd;
  90       continue;
  91     }
  92
  93     AssertCommand* assert = dynamic_cast<AssertCommand*>(cmd);
  94     if (assert) {
  95       assertions.push_back(engine.simplify(assert->getExpr()));
  96       delete cmd;
  97       continue;
  98     }
  99
 100     delete cmd;
 101   }
 102
 103   // Do the translation
 104   translate_to_redlog(input, command, info_tags, info_data, variables, assertions);
 105
 106   // Get rid of the parser
 107   delete parser;
 108 }
 109
 110 void translate_to_redlog_term(const map<Expr, unsigned>& variables, const Expr& term) {
 111   bool first;
 112
 113   unsigned n = term.getNumChildren();
 114
 115   if (n == 0) {
 116     if (term.getKind() == kind::CONST_RATIONAL) {
 117       cout << term.getConst<Rational>();
 118     } else {
 119       assert(variables.find(term) != variables.end());
 120       cout << "x" << variables.find(term)->second;
 121     }
 122   } else {
 123
 124     switch (term.getKind()) {
 125       case kind::PLUS:
 126         cout << "(";
 127         first = true;
 128         for (unsigned i = 0; i < n; ++ i) {
 129           if (!first) {
 130             cout << " + ";
 131           }
 132           first = false;
 133           translate_to_redlog_term(variables, term[i]);
 134         }
 135         cout << ")";
 136         break;
 137       case kind::MULT:
 138         cout << "(";
 139         first = true;
 140         for (unsigned i = 0; i < n; ++ i) {
 141           if (!first) {
 142             cout << " * ";
 143           }
 144           first = false;
 145           translate_to_redlog_term(variables, term[i]);
 146         }
 147         cout << ")";
 148         break;
 149       case kind::MINUS:
 150         cout << "(";
 151         translate_to_redlog_term(variables, term[0]);
 152         cout << " - ";
 153         translate_to_redlog_term(variables, term[1]);
 154         cout << ")";
 155         break;
 156       case kind::DIVISION:
 157         cout << "(";
 158         translate_to_redlog_term(variables, term[0]);
 159         cout << " / ";
 160         translate_to_redlog_term(variables, term[1]);
 161         cout << ")";
 162         break;
 163       case kind::UMINUS:
 164         cout << "(-(";
 165         translate_to_redlog_term(variables, term[0]);
 166         cout << "))";
 167         break;
 168       default:
 169         assert(false);
 170         break;
 171     }
 172   }
 173 }
 174
 175 void translate_to_redlog(const map<Expr, unsigned>& variables, const Expr& assertion) {
 176   bool first;
 177
 178   unsigned n = assertion.getNumChildren();
 179
 180   if (n == 0) {
 181     if (assertion.isConst()) {
 182       if (assertion.getConst<bool>()) {
 183         cout << "(1 > 0)";
 184       } else {
 185         cout << "(1 < 0)";
 186       }
 187     } else {
 188       assert(false);
 189     }
 190   } else {
 191
 192     std::string op;
 193     bool binary = false;
 194     bool theory = false;
 195
 196     switch (assertion.getKind()) {
 197       case kind::NOT:
 198         cout << "(not ";
 199         translate_to_redlog(variables, assertion[0]);
 200         cout << ")";
 201         break;
 202       case kind::OR:
 203         first = true;
 204         cout << "(";
 205         for (unsigned i = 0; i < n; ++ i) {
 206           if (!first) {
 207             cout << " or ";
 208           }
 209           first = false;
 210           translate_to_redlog(variables, assertion[i]);
 211         }
 212         cout << ")";
 213         break;
 214       case kind::AND:
 215         first = true;
 216         cout << "(";
 217         for (unsigned i = 0; i < n; ++ i) {
 218           if (!first) {
 219             cout << " and ";
 220           }
 221           first = false;
 222           translate_to_redlog(variables, assertion[i]);
 223         }
 224         cout << ")";
 225         break;
 226       case kind::IMPLIES:
 227         cout << "(";
 228         translate_to_redlog(variables, assertion[0]);
 229         cout << " impl ";
 230         translate_to_redlog(variables, assertion[1]);
 231         cout << ")";
 232         break;
 233       case kind::IFF:
 234         cout << "(";
 235         translate_to_redlog(variables, assertion[0]);
 236         cout << " equiv ";
 237         translate_to_redlog(variables, assertion[1]);
 238         cout << ")";
 239         break;
 240       case kind::EQUAL:
 241         op = "=";
 242         theory = true;
 243         break;
 244       case kind::LT:
 245         op = "<";
 246         theory = true;
 247         break;
 248       case kind::LEQ:
 249         op = "<=";
 250         theory = true;
 251         break;
 252       case kind::GT:
 253         op = ">";
 254         theory = true;
 255         break;
 256       case kind::GEQ:
 257         op = ">=";
 258         theory = true;
 259         break;
 260       default:
 261         assert(false);
 262         break;
 263     }
 264
 265     if (binary) {
 266       cout << "(";
 267       translate_to_redlog(variables, assertion[0]);
 268       cout << " " << op << " ";
 269       translate_to_redlog(variables, assertion[1]);
 270       cout << ")";
 271     }
 272
 273     if (theory) {
 274       cout << "(";
 275       translate_to_redlog_term(variables, assertion[0]);
 276       cout << " " << op << " ";
 277       translate_to_redlog_term(variables, assertion[1]);
 278       cout << ")";
 279     }
 280   }
 281 }
 282
 283 void translate_to_redlog(
 284         string input,
 285         string command,
 286         const vector<string>& info_tags,
 287         const vector<string>& info_data,
 288         const std::map<Expr, unsigned>& variables,
 289         const vector<Expr>& assertions)
 290 {
 291   bool first;
 292
 293   // Dump out the information
 294   cout << "load redlog;" << endl;
 295   cout << "rlset ofsf;" << endl;
 296
 297   // Dump the variables
 298
 299   cout << "phi := ex({";
 300   first = true;
 301   for (unsigned i = 0; i < variables.size(); ++ i) {
 302     if (!first) {
 303       cout << ",";
 304     }
 305     cout << " x" << i;
 306     if (first) {
 307       first = false;
 308     }
 309   }
 310   cout << "},";
 311
 312   // The assertions
 313   first = true;
 314   for (unsigned i = 0; i < assertions.size(); ++ i) {
 315     if (first == false) {
 316       cout << " and ";
 317     }
 318     first = false;
 319     translate_to_redlog(variables, assertions[i]);
 320
 321   }
 322   cout << ");" << endl;
 323
 324   cout << "result := " << command << " phi;" << endl;
 325   cout << "result;" << endl;
 326   cout << "quit;" << endl;
 327
 328 }
 329