diff options
author | barrettcw <barrett@cs.nyu.edu> | 2015-05-12 13:53:34 -0700 |
---|---|---|
committer | barrettcw <barrett@cs.nyu.edu> | 2015-05-12 13:53:34 -0700 |
commit | 63da8b80c77ef405d84c0faa1e31323c7cc01540 (patch) | |
tree | 0bd8d30cd09008da3cd33c879474aa87c0ff7270 /src/prop | |
parent | 54f1d00d5475710ec5a4c3eab82d786ba95dfdde (diff) | |
parent | ca31b5f9de8575b9d6878c7ad7a674e48ae3c6df (diff) |
Merge pull request #74 from finnhaedicke/namespace_minisat
moved Minisat namespace into CVC4
Diffstat (limited to 'src/prop')
-rw-r--r-- | src/prop/minisat/core/Dimacs.h | 2 | ||||
-rw-r--r-- | src/prop/minisat/core/Main.cc | 2 | ||||
-rw-r--r-- | src/prop/minisat/core/Solver.cc | 2 | ||||
-rw-r--r-- | src/prop/minisat/core/Solver.h | 2 | ||||
-rw-r--r-- | src/prop/minisat/core/SolverTypes.h | 4 | ||||
-rw-r--r-- | src/prop/minisat/mtl/Alg.h | 2 | ||||
-rw-r--r-- | src/prop/minisat/mtl/Alloc.h | 2 | ||||
-rw-r--r-- | src/prop/minisat/mtl/Heap.h | 2 | ||||
-rw-r--r-- | src/prop/minisat/mtl/Map.h | 2 | ||||
-rw-r--r-- | src/prop/minisat/mtl/Queue.h | 2 | ||||
-rw-r--r-- | src/prop/minisat/mtl/Sort.h | 2 | ||||
-rw-r--r-- | src/prop/minisat/mtl/Vec.h | 2 | ||||
-rw-r--r-- | src/prop/minisat/mtl/XAlloc.h | 2 | ||||
-rw-r--r-- | src/prop/minisat/simp/SimpSolver.cc | 2 | ||||
-rw-r--r-- | src/prop/minisat/simp/SimpSolver.h | 2 | ||||
-rw-r--r-- | src/prop/minisat/utils/Options.h | 2 | ||||
-rw-r--r-- | src/prop/minisat/utils/ParseUtils.h | 2 |
17 files changed, 33 insertions, 3 deletions
diff --git a/src/prop/minisat/core/Dimacs.h b/src/prop/minisat/core/Dimacs.h index 6bd19fb5b..e4728f6b6 100644 --- a/src/prop/minisat/core/Dimacs.h +++ b/src/prop/minisat/core/Dimacs.h @@ -26,6 +26,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include "prop/minisat/utils/ParseUtils.h" #include "prop/minisat/core/SolverTypes.h" +namespace CVC4 { namespace Minisat { //================================================================================================= @@ -85,5 +86,6 @@ static void parse_DIMACS(gzFile input_stream, Solver& S) { //================================================================================================= } +} #endif diff --git a/src/prop/minisat/core/Main.cc b/src/prop/minisat/core/Main.cc index de73b7327..cb33d194e 100644 --- a/src/prop/minisat/core/Main.cc +++ b/src/prop/minisat/core/Main.cc @@ -29,7 +29,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include "prop/minisat/core/Dimacs.h" #include "prop/minisat/core/Solver.h" -using namespace Minisat; +using namespace CVC4::Minisat; //================================================================================================= diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc index e54a03435..56316ca0b 100644 --- a/src/prop/minisat/core/Solver.cc +++ b/src/prop/minisat/core/Solver.cc @@ -33,7 +33,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include "proof/proof_manager.h" #include "proof/sat_proof.h" -using namespace Minisat; +using namespace CVC4::Minisat; using namespace CVC4; using namespace CVC4::prop; diff --git a/src/prop/minisat/core/Solver.h b/src/prop/minisat/core/Solver.h index ecebb086d..9243a2b35 100644 --- a/src/prop/minisat/core/Solver.h +++ b/src/prop/minisat/core/Solver.h @@ -44,6 +44,7 @@ namespace CVC4 { }/* CVC4::prop namespace */ }/* CVC4 namespace */ +namespace CVC4 { namespace Minisat { //================================================================================================= @@ -557,5 +558,6 @@ inline void Solver::toDimacs (const char* file, Lit p, Lit q, Lit r){ ve //================================================================================================= }/* Minisat namespace */ +} #endif diff --git a/src/prop/minisat/core/SolverTypes.h b/src/prop/minisat/core/SolverTypes.h index 46c2666c8..0df5eb123 100644 --- a/src/prop/minisat/core/SolverTypes.h +++ b/src/prop/minisat/core/SolverTypes.h @@ -31,6 +31,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include "prop/minisat/mtl/Map.h" #include "prop/minisat/mtl/Alloc.h" +namespace CVC4 { namespace Minisat { //================================================================================================= @@ -169,6 +170,7 @@ inline std::ostream& operator <<(std::ostream& out, Minisat::lbool val) { } /* Minisat */ +} @@ -182,6 +184,7 @@ public: +namespace CVC4 { namespace Minisat{ //================================================================================================= @@ -499,5 +502,6 @@ inline void Clause::strengthen(Lit p) //================================================================================================= } +} #endif diff --git a/src/prop/minisat/mtl/Alg.h b/src/prop/minisat/mtl/Alg.h index 6c3a18450..365b2d5aa 100644 --- a/src/prop/minisat/mtl/Alg.h +++ b/src/prop/minisat/mtl/Alg.h @@ -23,6 +23,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include "prop/minisat/mtl/Vec.h" +namespace CVC4 { namespace Minisat { //================================================================================================= @@ -80,5 +81,6 @@ static inline void append(const vec<T>& from, vec<T>& to){ copy(from, to, true); //================================================================================================= } +} #endif diff --git a/src/prop/minisat/mtl/Alloc.h b/src/prop/minisat/mtl/Alloc.h index 71f9f7281..e5b171bac 100644 --- a/src/prop/minisat/mtl/Alloc.h +++ b/src/prop/minisat/mtl/Alloc.h @@ -24,6 +24,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include "prop/minisat/mtl/XAlloc.h" #include "prop/minisat/mtl/Vec.h" +namespace CVC4 { namespace Minisat { //================================================================================================= @@ -127,5 +128,6 @@ RegionAllocator<T>::alloc(int size) //================================================================================================= } +} #endif diff --git a/src/prop/minisat/mtl/Heap.h b/src/prop/minisat/mtl/Heap.h index 5b9fb5822..c990f9a99 100644 --- a/src/prop/minisat/mtl/Heap.h +++ b/src/prop/minisat/mtl/Heap.h @@ -23,6 +23,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include "prop/minisat/mtl/Vec.h" +namespace CVC4 { namespace Minisat { //================================================================================================= @@ -144,5 +145,6 @@ class Heap { //================================================================================================= } +} #endif diff --git a/src/prop/minisat/mtl/Map.h b/src/prop/minisat/mtl/Map.h index 72563e6d3..17572713f 100644 --- a/src/prop/minisat/mtl/Map.h +++ b/src/prop/minisat/mtl/Map.h @@ -23,6 +23,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include "prop/minisat/mtl/IntTypes.h" #include "prop/minisat/mtl/Vec.h" +namespace CVC4 { namespace Minisat { //================================================================================================= @@ -190,5 +191,6 @@ class Map { //================================================================================================= } +} #endif diff --git a/src/prop/minisat/mtl/Queue.h b/src/prop/minisat/mtl/Queue.h index 2c818fcc9..ca2014429 100644 --- a/src/prop/minisat/mtl/Queue.h +++ b/src/prop/minisat/mtl/Queue.h @@ -23,6 +23,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include "prop/minisat/mtl/Vec.h" +namespace CVC4 { namespace Minisat { //================================================================================================= @@ -65,5 +66,6 @@ public: //================================================================================================= } +} #endif diff --git a/src/prop/minisat/mtl/Sort.h b/src/prop/minisat/mtl/Sort.h index 644c39789..2c3454aa3 100644 --- a/src/prop/minisat/mtl/Sort.h +++ b/src/prop/minisat/mtl/Sort.h @@ -27,6 +27,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA // Some sorting algorithms for vec's +namespace CVC4 { namespace Minisat { template<class T> @@ -94,5 +95,6 @@ template <class T> void sort(vec<T>& v) { //================================================================================================= } +} #endif diff --git a/src/prop/minisat/mtl/Vec.h b/src/prop/minisat/mtl/Vec.h index 5f85f6fcd..cb81ee580 100644 --- a/src/prop/minisat/mtl/Vec.h +++ b/src/prop/minisat/mtl/Vec.h @@ -27,6 +27,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include "prop/minisat/mtl/IntTypes.h" #include "prop/minisat/mtl/XAlloc.h" +namespace CVC4 { namespace Minisat { //================================================================================================= @@ -126,5 +127,6 @@ void vec<T>::clear(bool dealloc) { //================================================================================================= } +} #endif diff --git a/src/prop/minisat/mtl/XAlloc.h b/src/prop/minisat/mtl/XAlloc.h index 1da176028..f1221f94f 100644 --- a/src/prop/minisat/mtl/XAlloc.h +++ b/src/prop/minisat/mtl/XAlloc.h @@ -24,6 +24,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include <errno.h> #include <stdlib.h> +namespace CVC4 { namespace Minisat { //================================================================================================= @@ -41,5 +42,6 @@ static inline void* xrealloc(void *ptr, size_t size) //================================================================================================= } +} #endif diff --git a/src/prop/minisat/simp/SimpSolver.cc b/src/prop/minisat/simp/SimpSolver.cc index 71e747f72..8408503e2 100644 --- a/src/prop/minisat/simp/SimpSolver.cc +++ b/src/prop/minisat/simp/SimpSolver.cc @@ -23,8 +23,8 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include "prop/minisat/utils/System.h" #include "prop/options.h" #include "proof/proof.h" -using namespace Minisat; using namespace CVC4; +using namespace CVC4::Minisat; //================================================================================================= // Options: diff --git a/src/prop/minisat/simp/SimpSolver.h b/src/prop/minisat/simp/SimpSolver.h index e1dfeb95e..370304d22 100644 --- a/src/prop/minisat/simp/SimpSolver.h +++ b/src/prop/minisat/simp/SimpSolver.h @@ -33,6 +33,7 @@ namespace prop { } } +namespace CVC4 { namespace Minisat { //================================================================================================= @@ -235,5 +236,6 @@ inline lbool SimpSolver::solveLimited (const vec<Lit>& assumps, bool do_simp, bo //================================================================================================= } +} #endif diff --git a/src/prop/minisat/utils/Options.h b/src/prop/minisat/utils/Options.h index b04799c4e..0577cbbd0 100644 --- a/src/prop/minisat/utils/Options.h +++ b/src/prop/minisat/utils/Options.h @@ -29,6 +29,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include "prop/minisat/mtl/Vec.h" #include "prop/minisat/utils/ParseUtils.h" +namespace CVC4 { namespace Minisat { //================================================================================================== @@ -382,5 +383,6 @@ class BoolOption : public Option //================================================================================================= } +} #endif diff --git a/src/prop/minisat/utils/ParseUtils.h b/src/prop/minisat/utils/ParseUtils.h index e9dc817c0..128205967 100644 --- a/src/prop/minisat/utils/ParseUtils.h +++ b/src/prop/minisat/utils/ParseUtils.h @@ -27,6 +27,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA //#include <zlib.h> #include <unistd.h> +namespace CVC4 { namespace Minisat { //------------------------------------------------------------------------------------------------- @@ -119,5 +120,6 @@ static bool eagerMatch(B& in, const char* str) { //================================================================================================= } +} #endif |