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

import Data.SBV

7
import Util
8
9
import Property

10
evaluateTerm :: (Ord a, Show a) => Term a -> SIMap a -> SInteger
11
evaluateTerm (Var x) m = val m x
12
13
14
15
16
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
17
18
19
20
21

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

26
evaluateFormula :: (Ord a, Show a) => Formula a -> SIMap a -> SBool
27
28
29
30
31
32
33
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