src/parser/smt2/smt2.cpp

   1 /*********************                                                        */
   2 /*! \file smt2.cpp
   3  ** \verbatim
   4  ** Original author: Christopher L. Conway
   5  ** Major contributors: Morgan Deters
   6  ** Minor contributors (to current version): Clark Barrett
   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 Definitions of SMT2 constants.
  13  **
  14  ** Definitions of SMT2 constants.
  15  **/
  16
  17 #include "expr/type.h"
  18 #include "expr/command.h"
  19 #include "parser/parser.h"
  20 #include "parser/smt1/smt1.h"
  21 #include "parser/smt2/smt2.h"
  22
  23 namespace CVC4 {
  24 namespace parser {
  25
  26 Smt2::Smt2(ExprManager* exprManager, Input* input, bool strictMode, bool parseOnly) :
  27   Parser(exprManager,input,strictMode,parseOnly),
  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 void Smt2::addBitvectorOperators() {
  46   addOperator(kind::BITVECTOR_CONCAT);
  47   addOperator(kind::BITVECTOR_AND);
  48   addOperator(kind::BITVECTOR_OR);
  49   addOperator(kind::BITVECTOR_XOR);
  50   addOperator(kind::BITVECTOR_NOT);
  51   addOperator(kind::BITVECTOR_NAND);
  52   addOperator(kind::BITVECTOR_NOR);
  53   addOperator(kind::BITVECTOR_XNOR);
  54   addOperator(kind::BITVECTOR_COMP);
  55   addOperator(kind::BITVECTOR_MULT);
  56   addOperator(kind::BITVECTOR_PLUS);
  57   addOperator(kind::BITVECTOR_SUB);
  58   addOperator(kind::BITVECTOR_NEG);
  59   addOperator(kind::BITVECTOR_UDIV);
  60   addOperator(kind::BITVECTOR_UREM);
  61   addOperator(kind::BITVECTOR_SDIV);
  62   addOperator(kind::BITVECTOR_SREM);
  63   addOperator(kind::BITVECTOR_SMOD);
  64   addOperator(kind::BITVECTOR_SHL);
  65   addOperator(kind::BITVECTOR_LSHR);
  66   addOperator(kind::BITVECTOR_ASHR);
  67   addOperator(kind::BITVECTOR_ULT);
  68   addOperator(kind::BITVECTOR_ULE);
  69   addOperator(kind::BITVECTOR_UGT);
  70   addOperator(kind::BITVECTOR_UGE);
  71   addOperator(kind::BITVECTOR_SLT);
  72   addOperator(kind::BITVECTOR_SLE);
  73   addOperator(kind::BITVECTOR_SGT);
  74   addOperator(kind::BITVECTOR_SGE);
  75   addOperator(kind::BITVECTOR_BITOF);
  76   addOperator(kind::BITVECTOR_EXTRACT);
  77   addOperator(kind::BITVECTOR_REPEAT);
  78   addOperator(kind::BITVECTOR_ZERO_EXTEND);
  79   addOperator(kind::BITVECTOR_SIGN_EXTEND);
  80   addOperator(kind::BITVECTOR_ROTATE_LEFT);
  81   addOperator(kind::BITVECTOR_ROTATE_RIGHT);
  82 }
  83
  84 void Smt2::addTheory(Theory theory) {
  85   switch(theory) {
  86   case THEORY_CORE:
  87     defineType("Bool", getExprManager()->booleanType());
  88     defineVar("true", getExprManager()->mkConst(true));
  89     defineVar("false", getExprManager()->mkConst(false));
  90     addOperator(kind::AND);
  91     addOperator(kind::DISTINCT);
  92     addOperator(kind::EQUAL);
  93     addOperator(kind::IFF);
  94     addOperator(kind::IMPLIES);
  95     addOperator(kind::ITE);
  96     addOperator(kind::NOT);
  97     addOperator(kind::OR);
  98     addOperator(kind::XOR);
  99     break;
 100
 101   case THEORY_ARRAYS:
 102     addOperator(kind::SELECT);
 103     addOperator(kind::STORE);
 104     break;
 105
 106   case THEORY_REALS_INTS:
 107     defineType("Real", getExprManager()->realType());
 108     addOperator(kind::DIVISION);
 109     // falling through on purpose, to add Ints part of Reals_Ints
 110
 111   case THEORY_INTS:
 112     defineType("Int", getExprManager()->integerType());
 113     addArithmeticOperators();
 114     addOperator(kind::INTS_DIVISION);
 115     addOperator(kind::INTS_MODULUS);
 116     break;
 117
 118   case THEORY_REALS:
 119     defineType("Real", getExprManager()->realType());
 120     addArithmeticOperators();
 121     addOperator(kind::DIVISION);
 122     break;
 123
 124   case THEORY_BITVECTORS:
 125     addBitvectorOperators();
 126     break;
 127
 128   case THEORY_QUANTIFIERS:
 129     break;
 130
 131   default:
 132     std::stringstream ss;
 133     ss << "internal error: unsupported theory " << theory;
 134     throw ParserException(ss.str());
 135   }
 136 }
 137
 138 bool Smt2::logicIsSet() {
 139   return d_logicSet;
 140 }
 141
 142 void Smt2::setLogic(const std::string& name) {
 143   d_logicSet = true;
 144   d_logic = name;
 145
 146   // Core theory belongs to every logic
 147   addTheory(THEORY_CORE);
 148
 149   if(d_logic.isTheoryEnabled(theory::THEORY_UF)) {
 150     addOperator(kind::APPLY_UF);
 151   }
 152
 153   if(d_logic.isTheoryEnabled(theory::THEORY_ARITH)) {
 154     if(d_logic.areIntegersUsed()) {
 155       addTheory(THEORY_INTS);
 156     }
 157
 158     if(d_logic.areRealsUsed()) {
 159       addTheory(THEORY_REALS);
 160     }
 161   }
 162
 163   if(d_logic.isTheoryEnabled(theory::THEORY_ARRAY)) {
 164     addTheory(THEORY_ARRAYS);
 165   }
 166
 167   if(d_logic.isTheoryEnabled(theory::THEORY_BV)) {
 168     addTheory(THEORY_BITVECTORS);
 169   }
 170
 171   if(d_logic.isQuantified()) {
 172     addTheory(THEORY_QUANTIFIERS);
 173   }
 174 }/* Smt2::setLogic() */
 175
 176 void Smt2::setInfo(const std::string& flag, const SExpr& sexpr) {
 177   // TODO: ???
 178 }
 179
 180 void Smt2::setOption(const std::string& flag, const SExpr& sexpr) {
 181   // TODO: ???
 182 }
 183
 184 void Smt2::checkThatLogicIsSet() {
 185   if( ! logicIsSet() ) {
 186     if( strictModeEnabled() ) {
 187       parseError("set-logic must appear before this point.");
 188     } else {
 189       warning("No set-logic command was given before this point.");
 190       warning("CVC4 will assume the non-standard ALL_SUPPORTED logic.");
 191       warning("Consider setting a stricter logic for (likely) better performance.");
 192       warning("To suppress this warning in the future use (set-logic ALL_SUPPORTED).");
 193
 194       setLogic("ALL_SUPPORTED");
 195
 196       Command* c = new SetBenchmarkLogicCommand("ALL_SUPPORTED");
 197       c->setMuted(true);
 198       preemptCommand(c);
 199     }
 200   }
 201 }
 202
 203 }/* CVC4::parser namespace */
 204 }/* CVC4 namespace */