toysolver-0.8.1: Assorted decision procedures for SAT, SMT, Max-SAT, PB, MIP, etc
Copyright(c) Masahiro Sakai 2014
LicenseBSD-style
Maintainermasahiro.sakai@gmail.com
Stabilityprovisional
Portabilityportable
Safe HaskellSafe-Inferred
LanguageHaskell2010

ToySolver.Arith.VirtualSubstitution

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

type QFFormula = BoolExpr (Atom Rational) Source #

Quantifier-free formula of LRA

type Model r = VarMap r Source #

A Model is a map from variables to values.

class Eval m e v | m e -> v where Source #

Evaluataion of something (e.g. expression or formula) under the model.

Methods

eval :: m -> e -> v Source #

Instances

Instances details
Eval m a Bool => Eval m (BoolExpr a) Bool Source # 
Instance details

Defined in ToySolver.Data.BoolExpr

Methods

eval :: m -> BoolExpr a -> Bool Source #

(Eval m e a, Ord a) => Eval m (OrdRel e) Bool Source # 
Instance details

Defined in ToySolver.Data.OrdRel

Methods

eval :: m -> OrdRel e -> Bool Source #

Eval (Model Rational) Constr Bool Source # 
Instance details

Defined in ToySolver.Arith.FourierMotzkin.Base

Eval (Model Integer) Lit Bool Source # 
Instance details

Defined in ToySolver.Arith.Cooper.Base

Methods

eval :: Model Integer -> Lit -> Bool Source #

Fractional r => Eval (Model r) (Expr r) r Source # 
Instance details

Defined in ToySolver.Data.FOL.Arith

Methods

eval :: Model r -> Expr r -> r Source #

Num r => Eval (Model r) (Expr r) r Source # 
Instance details

Defined in ToySolver.Data.LA

Methods

eval :: Model r -> Expr r -> r Source #

Projection

project :: Var -> QFFormula -> (QFFormula, Model Rational -> Model Rational) Source #

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

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

projectN :: VarSet -> QFFormula -> (QFFormula, Model Rational -> Model Rational) Source #

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 :: Var -> QFFormula -> [(QFFormula, Model Rational -> Model Rational)] Source #

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 :: VarSet -> QFFormula -> [(QFFormula, Model Rational -> Model Rational)] Source #

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 φ.

Constraint solving

solve :: VarSet -> [Atom Rational] -> Maybe (Model Rational) Source #

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 :: VarSet -> QFFormula -> Maybe (Model Rational) Source #

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}.