Skip to content

Commit

Permalink
Use a better representation of constraints
Browse files Browse the repository at this point in the history 
Hopefully addresses #460
  • Loading branch information
@LeventErkok
LeventErkok committed Mar 3, 2019
1 parent 4580fb1 commit 692094a
Show file tree
Hide file tree
Showing 6 changed files with 34 additions and 31 deletions.
4 changes: 4 additions & 0 deletions CHANGES.md
View file
Expand Up @@ -162,6 +162,10 @@
we can create a custom version for you; though I'd much rather avoid this
if at all possible.

* Improved the internal representation of constraints to address performance
issues See http://github.com/LeventErkok/sbv/issues/460. Thanks to
Thanks Jeffrey Young for reporting.

### Version 8.0, 2019-01-14

* This is a major release of SBV, with several BACKWARDS COMPATIBILITY breaking
Expand Down
4 changes: 3 additions & 1 deletion Data/SBV/Core/Model.hs
View file
Expand Up @@ -70,6 +70,8 @@ import qualified Test.QuickCheck.Test as QC (isSuccess)
import qualified Test.QuickCheck as QC (quickCheckResult, counterexample)
import qualified Test.QuickCheck.Monadic as QC (monadicIO, run, assert, pre, monitor)

import qualified Data.Foldable as F (toList)

import Data.SBV.Core.AlgReals
import Data.SBV.Core.Data
import Data.SBV.Core.Symbolic
Expand Down Expand Up @@ -2178,7 +2180,7 @@ instance Testable (Symbolic SBool) where
where test = do (r, Result{resTraces=tvals, resObservables=ovals, resConsts=cs, resConstraints=cstrs, resUIConsts=unints}) <- runSymbolic Concrete prop

let cval = fromMaybe (error "Cannot quick-check in the presence of uninterpeted constants!") . (`lookup` cs)
cond = and [cvToBool (cval v) | (False, _, v) <- cstrs] -- Only pick-up "hard" constraints, as indicated by False in the fist component
cond = and [cvToBool (cval v) | (False, _, v) <- F.toList cstrs] -- Only pick-up "hard" constraints, as indicated by False in the fist component

getObservable (nm, f, v) = case v `lookup` cs of
Just cv -> if f cv then Just (nm, cv) else Nothing
Expand Down
18 changes: 9 additions & 9 deletions Data/SBV/Core/Symbolic.hs
View file
Expand Up @@ -642,7 +642,7 @@ data Result = Result { reskinds :: Set.Set Kind
, resUIConsts :: [(String, SBVType)] -- ^ uninterpreted constants
, resAxioms :: [(String, [String])] -- ^ axioms
, resAsgns :: SBVPgm -- ^ assignments
, resConstraints :: [(Bool, [(String, String)], SV)] -- ^ additional constraints (boolean)
, resConstraints :: S.Seq (Bool, [(String, String)], SV) -- ^ additional constraints (boolean)
, resAssertions :: [(String, Maybe CallStack, SV)] -- ^ assertions
, resOutputs :: [SV] -- ^ outputs
}
Expand Down Expand Up @@ -675,7 +675,7 @@ instance Show Result where
++ ["DEFINE"]
++ map (\(s, e) -> " " ++ shs s ++ " = " ++ show e) (F.toList (pgmAssignments xs))
++ ["CONSTRAINTS"]
++ map ((" " ++) . shCstr) cstrs
++ map ((" " ++) . shCstr) (F.toList cstrs)
++ ["ASSERTIONS"]
++ map ((" "++) . shAssert) asserts
++ ["OUTPUTS"]
Expand Down Expand Up @@ -830,7 +830,7 @@ data IncState = IncState { rNewInps :: IORef [NamedSymVar] -- always ex
, rNewTbls :: IORef TableMap
, rNewUIs :: IORef UIMap
, rNewAsgns :: IORef SBVPgm
, rNewConstraints :: IORef [(Bool, [(String, String)], SV)]
, rNewConstraints :: IORef (S.Seq (Bool, [(String, String)], SV))
}

