CVC3  2.4.1
minisat_types.cpp
Go to the documentation of this file.
1 /*****************************************************************************/
2 /*!
3  *\file minisat_types.cpp
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 
22 
23 #include "minisat_types.h"
24 
25 using namespace std;
26 
27 namespace MiniSat {
28 
29  // static class members
30  Clause* Clause::s_decision = NULL;
31  Clause* Clause::s_theoryImplication = NULL;
32 
33  const int clause_mem_base =
34  sizeof(unsigned int)
35  + 2 * sizeof(int)
36  + sizeof(float)
37  + sizeof (CVC3::Theorem);
38 
39  void* malloc_clause(const vector<Lit>& ps) {
40  return xmalloc<char>
41  (clause_mem_base + sizeof(Lit) * (max(size_t(1), ps.size())));
42  }
43 
44  Clause* Clause_new(const vector<Lit>& ps, CVC3::Theorem theorem, int id) {
45  void* mem = malloc_clause(ps);
46  return new (mem) Clause(false, ps, theorem, id, id);
47  }
48 
49  Clause* Lemma_new(const vector<Lit>& ps, int id, int pushID) {
50  void* mem = malloc_clause(ps);
51  return new (mem) Clause(true, ps, CVC3::Theorem(), id, pushID);
52  }
53 
54  Clause* Clause::Decision() {
55  if (s_decision == NULL) {
56  vector<Lit> lits;
57  s_decision = Clause_new(lits, CVC3::Theorem(), -1);
58  }
59 
60  return s_decision;
61  }
62 
63  Clause* Clause::TheoryImplication() {
64  if (s_theoryImplication == NULL) {
65  vector<Lit> lits;
66  s_theoryImplication = Clause_new(lits, CVC3::Theorem(), -2);
67  }
68 
69  return s_theoryImplication;
70  }
71 
72  void Clause::toLit(vector<Lit>& literals) const {
73  for (int i = 0; i < size(); ++i) {
74  literals.push_back(d_data[i]);
75  }
76  }
77 
78 }