Documentation
¶
Overview ¶
The preprocess package consists of all the preprocessing operations we can do. In the proposal, preprocessing was optional, but that is not the case now. We should at least apply the transitivity rule so that we can use binary search on the clauses if we want to in the future.
Index ¶
Constants ¶
This section is empty.
Variables ¶
var Preprocessors = map[string]Preprocessor{ "nil": Nil{}, "t-lin": TLin{}, "t-quad": TQuad{}, "tie-lin": TIELin{}, "tie-quad": TIEQuad{}, }
The Preprocessors variable stores a map from strings to the Preprocessor they are associated with. We use this map when processing command-line arguments.
Functions ¶
This section is empty.
Types ¶
type Preprocessor ¶
The Preprocessor interface has a single method that applies preprocessing to a db.DB of clauses. It's allowed to add extra clauses, but it should leave all the other variables untouched.
type TIELin ¶
type TIELin struct{}
The TIELin preprocessor applies all the preprocessing rules, effectively eagerly adding constraints for each pair of difference constraints. However, it only applies it to ones that imply all the others so that the number of extra clauses is linear.
func (TIELin) Preprocess ¶
type TIEQuad ¶
type TIEQuad struct{}
The TIEQuad preprocessor applies all the preprocessing rules, effectively eagerly adding constraints for each pair of difference constraints. It does so by looping over all the possibilities, causing a quadratic increase in the number of clauses.
func (TIEQuad) Preprocess ¶
type TLin ¶
type TLin struct{}
The TLin preprocessor only applies the transitivity rule. To do this, it scans across each variable pair's atoms array and says that one implies the next. In this way, the number of extra clauses is linear in the number of atoms associated with a pair of variables.
func (TLin) Preprocess ¶
type TQuad ¶
type TQuad struct{}
The TQuad preprocessor only applies the transitivity rule. To do this, it tries to apply it to every pair of atoms for each variable pair. In this way, the number of extra clauses is quadratic in the number of atoms.
Source Files