Formula.hs 1.12 KB
Newer Older
1
2
3
4
5
module Solver.Formula
    (evaluateFormula)
where

import Data.SBV
6
import qualified Data.Map as M
7

8
import Util
9
10
import Property

11
evaluateTerm :: (Ord a, Show a) => Term a -> SIMap a -> SInteger
12
evaluateTerm (Var x) m = val m x
13
14
15
16
17
evaluateTerm (Const c) _ = literal c
evaluateTerm (Minus t) m = - evaluateTerm t m
evaluateTerm (t :+: u) m = evaluateTerm t m + evaluateTerm u m
evaluateTerm (t :-: u) m = evaluateTerm t m - evaluateTerm u m
evaluateTerm (t :*: u) m = evaluateTerm t m * evaluateTerm u m
18
19
20
21
22

opToFunction :: Op -> SInteger -> SInteger -> SBool
opToFunction Gt = (.>)
opToFunction Ge = (.>=)
opToFunction Eq = (.==)
23
opToFunction Ne = (./=)
24
25
26
opToFunction Le = (.<=)
opToFunction Lt = (.<)

27
evaluateFormula :: (Ord a, Show a) => Formula a -> SIMap a -> SBool
28
29
30
31
32
33
34
evaluateFormula FTrue _ = true
evaluateFormula FFalse _ = false
evaluateFormula (LinearInequation lhs op rhs) m =
        opToFunction op (evaluateTerm lhs m) (evaluateTerm rhs m)
evaluateFormula (Neg p) m = bnot $ evaluateFormula p m
evaluateFormula (p :&: q) m = evaluateFormula p m &&& evaluateFormula q m
evaluateFormula (p :|: q) m = evaluateFormula p m ||| evaluateFormula q m