src/parser/smt2/smt2.cpp

   1 /*********************                                                        */
   2 /*! \file smt2.cpp
   3  ** \verbatim
   4  ** Original author: cconway
   5  ** Major contributors: none
   6  ** Minor contributors (to current version): none
   7  ** This file is part of the CVC4 prototype.
   8  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
   9  ** Courant Institute of Mathematical Sciences
  10  ** New York University
  11  ** See the file COPYING in the top-level source directory for licensing
  12  ** information.\endverbatim
  13  **
  14  ** \brief Definitions of SMT2 constants.
  15  **
  16  ** Definitions of SMT2 constants.
  17  **/
  18
  19 #include "parser/parser.h"
  20 #include "parser/smt/smt.h"
  21 #include "parser/smt2/smt2.h"
  22
  23 namespace CVC4 {
  24 namespace parser {
  25
  26 Smt2::Smt2(ExprManager* exprManager, Input* input, bool strictMode) :
  27   Parser(exprManager,input,strictMode),
  28   d_logicSet(false) {
  29   if( !strictModeEnabled() ) {
  30     addTheory(Smt2::THEORY_CORE);
  31   }
  32 }
  33
  34 void Smt2::addArithmeticOperators() {
  35   addOperator(kind::PLUS);
  36   addOperator(kind::MINUS);
  37   addOperator(kind::UMINUS);
  38   addOperator(kind::MULT);
  39   addOperator(kind::LT);
  40   addOperator(kind::LEQ);
  41   addOperator(kind::GT);
  42   addOperator(kind::GEQ);
  43 }
  44
  45 /**
  46  * Add theory symbols to the parser state.
  47  *
  48  * @param parser the CVC4 Parser object
  49  * @param theory the theory to open (e.g., Core, Ints)
  50  */
  51 void Smt2::addTheory(Theory theory) {
  52   switch(theory) {
  53   case THEORY_CORE:
  54     defineType("Bool", getExprManager()->booleanType());
  55     defineVar("true", getExprManager()->mkConst(true));
  56     defineVar("false", getExprManager()->mkConst(false));
  57     addOperator(kind::AND);
  58     addOperator(kind::EQUAL);
  59     addOperator(kind::IFF);
  60     addOperator(kind::IMPLIES);
  61     addOperator(kind::ITE);
  62     addOperator(kind::NOT);
  63     addOperator(kind::OR);
  64     addOperator(kind::XOR);
  65     break;
  66
  67   case THEORY_REALS_INTS:
  68     defineType("Real", getExprManager()->realType());
  69     // falling-through on purpose, to add Ints part of RealsInts
  70
  71   case THEORY_INTS:
  72     defineType("Int", getExprManager()->integerType());
  73     addArithmeticOperators();
  74     break;
  75
  76   case THEORY_REALS:
  77     defineType("Real", getExprManager()->realType());
  78     addArithmeticOperators();
  79     break;
  80
  81   default:
  82     Unhandled(theory);
  83   }
  84 }
  85
  86 bool Smt2::logicIsSet() {
  87   return d_logicSet;
  88 }
  89
  90 /**
  91  * Sets the logic for the current benchmark. Declares any logic and theory symbols.
  92  *
  93  * @param parser the CVC4 Parser object
  94  * @param name the name of the logic (e.g., QF_UF, AUFLIA)
  95  */
  96 void Smt2::setLogic(const std::string& name) {
  97   d_logicSet = true;
  98   d_logic = Smt::toLogic(name);
  99
 100   // Core theory belongs to every logic
 101   addTheory(THEORY_CORE);
 102
 103   switch(d_logic) {
 104   case Smt::QF_SAT:
 105     /* No extra symbols necessary */
 106     break;
 107
 108   case Smt::QF_IDL:
 109   case Smt::QF_LIA:
 110   case Smt::QF_NIA:
 111     addTheory(THEORY_INTS);
 112     break;
 113
 114   case Smt::QF_LRA:
 115   case Smt::QF_RDL:
 116     addTheory(THEORY_REALS);
 117     break;
 118
 119   case Smt::QF_UFIDL:
 120     addTheory(THEORY_INTS);
 121     // falling-through on purpose, to add UF part of UFIDL
 122
 123   case Smt::QF_UF:
 124     addOperator(kind::APPLY_UF);
 125     break;
 126
 127   case Smt::AUFLIA:
 128   case Smt::AUFLIRA:
 129   case Smt::AUFNIRA:
 130   case Smt::QF_AUFBV:
 131   case Smt::QF_AUFLIA:
 132   case Smt::QF_AX:
 133   case Smt::QF_BV:
 134     Unhandled(name);
 135   }
 136 }
 137
 138 void Smt2::setInfo(const std::string& flag, const SExpr& sexpr) {
 139   // TODO: ???
 140 }
 141
 142 }/* CVC4::parser namespace */
 143 }/* CVC4 namespace */