translator.cpp

Go to the documentation of this file.

/*****************************************************************************/
/*!
 * \file translator.cpp
 * \brief Description: Code for translation between languages
 * 
 * Author: Clark Barrett
 * 
 * Created: Sat Jun 25 18:06:52 2005
 *
 * <hr>
 * Copyright (C) 2003 by the Board of Trustees of Leland Stanford
 * Junior University and by New York University. 
 *
 * License to use, copy, modify, sell and/or distribute this software
 * and its documentation for any purpose is hereby granted without
 * royalty, subject to the terms and conditions defined in the \ref
 * LICENSE file provided with this distribution.  In particular:
 *
 * - The above copyright notice and this permission notice must appear
 * in all copies of the software and related documentation.
 *
 * - THE SOFTWARE IS PROVIDED "AS-IS", WITHOUT ANY WARRANTIES,
 * EXPRESSED OR IMPLIED.  USE IT AT YOUR OWN RISK.
 * 
 * <hr>
 * 
 */
/*****************************************************************************/


#include "translator.h"
#include "expr.h"
#include "theory_arith.h"


using namespace std;


namespace CVCL {


Expr Translator::preprocessRec(const Expr& e, ExprMap<Expr>& cache)
{
  if (e.arity() == 0) return e;
  ExprMap<Expr>::iterator i(cache.find(e));
  if(i != cache.end()) {
    return (*i).second;
  }

  Expr e2(e);
  vector<Expr> children;
  bool diff = false;

  for(int k = 0; k < e.arity(); ++k) {
    // Recursively preprocess the kids
    Expr child = preprocessRec(e[k], cache);
    if (child != e[k]) diff = true;
    children.push_back(child);
  }
  if (diff) {
    e2 = Expr(e.getOp(), children);
  }

  switch (e2.getKind()) {
    case CONSTDEF:
      if (e2.arity() == 2) {
        cache[e] = e2[1];
        return e2[1];
      }
      break;
    case EQ:
      if (d_theoryArith->getBaseType(e[0]) != d_theoryArith->realType())
        break;
    case LT:
    case GT:
    case LE:
    case GE:
    case UMINUS:
    case PLUS:
    case MINUS:
    case MULT:
    case DIVIDE:
    case POW:
    case INTDIV:
    case MOD:

      if (d_iteLiftArith) {
        diff = false;
        children.clear();
        vector<Expr> children2;
        Expr cond;
        for (int k = 0; k < e2.arity(); ++k) {
          if (e2[k].getKind() == ITE && !diff) {
            diff = true;
            cond = e2[k][0];
            children.push_back(e2[k][1]);
            children2.push_back(e2[k][2]);
          }
          else {
            children.push_back(e2[k]);
            children2.push_back(e2[k]);
          }
        }
        if (diff) {
          Expr thenpart = Expr(e2.getOp(), children);
          Expr elsepart = Expr(e2.getOp(), children2);
          e2 = cond.iteExpr(thenpart, elsepart);
          e2 = preprocessRec(e2, cache);
          cache[e] = e2;
          return e2;
        }
      }

      if (d_convertToDiff && d_theoryArith->isAtomicArithFormula(e2)) {
        e2 = d_theoryArith->rewriteToDiff(e2);
        cache[e] = e2;
        return e2;
      }

      break;
    default:
      break;
  }
  cache[e] = e2;
  return e2;
}


Expr Translator::preprocess(const Expr& e)
{
  ExprMap<Expr> cache;
  return preprocessRec(e, cache);
}


}

---