db

Documentation

Overview

Package db is the internal representation of a QF_IDL formula in CNF. It takes in the AST and converts it using Tseiten's transformation, adding the clauses to the database. It also provides facilities to query atoms and to add new clauses.

Index

• type AtomID
  • func ToAtomID(l Lit) AtomID
• type DB
  • func FromFile(ast file.File) (db DB, err error)
  • func (db *DB) AddClauses(clauses ...[]Lit)
  • func (db DB) GetAtomForDiff(c DifferenceConstraint) (AtomID, error)
  • func (db *DB) SATSolve() file.Status
  • func (db DB) Value(lit Lit) bool
• type DifferenceConstraint
• type Lit
• type VariableID
• type VariablePair

Types

type AtomID

type AtomID = int

The AtomID type represents an identifier for an atom, whether that be a boolean variable or a difference constraint. It must be strictly positive.

func ToAtomID

func ToAtomID(l Lit) AtomID

The ToAtomID function takes in a Lit and converts it to its corresponding AtomID, checking for zero just in case.

type DB

type DB struct {

	// The Clauses variable stores the CNF form of what we want to satisfy. It's
	// represented by an instance of the SAT solver we will use. Call
	// [GetSolution] to get a solution to the clauses, which may not be theory
	// consistent.
	Clauses *gini.Gini

	// The NextAtom field reads one more than how many atoms have been created.
	// It is also the value of the next atom to be created.
	NextAtom int
	// The NextVariable field reads how many variables have been created. It is
	// also the value of the next variable to be created.
	NextVariable uint

	// The AtomIDToDiff map goes from atom identifiers to [DifferenceConstraint]
	// in the problem. If an ID doesn't show up in the domain, it has no
	// [DifferenceConstraint] associated with it, and it's just a boolean.
	//
	// Note that there is no way to go the other way. This is because difference
	// constraints use big integers, which are not comparable.
	AtomID2Diff map[AtomID]*DifferenceConstraint

	// The Variables2AtomIDs map takes in a pair of variables and maps them to a
	// list of all the [DifferenceConstraint] they participate in, indirected by
	// their [AtomID]. When the [FromFile] method returns, this list is in
	// sorted order by the constant.
	Variables2AtomIDs map[VariablePair][]AtomID
}

A DB is a database consisting of all the asserted clauses in CNF, along with all of the atoms. An atom is either a boolean variable, represented by an integer identifier or a difference constraint, represented by a DifferenceConstraint.

The DB doesn't store any information about the names of the variables. It instead uses numeric identifiers, which are assigned in order. This way, we know for example how many verticies to have in the constraint graph.

func FromFile

func FromFile(ast file.File) (db DB, err error)

The FromFile function ingests an AST and outputs a DB corresponding to it. In essence, this function applies Tsieten's transformation. It returns an error if the same scope defines the same variable twice, if we use an undeclared variable, or if we don't have well-sortedness.

func (*DB) AddClauses

func (db *DB) AddClauses(clauses ...[]Lit)

The AddClauses method adds a set of clauses to the solver. We wrap this method because there's some plumbing.

func (DB) GetAtomForDiff

func (db DB) GetAtomForDiff(c DifferenceConstraint) (AtomID, error)

The GetAtomForDiff method tries to lookup the atom corresponding to a given difference constraint.

Note that this takes linear time in the number of atoms already corresponding to the variables in the constraint. However, this number is usually small, and it's a one-time cost.

func (*DB) SATSolve

func (db *DB) SATSolve() file.Status

The SATSolve method runs solving on the known clauses. It doesn't consider any theory. It panics if the solver returns unknown.

func (DB) Value

func (db DB) Value(lit Lit) bool

The Value method gets the value of a particular literal once we've tried to solve it. It does the conversion from DIMACS to an internal representation.

type DifferenceConstraint

type DifferenceConstraint struct {
	X VariableID
	Y VariableID
	K *big.Int
}

A DifferenceConstraint is an atom of this type. It has the form x <= y + k, where x and y are variables from the instance, and k is a constant. The other type of atom is a boolean atom, which is either true or false.

type Lit

type Lit = int

An Lit is either an AtomID or its negation. Positive numbers represent positive literals, while negative numbers represent negative literals, just like in DIMACS format. Zero is not allowed.

type VariableID

type VariableID = uint

VariableIDs are assigned to each symbol of sort Int. These are used by DifferenceConstraint to keep track of which variables take part in the constraint.

type VariablePair

type VariablePair struct {
	Fst VariableID
	Snd VariableID
}

A VariablePair is an ordered pair of two variables. These are used by the DB to store difference constraints by the variables they reference.