From b860d0ed07cf8a6d13196ba6293ac6144bb2b190 Mon Sep 17 00:00:00 2001 From: Brian Huffman Date: Sun, 17 Jan 2021 12:04:19 -0800 Subject: [PATCH] Make `goal_eval` preserve pi-bound variables in goals. Fixes #985. --- src/SAWScript/Builtins.hs | 14 ++++++++++++-- 1 file changed, 12 insertions(+), 2 deletions(-) diff --git a/src/SAWScript/Builtins.hs b/src/SAWScript/Builtins.hs index f249d1e6d3..57b6972925 100644 --- a/src/SAWScript/Builtins.hs +++ b/src/SAWScript/Builtins.hs @@ -536,13 +536,23 @@ goal_eval unints = withFirstGoal $ \goal -> do sc <- getSharedContext unintSet <- resolveNames unints - t0 <- liftIO $ propToPredicate sc (goalProp goal) + -- replace all pi-bound quantified variables with new free variables + let (args, body) = asPiList (unProp (goalProp goal)) + body' <- + case asEqTrue body of + Just t -> pure t + Nothing -> fail "goal_eval: expected EqTrue" + ecs <- liftIO $ traverse (\(nm, ty) -> scFreshEC sc (Text.unpack nm) ty) args + vars <- liftIO $ traverse (scExtCns sc) ecs + t0 <- liftIO $ instantiateVarList sc 0 (reverse vars) body' let gen = globalNonceGenerator sym <- liftIO $ Crucible.newSAWCoreBackend FloatRealRepr sc gen (_names, (_mlabels, p)) <- liftIO $ W4Sim.w4Eval sym sc Map.empty unintSet t0 t1 <- liftIO $ Crucible.toSC sym p t2 <- liftIO $ scEqTrue sc t1 - return ((), mempty, Just (goal { goalProp = Prop t2 })) + -- turn the free variables we generated back into pi-bound variables + t3 <- liftIO $ scGeneralizeExts sc ecs t2 + return ((), mempty, Just (goal { goalProp = Prop t3 })) beta_reduce_goal :: ProofScript () beta_reduce_goal =