ToySolver.Arith.VirtualSubstitution

Contents

Description

Naive implementation of virtual substitution

Reference:

V. Weispfenning. The complexity of linear problems in fields. Journal of Symbolic Computation, 5(1-2): 3-27, Feb.-Apr. 1988.
Hirokazu Anai, Shinji Hara. Parametric Robust Control by Quantifier Elimination. J.JSSAC, Vol. 10, No. 1, pp. 41-51, 2003.

Synopsis

Documentation

Quantifier-free formula of LRA

evalQFFormula M φ returns whether M ⊧_LRA φ or not.

Projection

project x φ returns (ψ, lift) such that:

projectN {x1,…,xm} φ returns (ψ, lift) such that:

⊢_LRA ∀y1, …, yn. (∃x1, …, xm. φ) ↔ ψ where {y1, …, yn} = FV(φ) \ {x1,…,xm}, and
if M ⊧_LRA ψ then lift M ⊧_LRA φ.

projectCases x φ returns [(ψ_1, lift_1), …, (ψ_m, lift_m)] such that:

⊢_LRA ∀y1, …, yn. (∃x. φ) ↔ (ψ_1 ∨ … ∨ φ_m) where {y1, …, yn} = FV(φ) \ {x}, and
if M ⊧_LRA ψ_i then lift_i M ⊧_LRA φ.

projectCasesN {x1,…,xm} φ returns [(ψ_1, lift_1), …, (ψ_n, lift_n)] such that:

⊢_LRA ∀y1, …, yp. (∃x. φ) ↔ (ψ_1 ∨ … ∨ φ_n) where {y1, …, yp} = FV(φ) \ {x1,…,xm}, and
if M ⊧_LRA ψ_i then lift_i M ⊧_LRA φ.

solve {x1,…,xn} φ returns Just M such that M ⊧_LRA φ when such M exists, returns Nothing otherwise.

FV(φ) must be a subset of {x1,…,xn}.

solveQFFormula {x1,…,xn} φ returns Just M such that M ⊧_LRA φ when such M exists, returns Nothing otherwise.

FV(φ) must be a subset of {x1,…,xn}.