1 /********************* */ 2 /*! \file logic_request.h 3 ** \verbatim 4 ** Top contributors (to current version): 5 ** Martin Brain, Tim King, Mathias Preiner 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 An object to request logic widening in the running SmtEngine 13 ** 14 ** An object to request logic widening in the running SmtEngine. This 15 ** class exists as a proxy between theory code and the SmtEngine, allowing 16 ** a theory to enable another theory in the SmtEngine after initialization 17 ** (thus the usual, public setLogic() cannot be used). This is mainly to 18 ** support features like uninterpreted divide-by-zero (to support the 19 ** partial function DIVISION), where during theory expansion, the theory 20 ** of uninterpreted functions needs to be added to the logic to support 21 ** partial functions. 22 **/ 23 24 #include "cvc4_private.h" 25 26 #ifndef __CVC4__LOGIC_REQUEST_H 27 #define __CVC4__LOGIC_REQUEST_H 28 29 #include "expr/kind.h" 30 31 namespace CVC4 { 32 33 class SmtEngine; 34 35 class LogicRequest { 36 /** The SmtEngine at play. */ 37 SmtEngine& d_smt; 38 39 public: LogicRequest(SmtEngine & smt)40 LogicRequest(SmtEngine& smt) : d_smt(smt) { } 41 42 /** Widen the logic to include the given theory. */ 43 void widenLogic(theory::TheoryId id); 44 45 /** Enable Integers. */ 46 void enableIntegers(); 47 48 };/* class LogicRequest */ 49 50 }/* CVC4 namespace */ 51 52 #endif /* __CVC4__LOGIC_REQUEST_H */ 53