removing SATPlan and adding conda and sypet
[Benchmarks_CSolver.git] / satPlan2006 / include / GeneralSolver.cpp
diff --git a/satPlan2006/include/GeneralSolver.cpp b/satPlan2006/include/GeneralSolver.cpp
deleted file mode 100644 (file)
index d2a114d..0000000
+++ /dev/null
@@ -1,178 +0,0 @@
-// Files included
-#include "Assertion.h"
-#include "ByLine.h"
-#include "CommonErrors.h"
-#include "Exceptions.h"
-#include "GeneralSolver.h"
-#include "SolverTraits.h"
-#include "StringAlgorithms.h"
-
-
-/*============================================================================//
-    GeneralSolver.cpp: Implementation of the GeneralSolver.  
-
-    Implementation: Shane J. Neph, June 2004, University of Washington
-//============================================================================*/
-
-
-namespace {
-    typedef CE::ProgramError PE;
-
-    SolverInterface* Create() { 
-        return(new GeneralSolver()); 
-    }
-
-    struct Tmp {
-        static bool func() {
-            // register GeneralSolver as a possible solver
-            bool reg = SolverTraits::SolverFactoryType::Instance()->Register(
-                                               GeneralSolver::Name(), Create);
-            Assert<PE>(reg, "Creation of " + GeneralSolver::Name());
-            return(reg);
-        }
-    };
-    static bool reg = Tmp::func();
-
-    std::string unsat = "UNSATISFIABLE";
-    std::string sat = "SATISFIABLE";
-    std::string error = "ERROR";
-
-    long maxNum(const std::vector<std::string>& vec) {
-        /* make sure everything in vec is a number! */
-        long toRtn = -100000;
-        std::vector<std::string>::const_iterator i = vec.begin(), j = vec.end();
-        while ( i != j ) {
-            long tmp = convert<long>(*i);
-            if ( tmp < 0 ) tmp = -tmp;
-            if ( tmp > toRtn ) toRtn = tmp;
-            ++i;
-        }
-        return(toRtn);
-    }
-
-    std::vector<std::string> getNums(const std::string& in) {
-        std::vector<std::string> toRtn = StringAlgs::SplitString(in, ' ');
-        std::vector<std::string>::iterator i = toRtn.begin(), j = toRtn.end();
-        while ( i != j ) {
-            if ( !StringAlgs::IsInteger(*i) ) {
-                toRtn.clear();
-                break;
-            }
-            ++i;
-        }
-        return(toRtn);
-    }
-} // end unnamed namespace
-
-
-//==================
-// evaluateReturn()
-//==================
-bool GeneralSolver::evaluateReturn(int rtnVal) {
-    std::ifstream ifile(getTempFile().c_str());
-    if ( !ifile ) return(false);
-    std::istream_iterator<ByLine> in(ifile), eof;
-    long absMax = -1;
-
-    // Copy file content to 'lst' --> see if !sat and take appropriate action
-    std::list<std::string> lst;
-    std::copy(in, eof, std::back_inserter(lst));
-    std::vector<std::string> cpy(lst.begin(), lst.end());
-
-    // Set up file with real solution or 'unsat'
-    using StringAlgs::SplitString;
-    std::ofstream out(getSolutionName().c_str());
-    Assert<CE::FileError>(out, "can't open: " + getSolutionName());
-    if ( !isSat(cpy) ) // make file for unsat
-        out << unsat << std::endl;
-    else { // sat!
-        out << sat << std::endl;
-        std::ostream_iterator<std::string> ofile(out, "\n");
-        std::list<std::string>::iterator i = lst.begin(), j;
-        std::string::size_type npos = std::string::npos;
-        bool done = false;
-        while ( i != lst.end() ) {
-            std::string next = StringAlgs::Trim(*i);
-            if ( !next.empty() && (next.find(sat) != npos) ) {
-                done = true;
-                j = i;
-                bool justNumbers = false;
-                while ( ++j != lst.end() ) {
-                    next = StringAlgs::Trim(*j);
-                    std::vector<std::string> allNumbers = getNums(next);
-                    long max = maxNum(allNumbers);
-                    if ( max > absMax )
-                        absMax = max;
-                    if ( !allNumbers.empty() ) {
-                        std::copy(allNumbers.begin(), allNumbers.end(), ofile);
-                        justNumbers = true;
-                    }
-                    else if ( justNumbers )
-                        break;
-                } // while
-            }
-            if ( done ) break;
-            ++i;
-        } // while
-
-        // Perform sanity checks
-        std::string err = "No variable assignments found in solution file!";
-        Assert<CE::FileError>(absMax > 0, err);
-
-        err = "Solution file had only " + convert<std::string>(absMax);
-        err += " variable assignments, but WFF had ";
-        err += convert<std::string>(numVars_);
-        err += " variables...Invalid Solution";
-        Assert<CE::FileError>(absMax == numVars_, err);
-    }
-    return((0 == rtnVal) || (1 == rtnVal)); // 0 sat; 1 unsat
-}
-
-//======================
-// getNumberVariables()
-//======================
-long GeneralSolver::getNumberVariables(const std::string& wff) {
-     std::ifstream infile(wff.c_str());
-     Assert<CE::FileError>(infile, "unable to open: " + wff);
-     std::istream_iterator<ByLine> in(infile), eof;
-     std::list<std::string> lst;
-     std::copy(in, eof, std::back_inserter(lst));
-     std::list<std::string>::iterator i = lst.begin(), j = lst.end();
-     long absMax = -1;
-     while ( i != j ) {
-         long max = maxNum(getNums(*i));
-         if ( max > absMax )
-             absMax = max;
-         ++i;
-     }
-     return(absMax);
-}
-
-//=========
-// isSat()
-//=========
-bool GeneralSolver::isSat(const std::vector<std::string>& vec) {
-    typedef SolverInterface::AbortedMission AM;
-    std::vector<std::string>::const_iterator i = vec.begin(), j = vec.end();
-    while ( i != j ) {
-        if ( i->find(unsat) != std::string::npos )
-            return(false);
-        else if ( i->find(sat) != std::string::npos )
-            return(true);
-        Assert<AM>(i->find(error) == std::string::npos, "Solver Aborted");
-        ++i;
-    }
-    bool toThrow = false;
-    Assert<AM>(toThrow, "Improper solution file format...assumed Solver Aborted");
-    return(false);
-}
-
-//===============
-// listOptions()
-//===============
-void GeneralSolver::listOptions(std::ostream& os) {
-    try {
-        SolverInterface::runSolver(exe());
-    } catch(...) { /* */ }
-}
-