1 // 2 // Copyright (c) 2006-2017 Benjamin Kaufmann 3 // 4 // This file is part of Clasp. See http://www.cs.uni-potsdam.de/clasp/ 5 // 6 // Permission is hereby granted, free of charge, to any person obtaining a copy 7 // of this software and associated documentation files (the "Software"), to 8 // deal in the Software without restriction, including without limitation the 9 // rights to use, copy, modify, merge, publish, distribute, sublicense, and/or 10 // sell copies of the Software, and to permit persons to whom the Software is 11 // furnished to do so, subject to the following conditions: 12 // 13 // The above copyright notice and this permission notice shall be included in 14 // all copies or substantial portions of the Software. 15 // 16 // THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR 17 // IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, 18 // FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE 19 // AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER 20 // LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING 21 // FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS 22 // IN THE SOFTWARE. 23 // 24 #ifndef CLASP_CB_ENUMERATOR_H 25 #define CLASP_CB_ENUMERATOR_H 26 27 #ifdef _MSC_VER 28 #pragma once 29 #endif 30 31 #include <clasp/enumerator.h> 32 33 namespace Clasp { 34 35 //! Enumerator for computing the brave/cautious consequences of a logic program. 36 /*! 37 * \ingroup enumerator 38 */ 39 class CBConsequences : public Enumerator { 40 public: 41 enum Type { 42 Brave = Model::Brave, 43 Cautious = Model::Cautious, 44 }; 45 enum Algo { Default, Query }; 46 /*! 47 * \param type Type of consequences to compute. 48 * \param a Type of algorithm to apply if type is Cautious. 49 */ 50 explicit CBConsequences(Type type, Algo a = Default); 51 ~CBConsequences(); modelType()52 int modelType() const { return type_; } exhaustive()53 bool exhaustive()const { return true; } 54 bool supportsSplitting(const SharedContext& problem) const; 55 int unsatType() const; 56 private: 57 class CBFinder; 58 class QueryFinder; 59 class SharedConstraint; 60 ConPtr doInit(SharedContext& ctx, SharedMinimizeData* m, int numModels); 61 void addLit(SharedContext& ctx, Literal p); 62 void addCurrent(Solver& s, LitVec& con, ValueVec& m, uint32 rootL = 0); 63 LitVec cons_; 64 SharedConstraint* shared_; 65 Type type_; 66 Algo algo_; 67 }; 68 69 } 70 #endif 71