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