#include "sos.h"

This page has information from files sos.h and sos.c.

Public Routines
Public Definitions
Introduction

Public Routines in File sos.c

Index

clauses_of_weight	insert_into_sos	p_sos_tree	wt_of_clause_at
first_sos_clause	lightest_sos_clause	remove_from_sos	zap_sos_index
index_sos	p_sos_dist	worst_sos_clause

Details

int clauses_of_weight(int wt, int set);

Topform first_sos_clause(Clist lst);

Given a nonempty Clist, return the first clause. This does not remove the clause from any lists. (Call remove_from_sos(Topform) to do that.)

void index_sos(Topform c, int set);

This routine updates the (private) index for extracting sos clauses.

void insert_into_sos(Topform c, Clist sos, int set);

This routine appends a clause to the sos list and updates the (private) index for extracting sos clauses.

Topform lightest_sos_clause(int set);

Return the first (oldest) of the lightest sos clauses. This does not remove the clause from any lists. (Call remove_from_sos(Topform, Clist) to do that.)

void p_sos_dist(void);

void p_sos_tree(void);

void remove_from_sos(Topform c, Clist sos, int set);

This routine removes a clause from the sos list and updates the index for extracting the lightest and heaviest clauses.

Topform worst_sos_clause(Clist sos, int method);

int wt_of_clause_at(int set, double part);

Consider sos, ordered by weight. Assume 0 <= part <= 1; if not, we make it so. Return the weight of the clause at the part. If sos is empty, return INT_MAX.

void zap_sos_index(void);

Public Definitions in File sos.h

enum { BY_AGE, BY_WEIGHT, BY_RATIO };
enum { SOS1, SOS2 };

Introduction

This package has routines for efficiently managing selection of the given clause from the Sos list when using the given-clause algorithm.

We use a private index to quickly find the first, shortest clause in Sos. Here are the routines to use under ordinary circumstances.

insert_into_sos_lightest(Topform c, Clist sos);
remove_from_sos_lightest(Topform c);
extract_lightest_clause(Clist sos);
extract_first_clause(Clist lst);

Here's how it works (you probably don't need to know this).

We use an auxiliary Clist "Lightest" so that we don't have to scan Sos each time we need a new given clause. At any given time, Lightest is either empty or contains all of the Sos clauses of minimum weight, in the same order as in Sos.

To insert a newly kept clause c into Sos: If c is the same weight as clauses in Lightest, append it to Lightest as well as to Sos. If c is heaaver than Lightest, append it to Sos only. If c is lighter than Lightest, remove all clauses from Lightest, (leaving Lightest empty), and append c to Sos.

To get the first, lightest clause: If Lightest is empty, build a new Lightest list. Now just take the first member of Lightest.