SimpSolver.cc File Reference

#include "Sort.h"
#include "SimpSolver.h"
#include "System.h"

Include dependency graph for SimpSolver.cc:

Go to the source code of this file.

Macros
#define	__STDC_FORMAT_MACROS
#define	__STDC_LIMIT_MACROS

Functions
static void	mkElimClause (vec< uint32_t > &elimclauses, Lit x)
static void	mkElimClause (vec< uint32_t > &elimclauses, Var v, Clause &c)

Variables
static const char *	_cat = "SIMP"
static BoolOption	opt_use_asymm (_cat,"asymm","Shrink clauses by asymmetric branching.", false)
static BoolOption	opt_use_rcheck (_cat,"rcheck","Check if a clause is already implied. (costly)", false)
static BoolOption	opt_use_elim (_cat,"elim","Perform variable elimination.", true)
static IntOption	opt_grow (_cat,"grow","Allow a variable elimination step to grow by a number of clauses.", 0)
static IntOption	opt_clause_lim (_cat,"cl-lim","Variables are not eliminated if it produces a resolvent with a length above this limit. -1 means no limit", 20, IntRange(-1, INT32_MAX))
static IntOption	opt_subsumption_lim (_cat,"sub-lim","Do not check if subsumption against a clause larger than this. -1 means no limit.", 1000, IntRange(-1, INT32_MAX))
static DoubleOption	opt_simp_garbage_frac (_cat,"simp-gc-frac","The fraction of wasted memory allowed before a garbage collection is triggered during simplification.", 0.5, DoubleRange(0, false, HUGE_VAL, false))

Macro Definition Documentation

#define __STDC_FORMAT_MACROS

Definition at line 1 of file SimpSolver.cc.

#define __STDC_LIMIT_MACROS

Definition at line 2 of file SimpSolver.cc.

Function Documentation

static void mkElimClause ( vec< uint32_t > &  elimclauses, Lit  x  )

static

Definition at line 454 of file SimpSolver.cc.

{
    elimclauses.push(toInt(x));
    elimclauses.push(1);
}

Here is the call graph for this function:

Here is the caller graph for this function:

static void mkElimClause ( vec< uint32_t > &  elimclauses, Var  v, Clause &  c  )

static

Definition at line 461 of file SimpSolver.cc.

{
    int first = elimclauses.size();
    int v_pos = -1;

    // Copy clause to elimclauses-vector. Remember position where the
    // variable 'v' occurs:
    for (int i = 0; i < c.size(); i++){
        elimclauses.push(toInt(c[i]));
        if (var(c[i]) == v)
            v_pos = i + first;
    }
    assert(v_pos != -1);

    // Swap the first literal with the 'v' literal, so that the literal
    // containing 'v' will occur first in the clause:
    uint32_t tmp = elimclauses[v_pos];
    elimclauses[v_pos] = elimclauses[first];
    elimclauses[first] = tmp;

    // Store the length of the clause last:
    elimclauses.push(c.size());
}

Here is the call graph for this function:

Variable Documentation

const char* _cat = "SIMP"

static

Definition at line 33 of file SimpSolver.cc.

IntOption opt_clause_lim(_cat,"cl-lim","Variables are not eliminated if it produces a resolvent with a length above this limit. -1 means no limit", 20, IntRange(-1, INT32_MAX))

static

IntOption opt_grow(_cat,"grow","Allow a variable elimination step to grow by a number of clauses.", 0)

static

DoubleOption opt_simp_garbage_frac(_cat,"simp-gc-frac","The fraction of wasted memory allowed before a garbage collection is triggered during simplification.", 0.5, DoubleRange(0, false, HUGE_VAL, false))

static

IntOption opt_subsumption_lim(_cat,"sub-lim","Do not check if subsumption against a clause larger than this. -1 means no limit.", 1000, IntRange(-1, INT32_MAX))

static

BoolOption opt_use_asymm(_cat,"asymm","Shrink clauses by asymmetric branching.", false)

static

BoolOption opt_use_elim(_cat,"elim","Perform variable elimination.", true)

static

BoolOption opt_use_rcheck(_cat,"rcheck","Check if a clause is already implied. (costly)", false)

static