Forgot to remove the actual stp directory.

git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@161056 91177308-0d34-0410-b5e6-96231b3b80d8

1 files changed, 0 insertions, 356 deletions

diff --git a/stp/sat/Solver.h b/stp/sat/Solver.h
deleted file mode 100644
index 0a6dc87e..00000000
--- a/stp/sat/Solver.h
+++ /dev/null
@@ -1,356 +0,0 @@
-/****************************************************************************************[Solver.h]
-MiniSat -- Copyright (c) 2003-2005, Niklas Een, Niklas Sorensson
-
-Permission is hereby granted, free of charge, to any person obtaining a copy of this software and
-associated documentation files (the "Software"), to deal in the Software without restriction,
-including without limitation the rights to use, copy, modify, merge, publish, distribute,
-sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is
-furnished to do so, subject to the following conditions:
-
-The above copyright notice and this permission notice shall be included in all copies or
-substantial portions of the Software.
-
-THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT
-NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
-NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM,
-DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT
-OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
-**************************************************************************************************/
-
-#ifndef Solver_h
-#define Solver_h
-
-#include "SolverTypes.h"
-#include "VarOrder.h"
-
-namespace MINISAT {
-
-//=================================================================================================
-// Solver -- the main class:
-struct SolverStats {
-    int64   starts, decisions, propagations, conflicts;
-    int64   clauses_literals, learnts_literals, max_literals, tot_literals;
-    int64   subsumption_checks, subsumption_misses, merges;
-    SolverStats() : 
-        starts(0), decisions(0), propagations(0), conflicts(0)
-      , clauses_literals(0), learnts_literals(0), max_literals(0), tot_literals(0) 
-      , subsumption_checks(0), subsumption_misses(0), merges(0)
-    { }
-};
-
-
-struct SearchParams {
-    double  var_decay, clause_decay, random_var_freq;
-    double  restart_inc, learntsize_inc, learntsize_factor;
-    int     restart_first;
-    
-    SearchParams(double v = 0.95, double c = 0.999, double r = 0.02,
-                 double ri = 1.5, double li = 1.1, double lf = (double)1/(double)3,
-                 int rf = 100) : 
-        var_decay(v), clause_decay(c), random_var_freq(r),
-        restart_inc(ri), learntsize_inc(li), learntsize_factor(lf),
-        restart_first(rf) { }
-};
-
-  struct ElimLt {
-    const vec<int>& n_occ;
-    
-    ElimLt(const vec<int>& no) : n_occ(no) {}
-    int  cost      (Var x)        const { return n_occ[toInt(Lit(x))] * n_occ[toInt(~Lit(x))]; }
-    bool operator()(Var x, Var y) const { return cost(x) < cost(y); } 
-  };
-
-class Solver {
-protected:
-    // Solver state:    
-    bool                ok;               // If FALSE,the constraints are already unsatisfiable. 
-                                          // No part of solver state may be used!
-    vec<Clause*>        clauses;          // List of problem clauses.
-    vec<Clause*>        learnts;          // List of learnt clauses.
-    int                 n_bin_clauses;    // Keep track of number of binary clauses "inlined" into the watcher lists (we do this primarily to get identical behavior to the version without the binary clauses trick).
-    double              cla_inc;          // Amount to bump next clause with.
-    double              cla_decay;        // INVERSE decay factor for clause activity: stores 1/decay.
-
-    vec<double>         activity;         // A heuristic measurement of the activity of a variable.
-    double              var_inc;          // Amount to bump next variable with.
-    double              var_decay;        // INVERSE decay factor for variable activity: stores 1/decay. Use negative value for static variable order.
-    VarOrder            order;            // Keeps track of the decision variable order.
-    vec<char>           properties;       // TODO: describe!!!
-
-    vec<vec<Clause*> >  watches;          // 'watches[lit]' is a list of constraints watching 'lit' (will go there if literal becomes true).
-    vec<char>           assigns;          // The current assignments (lbool:s stored as char:s).
-    vec<Lit>            trail;            // Assignment stack; stores all assigments made in the order they were made.
-    vec<int>            trail_lim;        // Separator indices for different decision levels in 'trail'.
-    vec<Clause*>        reason;           // 'reason[var]' is the clause that implied the variables current value, or 'NULL' if none.
-    vec<TrailPos>       trailpos;         // 'trailpos[var]' contains the position in the trail at wich the assigment was made.
-    int                 qhead;            // Head of queue (as index into the trail -- no more explicit propagation queue in MiniSat).
-    int                 simpDB_assigns;   // Number of top-level assignments since last execution of 'simplifyDB()'.
-    int64               simpDB_props;     // Remaining number of propagations that must be made before next execution of 'simplifyDB()'.
-    vec<Lit>            assumptions;      // Current set of assumptions provided to solve by the user.
-
-    bool                subsumption;
-    vec<char>           touched;
-    vec<vec<Clause*> >  occurs;
-    vec<int>            n_occ;
-    Heap<ElimLt>        heap;
-    vec<Clause*>        subsumption_queue;
-
-    vec<Clause*>        eliminated;
-    vec<int>            eliminated_lim;
-    vec<Var>            eliminated_var;
-
-    // Temporaries (to reduce allocation overhead). Each variable is prefixed by the method in which it is
-    // used, exept 'seen' wich is used in several places.
-    //
-    vec<char>           seen;
-    vec<Lit>            analyze_stack;
-    vec<Lit>            analyze_toclear;
-    Clause*             propagate_tmpempty;
-    Clause*             propagate_tmpbin;
-    Clause*             analyze_tmpbin;
-    Clause*             bwdsub_tmpunit;
-
-    vec<Lit>            addBinary_tmp;
-    vec<Lit>            addTernary_tmp;
-
-    // Main internal methods:
-    //
-    bool        assume           (Lit p);
-    void        cancelUntil      (int level);
-    void        record           (const vec<Lit>& clause);
-
-    void        analyze          (Clause* confl, vec<Lit>& out_learnt, int& out_btlevel); // (bt = backtrack)
-    bool        analyze_removable(Lit p, uint min_level);                                 // (helper method for 'analyze()')
-    void        analyzeFinal     (Lit p, vec<Lit>& out_conflict);
-    bool        enqueue          (Lit fact, Clause* from = NULL);
-    Clause*     propagate        ();
-    void        reduceDB         ();
-    Lit         pickBranchLit    ();
-    lbool       search           (int nof_conflicts, int nof_learnts);
-    double      progressEstimate ();
-
-    // Variable properties:
-    void        setVarProp (Var v, uint prop, bool b) { order.setVarProp(v, prop, b); }
-    bool        hasVarProp (Var v, uint prop) const   { return order.hasVarProp(v, prop); }
-    void        updateHeap (Var v) { 
-        if (hasVarProp(v, p_frozen))
-            heap.update(v); }
-
-    // Simplification methods:
-    //
-    void cleanOcc (Var v) {
-        assert(subsumption);
-        vec<Clause*>& occ = occurs[v];
-        int i, j;
-        for (i = j = 0; i < occ.size(); i++)
-            if (occ[i]->mark() != 1)
-                occ[j++] = occ[i];
-        occ.shrink(i - j); 
-    }
-
-    vec<Clause*>& getOccurs                (Var x) { cleanOcc(x); return occurs[x]; }
-    void          gather                   (vec<Clause*>& clauses);
-    Lit           subsumes                 (const Clause& c, const Clause& d);
-    bool          assymmetricBranching     (Clause& c);
-    bool          merge                    (const Clause& _ps, const Clause& _qs, Var v, vec<Lit>& out_clause);
-    
-    bool          backwardSubsumptionCheck ();
-    bool          eliminateVar             (Var v, bool fail = false);
-    bool          eliminate                ();
-    void          extendModel              ();
-
-    // Activity:
-    //
-    void     varBumpActivity(Lit p) {
-        if (var_decay < 0) return;     // (negative decay means static variable order -- don't bump)
-        if ( (activity[var(p)] += var_inc) > 1e100 ) varRescaleActivity();
-        order.update(var(p)); }
-    void     varDecayActivity  () { if (var_decay >= 0) var_inc *= var_decay; }
-    void     varRescaleActivity();
-    void     claDecayActivity  () { cla_inc *= cla_decay; }
-    void     claRescaleActivity();
-
-    // Operations on clauses:
-    //
-    bool     newClause(const vec<Lit>& ps, bool learnt = false, bool normalized = false);
-    void     claBumpActivity (Clause& c) { if ( (c.activity() += cla_inc) > 1e20 ) claRescaleActivity(); }
-    bool     locked          (const Clause& c) const { return reason[var(c[0])] == &c; }
-    bool     satisfied       (Clause& c) const;
-    bool     strengthen      (Clause& c, Lit l);
-    void     removeClause    (Clause& c, bool dealloc = true);
-
-    int      decisionLevel() const { return trail_lim.size(); }
-
-public:
-    Solver() : ok               (true)
-             , n_bin_clauses    (0)
-             , cla_inc          (1)
-             , cla_decay        (1)
-             , var_inc          (1)
-             , var_decay        (1)
-             , order            (assigns, activity)
-             , qhead            (0)
-             , simpDB_assigns   (-1)
-             , simpDB_props     (0)
-             , subsumption      (true)
-             , heap             (n_occ)
-             , params           ()
-             , expensive_ccmin  (true)
-             , verbosity        (0)
-             , progress_estimate(0)
-             {
-                vec<Lit> dummy(2,lit_Undef);
-                propagate_tmpbin   = Clause_new(dummy);
-                analyze_tmpbin     = Clause_new(dummy);
-                dummy.pop();
-                bwdsub_tmpunit     = Clause_new(dummy);
-                dummy.pop();
-                propagate_tmpempty = Clause_new(dummy);
-                addBinary_tmp .growTo(2);
-                addTernary_tmp.growTo(3);
-             }
-
-   ~Solver() {
-       xfree(propagate_tmpbin);
-       xfree(analyze_tmpbin);
-       xfree(bwdsub_tmpunit);
-       xfree(propagate_tmpempty);
-       for (int i = 0; i < eliminated.size(); i++) xfree(eliminated[i]);
-       for (int i = 0; i < learnts.size();    i++) xfree(learnts[i]);
-       for (int i = 0; i < clauses.size();    i++) xfree(clauses[i]); }
-
-    // Helpers: (semi-internal)
-    //
-    lbool   value(Var x) const { return toLbool(assigns[x]); }
-    lbool   value(Lit p) const { return sign(p) ? ~toLbool(assigns[var(p)]) : toLbool(assigns[var(p)]); }
-
-    int     nAssigns()   { return trail.size(); }
-    int     nClauses()   { return clauses.size(); }
-    int     nLearnts()   { return learnts.size(); }
-    int     nConflicts() { return (int)stats.conflicts; }
-
-    // Statistics: (read-only member variable)
-    //
-    SolverStats     stats;
-
-    // Mode of operation:
-    //
-    SearchParams    params;             // Restart frequency etc.
-    bool            expensive_ccmin;    // Controls conflict clause minimization. TRUE by default.
-    int             verbosity;          // Verbosity level. 0=silent, 1=some progress report, 2=everything
-
-    // Problem specification:
-    //
-    Var     newVar    (bool polarity = true, bool dvar = true);
-    int     nVars     ()                    { return assigns.size(); }
-    bool    addUnit   (Lit p)               { return ok && (ok = enqueue(p)); }
-    bool    addBinary (Lit p, Lit q)        { addBinary_tmp [0] = p; addBinary_tmp [1] = q; return addClause(addBinary_tmp); }
-    bool    addTernary(Lit p, Lit q, Lit r) { addTernary_tmp[0] = p; addTernary_tmp[1] = q; addTernary_tmp[2] = r; return addClause(addTernary_tmp); }
-    bool    addClause (const vec<Lit>& ps)  { if (ok && !newClause(ps)) ok = false; return ok; }
-
-    // Variable mode:
-    // 
-    void    freezeVar    (Var v) { setVarProp(v, p_frozen, true); updateHeap(v); }
-
-    // Solving:
-    //
-    bool    okay         () { return ok; }       // FALSE means solver is in a conflicting state
-    bool    simplifyDB   (bool expensive = true);
-    bool    solve        (const vec<Lit>& assumps);
-    bool    solve        () { vec<Lit> tmp; return solve(tmp); }
-    void    turnOffSubsumption() {
-        subsumption = false;
-        occurs.clear(true);
-        n_occ.clear(true);
-    }
-
-    double      progress_estimate;  // Set by 'search()'.
-    vec<lbool>  model;              // If problem is satisfiable, this vector contains the model (if any).
-    vec<Lit>    conflict;           // If problem is unsatisfiable (possibly under assumptions), this vector represent the conflict clause expressed in the assumptions.
-
-  double  returnActivity(int i) { return activity[i];}
-  void    updateInitialActivity(int i, double act) {activity[i] = act; order.heap.update(i);}
-};
-
-
-//=================================================================================================
-// Debug:
-
-
-#define L_LIT    "%sx%d"
-#define L_lit(p) sign(p)?"~":"", var(p)
-
-// Just like 'assert()' but expression will be evaluated in the release version as well.
-inline void check(bool expr) { assert(expr); }
-
-static void printLit(Lit l)
-{
-    fprintf(stderr, "%s%d", sign(l) ? "-" : "", var(l)+1);
-}
-
-template<class C>
-static void printClause(const C& c)
-{
-    for (int i = 0; i < c.size(); i++){
-        printLit(c[i]);
-        fprintf(stderr, " ");
-    }
-}
-
-//- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
-#ifdef _MSC_VER
-
-#include <ctime>
-
-static inline double cpuTime(void) {
-    return (double)clock() / CLOCKS_PER_SEC; }
-
-static inline int64 memUsed() {
-    return 0; }
-
-//- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
-#else
-
-#include <sys/time.h>
-#include <sys/resource.h>
-
-static inline double cpuTime(void) {
-    struct rusage ru;
-    getrusage(RUSAGE_SELF, &ru);
-    return (double)ru.ru_utime.tv_sec + (double)ru.ru_utime.tv_usec / 1000000; }
-
-#if defined(__linux__) || defined(__CYGWIN__)
-static inline int memReadStat(int field)
-{
-    char    name[256];
-    pid_t pid = getpid();
-    sprintf(name, "/proc/%d/statm", pid);
-    FILE*   in = fopen(name, "rb");
-    if (in == NULL) return 0;
-    int     value;
-    for (; field >= 0; field--) {
-      int res = fscanf(in, "%d", &value);
-      (void) res;
-    }
-    fclose(in);
-    return value;
-}
-
-static inline int64 memUsed() { return (int64)memReadStat(0) * (int64)getpagesize(); }
-#else
-// use this by default. Mac OS X (Darwin) does not define an os type
-//defined(__FreeBSD__)
-
-static inline int64 memUsed(void) {
-    struct rusage ru;
-    getrusage(RUSAGE_SELF, &ru);
-    return ru.ru_maxrss*1024; }
-
-#endif
-
-//- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
-#endif
-
-//=================================================================================================
-}
-#endif