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

ToySolver.Arith.OmegaTest

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 #

Options for solving.

The default option can be obtained by def.

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

Instances details
Default Options Source # 
Instance details

Defined in ToySolver.Arith.OmegaTest.Base

Methods

def :: Options #