Skip to content

Commit

Permalink
Merge pull request #485 from GaloisInc/issue484
Browse files Browse the repository at this point in the history
Fix write_smtlib2 predicate/proposition term conventions.
  • Loading branch information
brianhuffman authored Jun 11, 2019
2 parents 56e40a8 + f5918f5 commit 03919b1
Showing 1 changed file with 5 additions and 2 deletions.
7 changes: 5 additions & 2 deletions src/SAWScript/Prover/Exporter.hs
Original file line number Diff line number Diff line change
Expand Up @@ -36,6 +36,7 @@ import qualified Verifier.SAW.Simulator.BitBlast as BBSim


import SAWScript.SAWCorePrimitives( bitblastPrimitives )
import SAWScript.Proof (predicateToProp, Quantification(..))
import SAWScript.Prover.SolverStats
import SAWScript.Prover.Rewrite
import SAWScript.Prover.Util
Expand Down Expand Up @@ -152,11 +153,13 @@ write_cnf sc f (TypedTerm schema t) = do
writeSMTLib2 :: SharedContext -> FilePath -> Term -> IO ()
writeSMTLib2 sc f t = writeUnintSMTLib2 [] sc f t

-- | As above, but check that the type is monomorphic and boolean.
-- | Write a @Term@ representing a predicate (i.e. a monomorphic
-- function returning a boolean) to an SMT-Lib version 2 file.
write_smtlib2 :: SharedContext -> FilePath -> TypedTerm -> IO ()
write_smtlib2 sc f (TypedTerm schema t) = do
checkBooleanSchema schema
writeSMTLib2 sc f t
p <- predicateToProp sc Universal [] t
writeSMTLib2 sc f p

-- | Write a @Term@ representing a theorem to an SMT-Lib version
-- 2 file, treating some constants as uninterpreted.
Expand Down

0 comments on commit 03919b1

Please sign in to comment.