minisat_types.cpp

Go to the documentation of this file.
00001 /*****************************************************************************/
00002 /*!
00003  *\file minisat_types.cpp
00004  *\brief MiniSat internal types
00005  *
00006  * Author: Alexander Fuchs
00007  *
00008  * Created: Fri Sep 08 11:04:00 2006
00009  *
00010  * <hr>
00011  *
00012  * License to use, copy, modify, sell and/or distribute this software
00013  * and its documentation for any purpose is hereby granted without
00014  * royalty, subject to the terms and conditions defined in the \ref
00015  * LICENSE file provided with this distribution.
00016  * 
00017  * <hr>
00018  */
00019 /*****************************************************************************/
00020 
00021 
00022 
00023 #include "minisat_types.h"
00024 
00025 using namespace std;
00026 
00027 namespace MiniSat {
00028 
00029   // static class members
00030   Clause* Clause::s_decision = NULL;
00031   Clause* Clause::s_theoryImplication = NULL;
00032 
00033   const int clause_mem_base =
00034     sizeof(unsigned int)
00035     + 2 * sizeof(int)
00036     + sizeof(float)
00037     + sizeof (CVC3::Theorem);
00038 
00039   void* malloc_clause(const vector<Lit>& ps) {
00040     return xmalloc<char>
00041       (clause_mem_base + sizeof(Lit) * (max(size_t(1), ps.size())));
00042   }
00043 
00044   Clause* Clause_new(const vector<Lit>& ps, CVC3::Theorem theorem, int id) {
00045     void* mem = malloc_clause(ps);
00046     return new (mem) Clause(false, ps, theorem, id, id);
00047   }
00048 
00049   Clause* Lemma_new(const vector<Lit>& ps, int id, int pushID) {
00050     void* mem = malloc_clause(ps);
00051     return new (mem) Clause(true, ps, CVC3::Theorem(), id, pushID);
00052   }
00053 
00054   Clause* Clause::Decision() {
00055     if (s_decision == NULL) {
00056       vector<Lit> lits;
00057       s_decision = Clause_new(lits, CVC3::Theorem(), -1);
00058     }
00059     
00060     return s_decision;
00061   }
00062   
00063   Clause* Clause::TheoryImplication() {
00064     if (s_theoryImplication == NULL) {
00065       vector<Lit> lits;
00066       s_theoryImplication = Clause_new(lits, CVC3::Theorem(), -2);
00067     }
00068     
00069     return s_theoryImplication;
00070   }
00071 
00072   void Clause::toLit(vector<Lit>& literals) const {
00073     for (int i = 0; i < size(); ++i) {
00074       literals.push_back(d_data[i]);
00075     }
00076   }
00077 
00078 }

Generated on Wed Nov 18 16:13:30 2009 for CVC3 by  doxygen 1.5.2