-- | Get a new IncState
Expand All @@ -843,7 +843,7 @@ newIncState = do
tm <- newIORef Map.empty
ui <- newIORef Map.empty
pgm <- newIORef (SBVPgm S.empty)
cstrs <- newIORef []
cstrs <- newIORef S.empty
return IncState { rNewInps = is
, rNewKinds = ks
, rNewConsts = nc
Expand Down Expand Up @@ -874,7 +874,7 @@ data State = State { pathCond :: SVal -- ^ kind
, rUsedKinds :: IORef KindSet
, rUsedLbls :: IORef (Set.Set String)
, rinps :: IORef ([(Quantifier, NamedSymVar)], [NamedSymVar]) -- User defined, and internal existential
, rConstraints :: IORef [(Bool, [(String, String)], SV)]
, rConstraints :: IORef (S.Seq (Bool, [(String, String)], SV))
, routs :: IORef [SV]
, rtblMap :: IORef TableMap
, spgm :: IORef SBVPgm
Expand Down Expand Up @@ -1376,7 +1376,7 @@ runSymbolic currentRunMode (SymbolicT c) = do
faiCache <- newIORef IMap.empty
usedKinds <- newIORef Set.empty
usedLbls <- newIORef Set.empty
cstrs <- newIORef []
cstrs <- newIORef S.empty
smtOpts <- newIORef []
optGoals <- newIORef []
asserts <- newIORef []
Expand Down Expand Up @@ -1448,7 +1448,7 @@ extractSymbolicSimulationState st@State{ spgm=pgm, rinps=inps, routs=outs, rtblM

traceVals <- reverse <$> readIORef cInfo
observables <- reverse <$> readIORef observes
extraCstrs <- reverse <$> readIORef cstrs
extraCstrs <- readIORef cstrs
assertions <- reverse <$> readIORef asserts

return $ Result knds traceVals observables cgMap inpsO cnsts tbls arrs unint axs (SBVPgm rpgm) extraCstrs assertions outsO
Expand All @@ -1472,8 +1472,8 @@ internalConstraint :: State -> Bool -> [(String, String)] -> SVal -> IO ()
internalConstraint st isSoft attrs b = do v <- svToSV st b
let c = (isSoft, attrs, v)
unless (null attrs && v == trueSV) $
modifyState st rConstraints (c:)
$ modifyIncState st rNewConstraints (c:)
modifyState st rConstraints (S.|> c)
$ modifyIncState st rNewConstraints (S.|> c)

-- | Generalization of 'Data.SBV.addSValOptGoal'
addSValOptGoal :: MonadSymbolic m => Objective SVal -> m ()
Expand Down
12 changes: 3 additions & 9 deletions Data/SBV/SMT/SMTLib2.hs
View file
Expand Up @@ -274,7 +274,7 @@ cvt ctx kindInfo isSat comments (inputs, trackerVars) skolemInps consts tbls arr

where finals = cstrs' ++ maybe [] (\r -> [(False, [], r)]) mbO

cstrs' = [(isSoft, attrs, c') | (isSoft, attrs, c) <- cstrs, Just c' <- [pos c]]
cstrs' = [(isSoft, attrs, c') | (isSoft, attrs, c) <- F.toList cstrs, Just c' <- [pos c]]

mbO | isSat = pos out
| True = neg out
Expand Down Expand Up @@ -408,10 +408,8 @@ cvtInc afterAPush inps newKs consts arrs tbls uis (SBVPgm asgnsSeq) cstrs cfg =
++ concat arrayDelayeds
-- array setups
++ concat arraySetups
-- extra hard constraints
++ map (\(attr, v) -> "(assert " ++ addAnnotations attr (cvtSV skolemMap v) ++ ")") hardAsserts
-- extra soft constraints
++ map (\(attr, v) -> "(assert-soft " ++ addAnnotations attr (cvtSV skolemMap v) ++ ")") softAsserts
-- extra constraints
++ map (\(isSoft, attr, v) -> "(assert" ++ (if isSoft then "-soft " else " ") ++ addAnnotations attr (cvtSV skolemMap v) ++ ")") (F.toList cstrs)
where -- NB. The below setting of skolemMap to empty is OK, since we do
-- not support queries in the context of skolemized variables
skolemMap = M.empty
Expand All @@ -428,10 +426,6 @@ cvtInc afterAPush inps newKs consts arrs tbls uis (SBVPgm asgnsSeq) cstrs cfg =
tableMap = IM.fromList $ map mkTable allTables
where mkTable (((t, _, _), _), _) = (t, "table" ++ show t)

hardAsserts, softAsserts :: [([(String, String)], SV)]
hardAsserts = [(attr, v) | (False, attr, v) <- cstrs]
softAsserts = [(attr, v) | (True, attr, v) <- cstrs]

-- If we need flattening in models, do emit the required lines if preset
settings
| any needsFlattening newKinds
Expand Down
23 changes: 12 additions & 11 deletions Data/SBV/SMT/Utils.hs
View file
Expand Up @@ -31,7 +31,8 @@ import Data.SBV.Core.Symbolic (QueryContext)
import Data.SBV.Utils.Lib (joinArgs)

import Data.List (intercalate)
import qualified Data.Set as Set (Set)
import qualified Data.Set as Set (Set)
import qualified Data.Sequence as S (Seq)

import System.Exit (ExitCode(..))

Expand All @@ -48,21 +49,21 @@ type SMTLibConverter a = QueryContext -- ^ Int
-> [(String, SBVType)] -- ^ uninterpreted functions/constants
-> [(String, [String])] -- ^ user given axioms
-> SBVPgm -- ^ assignments
-> [(Bool, [(String, String)], SV)] -- ^ extra constraints
-> S.Seq (Bool, [(String, String)], SV) -- ^ extra constraints
-> SV -- ^ output variable
-> SMTConfig -- ^ configuration
-> a

-- | An instance of SMT-Lib converter; instantiated for SMT-Lib v1 and v2. (And potentially for newer versions in the future.)
type SMTLibIncConverter a = [NamedSymVar] -- ^ inputs
-> Set.Set Kind -- ^ new kinds
-> [(SV, CV)] -- ^ constants
-> [(Int, ArrayInfo)] -- ^ newly created arrays
-> [((Int, Kind, Kind), [SV])] -- ^ newly created tables
-> [(String, SBVType)] -- ^ newly created uninterpreted functions/constants
-> SBVPgm -- ^ assignments
-> [(Bool, [(String, String)], SV)] -- ^ extra constraints
-> SMTConfig -- ^ configuration
type SMTLibIncConverter a = [NamedSymVar] -- ^ inputs
-> Set.Set Kind -- ^ new kinds
-> [(SV, CV)] -- ^ constants
-> [(Int, ArrayInfo)] -- ^ newly created arrays
-> [((Int, Kind, Kind), [SV])] -- ^ newly created tables
-> [(String, SBVType)] -- ^ newly created uninterpreted functions/constants
-> SBVPgm -- ^ assignments
-> S.Seq (Bool, [(String, String)], SV) -- ^ extra constraints
-> SMTConfig -- ^ configuration
-> a

-- | Create an annotated term
Expand Down
4 changes: 3 additions & 1 deletion Data/SBV/Tools/GenTest.hs
View file
Expand Up @@ -25,6 +25,8 @@ import Data.SBV.Core.Data

import Data.SBV.Utils.PrettyNum

import qualified Data.Foldable as F (toList)

-- | Type of test vectors (abstract)
newtype TestVectors = TV [([CV], [CV])]

Expand All @@ -46,7 +48,7 @@ genTest n m = gen 0 []
gen (i+1) (t:sofar)
tc = do (_, Result {resTraces=tvals, resConsts=cs, resConstraints=cstrs, resOutputs=os}) <- runSymbolic Concrete (m >>= output)
let cval = fromMaybe (error "Cannot generate tests in the presence of uninterpeted constants!") . (`lookup` cs)
cond = and [cvToBool (cval v) | (False, _, v) <- cstrs] -- Only pick-up "hard" constraints, as indicated by False in the fist component
cond = and [cvToBool (cval v) | (False, _, v) <- F.toList cstrs] -- Only pick-up "hard" constraints, as indicated by False in the fist component
if cond
then return (map snd tvals, map cval os)
else tc -- try again, with the same set of constraints
Expand Down

0 comments on commit 692094a

Please sign in to comment.