toysolver-0.2.0: Assorted decision procedures for SAT, Max-SAT, PB, MIP, etc

Copyright(c) Masahiro Sakai 2011
LicenseBSD-style
Maintainermasahiro.sakai@gmail.com
Stabilityprovisional
Portabilityportable
Safe HaskellNone
LanguageHaskell2010

ToySolver.Arith.OmegaTest

Contents

Description

(incomplete) implementation of Omega Test

References:

See also:

Synopsis

Solving

type Model r = VarMap r Source

A Model is a map from variables to values.

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

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

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

solveQFLIRAConj :: Options -> VarSet -> [Atom Rational] -> VarSet -> Maybe (Model Rational) Source

solveQFLIRAConj {x1,…,xn} φ I returns Just M that M ⊧_LIRA φ when such M exists, returns Nothing otherwise.

  • FV(φ) must be a subset of {x1,…,xn}.
  • I is a set of integer variables and must be a subset of {x1,…,xn}.

Options for solving

data Options Source

Constructors

Options 

Fields

optCheckReal :: VarSet -> [Atom Rational] -> Bool

optCheckReal is used for checking whether real shadow is satisfiable.

  • If it returns True, the real shadow may or may not be satisfiable.
  • If it returns False, the real shadow must be unsatisfiable

Instances