Abstract:
The method provides a sound and complete online decision method for the combination of canonizable and solvable theories together with uninterpreted function and predicate symbols. It also provides the representation of a solution state in terms of theory-wise solution sets that are used to capture the equality information extracted from the processed equalities. The method includes a context-sensitive canonizer that uses theory-specific canonizers and the solution state to obtain the canonical form of an expression with respect to the given equality information. Moreover, included is the variable abstraction operation for reducing and equality between term to an equality between variables and an enhanced solution state. The closure operation for propagating equality information between solution sets for individual theories uses the theory-specific solvers. The invention teaches a modular method for combining solvers and canonizers into a combination decision procedure. Furthermore, the modular method is useful for integrating Shostak-style decision procedures within a Nelson-Oppen combination so that equality information can be exchanged between theories that are canonizable and solvable, and those that are not. The invention provides a method for deciding a formula with respect to a state comprising: canonizing the formula to create a canonical formula; abstracting the variables in the canonical formula and the state to create an abstracted formula and an abstracted state; asserting the abstracted formula into the abstracted state to create an asserted state; and closing the asserted state.