Removed previous encodings

Author: DhritiKhanna

scheduler/Encoding.cpp

@@ -3,26 +3,28 @@
 
 std::stringstream formula;
 
-Encoding::Encoding(ITree *it, M *m, propt *_slv)
+Encoding::Encoding(ITree *it, M *m)
 {
   _m = m;
   _it = it;
   last_node = it->_slist[it->_slist.size() -1] ; 
   traceSize = it->_slist.size()-1;
   _deadlock_found = false;
-  slv = _slv;
-  bvUtils = new bv_utilst(*slv);
+
+  //Dhriti
+  // slv = _slv;
+  // bvUtils = new bv_utilst(*slv);
 
   // instantiating two variables in the solver memory
-  one = slv->new_variable();
-  zero = slv->new_variable();
+  // one = slv->new_variable();
+  // zero = slv->new_variable();
 
   //slv->constraintStream << "one = " << one.get() <<std::endl; 
   //xslv->constraintStream << "zero = " << zero.get() <<std::endl; 
   // setting one to true and zero to false
 
-  slv->l_set_to(one, true);
-  slv->l_set_to(zero, false);
+  // slv->l_set_to(one, true);
+  // slv->l_set_to(zero, false);
 
 }
 

scheduler/Encoding.hpp

@@ -50,7 +50,7 @@ typedef satcheck_minisat_simplifiert satcheck_simplifiert;
 class Encoding{
 public:
   Encoding() {}
-  Encoding(ITree *it, M *m, propt *); 
+  Encoding(ITree *it, M *m); 
   ~Encoding(){}
 
   virtual std::string getLitName(expr a);

scheduler/Makefile.am

@@ -1,12 +1,12 @@
 CC = @CXX@
 AM_LDFLAGS = -pthread -lz3 $(LIBOPTS_LDADD)
 if COND_STATIC_LINK
-  AM_LDFLAGS +=
+  AM_LDFLAGS += -static ../solver/solver-src/solvers.a ../solver/big-int/big-int.a 
 endif
 AM_CXXFLAGS =  -DHAVE_STDINT_H -Wall $(LIBOPTS_CFLAGS) -g -O2 -DFIB -std=c++11 -D_GLIBCXX_USE_CXX11_ABI=0
 AM_CFLAGS = -DHAVE_STDINT_H -Wall $(LIBOPTS_CFLAGS) -g -O2 -DFIB -std=c++11 -D_GLIBCXX_USE_CXX11_ABI=0
 #//-O2
-INCLUDES = 
+INCLUDES = -I ../solver 
 bin_PROGRAMS = isp.exe
 isp_exe_SOURCES = Socket.cpp ServerSocket.cpp MpiProc.cpp Envelope.cpp \
                   name2id.cpp  Scheduler.cpp  Counter.cpp Transition.cpp TransitionList.cpp \

scheduler/Makefile.in

@@ -110,8 +110,8 @@ am_isp_exe_OBJECTS = Socket.$(OBJEXT) ServerSocket.$(OBJEXT) \
 	Scheduler.$(OBJEXT) Counter.$(OBJEXT) Transition.$(OBJEXT) \
 	TransitionList.$(OBJEXT) InterleavingTree.$(OBJEXT) \
 	utility.$(OBJEXT) Mo.$(OBJEXT) Wu.$(OBJEXT) Encoding.$(OBJEXT) \
-	SMTEncoding.$(OBJEXT) \
-	MultiReceive.$(OBJEXT) sched-opt.$(OBJEXT) main.$(OBJEXT)
+	SMTEncoding.$(OBJEXT) MultiReceive.$(OBJEXT) \
+	sched-opt.$(OBJEXT) main.$(OBJEXT)
 isp_exe_OBJECTS = $(am_isp_exe_OBJECTS)
 isp_exe_LDADD = $(LDADD)
 AM_V_lt = $(am__v_lt_@AM_V@)
@@ -254,7 +254,6 @@ LIBTOOL_DEPS = @LIBTOOL_DEPS@
 LIPO = @LIPO@
 LN_S = @LN_S@
 LTLIBOBJS = @LTLIBOBJS@
-LT_SYS_LIBRARY_PATH = @LT_SYS_LIBRARY_PATH@
 MAINT = @MAINT@
 MAKEINFO = @MAKEINFO@
 MANIFEST_TOOL = @MANIFEST_TOOL@
@@ -349,11 +348,11 @@ AM_LDFLAGS = -pthread -lz3 $(LIBOPTS_LDADD) $(am__append_1)
 AM_CXXFLAGS = -DHAVE_STDINT_H -Wall $(LIBOPTS_CFLAGS) -g -O2 -DFIB -std=c++11 -D_GLIBCXX_USE_CXX11_ABI=0
 AM_CFLAGS = -DHAVE_STDINT_H -Wall $(LIBOPTS_CFLAGS) -g -O2 -DFIB -std=c++11 -D_GLIBCXX_USE_CXX11_ABI=0
 #//-O2
-INCLUDES = -I ../solver
+INCLUDES = -I ../solver 
 isp_exe_SOURCES = Socket.cpp ServerSocket.cpp MpiProc.cpp Envelope.cpp \
                   name2id.cpp  Scheduler.cpp  Counter.cpp Transition.cpp TransitionList.cpp \
                   InterleavingTree.cpp utility.cpp Mo.cpp Wu.cpp Encoding.cpp SMTEncoding.cpp \
-	          MultiReceive.cpp sched-opt.c main.cpp
+		  MultiReceive.cpp sched-opt.c main.cpp
 
 all: config.hpp
 	$(MAKE) $(AM_MAKEFLAGS) all-am

scheduler/OptEncoding.cpp

@@ -34,7 +34,7 @@ class Cover
 class SMTEncoding : public Encoding {
 
 public:
-  SMTEncoding(ITree *it, M *m, propt *_slv): Encoding(it, m, _slv), width(0), eventSize(0) 
+  SMTEncoding(ITree *it, M *m): Encoding(it, m), width(0), eventSize(0) 
   {
     noVars = 1;
     s = new solver(c);

scheduler/OptEncoding.hpp

@@ -889,28 +889,18 @@ void Scheduler::StartMC () {
     //   // }
     // }
 
-    if(Scheduler::_solver.compare("minisat") == 0)
-      slv = static_cast<propt*> (new satcheck_simplifiert);
-    else if (Scheduler::_solver.compare("lingeling") == 0)
-      slv = static_cast<propt*> (new satcheck_lingelingt);
-    else if (Scheduler::_solver.compare("z3") == 0) //dhriti
-      slv = static_cast<propt*> (new satcheck_simplifiert); //dhriti
-    else 
+    if (Scheduler::_solver.compare("z3") == 0) //dhriti 
     {
-      std::cout << "Only minisat and lingeling supported. QUITING!" << std::endl;
+      std::cout << "Only z3 supported. QUITING!" << std::endl;
       ExitMpiProcessAndWait (true);
       exit(0);
     }
 
     if(Scheduler::_encoding == 0)
-    {
-      /*std::cout << "Executing the FM encoding" <<std::endl;
-      fm = new FMEncoding(it, m, slv); 
-      fm->encodingPartialOrders();*/
-      
+    {      
       //dhriti
       std::cout << "\nExecuting the SMT encoding" << std::endl;
-      smt = new SMTEncoding(it, m, slv);
+      smt = new SMTEncoding(it, m);
       bool res;
       smt->encodingPartialOrders();
       smt->encodingConditionals(Scheduler::assertsData, atoi(_num_procs.c_str()));
@@ -959,21 +949,9 @@ void Scheduler::StartMC () {
         exit(0);
       }
     }
-    // else if (Scheduler::_encoding == 1)
-    // {
-    //   std::cout << "Executing the SPO encoding" <<std::endl;
-    //   spo = new SPOEncoding(it, m, slv);
-    //   spo->poEnc();
-    // }
-    // else if (Scheduler::_encoding == 2)
-    // {
-    //   std::cout << "Executing the MultiReceives encoding" <<std::endl;
-    //   opt = new OptEncoding(it, m, slv);
-    //   opt->encodingPartialOrders();
-    // }
     else 
     {
-      std::cout << "ENCODINGTYPE is not set to FMEncoding" <<std::endl;
+      std::cout << "ENCODINGTYPE is not set to SMTEncoding" <<std::endl;
       ExitMpiProcessAndWait (true);
       exit(0);
     }