1 2 /* 3 * File LiteralSelector.hpp. 4 * 5 * This file is part of the source code of the software program 6 * Vampire. It is protected by applicable 7 * copyright laws. 8 * 9 * This source code is distributed under the licence found here 10 * https://vprover.github.io/license.html 11 * and in the source directory 12 * 13 * In summary, you are allowed to use Vampire for non-commercial 14 * purposes but not allowed to distribute, modify, copy, create derivatives, 15 * or use in competitions. 16 * For other uses of Vampire please contact developers for a different 17 * licence, which we will make an effort to provide. 18 */ 19 /** 20 * @file LiteralSelector.hpp 21 * Defines class LiteralSelector and its descendants implementing literal selection 22 * @since 05/01/2008 Torrevieja 23 */ 24 25 #ifndef __LiteralSelector__ 26 #define __LiteralSelector__ 27 28 #include "Forwards.hpp" 29 30 #include "Lib/Array.hpp" 31 32 #include "Lib/Allocator.hpp" 33 34 #include "Term.hpp" 35 36 namespace Kernel { 37 38 using namespace Lib; 39 using namespace Shell; 40 41 /** 42 * Class LiteralSelector is base class for 43 * literal selector objects 44 */ 45 class LiteralSelector 46 { 47 public: 48 CLASS_NAME(LiteralSelector); 49 USE_ALLOCATOR(LiteralSelector); 50 LiteralSelector(const Ordering & ordering,const Options & options)51 LiteralSelector(const Ordering& ordering, const Options& options) 52 : _ord(ordering), _opt(options), _reversePolarity(false) 53 { 54 } ~LiteralSelector()55 virtual ~LiteralSelector() 56 { 57 } 58 /** if eligible is 0, all literals are eligible */ 59 void select(Clause* c, unsigned eligible=0); 60 61 static LiteralSelector* getSelector(const Ordering& ordering, const Options& options, int selectorNumber); 62 63 static void ensureSomeColoredSelected(Clause* c, unsigned eligible); 64 65 /** 66 * Return true if literal @b l is positive for the purpose of 67 * literal selection 68 * 69 * This function is to allow for easy implementation of 70 * selection functions with negative numbers. Those functions 71 * consider all literals except for equality to be of 72 * opposite polarity. 73 */ 74 bool isPositiveForSelection(Literal* l) const; 75 76 static void reversePredicatePolarity(unsigned pred, bool reverse); 77 78 /** 79 * Return true if literal @b l is negative for the purpose of 80 * literal selection 81 * 82 * @see isPositiveForSelection 83 */ isNegativeForSelection(Literal * l) const84 bool isNegativeForSelection(Literal* l) const 85 { 86 return !isPositiveForSelection(l); 87 } 88 89 int getSelectionPriority(Literal* l) const; 90 91 /** 92 * Does the selection maintain completeness in the Bachmair-Ganzinger sense? 93 */ 94 virtual bool isBGComplete() const = 0; 95 96 protected: 97 /** 98 * Perform selection on the first @b eligible literals of clause @b c 99 * 100 * @b eligible has to be greater than 1. (Trivial cases should be taken 101 * care of separately.) 102 * 103 * It is a responsibility of this function to ensure that at least one 104 * colored literal is selected if there is some in the clause. 105 */ 106 virtual void doSelection(Clause* c, unsigned eligible) = 0; 107 108 const Ordering& _ord; 109 const Options& _opt; 110 private: 111 /** 112 * If true, the polarity of all literals except for equality ones is 113 * considered to be reversed for the purposes of literal selection. 114 * 115 * @see isPositiveForSelection 116 */ 117 bool _reversePolarity; 118 119 static ZIArray<bool> _reversePredicate; 120 }; 121 122 /** 123 * Class EagerLiteralSelection implements literal 124 * selector that selects all literals 125 */ 126 class TotalLiteralSelector 127 : public LiteralSelector 128 { 129 public: 130 CLASS_NAME(TotalLiteralSelector); 131 USE_ALLOCATOR(TotalLiteralSelector); 132 TotalLiteralSelector(const Ordering & ordering,const Options & options)133 TotalLiteralSelector(const Ordering& ordering, const Options& options) 134 : LiteralSelector(ordering, options) {} 135 isBGComplete() const136 bool isBGComplete() const override { 137 // this is on purpose; we don't want any extra checks with total selection 138 return false; 139 } 140 protected: 141 void doSelection(Clause* c, unsigned eligible) override; 142 }; 143 144 145 146 } 147 148 #endif /* __LiteralSelector__ */ 149