support Real/Rat type

[mischel]

minismt supports Rat and Real type. In many of our applications this would be sound. For the LP solver interface (issue #1), we should have a Real type anyway.

The extension is not trivial, as we have to extend/generalize the Formula type. There are some points that should be clarified beforehand.

• how is the SMT theory Real defined (see http://smtlib.cs.uiowa.edu/theories-Reals_Ints.shtml)
• can we have mixed formulas (probably yes)
• can we have mixed expressions (probably no)
• what theory is supported by the solvers (ie Real_Ints defineds to_int which is not supported by minismt)

[mischel]

minismt

• supports Real and Rat
• only reads integer constants
• no casting necessary
  • num types have the same internal represenation (ie c + sqrt(m)d) together with a specification (eg allow negative, denomiator, ...)

z3

• has Real constants (eg 0.5)
• explicit casting to_real and to_int

The behavior of z3 is not quite clear to me: Following formula returns sat ((x 1) (y 2.0).

(declare-fun x () Int)
(declare-fun y () Real)
(assert (= x 1.5))
(assert (= 1 1.5))
(assert (= y 2.0))
(assert (< x y))
(check-sat)
(get-value (x y))

On the other hand, this example returns unsat.

(declare-fun x () Int)
(declare-fun y () Real)
(assert (= (to_real x) 1.5))
(assert (= y 2.0))
(assert (< x y))
(check-sat)
(get-value (x y))

It seems there is some casting going on: This example returns sat

(assert (= 1 1.1))
(check-sat)

whereas this returns unsat.

(assert (= 1.1 1))
(check-sat)

[mischel]

Possible Approach:

• generalize Formula v to Formula v k
• provide smart constructors

data F v k where                                                                                                                                                                                                                                                         
   BVal :: Bool -> F v Bool
   BVar :: v -> F v Bool
   And :: [F v Bool] -> F v Bool

   AVal :: k -> F v k 
   AVar :: v -> F v k
   AEq  :: Show k => F v k -> F v k -> F v Bool

ivar :: v -> F v Int
ivar = AVAR

pros

• simple extension
• works fine with current decoding mechanism
• avoids casts
  • clear semantics
  • simple processing of results
• should work fine with minismt, z3 and _lpsolve (if available at some point)

cons

• less inflexible than eg minismt
• we still need to do some (non-invasive) casts
  • pretty printing constants for minismt
  • for mixed integer programming