1 /*****************************************************************************/
2 /*!
3  *\file minisat_types.h
4  *\brief MiniSat internal types
5  *
6  * Author: Alexander Fuchs
7  *
8  * Created: Fri Sep 08 11:04:00 2006
9  *
10  * <hr>
11  *
12  * License to use, copy, modify, sell and/or distribute this software
13  * and its documentation for any purpose is hereby granted without
14  * royalty, subject to the terms and conditions defined in the \ref
15  * LICENSE file provided with this distribution.
16  *
17  * <hr>
18  */
19 /*****************************************************************************/
20 
21 /***********************************************************************************[SolverTypes.h]
22 MiniSat -- Copyright (c) 2003-2005, Niklas Een, Niklas Sorensson
23 
24 Permission is hereby granted, free of charge, to any person obtaining a copy of this software and
25 associated documentation files (the "Software"), to deal in the Software without restriction,
26 including without limitation the rights to use, copy, modify, merge, publish, distribute,
27 sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is
28 furnished to do so, subject to the following conditions:
29 
30 The above copyright notice and this permission notice shall be included in all copies or
31 substantial portions of the Software.
32 
33 THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT
34 NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
35 NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM,
36 DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT
37 OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
38 **************************************************************************************************/
39 
40 #ifndef _cvc3__minisat__types_h_
41 #define _cvc3__minisat__types_h_
42 
43 //=================================================================================================
44 // Variables, literals, clause IDs:
45 
46 #include "minisat_global.h"
47 #include "theorem.h"
48 #include <vector>
49 
50 namespace MiniSat {
51 
52   // NOTE! Variables are just integers. No abstraction here. They should be chosen from 0..N,
53   // so that they can be used as array indices.
54   // CVC additionally requires that N >= 2.
55   typedef int Var;
56   const int var_Undef = -1;
57 
58 
59   class Lit {
60     int     x;
61 
Lit(int index)62     explicit Lit(int index) : x(index) {}   // (lit_Undef)
63   public:
Lit()64     Lit() : x(2*var_Undef) {}   // (lit_Undef)
Lit(Var var,bool sgn)65     explicit Lit(Var var, bool sgn) : x((var+var) + (int)sgn) {}
66     Lit operator~ () const { return Lit(x ^ 1); };
67 
sign()68     bool sign  () const { return x & 1; };
var()69     int  var   () const { return x >> 1; };
index()70     int  index () const { return x; };
toLit(int i)71     static Lit  toLit (int i) { return Lit(i); };
unsign()72     Lit  unsign() const { return Lit(x & ~1); };
id(Lit p,bool sgn)73     static Lit  id  (Lit p, bool sgn) { return Lit(p.x ^ (int)sgn); };
74 
75     bool operator == (const Lit q) const { return index() == q.index(); };
76     bool operator != (const Lit q) const { return !(operator==(q)); };
77     // '<' guarantees that p, ~p are adjacent in the ordering.;
78     bool operator <  (const Lit q) const { return index() < q.index(); }
79 
hash()80     unsigned int hash() const { return (unsigned int)x; }
81 
toString()82     std::string toString() const {
83       std::ostringstream buffer;
84       if (sign())
85 	buffer << "+";
86       else
87 	buffer << "-";
88       buffer << var();
89       return buffer.str();
90     }
91 
toDimacs()92     int toDimacs() const { return sign() ? -var() - 1 : var() + 1; }
93   };
94 
95   const Lit lit_Undef(var_Undef, false);  // }- Useful special constants.
96   const Lit lit_Error(var_Undef, true );  // }
97 
98 
99 
100   // Clause -- a simple class for representing a clause:
101   class Clause {
102     unsigned int   d_size_learnt;
103     int            d_id;
104     int            d_pushID;
105     float          d_activity;
106     // The derivation of this SAT clause
107     CVC3::Theorem  d_theorem;
108     Lit            d_data[1];
109 
110     static Clause* s_decision;
111     static Clause* s_theoryImplication;
112   public:
113     // NOTE: This constructor cannot be used directly,
114     // it doesn't allocate enough memory for d_data[].
115     //
116     // using the hand-made allocator allows to allocate the data[]
117     // like a static array within clause instead of as a pointer to the array.
118     // this shows significant performance improvements
Clause(bool learnt,const std::vector<Lit> & ps,CVC3::Theorem theorem,int id,int pushID)119     Clause(bool learnt, const std::vector<Lit>& ps, CVC3::Theorem theorem,
120 	   int id, int pushID) {
121       d_size_learnt = (ps.size() << 1) | (int)learnt;
122       d_id = id;
123       d_pushID = pushID;
124       d_activity = 0;
125       d_theorem = theorem;
126       for (std::vector<Lit>::size_type i = 0; i < ps.size(); i++) d_data[i] = ps[i];
127     }
128 
129     // -- use this function instead:
130     friend Clause* Clause_new(const std::vector<Lit>& ps, CVC3::Theorem theorem, int id);
131     friend Clause* Lemma_new(const std::vector<Lit>& ps, int id, int pushID);
132 
size()133     int       size        ()      const { return d_size_learnt >> 1; }
learnt()134     bool      learnt      ()      const { return d_size_learnt & 1; }
135     Lit       operator [] (int i) const { return d_data[i]; }
136     Lit&      operator [] (int i)       { return d_data[i]; }
137     // intended to be unique id per clause, > 0, or clauseIDNull
id()138     int       id          ()      const { return d_id; }
139 
140     // used with Solver::push/pop:
141     // this is the highest id of all clauses used in the regression /
142     // resolution / creation of this lemma
pushID()143     int      pushID      ()      const  { return d_pushID; }
activity()144     float    activity    ()      const {
145       DebugAssert(learnt(), "MiniSat::Types:activity: not a lemma");
146       return d_activity;
147     }
setActivity(float activity)148     void     setActivity (float activity) {
149       DebugAssert(learnt(), "MiniSat::Types:setActivity: not a lemma");
150       d_activity = activity;
151     }
152     void      toLit       (std::vector<Lit>& literals) const;
getTheorem()153     CVC3::Theorem getTheorem() const { return d_theorem; };
154 
ClauseIDNull()155     static int ClauseIDNull() { return 0; }
156 
157     // special Clause, used to mark that an implication is a decision, id = -1.
158     static Clause* Decision();
159     // special Clause, used to mark that an implication is a theory implication
160     // and that the explanation has not been retrieved yet, id = -2.
161     static Clause* TheoryImplication();
162 
toString()163     std::string toString() const {
164       if (size() == 0) return "";
165 
166       std::ostringstream buffer;
167       buffer << d_data[0].toString();
168       for (int j = 1; j < size(); ++j) {
169 	buffer << " " << d_data[j].toString();
170       }
171       return buffer.str();
172     }
173 
contains(Lit l)174     bool contains(Lit l) {
175       for (int i = 0; i < size(); ++i) {
176 	if (d_data[i] == l) return true;
177       }
178       return false;
179     }
180   };
181 
182   Clause* Clause_new(const std::vector<Lit>& ps, CVC3::Theorem theorem, int id);
183   Clause* Lemma_new(const std::vector<Lit>& ps, int id, int pushID);
184 
185 }
186 
187 
188 
189 //=================================================================================================
190 #endif
191