1 /********************* */ 2 /*! \file smt2.h 3 ** \verbatim 4 ** Top contributors (to current version): 5 ** Andrew Reynolds, Morgan Deters, Christopher L. Conway 6 ** This file is part of the CVC4 project. 7 ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS 8 ** in the top-level source directory) and their institutional affiliations. 9 ** All rights reserved. See the file COPYING in the top-level source 10 ** directory for licensing information.\endverbatim 11 ** 12 ** \brief Definitions of SMT2 constants. 13 ** 14 ** Definitions of SMT2 constants. 15 **/ 16 17 #include "cvc4parser_private.h" 18 19 #ifndef __CVC4__PARSER__SMT2_H 20 #define __CVC4__PARSER__SMT2_H 21 22 #include <sstream> 23 #include <stack> 24 #include <string> 25 #include <unordered_map> 26 #include <utility> 27 28 #include "parser/parser.h" 29 #include "parser/smt1/smt1.h" 30 #include "theory/logic_info.h" 31 #include "util/abstract_value.h" 32 33 namespace CVC4 { 34 35 class SExpr; 36 37 namespace api { 38 class Solver; 39 } 40 41 namespace parser { 42 43 class Smt2 : public Parser { 44 friend class ParserBuilder; 45 46 public: 47 enum Theory 48 { 49 THEORY_ARRAYS, 50 THEORY_BITVECTORS, 51 THEORY_CORE, 52 THEORY_DATATYPES, 53 THEORY_INTS, 54 THEORY_REALS, 55 THEORY_TRANSCENDENTALS, 56 THEORY_REALS_INTS, 57 THEORY_QUANTIFIERS, 58 THEORY_SETS, 59 THEORY_STRINGS, 60 THEORY_UF, 61 THEORY_FP, 62 THEORY_SEP 63 }; 64 65 private: 66 bool d_logicSet; 67 LogicInfo d_logic; 68 std::unordered_map<std::string, Kind> operatorKindMap; 69 std::pair<Expr, std::string> d_lastNamedTerm; 70 // for sygus 71 std::vector<Expr> d_sygusVars, d_sygusVarPrimed, d_sygusConstraints, 72 d_sygusFunSymbols; 73 74 protected: 75 Smt2(api::Solver* solver, 76 Input* input, 77 bool strictMode = false, 78 bool parseOnly = false); 79 80 public: 81 /** 82 * Add theory symbols to the parser state. 83 * 84 * @param theory the theory to open (e.g., Core, Ints) 85 */ 86 void addTheory(Theory theory); 87 88 void addOperator(Kind k, const std::string& name); 89 90 Kind getOperatorKind(const std::string& name) const; 91 92 bool isOperatorEnabled(const std::string& name) const; 93 94 bool isTheoryEnabled(Theory theory) const; 95 96 bool logicIsSet() override; 97 98 /** 99 * Returns the expression that name should be interpreted as. 100 */ 101 Expr getExpressionForNameAndType(const std::string& name, Type t) override; 102 103 /** Make function defined by a define-fun(s)-rec command. 104 * 105 * fname : the name of the function. 106 * sortedVarNames : the list of variable arguments for the function. 107 * t : the range type of the function we are defining. 108 * 109 * This function will create a bind a new function term to name fname. 110 * The type of this function is 111 * Parser::mkFlatFunctionType(sorts,t,flattenVars), 112 * where sorts are the types in the second components of sortedVarNames. 113 * As descibed in Parser::mkFlatFunctionType, new bound variables may be 114 * added to flattenVars in this function if the function is given a function 115 * range type. 116 */ 117 Expr mkDefineFunRec( 118 const std::string& fname, 119 const std::vector<std::pair<std::string, Type> >& sortedVarNames, 120 Type t, 121 std::vector<Expr>& flattenVars); 122 123 /** Push scope for define-fun-rec 124 * 125 * This calls Parser::pushScope(bindingLevel) and sets up 126 * initial information for reading a body of a function definition 127 * in the define-fun-rec and define-funs-rec command. 128 * The input parameters func/flattenVars are the result 129 * of a call to mkDefineRec above. 130 * 131 * func : the function whose body we are defining. 132 * sortedVarNames : the list of variable arguments for the function. 133 * flattenVars : the implicit variables introduced when defining func. 134 * 135 * This function: 136 * (1) Calls Parser::pushScope(bindingLevel). 137 * (2) Computes the bound variable list for the quantified formula 138 * that defined this definition and stores it in bvs. 139 */ 140 void pushDefineFunRecScope( 141 const std::vector<std::pair<std::string, Type> >& sortedVarNames, 142 Expr func, 143 const std::vector<Expr>& flattenVars, 144 std::vector<Expr>& bvs, 145 bool bindingLevel = false); 146 147 void reset() override; 148 149 void resetAssertions(); 150 151 /** 152 * Sets the logic for the current benchmark. Declares any logic and 153 * theory symbols. 154 * 155 * @param name the name of the logic (e.g., QF_UF, AUFLIA) 156 */ 157 void setLogic(std::string name); 158 159 /** 160 * Get the logic. 161 */ getLogic()162 const LogicInfo& getLogic() const { return d_logic; } 163 v2_0()164 bool v2_0() const { 165 return getLanguage() == language::input::LANG_SMTLIB_V2_0; 166 } 167 /** 168 * Are we using smtlib 2.5 or above? If exact=true, then this method returns 169 * false if the input language is not exactly SMT-LIB 2.5. 170 */ 171 bool v2_5(bool exact = false) const 172 { 173 return language::isInputLang_smt2_5(getLanguage(), exact); 174 } 175 /** 176 * Are we using smtlib 2.6 or above? If exact=true, then this method returns 177 * false if the input language is not exactly SMT-LIB 2.6. 178 */ 179 bool v2_6(bool exact = false) const 180 { 181 return language::isInputLang_smt2_6(getLanguage(), exact); 182 } 183 sygus()184 bool sygus() const { return getLanguage() == language::input::LANG_SYGUS; } 185 186 /** 187 * Returns true if the language that we are parsing (SMT-LIB version >=2.5 188 * and SyGuS) treats duplicate double quotes ("") as an escape sequence 189 * denoting a single double quote ("). 190 */ escapeDupDblQuote()191 bool escapeDupDblQuote() const { return v2_5() || sygus(); } 192 193 void setInfo(const std::string& flag, const SExpr& sexpr); 194 195 void setOption(const std::string& flag, const SExpr& sexpr); 196 197 void checkThatLogicIsSet(); 198 checkUserSymbol(const std::string & name)199 void checkUserSymbol(const std::string& name) { 200 if(name.length() > 0 && (name[0] == '.' || name[0] == '@')) { 201 std::stringstream ss; 202 ss << "cannot declare or define symbol `" << name << "'; symbols starting with . and @ are reserved in SMT-LIB"; 203 parseError(ss.str()); 204 } 205 else if (isOperatorEnabled(name)) 206 { 207 std::stringstream ss; 208 ss << "Symbol `" << name << "' is shadowing a theory function symbol"; 209 parseError(ss.str()); 210 } 211 } 212 213 void includeFile(const std::string& filename); 214 setLastNamedTerm(Expr e,std::string name)215 void setLastNamedTerm(Expr e, std::string name) { 216 d_lastNamedTerm = std::make_pair(e, name); 217 } 218 clearLastNamedTerm()219 void clearLastNamedTerm() { 220 d_lastNamedTerm = std::make_pair(Expr(), ""); 221 } 222 lastNamedTerm()223 std::pair<Expr, std::string> lastNamedTerm() { 224 return d_lastNamedTerm; 225 } 226 isAbstractValue(const std::string & name)227 bool isAbstractValue(const std::string& name) { 228 return name.length() >= 2 && name[0] == '@' && name[1] != '0' && 229 name.find_first_not_of("0123456789", 1) == std::string::npos; 230 } 231 mkAbstractValue(const std::string & name)232 Expr mkAbstractValue(const std::string& name) { 233 assert(isAbstractValue(name)); 234 return getExprManager()->mkConst(AbstractValue(Integer(name.substr(1)))); 235 } 236 237 void mkSygusVar(const std::string& name, 238 const Type& type, 239 bool isPrimed = false); 240 241 void mkSygusConstantsForType( const Type& type, std::vector<CVC4::Expr>& ops ); 242 243 void processSygusGTerm( CVC4::SygusGTerm& sgt, int index, 244 std::vector< CVC4::Datatype >& datatypes, 245 std::vector< CVC4::Type>& sorts, 246 std::vector< std::vector<CVC4::Expr> >& ops, 247 std::vector< std::vector<std::string> >& cnames, 248 std::vector< std::vector< std::vector< CVC4::Type > > >& cargs, 249 std::vector< bool >& allow_const, 250 std::vector< std::vector< std::string > >& unresolved_gterm_sym, 251 std::vector<CVC4::Expr>& sygus_vars, 252 std::map< CVC4::Type, CVC4::Type >& sygus_to_builtin, std::map< CVC4::Type, CVC4::Expr >& sygus_to_builtin_expr, 253 CVC4::Type& ret, bool isNested = false ); 254 255 static bool pushSygusDatatypeDef( Type t, std::string& dname, 256 std::vector< CVC4::Datatype >& datatypes, 257 std::vector< CVC4::Type>& sorts, 258 std::vector< std::vector<CVC4::Expr> >& ops, 259 std::vector< std::vector<std::string> >& cnames, 260 std::vector< std::vector< std::vector< CVC4::Type > > >& cargs, 261 std::vector< bool >& allow_const, 262 std::vector< std::vector< std::string > >& unresolved_gterm_sym ); 263 264 static bool popSygusDatatypeDef( std::vector< CVC4::Datatype >& datatypes, 265 std::vector< CVC4::Type>& sorts, 266 std::vector< std::vector<CVC4::Expr> >& ops, 267 std::vector< std::vector<std::string> >& cnames, 268 std::vector< std::vector< std::vector< CVC4::Type > > >& cargs, 269 std::vector< bool >& allow_const, 270 std::vector< std::vector< std::string > >& unresolved_gterm_sym ); 271 272 void setSygusStartIndex( std::string& fun, int startIndex, 273 std::vector< CVC4::Datatype >& datatypes, 274 std::vector< CVC4::Type>& sorts, 275 std::vector< std::vector<CVC4::Expr> >& ops ); 276 277 void mkSygusDatatype( CVC4::Datatype& dt, std::vector<CVC4::Expr>& ops, 278 std::vector<std::string>& cnames, std::vector< std::vector< CVC4::Type > >& cargs, 279 std::vector<std::string>& unresolved_gterm_sym, 280 std::map< CVC4::Type, CVC4::Type >& sygus_to_builtin ); 281 282 283 /** 284 * Smt2 parser provides its own checkDeclaration, which does the 285 * same as the base, but with some more helpful errors. 286 */ 287 void checkDeclaration(const std::string& name, 288 DeclarationCheck check, 289 SymbolType type = SYM_VARIABLE, 290 std::string notes = "") 291 { 292 // if the symbol is something like "-1", we'll give the user a helpful 293 // syntax hint. (-1 is a valid identifier in SMT-LIB, NOT unary minus.) 294 if( check != CHECK_DECLARED || 295 name[0] != '-' || 296 name.find_first_not_of("0123456789", 1) != std::string::npos ) { 297 this->Parser::checkDeclaration(name, check, type, notes); 298 return; 299 }else{ 300 //it is allowable in sygus 301 if( sygus() && name[0]=='-' ){ 302 //do not check anything 303 return; 304 } 305 } 306 307 std::stringstream ss; 308 ss << notes 309 << "You may have intended to apply unary minus: `(- " 310 << name.substr(1) 311 << ")'\n"; 312 this->Parser::checkDeclaration(name, check, type, ss.str()); 313 } 314 checkOperator(Kind kind,unsigned numArgs)315 void checkOperator(Kind kind, unsigned numArgs) 316 { 317 Parser::checkOperator(kind, numArgs); 318 // strict SMT-LIB mode enables extra checks for some bitvector operators 319 // that CVC4 permits as N-ary but the standard requires is binary 320 if(strictModeEnabled()) { 321 switch(kind) { 322 case kind::BITVECTOR_CONCAT: 323 case kind::BITVECTOR_AND: 324 case kind::BITVECTOR_OR: 325 case kind::BITVECTOR_XOR: 326 case kind::BITVECTOR_MULT: 327 case kind::BITVECTOR_PLUS: 328 if(numArgs != 2) { 329 parseError("Operator requires exact 2 arguments in strict SMT-LIB " 330 "compliance mode: " + kindToString(kind)); 331 } 332 break; 333 default: 334 break; /* no problem */ 335 } 336 } 337 } 338 339 // Throw a ParserException with msg appended with the current logic. parseErrorLogic(const std::string & msg)340 inline void parseErrorLogic(const std::string& msg) 341 { 342 const std::string withLogic = msg + getLogic().getLogicString(); 343 parseError(withLogic); 344 } 345 346 private: 347 std::map< CVC4::Expr, CVC4::Type > d_sygus_bound_var_type; 348 std::map< CVC4::Expr, std::vector< CVC4::Expr > > d_sygus_let_func_to_vars; 349 std::map< CVC4::Expr, CVC4::Expr > d_sygus_let_func_to_body; 350 std::map< CVC4::Expr, unsigned > d_sygus_let_func_to_num_input_vars; 351 //auxiliary define-fun functions introduced for production rules 352 std::vector< CVC4::Expr > d_sygus_defined_funs; 353 354 void collectSygusLetArgs( CVC4::Expr e, std::vector< CVC4::Type >& sygusArgs, std::vector< CVC4::Expr >& builtinArgs ); 355 356 Type processSygusNestedGTerm( int sub_dt_index, std::string& sub_dname, std::vector< CVC4::Datatype >& datatypes, 357 std::vector< CVC4::Type>& sorts, 358 std::vector< std::vector<CVC4::Expr> >& ops, 359 std::vector< std::vector<std::string> >& cnames, 360 std::vector< std::vector< std::vector< CVC4::Type > > >& cargs, 361 std::vector< bool >& allow_const, 362 std::vector< std::vector< std::string > >& unresolved_gterm_sym, 363 std::map< CVC4::Type, CVC4::Type >& sygus_to_builtin, 364 std::map< CVC4::Type, CVC4::Expr >& sygus_to_builtin_expr, Type sub_ret ); 365 366 void processSygusLetConstructor( std::vector< CVC4::Expr >& let_vars, int index, 367 std::vector< CVC4::Datatype >& datatypes, 368 std::vector< CVC4::Type>& sorts, 369 std::vector< std::vector<CVC4::Expr> >& ops, 370 std::vector< std::vector<std::string> >& cnames, 371 std::vector< std::vector< std::vector< CVC4::Type > > >& cargs, 372 std::vector<CVC4::Expr>& sygus_vars, 373 std::map< CVC4::Type, CVC4::Type >& sygus_to_builtin, 374 std::map< CVC4::Type, CVC4::Expr >& sygus_to_builtin_expr ); 375 376 /** make sygus bound var list 377 * 378 * This is used for converting non-builtin sygus operators to lambda 379 * expressions. It takes as input a datatype and constructor index (for 380 * naming) and a vector of type ltypes. 381 * It appends a bound variable to lvars for each type in ltypes, and returns 382 * a bound variable list whose children are lvars. 383 */ 384 Expr makeSygusBoundVarList(Datatype& dt, 385 unsigned i, 386 const std::vector<Type>& ltypes, 387 std::vector<Expr>& lvars); 388 389 void addArithmeticOperators(); 390 391 void addTranscendentalOperators(); 392 393 void addBitvectorOperators(); 394 395 void addStringOperators(); 396 397 void addFloatingPointOperators(); 398 399 void addSepOperators(); 400 401 InputLanguage getLanguage() const; 402 };/* class Smt2 */ 403 404 }/* CVC4::parser namespace */ 405 }/* CVC4 namespace */ 406 407 #endif /* __CVC4__PARSER__SMT2_H */ 408