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