Skip to content

Commit b74252b

Browse files
author
Eddy Westbrook
committed
added the termIsClosed function to test if a SAW core term is closed
1 parent 693883d commit b74252b

File tree

1 file changed

+5
-1
lines changed

1 file changed

+5
-1
lines changed

saw-core/src/Verifier/SAW/Term/Functor.hs

+5-1
Original file line numberDiff line numberDiff line change
@@ -60,7 +60,7 @@ module Verifier.SAW.Term.Functor
6060
, BitSet, emptyBitSet, inBitSet, unionBitSets, intersectBitSets
6161
, decrBitSet, multiDecrBitSet, completeBitSet, singletonBitSet, bitSetElems
6262
, smallestBitSetElem
63-
, looseVars, smallestFreeVar
63+
, looseVars, smallestFreeVar, termIsClosed
6464
) where
6565

6666
import Data.Bits
@@ -609,3 +609,7 @@ looseVars (Unshared f) = freesTermF (fmap looseVars f)
609609
-- | Compute the value of the smallest variable in the term, if any.
610610
smallestFreeVar :: Term -> Maybe Int
611611
smallestFreeVar = smallestBitSetElem . looseVars
612+
613+
-- | Test whether a 'Term' is closed, i.e., has no free variables
614+
termIsClosed :: Term -> Bool
615+
termIsClosed t = looseVars t == emptyBitSet

0 commit comments

Comments
 (0)