-- | Process a "crucible_equal" statement from the precondition
-- section of the CrucibleSetup block.
learnEqual ::
  Options                                          ->
  SharedContext                                    ->
  JVMCrucibleContext                                  ->
  CrucibleMethodSpecIR                             ->
  W4.ProgramLoc                                    ->
  PrePost                                          ->
  SetupValue       {- ^ first value to compare  -} ->
  SetupValue       {- ^ second value to compare -} ->
  OverrideMatcher CJ.JVM w ()
learnEqual opts sc cc spec loc prepost v1 v2 =
  do val1 <- resolveSetupValueJVM opts cc sc spec v1
     val2 <- resolveSetupValueJVM opts cc sc spec v2
     p <- liftIO (equalValsPred cc val1 val2)
     let name = "equality " ++ stateCond prepost
     addAssert p (Crucible.SimError loc (Crucible.AssertFailureSimError name ""))

-- | Process a "crucible_precond" statement from the precondition
-- section of the CrucibleSetup block.
learnEqual ::
  Options                                          ->
  SharedContext                                    ->
  JVMCrucibleContext                                  ->
  CrucibleMethodSpecIR                             ->
  W4.ProgramLoc                                    ->
  PrePost                                          ->
  SetupValue       {- ^ first value to compare  -} ->
  SetupValue       {- ^ second value to compare -} ->
  OverrideMatcher CJ.JVM w ()
learnEqual opts sc cc spec loc prepost v1 v2 =
  do val1 <- resolveSetupValueJVM opts cc sc spec v1
     val2 <- resolveSetupValueJVM opts cc sc spec v2
     p <- liftIO (equalValsPred cc val1 val2)
     let name = "equality " ++ stateCond prepost
     addAssert p (Crucible.SimError loc (Crucible.AssertFailureSimError name ""))

-- | Process a "crucible_precond" statement from the precondition
-- section of the CrucibleSetup block.
learnEqual opts sc cc spec loc prepost v1 v2 =
  do val1 <- resolveSetupValueJVM opts cc sc spec v1
     val2 <- resolveSetupValueJVM opts cc sc spec v2
     p <- liftIO (equalValsPred cc val1 val2)
     let name = "equality " ++ stateCond prepost
     addAssert p (Crucible.SimError loc (Crucible.AssertFailureSimError name ""))

-- | Process a "crucible_precond" statement from the precondition
-- section of the CrucibleSetup block.